Certificate translation for optimizing compilers
- 1 June 2009
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 31 (5) , 1-45
- https://doi.org/10.1145/1538917.1538919
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.Keywords
This publication has 31 references indexed in Scilit:
- Formal verification of translation validatorsACM SIGPLAN Notices, 2008
- Type systems equivalent to data-flow analyses for imperative languagesTheoretical Computer Science, 2006
- Formal certification of a compiler back-end orACM SIGPLAN Notices, 2006
- Bytecode Analysis for Proof Carrying CodeElectronic Notes in Theoretical Computer Science, 2005
- A Program Logic for BytecodeElectronic Notes in Theoretical Computer Science, 2005
- A type system for certified binariesACM Transactions on Programming Languages and Systems, 2005
- VOCElectronic Notes in Theoretical Computer Science, 2002
- Translation validation for an optimizing compilerACM SIGPLAN Notices, 2000
- The design and implementation of a certifying compilerACM SIGPLAN Notices, 1998
- VLISP: A verified implementation of SchemeHigher-Order and Symbolic Computation, 1995