Reference. A Verified LL(1) Parser Generator
An LL(1) parser is a recursive descent algorithm that uses a single token of lookahead to build a grammatical derivation for an input sequence. We present an LL(1) parser generator that, when applied to grammar G, produces an LL(1) parser for G if such a parser exists. We use the Coq Proof Assistant to verify that the generator and the parsers that it produces are sound and complete, and that they terminate on all inputs without using fuel parameters. As a case study, we extract the tool’s source code and use it to generate a JSON parser. The generated parser runs in linear time; it is two to four times slower than an unverified parser for the same grammar.
Cite
Cited by (5)
Verified ALL(*) Parsing with Semantic Actions and Dynamic Input Validation lasserCoStar2023
Verbatim++: verified, optimized, and semantically rich lexing with derivatives egolf-2022-verbatim
CoStar: A verified ALL(*) parser lasserCoStarVerifiedALL2021
Parsers are security-critical components of many software systems, and verified parsing therefore has a key role to play in secure software design. However, existing verified parsers for context-free grammars are limited in their expressiveness, termination properties, or performance characteristics. They are only compatible with a restricted class of grammars, they are not guaranteed to terminate on all inputs, or they are not designed to be performant on grammars for real-world programming languages and data formats. In this work, we present CoStar, a verified parser that addresses these limitations. The parser is implemented with the Coq Proof Assistant and is based on the ALL(*) parsing algorithm. CoStar is sound and complete for all non-left-recursive grammars; it produces a correct parse tree for its input whenever such a tree exists, and it correctly detects ambiguous inputs. CoStar also provides strong termination guarantees; it terminates without error on all inputs when applied to a non-left-recursive grammar. Finally, CoStar achieves linear-time performance on a range of unambiguous grammars for commonly used languages and data formats.
Verbatim: A verified lexer generator egolfVerbatim
Lexers and parsers are often used as front ends to connect input from the outside world with the internals of a larger software system. These front ends are natural targets for attackers who wish to compromise the larger system. A formally verified tool that performs mechanized lexical analysis would render attacks on these front ends less effective. In this paper we present Verbatim, an executable lexer that is implemented and verified with the Coq Proof Assistant. We prove that Verbatim is correct with respect to a standard lexer specification. We also analyze its theoretical complexity and give results of an empirical performance evaluation. All correctness proofs have been mechanized in Coq.
Zippy LL(1) parsing with derivatives EdelmannZippy2020
In this paper, we present an efficient, functional, and formally verified parsing algorithm for LL(1) context-free expressions based on the concept of derivatives of formal languages. Parsing with derivatives is an elegant parsing technique, which, in the general case, suffers from cubic worst-case time complexity and slow performance in practice. We specialise the parsing with derivatives algorithm to LL(1) context-free expressions, where alternatives can be chosen given a single token of lookahead. We formalise the notion of LL(1) expressions and show how to efficiently check the LL(1) property. Next, we present a novel linear-time parsing with derivatives algorithm for LL(1) expressions operating on a zipper-inspired data structure. We prove the algorithm correct in Coq and present an implementation as a part of Scallion, a parser combinators framework in Scala with enumeration and pretty printing capabilities.
Cites 20 works (3 here)
With notes (3)
Adaptive LL(*) parsing: the power of dynamic analysis parr-2014-adaptive
Validating LR(1) Parsers jourdanValidatingLRParsers2012
An LR(1) parser is a finite-state automaton, equipped with a stack, which uses a combination of its current state and one lookahead symbol in order to determine which action to perform next. We present a validator which, when applied to a context-free grammar G and an automaton A, checks that A and G agree. Validating the parser provides the correctness guarantees required by verified compilers and other high-assurance software that involves parsing. The validation process is independent of which technique was used to construct A. The validator is implemented and proved correct using the Coq proof assistant. As an application, we build a formally-verified parser for the C99 language.
LL(*): the foundation of the ANTLR parser generator parr-2011-ll
External (17)
- The Coq Proof Assistant, version 8.9.0 (2019)
- Failure to patch two-month-old bug led to massive Equifax breach (2017)
- Cloudflare Reverse Proxies are Dumping Uninitialized Memory (2017)
- CVE-2017-5638 (2017)
- CVE-2016-0101 (2016)
- Menhir reference manual (2016)
- Real World OCaml: Functional programming for the masses (2013)
- TRX: A formally verified parser interpreter (2010)
- Certified web services in Ynot (2010)
- Verified, executable parsing (2009)
- Mechanized semantics for the Clight subset of the C language (2009)
- Extraction in Coq: An overview (2008)
- PROGRAM-ing finger trees in Coq (2007)
- Parsing Techniques (Monographs in Computer Science) (2006)
- Parsing Expression Grammars: A Recognition-based Syntactic Foundation (2004)
- Modern Compiler Implementation in ML (1998)
- A theory of type polymorphism in programming (1978)