Reference. Verbatim++: verified, optimized, and semantically rich lexing with derivatives

Derek Egolf, Sam Lasser, Kathleen Fisher · CPP · 2022 · parsing · PDF · DOI · pldb

Cite
Cite as @egolf-2022-verbatim (helia, typst) · \cite{egolf-2022-verbatim} (LaTeX)
BibTeX
bibtex · 1 line
@inproceedings{egolf-2022-verbatim, series={CPP ’22}, title={Verbatim++: verified, optimized, and semantically rich lexing with derivatives}, url={http://dx.doi.org/10.1145/3497775.3503694}, DOI={10.1145/3497775.3503694}, booktitle={Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs}, publisher={ACM}, author={Egolf, Derek and Lasser, Sam and Fisher, Kathleen}, year={2022}, month=Jan, pages={27–39}, collection={CPP ’22} }
hayagriva YAML (typst)
yaml · 19 lines
egolf-2022-verbatim:
  type: article
  title: 'Verbatim++: verified, optimized, and semantically rich lexing with derivatives'
  author:
  - Egolf, Derek
  - Lasser, Sam
  - Fisher, Kathleen
  date: 2022-01
  page-range: 27-39
  url: http://dx.doi.org/10.1145/3497775.3503694
  serial-number:
    doi: 10.1145/3497775.3503694
  parent:
    type: proceedings
    title: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs
    publisher: ACM
    parent:
      type: proceedings
      title: CPP ’22
Download: egolf-2022-verbatim.bib · egolf-2022-verbatim.yml
Cited by (2)

Coqlex: Generating formally verified lexers Ouedraogo_2023Programming · 2023

A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of each component of the tool-chain. An example is the CompCert project, a formally verified C compiler, that comes with associated tools and proofs that allow to formally verify most of those components.

However, some components, in particular the lexer, remain unverified. In fact, the lexer of Compcert is generated using OCamllex, a lex-like OCaml lexer generator that produces lexers from a set of regular expressions with associated semantic actions. Even though there exist various approaches, like CakeML or Verbatim++, to write verified lexers, they all have only limited practical applicability.

In order to contribute to the end-to-end verification of compilers, we implemented a generator of verified lexers whose usage is similar to OCamllex. Our software, called Coqlex, reads a lexer specification and generates a lexer equipped with a Coq proof of its correctness. It provides a formally verified implementation of most features of standard, unverified lexer generators.

The conclusions of our work are two-fold: Firstly, verified lexers gain to follow a user experience similar to lex/flex or OCamllex, with a domain-specific syntax to write lexers comfortably. This introduces a small gap between the written artifact and the verified lexer, but our design minimizes this gap and makes it practical to review the generated lexer. The user remains able to prove further properties of their lexer. Secondly, it is possible to combine simplicity and decent performance. Our implementation approach that uses Brzozowski derivatives is noticeably simpler than the previous work in Verbatim++ that tries to generate a deterministic finite automaton (DFA) ahead of time, and it is also noticeably faster thanks to careful design choices.

We wrote several example lexers that suggest that the convenience of using Coqlex is close to that of standard verified generators, in particular, OCamllex. We used Coqlex in an industrial project to implement a verified lexer of Ada. This lexer is part of a tool to optimize safety-critical programs, some of which are very large. This experience confirmed that Coqlex is usable in practice, and in particular that its performance is good enough. Finally, we performed detailed performance comparisons between Coqlex, OCamllex, and Verbatim++. Verbatim++ is the state-of-the-art tool for verified lexers in Coq, and the performance of its lexer was carefully optimized in previous work by Egolf and al. (2022). Our results suggest that Coqlex is two orders of magnitude slower than OCamllex, but two orders of magnitude faster than Verbatim++.

Verified compilers and other language-processing tools are becoming important tools for safety-critical or security-critical applications. They provide trust and replace more costly approaches to certification, such as manually reading the generated code. Verified lexers are a missing piece in several Coq-based verified compilers today. Coqlex comes with safety guarantees, and thus shows that it is possible to build formally verified front-ends.

DOI

Verified ALL(*) Parsing with Semantic Actions and Dynamic Input Validation lasserCoStar2023NFM · 2023

Follow up to CoStar.

DOI
Cites 32 works (5 here)
With notes (5)

Verbatim: A verified lexer generator egolfVerbatimSPW · 2021
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.
DOI

A Verified LL(1) Parser Generator lasserLL1_2019ITP · 2019
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.

Predecessor to CoStar and CoStar++.

DOI

Validating LR(1) Parsers jourdanValidatingLRParsers2012Programming Languages and Systems · 2012
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.
PDF · DOI · pldb

Regular-expression derivatives re-examined owensRegularexpressionDerivativesReexamined2009JFP · 2009
Abstract Regular-expression derivatives are an old, but elegant, technique for compiling regular expressions to deterministic finite-state machines. It easily supports extending the regular-expression operators with boolean operations, such as intersection and complement. Unfortunately, this technique has been lost in the sands of time and few computer scientists are aware of it. In this paper, we reexamine regular-expression derivatives and report on our experiences in the context of two different functional-language implementations. The basic implementation is simple and we show how to extend it to handle large character sets (e.g., Unicode). We also show that the derivatives approach leads to smaller state machines than the traditional algorithm given by McNaughton and Yamada.
PDF · DOI · pldb

Derivatives of Regular Expressions brzozowskiDerivativesRegularExpressions1964JACM · 1964
Kleene’s regular expressions, which can be used for describing sequential circuits, were defined using three operators (union, concatenation and iterate) on sets of sequences. Word descriptions of problems can be more easily put in the regular expression language if the language is enriched by the inclusion of other logical operations. However, in the problem of converting the regular expression description to a state diagram, the existing methods either cannot handle expressions with additional operators, or are made quite complicated by the presence of such operators.In this paper the notion of a derivative of a regular expression is introduced and the properties of derivatives are discussed. This leads, in a very natural way, to the construction of a state diagram from a regular expression containing any number of logical operators.
DOI
External (27)
egolf-2022-verbatim reference entries/refs/egolf-2022-verbatim/egolf-2022-verbatim.hel