ABSTRACT

 

This project studies new architectures for verifiably safe execution of software. The first area of research is the production of a new generation of compilers, called verifying compilers, that can only compile safe code according to pre-determined safety policies, such as protection of private information and resource-bounded computation. The second area is the production of code accompanied by formal proofs guaranteeing that code's compliance with pre-determined safety policies, in the style of Proof-Carrying Code (PCC).

 

Typed languages guaranteeing different notions of safety criteria, including assembly languages and machine code, will be defined, studied, and modeled. These languages will be relevant to both the design of verifying compilers and the PCC project. One approach will be using dependent type systems to define powerful intermediate and assembly languages. Furthermore, a prototype verifying compiler will be built by extending an existing compiler with a verifying module, using a type-theory based approach to program safety. Representative safety policies will be implemented, and examples developed to show that malicious code cannot be certified. The research component will be adapted for inclusion in the graduate curriculum. Furthermore, a student will be supervised towards a PhD in state-of-the-art compiler technology.

 

This material is based upon work supported by the National Science Foundation under Grant No. 0093362, and the New Jersey Commission on Science and Technology.

 

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation or the New Jersey Commission on Science and Technology.