Lenore Zuck and Venkat Venkatakrishnan

Security flaws are the most pervasive form of software errors today. This project proposes to design and implement DOC: a Defensive Optimizing Compiler for both C and Java that will employ aggressive optimizations and defend code against the coding errors listed in “The 2011 CWE/SANS Top 25 Most Dangerous Software Errors” referred to hereon as MITRE-25. In addition to being an optimizing compiler in the traditional sense, DOC is defensive by its ability to prevent security flaws by halting execution when a MITRE-25 error is unavoidable.

We expect DOC to be useful to the entire community of software developers as it will considerably improve performance while also significantly enhancing security. Any code “exposed” to the outside world, e.g., web applications, database programs, and networking code, would benefit from DOC by being verified and optimized.

A compiler such as DOC is out of reach today because of the complexity of program analysis required to attain it. Current compiler optimizations build upon sophisticated and fast program analysis, and solve, in as much as possible, polynomial-time problems. Suppose, however, that we had at our disposal an oracle to perform highly complex analysis. Armed with such an oracle, we should be able to construct a defensive compiler. The parent  DARPA program  envisions building such  an oracle – a complete program verification can supply one with constructs, such as invariants and ranking functions, which are infeasible to compute using the limited program analysis in current compilers. With full proofs and their artifacts, a much deeper program analysis is obtained which can considerably expand the reach of currently available optimizations.

We anticipate DOC to interact with the other efforts of the DARPA program by generating proof obligations whose verification would enable aggressive, non-trivial optimizations. Because of its aggressive optimizations, DOC will include a “translation validation” (TV) option that will, for each run, generate a proof of correctness that can be independently checked by any theorem prover. This is likely to be useful for safety-critical software where the cost of translation errors may be catastrophic.

DOC will be evaluated on large benchmark programs provided by DARPA and other widely- used open-source software. It will generate code that significantly outperforms code generated by current compilers. Our main metric is execution time and we expect DOC to offer significantly  large speed-ups compared to GCC with optimizations. For programs that require insertion of defensive code to run securely, DOC will generate code with a minimal number of security checks.