Code security analysis with assertions

Abstract

Designing and implementing cryptographic protocols is known to be difficult. A lot of research has been devoted to develop formal techniques to analyze abstract designs of cryptographic protocols. Less attention has been paid to the verification of implementation-relevant aspects of cryptographic protocols. 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. We propose an approach to determine security goals provided by a protocol implementation based on control flow graphs and automated theorem provers for first-order logic. More specifically, here we explain how to make use of assertions in the source code for a practical and efficient security analysis.