Abstract:
Many software systems employ parsing techniques to map sequential input to structured output. Often, a parser is the system component that consumes data from an untrusted source. Because parsers mediate between the outside world and application internals, they are good targets for formal verification; parsers that come with strong correctness guarantees are likely to increase the overall security of applications that rely on them.
In this talk, I will present a verified parser generator based on the linear-time LL(1) parsing algorithm. When applied to a context-free grammar, the tool produces an LL(1) parser for the grammar 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 with respect to the input grammar’s semantics, and that they terminate with meaningful results on both valid and invalid inputs.
Bio:
Sam Lasser is a third-year computer science PhD student at Tufts University, where he is advised by Dr. Kathleen Fisher. His research involves using interactive theorem proving techniques to produce verified software for data processing and programming language implementation. He is a Draper Fellowship recipient.