Around all of it

Compiler Correctness & Security

The one program whose bugs are everyone else’s bugs: miscompilation, differential testing, fuzzing, translation validation and formal verification.

Miscompilation
▶ lab

The compiler turns a valid program into behavior the language does not allow it to have. It is the only bug class where reading your own source cannot find it, and it silently invalidates every test you have — including the ones that pass.

Q · How would I ever know whether the wrong answer came from my code or from the compiler?
Testing a Compiler
▶ lab

Seven layers, from a unit test on one pass to a fuzzer generating programs nobody wrote. The highest-value test in any compiler is the property that optimization never changes what a program prints — and it is the one most compilers add last.

Q · What does a serious test suite for a compiler actually contain, and which test earns the most?
Golden Tests

Record the emitted IR, assembly or diagnostics in a file and diff against it on every change. Excellent at catching what you did not mean to do, useless at telling you whether what you meant was right — and completely dependent on the compiler being deterministic.

Q · When is a recorded-output test worth its maintenance cost, and what can it never tell me?
Differential Testing
▶ lab

Compile and run the same program through two compilers, two versions or two optimization levels, and compare. It needs no oracle — the implementations are each other’s oracle — but it needs programs whose behavior the language actually pins down, which is the entire difficulty.

Q · How can I test a compiler when I have no way of knowing what the right answer is?
Compiler Fuzzing
▶ lab

Generate programs nobody wrote to find crashes and, far more valuably, wrong code. Csmith and YARPGen construct programs that are well-defined by design; EMI takes the opposite route and mutates code that provably never executes, so the output must not change.

Q · How do people actually find compiler bugs, given that nobody is writing the programs that trigger them?
Translation Validation
▶ lab

Do not prove the optimizer correct — prove that *this* compilation preserved semantics. A checker runs alongside the compiler, compares the IR before and after each transformation, and reports the ones it cannot justify. Alive2 does this for LLVM, and it found bugs that had been shipping for years.

Q · Can I get some of the assurance of a verified compiler without rewriting the compiler in a proof assistant?
Verified Compilers

CompCert’s middle-end and backend carry a machine-checked proof that the compiled code refines the source semantics. The honest evidence is the Yang et al. fuzzing result: every other compiler tested had wrong-code bugs found, and the verified part of CompCert had none. What is *not* proven matters just as much.

Q · What does it actually mean for a compiler to be proven correct, and what is still not proven?
Compilers and Security

The compiler is a trusted component that can delete your security code, exploit your undefined behavior into a vulnerability, or be malicious itself. The canonical case is a `memset` that zeroes a password buffer being removed as a dead store — which is why `explicit_bzero` and `SecureZeroMemory` exist.

Q · In what ways is the compiler part of my threat model rather than part of my toolbox?