Abstract
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].
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media New York
About this chapter
Cite this chapter
Goerigk, W. (2000). Compiler Verification Revisited. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds) Computer-Aided Reasoning. Advances in Formal Methods, vol 4. Springer, Boston, MA. https://doi.org/10.1007/978-1-4757-3188-0_15
Download citation
DOI: https://doi.org/10.1007/978-1-4757-3188-0_15
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-4981-3
Online ISBN: 978-1-4757-3188-0
eBook Packages: Springer Book Archive