Reflections on Ken Thompson's Reflections on Trusting Trust
Institut für Informatik
und Prakt. Mathematik, Christian-Albrechts-Universität
Olshausenstr. 40, D-24098 Kiel, Germany, Email: email@example.com
Computer based systems are often heavily annoying their users. Errors, failures and crashes occur, due to bugs in design, implementation or integration. Hardware bugs are sensations, whereas software errors are commonplace. Even intentional errors like viruses and Trojan Horses show up time by time. Although compilation is a major topic in theoretical and practical computer science research and development since more than 40 years, correctness of realistic compilation is still a severe gap in trusted software production.
In this talk we will present a security-related motivation for proving compilers correct, and in particular for binary compiler implementation verification. We will adopt the scenario of a well-known attack to Unix operating system programs due to Trojan Horses deeply hidden within a compiler executable. Such a compiler passes nearly every test, even Wirth's strong bootstrap test, state of the art compiler validation, and no amount of source level scrutiny, code inspection or verification does help. It nevertheless might eventually cause a catastrophe.
We will show such a program in detail and give a running demonstration.
Based on self-reproducing and reflective code, it is surprisingly easy
to construct. In that, we share a common experience with Ken Thompson,
who documented such kind of attacks in his Turing Award Lecture in 1984.
We will also sketch a correct way out and some other recent work from the
context of the German joint project Verifix on Correct Compilers.