Formal certification of a compiler back-end or: programming a compiler with a proof assistant

ABSTRACT

This paper reports on the development and formal certification (proof of semantic preservation) of a compiler from Cminor (a C-like imperative language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a certified compiler is useful in the context of formal methods applied to the certification of critical software: the certification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.

REFERENCES

• 1: Gilles Barthe , Pierre Courtieu , Guillaume Dufay , Simão Melo de Sousa, Tool-Assisted Specification and Verification of the JavaCard Platform, Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology, p.41-59, September 09-13, 2002
• 2: Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
• 3: Y. Bertot, B. Grégoire, and X. Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In Types for Proofs and Programs, Workshop TYPES 2004, LNCS. Springer-Verlag, 2005.
• 4: S. Blazy and X. Leroy. Formal verification of a memory model for C-like imperative languages. In International Conference on Formal Engineering Methods (ICFEM 2005), volume 3785 of LNCS, pages 280--299. Springer-Verlag, 2005.
• 5: J. O. Blech, S. Glesner, J. Leitner, and S. Mülling. Optimizing code generation from SSA form: A comparison between two formal correctness proofs in Isabelle/HOL. In Proc. COCV Workshop (Compiler Optimization meets Compiler Verification), 2005.
• 6: D. Cachera, T. Jensen, D. Pichardie, and V. Rusu. Extracting a data flow analyser in constructive logic. In European Symposium on Programming 2004, volume 2986 of LNCS, pages 385--400. Springer-Verlag, 2004. Extended version to appear in Theor. Comp. Sci.
• 7: G. J. Chaitin, Register allocation & spilling via graph coloring, Proceedings of the 1982 SIGPLAN symposium on Compiler construction, p.98-105, June 23-25, 1982, Boston, Massachusetts, United States
• 8: S. Coupet-Grimal and W. Delobel. A Uniform and Certified Approach for Two Static Analyses. Research report 24-2005, Laboratoire d'Informatique Fondamentale, Marseille, France, April 2005.
• 9: P. Cousot. The calculational design of a generic abstract interpreter. In M. Broy and R. Steinbrüggen, editors, Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam, 1999.
• 10: Maulik A. Dave, Compiler verification: a bibliography, ACM SIGSOFT Software Engineering Notes, v.28 n.6, November 2003 [doi>10.1145/966221.966235]
• 11: Axel Dold , Vincent Vialard, A Mechanically Verified Compiling Specification for a Lisp Compiler, Proceedings of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science, p.144-155, December 13-15, 2001
• 12: Lal George , Andrew W. Appel, Iterated register coalescing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.3, p.300-324, May 1996 [doi>10.1145/229542.229546]
• 13: Gerhard Goos , Wolf Zimmermann, Verification of Compilers, Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel), p.201-230, January 1999
• 14: B. Grégoire. Compilation des termes de preuves: un (nouveau) mariage entre Coq et Ocaml. PhD thesis, University Paris 7, 2003.
• 15: G. Klein and T. Nipkow. A machine-checked model for a Java-like language, virtual machine and compiler. Technical Report 0400001T.1, National ICT Australia, Mar. 2004. To appear in ACM TOPLAS.
• 16: Jens Knoop , Dirk Koschützki , Bernhard Steffen, Basic-Block Graphs: Living Dinosaurs?, Proceedings of the 7th International Conference on Compiler Construction, p.65-79, March 28-April 04, 1998
• 17: Dirk Leinenbach , Wolfgang Paul , Elena Petrova, Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes, Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, p.2-12, September 07-09, 2005 [doi>10.1109/SEFM.2005.51]
• 18: Sorin Lerner , Todd Millstein , Erika Rice , Craig Chambers, Automated soundness proofs for dataflow analyses and transformations via local rules, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.364-377, January 12-14, 2005, Long Beach, California, USA
• 19: P. Letouzey. A new extraction for Coq. In Types for Proofs and Programs, Workshop TYPES 2002, volume 2646 of LNCS, pages 200--219. Springer-Verlag, 2003.
• 20: J. Strother Moore, A mechanically verified language implementation, Journal of Automated Reasoning, v.5 n.4, p.461-492, Dec. 1989
• 21: J. Strother Moore, Piton: a mechanically verified assembly-level language, Kluwer Academic Publishers, Norwell, MA, 1996
• 22: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 23: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 24: George C. Necula, Translation validation for an optimizing compiler, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.83-94, June 18-21, 2000, Vancouver, British Columbia, Canada
• 25: George C. Necula , S. P. Rahul, Oracle-based checking of untrusted software, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.142-154, January 2001, London, United Kingdom
• 26: Simon L. Peyton Jones , Norman Ramsey , Fermin Reig, C--: A Portable Assembly Language that Supports Garbage Collection, Proceedings of the International Conference PPDP'99 on Principles and Practice of Declarative Programming, p.1-28, September 29-October 01, 1999
• 27: D. Pichardie. Interprétation abstraite en logique intuitionniste: extraction d'analyseurs Java certifiés. PhD thesis, University Rennes 1, Dec. 2005.
• 28: Amir Pnueli , Michael Siegel , Eli Singerman, Translation Validation, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.151-166, March 28-April 04, 1998
• 29: L. Rideau and B. P. Serpette. Coq à la conquête des moulins. In Journées françaises des langages applicatifs (JFLA 2005), pages 169--180. INRIA, 2005.
• 30: M. Rinard and D. Marinov. Credible compilation with pointers. In Proc. FLoC Workshop on Run-Time Result Verification, 1999.
• 31: Xavier Rival, Symbolic transfer function-based approaches to certified compilation, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-13, January 14-16, 2004, Venice, Italy
• 32: R. Stärk, J. Schmid, and E. Börger. Java and the Java Virtual Machine. Springer-Verlag, 2001.
• 33: Martin Strecker, Formal Verification of a Java Compiler in Isabelle, Proceedings of the 18th International Conference on Automated Deduction, p.63-77, July 27-30, 2002
• 34: M. Strecker. Compiler verification for C0. Technical report, Université Paul Sabatier, Toulouse, April 2005.
• 35: L. D. Zuck, A. Pnueli, Y. Fang, and B. Goldberg. VOC: A translation validator for optimizing compilers. Electr. Notes Theor. Comput. Sci., 65(2), 2002.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability; Correctness proofs; Formal methods
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers; Optimization

General Terms:
Languages, Reliability, Security, Verification

Keywords:
certified compilation, compiler transformations and optimizations, program proof, semantic preservation, the Coq theorem prover