In Proceedings of the 13th International Static Analysis Symposium (SAS), Seoul, Korea, August 2006. LNCS, (c) Springer-Verlag.

Gilles Barthe, Benjamin Grégoire, César Kunz, and Tamara Rezk
INRIA Sophia-Antipolis, Project EVEREST.

Abstract. Certifying compilation provides a means to ensure that untrusted mobile code satisfies its functional specification. A certifying compiler generates code as well as a machine-checkable “certificate”, i.e. a formal proof that establishes adherence of the code to specified properties. While certificates for safety properties can be built fully automatically, certificates for more expressive and complex properties often require the use of interactive code verification. We propose a technique to provide code consumers with the benefits of interactive source code verification. Our technique, certificate translation, extends program transformations by offering the means to turn certificates of functional correctness for programs in high-level languages into certificates for executable code. The article outlines the principles of certificate translation, using specifications written in first order logic. This translation is instantiated for standard compiler optimizations in the context of an intermediate RTL Language.