Скачать или смотреть Certified Compilation based on Gödel Numbers - MSc Defense

This video presents the MSc defense presentation of Guilherme Oliveira on a novel method to verify compiler trustworthiness.

The "Thompson Hack," illustrated in Ken Thompson's seminal 1984 Turing Award lecture, reveals a terrifying vulnerability: a malicious compiler can insert hidden backdoors into the software it builds and even into future versions of itself. This creates a deep-seated chain of distrust—how can we ever truly trust the tools we use to build our software?

Existing countermeasures, like Diverse Double-Compiling (DDC), often lead back to this same fundamental question of trust.

In this thesis, Guilherme Oliveira proposes a novel solution. He introduces a method to generate a compact, verifiable certificate that guarantees a binary perfectly matches its source code. This certificate ensures:

Completeness: The binary contains all statements from the source.
Fidelity: It contains only those statements.
Preservation: It preserves the original statement order and def-use dependencies.

To prove its practicality, Guilherme developed Charon, a compiler for a subset of C that is expressive enough to compile FaCT, a cryptographic programming language.

Try Charon on GitHub: https://github.com/guilhermeolivsilva...