{"ID":2881679,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2508.12054","arxiv_id":"2508.12054","title":"Certified Compilation based on Gödel Numbers","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.","short_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 co...","url_abs":"https://arxiv.org/abs/2508.12054","url_pdf":"https://arxiv.org/pdf/2508.12054v1","authors":"[\"Guilherme de Oliveira Silva\",\"Fernando Magno Quintão Pereira\"]","published":"2025-08-16T14:12:55Z","proceeding":"cs.PL","tasks":"[\"cs.PL\"]","methods":"[]","has_code":false}