Towards Practical, End-to-End Formally Verified X.509 Certificate Validators (Verdict)#
USENIX Security '25 (34th USENIX Security Symposium) digest Program Core pick 13–15 August 2025
Zhengyao Lin et al., Carnegie Mellon University; Northeastern University — Core
- Why: X.509 validation bugs have a long history of real security vulnerabilities precisely because the standards are ambiguous and every validator deviates idiosyncratically — this is the first end-to-end formally verified validator, proven to match Chrome/Firefox/OpenSSL's actual (not just documented) behavior at scale.
- What: Verdict, a formally verified X.509 certificate validator (parsing, path building, path validation) with customizable, formally-specified validation policies compiled to efficient Rust code; validated against Chrome, Firefox, and OpenSSL policies on over ten million real Certificate Transparency certificates. (from abstract only)
- How: Validation policy is specified in first-order logic; a proof-producing compiler generates Rust code proven to conform to a subset of RFC requirements, and Verdict is shown to match each baseline's actual behavior and performance. (from abstract only)
- Where applicable: General; directly relevant to anyone building or auditing a TLS/PKI stack who wants provable conformance rather than "matches OpenSSL's quirks by accident."