Parsers are security-critical components of many software systems, and formally verified parsing therefore has a key role to play in secure software design. However, existing verified parsers for context-free grammars are limited either in their expressiveness or in their termination properties: they are only compatible with a restricted class of grammars, or they are not guaranteed to terminate on all inputs.
In this work, we present CoStar, a verified parser that overcomes both limitations. The parser is implemented with the Coq Proof Assistant and is based on a purely functional adaptation of the ALL(*) parsing algorithm. CoStar is compatible with non-left-recursive grammars of arbitrary complexity; if the parser is applied to a non-left-recursive grammar, 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. The parser is therefore a decision procedure for language membership. Finally, CoStar achieves linear-time performance on a range of unambiguous grammars for real-world languages and data formats.
Thu 16 JunDisplayed time zone: Pacific Time (US & Canada) change
10:40 - 12:00
|(ICFP 2021) Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model
|(PLDI 2020) Zippy LL(1) Parsing with Derivatives
|(PLDI 2021) CoStar: A Verified ALL(*) Parser
|(PLDI 2021) Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic