Recent Achievements
During the last five years, researchers from the Software Security Lab
at USTC (which forms the backbone of the new Center) have undertaken a
series of projects supported by grants from National Natural Science
Foundation of China, including:
(1) Security of mobile code based on techniques of programming language
theory and implementation
(2) Application Research of Type Theory in Software Security and Safety
(3) Verification and Compilation of Software Safety
(4) Languages, Logics, and Proofs for Certified Software Design
The lab has produced 14 PhD researchers in the fields of programming
language theory and implementation, software security and software
verification. Here are a few recent representative publications:
[1] X. Feng, Z. Shao, A. Vaynberg, S. Xiang, and Z. Ni. Modular
verification of assembly code with stack-based control
abstractions. In Proc. 2006 ACM Conference on Programming Language
Design and Implementation, pages 401-414, June 2006.
[2] Chunxian Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, and Yu
Guo. Foundational typed assembly language with certified garbage
collection. In Proceedings of 1st IEEE/IFIP International Symposium on
Theoretical Aspects of Software Engineering, pages 326-335, IEEE CS
press, June 2007.
[3] X. Feng, Z. Ni, Z. Shao, and Y. Guo. An open framework for
foundational proof-carrying code. In Proc. 2007 ACM SIGPLAN
International Workshop on Types in Language Design and Implementation,
pages 67-78, Jan. 2007.
[4] A. McCreight, Z. Shao, C. Lin, and L. Li. A General Framework for
Certifying Garbage Collectors and Their Mutators. In Proc. 2007 ACM
Conference on Programming Language Design and Implementation, pages
468-479, June 2007.
[5] X. Feng, Z. Shao, Y. Dong, and Y. Guo. Certifying Low-Level
Programs with Hardware Interrupts and Preemptive Threads. In
Proc. 2008 ACM Conference on Programming Language Design and
Implementation, pages 170-182, June 2008.
[6] X. Feng, Z. Shao, Y. Guo and Y. Dong. Combining Domain-Specific
and Foundational Logics to Verify Complete Software Systems. In
Proc. Second IFIP Working Conference on Verified Software: Theories,
Tools, and Experiments, October 2008.