Certification of programs via Gödel numbering
| dc.creator | Guilherme de Oliveira Silva | |
| dc.date.accessioned | 2025-11-14T16:28:15Z | |
| dc.date.issued | 2025-09-12 | |
| dc.description.abstract | Em sua palestra ao receber o Prêmio Turing em 1984, Ken Thompson demonstrou que um compilador poderia ser sistematicamente adulterado para que insira backdoors em programas que compila e para que perpetue este comportamento ao modificar qualquer compilador que construa posteriormente. A brecha apontada por Thompson já foi reproduzida em sistemas do mundo real para fins de demonstração. Diversas contramedidas foram propostas para se defender de backdoors desta natureza, incluindo a famosa técnica de Compilação Dupla Diversa (Diverse Double-Compiling, ou DDC), e as abordagens de validação de tradução e de compilação no estilo CompCert. Estas solução, entretanto, sempre retornam `a pergunta fundamental: “Como podemos confiar no compilador que compilou as ferramentas das quais dependemos?” Esta dissertação propõe uma nova abordagem para gerar certificados que garantam que um binário represente fielmente o código fonte. Estes certificados asseguram que o binário contém todas — e somente isto — as operações do código fonte, que preserve sua ordem, e que mantenha as mesmas relações de dependência entre definição e uso. O certificado é representado como um inteiro que possa ser derivado a partir de ambos o código fonte e o binário, utilizando um conjunto conciso de regras de derivação aplicáveis em tempo constante. Para demonstrar a praticidade do método proposto, apresentamos Charon, um compilador desenhado para lidar com um subconjunto da linguagem C expressivo o suficiente para compilar programas escritos na linguagem de programação criptográfica FaCT (the Flexible and Constant Time). | |
| dc.identifier.uri | https://hdl.handle.net/1843/846 | |
| dc.language | eng | |
| dc.publisher | Universidade Federal de Minas Gerais | |
| dc.rights | Acesso aberto | |
| dc.subject | Computação – Teses | |
| dc.subject | Compiladores (Programas de Computador) – Certificados e licenças – Teses | |
| dc.subject | Programas de Computador – Validação – Teses | |
| dc.subject.other | Program certification | |
| dc.subject.other | Translation validation | |
| dc.subject.other | Gödel numbering | |
| dc.title | Certification of programs via Gödel numbering | |
| dc.title.alternative | Certificação de programas por meio da numeração de Gödel | |
| dc.type | Dissertação de mestrado | |
| local.contributor.advisor1 | Fernando Magno Quintão Pereira | |
| local.contributor.advisor1Lattes | http://lattes.cnpq.br/4608001746330875 | |
| local.contributor.referee1 | Arthur Azevedo de Amorim | |
| local.contributor.referee1 | Xavier Rival | |
| local.creator.Lattes | http://lattes.cnpq.br/6286771923943513 | |
| local.description.resumo | In his 1984 Turing Award lecture, Ken Thompson showed that a compiler could be maliciously altered to insert backdoors intoprograms 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 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?” This thesis proposes 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. | |
| local.publisher.country | Brasil | |
| local.publisher.department | ICX - DEPARTAMENTO DE CIÊNCIA DA COMPUTAÇÃO | |
| local.publisher.initials | UFMG | |
| local.publisher.program | Programa de Pós-Graduação em Ciência da Computação | |
| local.subject.cnpq | CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::METODOLOGIA E TECNICAS DA COMPUTACAO::LINGUAGENS DE PROGRAMACAO |