Daedalus: Safer Document Parsing
Iavor S. Diatchki, Mike Dodds, Harrison Goldstein, Bill Harris, David A. Holland, Benoît Razet, Cole Schlesinger, Simon Winwood
Abstract
Despite decades of contributions to the theoretical foundations of parsing and the many tools available to aid in parser development, many security attacks in the wild still exploit parsers. The issues are myriad—flaws in memory management in contexts lacking memory safety, flaws in syntactic or semantic validation of input, and misinterpretation of hundred-page-plus standards documents. It remains challenging to build and maintain parsers for common, mature data formats. In response to these challenges, we present Daedalus, a new domain-specific language (DSL) and toolchain for writing safe parsers. Daedalus is built around functional-style parser combinators, which suit the rich data dependencies often found in complex data formats. It adds domain-specific constructs for stream manipulation, allowing the natural expression of parsing noncontiguous formats. Balancing between expressivity and domain-specific constructs lends Daedalus specifications simplicity and leaves them amenable to analysis. As a stand-alone DSL, Daedalus is able to generate safe parsers in multiple languages, currently C++ and Haskell. We have implemented 20 data formats with Daedalus, including two large, complex formats—PDF and NITF–and our evaluation shows that Daedalus parsers are concise and performant. Our experience with PDF forms our largest case study. We worked with the PDF Association to build a reference implementation, which was subject to a red-teaming exercise along with a number of other PDF parsers and was the only parser to be found free of defects.
Ask about this paper
Ask your agent about it.
Lune has read the top-tier papers around this one, so every answer names the papers it rests on.
Your agent calls
Lunesearch_papers
Free to start. No credit card required.
Terminal
Install the CLIlune papers get 98799e8f-a7f0-4dad-86ad-cb244de56393Cited by top-tier papers1
Ask how each one uses itRelated papers
- EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message FormatsTahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy et al.USENIX Security 2019 · 70 citations
- CoStar: a verified ALL(*) parserSam Lasser, Chris Casinghino, Kathleen Fisher, Cody RouxPLDI 2021 · 10 citations
- Vest: Verified, Secure, High-Performance Parsing and Serialization for RustYi Cai, Pratap Singh, Zhengyao Lin, Jay Bosamiya et al.USENIX Security 2025
- 3DGen: AI-Assisted Generation of Provably Correct Binary Format ParsersSarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro et al.ICSE 2025 · 2 citations
- Hardening attack surfaces with formally proven binary format parsersNikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova et al.PLDI 2022 · 18 citations
