Verification tools check the source program, not the binary the compiler produces, so code that is proven correct can still carry a back-door when a known compiler bug miscompiles it. In joint research with Cristian Cadar and Luís Pina at Imperial College London, I explored this attack vector: how it works, how to deploy it against the open-source programs Lighttpd and Vsftpd and how it could extend to cryptographic back-doors.
Compiler-based Back-doors
Aug 20173 posts
-
Compiler-based Back-doors - Part I
Learn about a new attack vector based on compiler wrong-code generation.
Read -
Compiler-based Back-doors - Part II
Design the attack for open-source applications Lighttpd and Vsftpd
Read -
Compiler-based Back-doors - Part III
Develop the attack by targeting powerful cryptographic back-doors, which constitute a motivation for further research.
Read