Cryptographic Protocol Analysis on Real C Code

Abstract. Implementations of cryptographic protocols, such as OpenSSL for example, contain bugs affecting security, which cannot be detected by just analyzing abstract protocols (e.g., SSL or TLS). We describe how cryptographic protocol verification techniques based on solving clause sets can be applied to detect vulnerabilities of C programs in the Dolev-Yao model, statically. This involves integrating fairly simple pointer analysis techniques with an analysis of which messages an external intruder may collect and forge. This also involves relating run-time data with abstract, logical terms representing messages. To this end, we make use of so-called trust assertions. The output of the analysis is a set of clauses in the decidable class § ¥ , which can then be solved independently. This can be used to establish secrecy properties, and to detect some other bugs.

• Type: Conference
• Year: 2005
• Where: VMCAI
• Authors: Jean Goubault-Larrecq, Fabrice Parrennes
• Keywords: Bugs Affecting Security, Cryptographic Protocol, Cryptographic Protocol Verification, Software Engineering, VMCAI 2005