Cryptographic Protocol Analysis on Real C Code

9 years 1 months ago
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.
Jean Goubault-Larrecq, Fabrice Parrennes
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Authors Jean Goubault-Larrecq, Fabrice Parrennes
Comments (0)