ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER
summary
Claims a first formalization of ASN.1 DER with a mechanized proof of non-malleability and a verified compiler in F that uses the EverParse framework to produce extracted OCaml parsers. It implements an automaton-style parser combinator, proves every well-formed ASN.1 declaration yields a non-malleable parser, and evaluates on X.509/CRL datasets where the OCaml parsers accept or reject inputs; notably about 7% of EFF certificates rejected*, manual checks confirm many rejections are genuine syntax errors. Performance and full semantic validation remain future work.
AI-written summary · about
chapters (8)
- 0:00Introduction to ASN.1
- 0:41Understanding ASN.1 and DER
- 4:30The ASN.1 Star approach
- 6:47Design challenges
- 8:21Formalizing semantics
- 11:54Implementation details
- 16:01Experimental evaluation
- 19:03Conclusion and Q&A
related talks
21mDaedalus: Safer Document Parsing
13mVest: Verified, Secure, High-Performance Parsing and Serialization for Rust
12mAutomated Synthesis of Verified Firewalls
27mGenerate Parsers! Prevent Exploits!- 12mAutomated Synthesis of Verified Firewalls
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
29mVale: Verifying High-Performance Cryptographic Assembly Code
41mMechanised Proofs of Atom Exhaustion in Erlang