Portal de Periódicos da CAPES

Compiler Verification Revisited

2000; Springer Nature; Linguagem: Inglês

10.1007/978-1-4757-3188-0_15

1567-7338

Wolfgang Goerigk,

Logic, programming, and type systems

This case study mainly focuses on the execution of programs. In particular we study the execution of compiler machine programs on an abstract machine that we implement in ACL2. But this article also presents a security-related motivation for compiler verification and in particular for binary compiler implementation verification. We will prove that source level verification is not sufficient to guarantee compiler correctness. For this, we will adopt the scenario of a well-known attack to Unix operating system programs due to intruded Trojan Horses in compiler executables. Such a compiler will pass nearly every test: state of the art compiler validation, the bootstrap test, and any amount of source code inspection and verification. But for all that, it nevertheless might eventually cause a catastrophe. We will show such a program in detail; it is surprisingly easy to construct such a program. In that, we share a common experience with Ken Thompson, who initially documented this kind of attack in 1984 in his Turing Award Lecture [106].