1. Analyzing Semantic Correctness with Symbolic Execution: A Case Study on PKCS#1 v1.5 Signature Verification 2019 FormalVerification NDSS Signatures
    Sze Yiu Chau and Moosa Yahyazadeh and Omar Chowdhury and Aniket Kate and Ninghui Li
    [View PDF on ndss-symposium.org]
    [Show BibTex Citation]

    @inproceedings{CYCKL2019PKCS,
    author = {Sze Yiu Chau and Moosa Yahyazadeh and Omar Chowdhury and Aniket Kate and Ninghui Li},
    title = {Analyzing Semantic Correctness with Symbolic Execution: A Case Study on {PKCS#1 v1.5} Signature Verification},
    booktitle = {26th Annual Network and Distributed System Security Symposium, {NDSS}
    2019, San Diego, California, USA},
    year = {2019}
    }

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.

  1.