Accessible Formal Methods for Verified Parser Development

Security flaws in Portable Document Format (PDF) readers may allow PDFs to conceal malware, exfiltrate information, and execute malicious code. For a PDF reader to identify these flawed PDFs requires first parsing the document syntactically, and then analyzing the semantic properties or structure of the parse result. This paper presents a language theoretic and developer-accessible approach to PDF parsing and validation using ACL2, a formal methods language and theorem prover. We develop two related components, a PDF syntax parser and a semantic validator. The ACL2-based parser, verified using the theorem prover, supports verification of a high-performance equivalent of itself or an existing PDF parser. The validator then extends the existing parser by checking the semantic properties in the parse result. The structure of the parser and semantic rules are defined by the PDF grammar and fall into certain patterns, and therefore can be automatically composed from a set of verified base functions. Instead of requiring a developer to be familiar with formal methods and to manually write ACL2 code, we use Tower, our modular metalanguage, to generate verified ACL2 functions and proofs and the equivalent C code to analyze semantic properties, which can then be integrated into our verified parser or an existing parser to support PDF validation.