Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2508.12054 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913993780625408 |
|---|---|
| author | Silva, Guilherme de Oliveira Pereira, Fernando Magno Quintão |
| author_facet | Silva, Guilherme de Oliveira Pereira, Fernando Magno Quintão |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_12054 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Certified Compilation based on Gödel Numbers Silva, Guilherme de Oliveira Pereira, Fernando Magno Quintão Programming Languages 11A51 D.3.1 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. |
| title | Certified Compilation based on Gödel Numbers |
| topic | Programming Languages 11A51 D.3.1 |
| url | https://arxiv.org/abs/2508.12054 |