Proof-transforming compilation of programs with abrupt termination

ABSTRACT

The execution of untrusted bytecode programs can produce undesired behavior. A proof on the bytecode programs can be generated to ensure safe execution. Automatic techniques to generate proofs, such as certifying compilation, can only be used for a restricted set of properties such as type safety. Interactive verification of bytecode is difficult due to its unstructured control flow. Our approach is verify programs on the source level and then translate the proof to the byte-code level. This translation is non-trivial for programs with abrupt termination. We present proof transforming compilation from Java to Java Bytecode. This paper formalizes the proof transformation and present a soundness result.

REFERENCES

• 1: F. Y. Bannwart and P. Müller. A Logic for Bytecode. In F. Spoto, editor, Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE), volume 141 of ENTCS, pages 255--273. Elsevier, 2005.
• 2: G. Barthe, B. Grégoire, C. Kunz, and T. Rezk. Certificate Translation for Optimizing Compilers. In 13th International Static Analysis Symposium (SAS), LNCS, Seoul, Korea, August 2006. Springer-Verlag.
• 3: G. Barthe, T. Rezk, and A. Saabas. Proof obligations preserving compilation. In Third International Workshop on Formal Aspects in Security and Trust, Newcastle, UK, pages 112--126, 2005.
• 4: Bor-Yuh Evan Chang , Adam Chlipala , George C. Necula , Robert R. Schneck, The open verifier framework for foundational verifiers, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.1-12, January 10-10, 2005, Long Beach, California, USA [doi>10.1145/1040294.1040295]
• 5: 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
• 6: P. Müller. Modular Specification and Verification of Object-Oriented Programs, volume 2262 of LNCS. Springer-Verlag, 2002.
• 7: P. Müller and M. Nordio. Proof-Transforming Compilation of Programs with Abrupt Termination. Technical Report 565, ETH Zurich, 2007.
• 8: George Ciprian Necula , Peter Lee, Compiling with proofs, Carnegie Mellon University, Pittsburgh, PA, 1998
• 9: 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
• 10: M. Pavlova. Java Bytecode verification and its applications. PhD thesis, University of Nice Sophia-Antipolis, 2007.
• 11: A. Poetzsch-Heffter and M. J. Gawkowski. Towards Proof Generating Compilers. ENTCS, 132(1):37--51, 2005.
• 12: Arnd Poetzsch-Heffter , Peter Müller, A Programming Logic for Sequential Java, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.162-176, March 22-28, 1999
• 13: A. Poetzsch-Heffter and N. Rauch. Soundness and Relative Completeness of a Programming Logic for a Sequential Java Subset. Technical report, Technische Universität Kaiserlautern, 2004.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Verification

Keywords:
proof-carrying code, proof-transforming compiler, trusted components