Practical Security Analysis of C Programs Using Automated Theorem Proving

Designing and implementing cryptographic protocols is known to be difficult. A lot of research has been devoted to develop formal techniques to analyze designs of cryptographic protocols. Less attention has been paid to the verification of protocol implementations. This is an important challenge since it is non-trivial to securely implement secure designs, because a specification by its nature is more abstract than the corresponding implementation, and the additional information may introduce attacks not present on the design level. In this paper, we address this problem in an approach which analyzes C code implementations of cryptographic protocols for high-level security requirements such as secrecy using abstraction techniques and automated theorem provers for first order logic. The approach is efficient and, by making use of abstraction tables, as automatic as possible. As an example of this approach for practical security analysis of crypto protocol implementations, we analyze part of the OpenSSH handshake implementation.     «

Designing and implementing cryptographic protocols is known to be difficult. A lot of research has been devoted to develop formal techniques to analyze designs of cryptographic protocols. Less attention has been paid to the verification of protocol implementations. This is an important challenge since it is non-trivial to securely implement secure designs, because a specification by its nature is more abstract than the corresponding implementation, and the additional information may introduce at...     »