Verbatim: A Verified Lexer Generator

Abstract

Undergraduate Thesis Defense:

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 talk 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. Finally, we discuss unverified optimizations and their performance. All correctness proofs have been mechanized in Coq.

Please join the meeting in Sococo VH 102, or Zoom.

Join Zoom Meeting: https://tufts.zoom.us/j/98610939077

PASSWORD: See colloquia email

Dial by your location: +1 646 558 8656 US (New York)

Meeting ID: 986 1093 9077

PASSCODE: See colloquia email