Verbatim: A Verified Lexer Generator

Lexers and parsers are often used as front ends to connect input from the outside world with th e internals of a larger software system. These front ends are natural targets for attackers who w ish to compromise the larger system. A formally verified tool that p erforms 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 th e Coq P ro o f Assistant. We prove that Verbatim is correct with respect to a standard lexer specification. We also analyze its theoretical com plexity and give results o f an em pirical performance evaluation. All correctness proofs have been mechanized in Coq.