Cryptographic Protocol Analysis on Real C Code
Cryptographic Protocol Analysis on Real C Code
复制标题
DOI：
10.1007/978-3-540-30579-8_24
复制
发表时间：
2005-01
期刊：
影响因子：
--
通讯作者：
J. Goubault-Larrecq;Fabrice Parrennes
中科院分区：
文献类型：
--
作者：
J. Goubault-Larrecq;Fabrice Parrennes
加密协议（例如 OpenSSL）的实现包含影响安全性的错误，仅通过分析抽象协议（例如 SSL 或 TLS）无法检测到这些错误。我们描述了如何应用基于求解子句集的密码协议验证技术来静态检测 Dolev-Yao 模型中 C 程序的漏洞。这涉及将相当简单的指针分析技术与外部入侵者可能收集和伪造哪些消息的分析相结合。这还涉及将具体的运行时数据与表示消息的抽象逻辑术语相关联。为此，我们利用所谓的信任断言。分析的输出是可判定类中的一组子句，然后可以独立求解它们。这可用于建立保密属性并检测其他一些错误。
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 concrete run-time data with abstract, logical terms representing messages. To this end, we make use of so-calledtrust 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.