This paper is to present 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 in order 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 strong bootstrap test, 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, and it is surprisingly easy to construct.  In
  that, we share a common experience with Ken Thompson, who initially
  documented this kind of attack.