Certification of programs via Gödel numbering
Carregando...
Arquivos
Data
Autor(es)
Título da Revista
ISSN da Revista
Título de Volume
Editor
Universidade Federal de Minas Gerais
Descrição
Tipo
Dissertação de mestrado
Título alternativo
Certificação de programas por meio da numeração de Gödel
Primeiro orientador
Membros da banca
Arthur Azevedo de Amorim
Xavier Rival
Xavier Rival
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.
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).
Assunto
Computação – Teses, Compiladores (Programas de Computador) – Certificados e licenças – Teses, Programas de Computador – Validação – Teses
Palavras-chave
Program certification, Translation validation, Gödel numbering