Analyzing Semantic Correctness with Symbolic Execution: A Case Study on PKCS#1 v1.5 Signature Verification
Analyzing Semantic Correctness with Symbolic Execution: A Case Study on PKCS#1 v1.5 Signature Verification
复制标题
DOI：
10.14722/ndss.2019.23430
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Sze Yiu Chau;Moosa Yahyazadeh;Omar Chowdhury;Aniket Kate;Ninghui Li
中科院分区：
文献类型：
--
作者：
Sze Yiu Chau;Moosa Yahyazadeh;Omar Chowdhury;Aniket Kate;Ninghui Li
- 我们讨论了符号执行如何不仅可以用来查找低级错误，而且还可以分析协议实现的语义正确性。为了避免手工制作测试用例，我们提出了一种元级搜索策略，它利用源于输入格式的约束自动生成concolic测试用例。此外，为了帮助根本原因分析，我们开发了约束出处跟踪（CPT），一种机制，将原子子公式的路径约束与其相应的源级别的起源。我们通过PKCS#1 v1.5签名验证的案例研究展示了符号分析的力量。利用元级搜索和CPT，我们分析了15个最近使用符号执行的开源实现，并在其中6个中发现了语义语法。对这些算法的进一步分析表明，4种实现容易受到Bleichenbacher低指数RSA签名伪造的新变体的影响。一种实现遭受了具有故意制作的签名的潜在拒绝服务攻击。我们已负责任地与受影响供应商分享所有发现。在已发现的火山岩中，6个新的火山岩已被分配给立即可开采的火山岩。
— We discuss how symbolic execution can be used to not only find low-level errors but also analyze the semantic correctness of protocol implementations. To avoid manually crafting test cases, we propose a strategy of meta-level search, which leverages constraints stemmed from the input formats to automatically generate concolic test cases. Additionally, to aid root-cause analysis, we develop constraint provenance tracking (CPT), a mechanism that associates atomic sub-formulas of path constraints with their corresponding source level origins. We demonstrate the power of symbolic analysis with a case study on PKCS#1 v1.5 signature verification. Leveraging meta-level search and CPT, we analyzed 15 recent open-source implementations using symbolic execution and found semantic flaws in 6 of them. Further analysis of these flaws showed that 4 implementations are susceptible to new variants of the Bleichenbacher low-exponent RSA signature forgery. One implementation suffers from potential denial of service attacks with purposefully crafted signatures. All our findings have been responsibly shared with the affected vendors. Among the flaws discovered, 6 new CVEs have been assigned to the immediately exploitable ones.