Certificate translation for optimizing compilers

ABSTRACT

Proof Carrying Code provides trust in mobile code by requiring certificates that ensure the code adherence to specific conditions. The prominent approach to generate certificates for compiled code is Certifying Compilation, that automatically generates certificates for simple safety properties.

In this work, we present Certificate Translation, a novel extension for standard compilers that automatically transforms formal proofs for more expressive and complex properties of the source program to certificates for the compiled code.

The article outlines the principles of certificate translation, instantiated for a nonoptimizing compiler and for standard compiler optimizations in the context of an intermediate RTL Language.

REFERENCES

• 1: Bannwart, F. Y. and Müller, P. 2005. A program logic for bytecode. Electron. Notes Theoret. Comput. Sci. 141, 255--273.
• 2: Barnett, M., Chang, B.-Y. E., DeLine, R., Jacobs, B., and Leino, K. R. M. 2005. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects. Lecture Notes in Computer Science, vol. 4111. Springer-Verlag.
• 3: Barnett, M., Leino, K. R. M., and Schulte, W. 2005. The Spec# programming system: An overview. In Construction and Analysis of Safe, Secure and Interoperable Smart Devices: Proceedings of the International Workshop CASSIS 2004, G. Barthe, L. Burdy, M. Huisman, J.-L. Lanet, and T. Muntean, Eds. Lecture Notes in Computer Science, vol. 3362. Springer-Verlag, 151--171.
• 4: Barrett, C. W., Fang, Y., Goldberg, B., Hu, Y., Pnueli, A., and Zuck, L. D. 2005. Tvoc: A translation validator for optimizing compilers. In Proceedings of the International Conference on Computer-Aided Verification, K. Etessami and S. K. Rajamani, Eds. Lecture Notes in Computer Science, vol. 3576, Springer-Verlag, 291--295.
• 5: Barthe, G., Burdy, L., Charles, J., Grégoire, B., Huisman, M., Lanet, J.-L., Pavlova, M., and Requet, A. 2007. JACK: A tool for validation of security and behaviour of Java applications. In Formal Methods for Components and Objects: Revised Lectures from the 5th International Symposium (FMCO'06). Lecture Notes in Computer Science, vol. 4709, Springer-Verlag, 152--174.
• 6: Barthe, G., Grégoire, B., Kunz, C., and Rezk, T. 2006. Certificate translation for optimizing compilers. In Proceedings of the Static Analysis Symposium, K. Yi, Ed. Lecture Notes in Computer Science. vol. 4134, Springer-Verlag, 301--317.
• 7: Gilles Barthe , Benjamin Grégoire , Mariela Pavlova, Preservation of Proof Obligations from Java to the Java Virtual Machine, Proceedings of the 4th international joint conference on Automated Reasoning, August 12-15, 2008, Sydney, Australia [doi>10.1007/978-3-540-71070-7_7]
• 8: Barthe, G. and Kunz, C. 2008. Certificate translation in abstract interpretation. In European Symposium on Programming. Lecture Notes in Computer Science, vol. 4960. Springer-Verlag, 368--382.
• 9: Gilles Barthe , Tamara Rezk , David Naumann, Deriving an Information Flow Checker and Certifying Compiler for Java, Proceedings of the 2006 IEEE Symposium on Security and Privacy, p.230-242, May 21-24, 2006 [doi>10.1109/SP.2006.13]
• 10: Barthe, G., T. Rezk, and Saabas, A. 2005. Proof obligations preserving compilation. In Workshop on Formal Aspects in Security and Trust, T. Dimitrakos, F. Martinelli, P. Ryan, and S. Schneider, Eds. Lecture Notes in Computer Science, vol. 3866. Springer-Verlag, 112--126.
• 11: Bertot, Y., Grégoire, B., and Leroy, X. 2004. A structured approach to proving compiler optimizations based on dataflow analysis. In TYPES, J. Filliâtre, C. Paulin-Mohring, and B. Werner, Eds. Lecture Notes in Computer Science, vol. 3839. Springer, 66--81.
• 12: Blazy, S., Dargaye, Z., and Leroy, X. 2006. Formal verification of a c compiler front-end. In Proceedings of the International Conference on Formal Methods (FM), J. Misra, T. Nipkow, and E. Sekerinski, Eds. Lecture Notes in Computer Science, vol. 4085. Springer, 460--475.
• 13: Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G., Leino, K., and Poll, E. 2003. An overview of JML tools and applications. In Proceedings of the Workshop on Formal Methods for Industrial Critical Systems. Electronic Notes in Theoretical Computer Science, vol. 80. Elsevier, 73--89.
• 14: Lilian Burdy , Mariela Pavlova, Java bytecode specification and verification, Proceedings of the 2006 ACM symposium on Applied computing, April 23-27, 2006, Dijon, France [doi>10.1145/1141277.1141708]
• 15: Chalin, P., Kiniry, J. R., Leavens, G. T., and Poll, E. 2006. Beyond assertions: Advanced specification and verification with JML and ESC/Java2. In Formal Methods for Components and Objects, Lecture Notes in Computer Science, vol. 4111. 342--363.
• 16: Joshua D. Guttman , John D. Ramsdell , Mitchell Wand, VLISP: a verified implementation of Scheme, Lisp and Symbolic Computation, v.8 n.1-2, p.5-32, March 1995 [doi>10.1007/BF01128406]
• 17: Peeter Laud , Tarmo Uustalu , Varmo Vene, Type systems equivalent to data-flow analyses for imperative languages, Theoretical Computer Science, v.364 n.3, p.292-310, 8 November 2006 [doi>10.1016/j.tcs.2006.08.013]
• 18: Leino, K. R. M. 2006. Specifying and verifying programs in spec#. In Proceedings of the Ershov Memorial Conference, I. Virbitskaite and A. Voronkov, Eds. Lecture Notes in Computer Science, vol. 4378. Springer, 20.
• 19: K. Rustan M. Leino , Wolfram Schulte, Exception Safety for C#, Proceedings of the Software Engineering and Formal Methods, Second International Conference, p.218-227, September 28-30, 2004 [doi>10.1109/SEFM.2004.14]
• 20: 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
• 21: Leroy, X. 2006a. Coinductive big-step operational semantics. In Programming Languages and Systems: Proceedings of the 15th European Symposium on Programming, (ESOP'06). Lecture Notes in Computer Science, vol. 3924. Springer-Verlag, 54--68.
• 22: Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
• 23: Peter Müller , Martin Nordio, Proof-transforming compilation of programs with abrupt termination, Proceedings of the 2007 conference on Specification and verification of component-based systems: 6th Joint Meeting of the European Conference on Software Engineering and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, p.39-46, September 03-04, 2007, Dubrovnik, Croatia [doi>10.1145/1292316.1292321]
• 24: George Ciprian Necula , Peter Lee, Compiling with proofs, Carnegie Mellon University, Pittsburgh, PA, 1998
• 25: 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]
• 26: George C. Necula, Translation validation for an optimizing compiler, ACM SIGPLAN Notices, v.35 n.5, p.83-94, May 2000
• 27: George C. Necula , Peter Lee, The design and implementation of a certifying compiler, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.333-344, June 17-19, 1998, Montreal, Quebec, Canada
• 28: Nordio, M., Müller, P., and Meyer, B. 2008a. Formalizing proof-transforming compilation of eiffel programs. Tech. rep. 587, ETH Zurich.
• 29: Nordio, M., Müller, P., and Meyer, B. 2008b. Proof-transforming compilation of eiffel programs. In TOOLS-EUROPE, R. Paige, Ed. Lecture Notes in Business and Information Processing. Springer-Verlag.
• 30: 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
• 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: Saabas, A. and Uustalu, T. 2008. Program and proof optimizations with type systems. J. Logic Algebra. Program. 77, 1--2, 131--154.
• 33: Seo, S., Yang, H., and Yi, K. 2003. Automatic construction of Hoare proofs from abstract interpretation results. In Proceedings of the Asian Programming Languages and Systems Symposium, A. Ohori, Ed. Lecture Notes in Computer Science, vol. 2895. Springer-Verlag, 230--245.
• 34: Zhong Shao , Valery Trifonov , Bratin Saha , Nikolaos Papaspyrou, A type system for certified binaries, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.1, p.1-45, January 2005 [doi>10.1145/1053468.1053469]
• 35: 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
• 36: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 37: Jean-Baptiste Tristan , Xavier Leroy, Formal verification of translation validators: a case study on instruction scheduling optimizations, ACM SIGPLAN Notices, v.43 n.1, January 2008
• 38: Wildmoser, M., Chaieb, A., and Nipkow, T. 2005. Bytecode analysis for proof carrying code. In Bytecode Semantics, Verification, Analysis and Transformation, F. Spoto, Ed. Electronic Notes in Theoretical Computer Science, vol. 141. Elsevier.
• 39: Zuck, L. D., Pnueli, A., Fang, Y., and Goldberg, B. 2002. Voc: A translation validator for optimizing compilers. Electron. Notes Theor. Comput. Sci. 65, 2.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Languages, Security, Verification

Keywords:
Proof-carrying code, program optimizations, program verification, static analysis