CAREER: Foundations and Verification of Parsers and Type Checkers

Parsing untrusted inputs into formats usable by software systems is a ubiquitous, security-critical task. Bugs in parsing components are one of the most common sources of critical security vulnerabilities in practice. As more software is automatically generated by AI systems, this problem exacerbates as manual human auditing for correctness and security is reduced or eliminated. The project's impacts are to enable mathematical verification of correctness, safety and security of parsing components for a variety of parsing domains encountered in practice. Any code using this system, even AI generated, will be mathematically proven to be free of security vulnerabilities, without manual human intervention. The project's novelties are in the design of new domain-specific programming languages in which these specifications and parsers are to be written, extending prior formalisms to more realistic specifications. The key technical idea is to use dependent Lambek calculus, an ordered linear type theory, as a language for specifying formal grammars as types and intrinsically verified parsers as well-typed terms. The investigator will lead the design and implementation of embedded domain-specific languages based on dependent Lambek calculus in the Lean proof assistant. The project will develop libraries for specification of grammars and verification of parsers as well as verified parser generators within the domain-specific language. The project will target a variety of parsing domains: regular expressions, context-free grammars, data-dependent formats and type systems. These libraries will enable the implementation of modular verified parsing components that can be used to support larger formally verified software systems. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria. NSF Award ID: 2540652 | Program: 01002930DB NSF RESEARCH & RELATED ACTIVIT,01002627DB NSF RESEARCH & RELATED ACTIVIT,01003031DB NSF RESEARCH & RELATED ACTIVIT | Principal Investigator: Max New | Institution: Regents of the University of Michigan - Ann Arbor, ANN ARBOR, MI | Award Amount: $424,806 View on NSF Award Search: https://www.nsf.gov/awardsearch/show-award/?AWD_ID=2540652 View on Research.gov: https://www.research.gov/awardapi-service/v1/awards/2540652.html