Implementing a Direct Method for Certificate Translation

Abstract. Certificate translation is a method that transforms certificates of source programs into certificates of their compilation. It provides strong guarantees on low-level code, and is useful for eliminating trust in the compiler (for high assurance code) and in the code producer for mobile code security. The theory of certificate translation has been developed in earlier work, but no implementation exists. As a result, it has been difficult to evaluate its practicality, and in particular the impact of certificate translation on the size of certificates. In this paper, we report on the development of a certificate translator prototype. The tool takes as input a high-level program, defined in a small subset of the C programming language, and a logical specification `a la ACSL, and computes a set of verification conditions for the Coq proof assistant. Once proof obligations are discharged, the tool compiles the source program into an intermediate RTL (i.e., three-address code) repre...

• Type: Journal
• Year: 2009
• Where: ICFEM
• Authors: Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet
• Keywords: Certificate, Certificate Translation, Code, ICFEM 2009, Software Engineering