SymCerts - Practical Symbolic Execution for Exposing Noncompliance in X.509 Certificate Validation

Explore a 21-minute conference talk presented at the 2017 IEEE Symposium on Security & Privacy that introduces SymCerts, a novel approach using symbolic execution to expose noncompliance in X.509 certificate validation implementations. Learn how this technique addresses the limitations of black-box fuzzing by providing better coverage and uncovering severe flaws in small footprint SSL/TLS libraries. Discover the challenges of applying symbolic execution to SSL/TLS libraries and how SymCerts, along with domain-specific optimizations, overcome the path explosion problem. Examine the process of extracting path constraints to identify missing checks and cross-validate constraints from different libraries to expose subtle noncompliance issues. Gain insights into the analysis of 9 small footprint X.509 implementations, which revealed 48 instances of noncompliance, and understand how these findings have contributed to improving the security of newer library versions.