Everparse: A Verifying Compiler from Data Format Specifications to Verified Efficient Parsers

on YouTube ↗08m

" summary

A verified compiler that takes dependent data-format descriptions and emits F specifications plus Low implementations extracted to high-performance C, with proofs of functional correctness and uniqueness of binary representation to prevent malleability attacks. It integrates with Everest’s verified crypto and concurrency libraries (HACL/miTLS style) and generates zero-copy validators* and accessor code that reads directly from the input buffer. Benchmarks show validators over 10× faster than Bitcoin Core for some formats, and the pipeline produces working, provably memory-safe C.

AI-written summary · about

" related talks

• 29mVale: Verifying High-Performance Cryptographic Assembly CodeSrinath Setty, Bryan Parno, Chris Hawblitzel, Barry Bond, Manos Kapritsos, Ashay Rane, K. Rustan M. Leino, Jacob R. Lorch, Laure Thompson · 26th USENIX Security Symposium (USENIX Security '17)
• 01h 02mLanguage Design meets Verifying CompilersDavid J. Pearce · GPCE 2022
• 23mA Verified Packrat Parser Interpreter for Parsing Expression GrammarsClément Blaudeau · CPP 2020
• 50mCompCert: a journey through the landscape of mechanized semantics for verified co...Sandrine Blazy · CPP 2023
• 01h 01mExpressive Compile Time ParsersAlon Wolf · Meeting C++ 2023
• 58mFast Cryptographic Code via Partial EvaluationAdam Chlipala · PEPM 2023
• 56mProof Assistants At the Hardware-Software InterfaceAdam Chipala · CPP 2020
• 29mMy Little Parser: Tooling is MagicChris Dickinson · CascadiaJS 2013