The design and implementation of a certifying compiler

ABSTRACT

This paper presents the design and implementation of a compiler that translates programs written in a type-safe subset of the C programming language into highly optimized DEC Alpha assembly language programs, and a certifier that automatically checks the type safety and memory safety of any assembly language program produced by the compiler. The result of the certifier is either a formal proof of type safety or a counterexample pointing to a potential violation of the type system by the target program. The ensemble of the compiler and the certifier is called a certifying compiler.Several advantages of certifying compilation over previous approaches can be claimed. The notion of a certifying compiler is significantly easier to employ than a formal compiler verification, in part because it is generally easier to verify the correctness of the result of a computation than to prove the correctness of the computation itself. Also, the approach can be applied even to highly optimizing compilers, as demonstrated by the fact that our compiler generates target code, for a range of realistic C programs, which is competitive with both the cc and gcc compilers with all optimizations enabled. The certifier also drastically improves the effectiveness of compiler testing because, for each test case, it statically signals compilation errors that might otherwise require many executions to detect. Finally, this approach is a practical way to produce the safety proofs for a Proof-Carrying Code system, and thus may be useful in a system for safe mobile code.

References

1. Boyer, R. and J. S. Moore (1979). A Computational Logic. Academic Press.
2. Cimatti, A. et al. (1997, June). A provably correct embedded verifier for the certification of safety critical software, in Computer Aided Verification. 9th International Conference. Proceedings, pp. 202-213. Springer- Verlag.
3. D.C. Luckham, e. (1979, March). Stanford Pascal verifier user manual. Technical Report STAN-CS-79-731, Dept. of Computer Science, Stanford Univ.
4. Detlefs, D. (1996). An overview of the Extended Static Checking system. In Proceedings of the First Formal Methods in Software Practice Workshop.
5. Dybjer, P. (1986). Using domain algebras to prove the correctness of a compiler. Lecture Notes in Computer Science (182).
6. Gordon, M. (1985, July). HOL: A machine oriented formulation of higher-order logic. Technical Report 85, University of Cambridge, Computer Laboratory.
7. Gosling, J., B. Joy, and G. L. Steele (1996). The Java Language Specification. The Java Series. Reading, MA, USA: Addison-Wesley.
8. Guttman, J. D., J. D. Ramsdell, and M. Wand (1995). VLISP: a verified implementation of Scheme. Lisp and Symbolic Computation (8), 5-32.
9. Harper, R., F. Honsell, and G. Plotkin (1993, January). A framework for defining logics. Journal o/the Association .for Computing Machinery ~0(1), 143-184.
10. Lindholm, T. and F. Yellin (1997, January). The Java Virtual Machine Specification. The Java Series. Reading, MA, USA: Addison-Wesley.
11. McCarthy, J. (1963). Towards a mathematical theory of computation. In C. M. Popplewell (Ed.), Proceedings of the International Congress on Information Processing, pp. 21-28. North-Holland.
12. Moore, J. S. (1989). A mechanically verified language implementation. Journal o/Automated Reasoning (5), 461-492.
13. Morris, F. L. (1973). Advice on structuring compilers and proving them correct. In Proceedings of the First A CM Symposium on Principles o/Programming Languages, pp. 144-152.
14. Morrisett, G., D. Walker, and K. Crary (1998, January). From System F to typed assembly language. In The ~5th Annual A CM Symposium on Principles o/Programming Languages. ACM. To appear.
15. Necula, G. C. (1997, January). Proof-carrying code. In The ~~th Annual A CM Symposium on Principles o/ Programming Languages, pp. 106-119. ACM.
16. Necula, G. C. and P. Lee (1996, October). Safe kernel extensions without run-time checking. In Second Symposium on Operating Systems Design and Implementa. tions, pp. 229-243. Usenix.
17. Necula, G. C. and P. Lee (1997, October). Efficient representation and validation of logical proofs. Technical Report CMU-CS-97-172, Computer Science Department, Carnegie Mellon University.
18. Nelson, G. and D. Oppen (1979, October). Simplification by cooperating decision procedures. A CM Transactions on Programming Languages and Systems I(2), 245-257.
19. Oliva, D. P., J. D. Ramsdell, and M. Wand (1995). The VLISP verified PreScheme compiler. Lisp and Symbolic Computation (8), 111-182.
20. Owre, S., J. M. Rushby, and N. Shankar (1992, June). PVS: A prototype verification system. In D. Kapur (Ed.), 11th International Con/erence on Automated Deduction (CADE), Volume 607 of Lecture Notes in Artificial Intelligence, Saratoga, NY, pp. 748-752. Springer-Verlag.
21. Shostak, R. (1981, October). Deciding linear inequalities by computing loop residues. Journal of the ACM ~8(4), 769-779.
22. Tarditi, D., J. G. Morrisett, P. Cheng, C. Stone, R. Harper, mad P. Lee (1996, May). TIL: A typedirected optimizing compiler for ML. In PLDI'96 Con- /erence on Programming Language Design and Implementation, pp. 181-192.
23. Thatcher, J. W., E. G. Wagner, and J. B. Wright (1980). More on advice on structuring compilers and proving them correct. LNCS'94: Proceedings o/a Workshop on Semantics-Directed Compiler Generation (94), 165- 188.
24. Young, W. D. (1989). A mechanically verified code generator. Journal of Automated Reasoning (5), 493-518.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • Compilers

    • General programming languages

      • Language types

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification