TY - GEN
T1 - Analyzing Semantic Correctness with Symbolic Execution
T2 - 26th Annual Network and Distributed System Security Symposium, NDSS 2019
AU - Chau, Sze Yiu
AU - Yahyazadeh, Moosa
AU - Chowdhury, Omar
AU - Kate, Aniket
AU - Li, Ninghui
N1 - Publisher Copyright:
© NDSS 2019.All rights reserved.
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/85119341699
U2 - 10.14722/ndss.2019.23430
DO - 10.14722/ndss.2019.23430
M3 - Conference contribution
AN - SCOPUS:85119341699
T3 - 26th Annual Network and Distributed System Security Symposium, NDSS 2019
BT - 26th Annual Network and Distributed System Security Symposium, NDSS 2019
PB - The Internet Society
Y2 - 24 February 2019 through 27 February 2019
ER -