Certified Compilation based on G\"odel Numbers

TL;DR

This paper introduces a novel certification method using G"odel numbers to verify that compiled binaries faithfully represent their source code, enhancing trust in compiler outputs and preventing malicious modifications.

Contribution

The paper presents a new certification approach based on G"odel numbers, providing a formal guarantee that binaries match source code, along with a practical implementation called Charon for a subset of C.

Findings

Certificates can be derived in constant time from source and binary

Charon successfully compiles a cryptographic language subset with verified certificates

The method ensures binary statements and dependencies match source code

Abstract

In his 1984 Turing Award lecture, Ken Thompson showed that a compiler could be maliciously altered to insert backdoors into programs it compiles and perpetuate this behavior by modifying any compiler it subsequently builds. Thompson's hack has been reproduced in real-world systems for demonstration purposes. Several countermeasures have been proposed to defend against Thompson-style backdoors, including the well-known {\it Diverse Double-Compiling} (DDC) technique, as well as methods like translation validation and CompCert-style compilation. However, these approaches ultimately circle back to the fundamental question: "How can we trust the compiler used to compile the tools we rely on?" In this paper, we introduce a novel approach to generating certificates to guarantee that a binary image faithfully represents the source code. These certificates ensure that the binary contains all and only the statements from the source code, preserves their order, and maintains equivalent def-use dependencies. The certificate is represented as an integer derivable from both the source code and the binary using a concise set of derivation rules, each applied in constant time. To demonstrate the practicality of our method, we present Charon, a compiler designed to handle a subset of C expressive enough to compile FaCT, the Flexible and Constant Time cryptographic programming language.