Parser assurance

The security of many software systems critically depends on the correctness of their parsers that parse potentially malicious input files. However, the software community lacks methodologies for constructing high-assurance parsers. This project studies general methodologies of increasing parser insurance, by adopting formal verification and fuzzing.

Participants

• Xiaodong Jia
• Ashish Kumar
• Jialun Zhang
• Gang Tan

Publications

• Jia, X., Kumar, A., and Tan, G. (2021). A derivative-based parser generator for visibly pushdown grammars. Proceedings of the ACM on Programming Languages, 5(OOPSLA), 1–24. [paper]
• Paranjpe, A. and Tan, G. (2021). Bohemia: A validator for parser frameworks. In 7th Workshop on Language-Theoretic Security (LangSec). [paper]
• Tan, G. and Morrisett, G. (2018). Bidirectional grammars for machine-code decoding and encoding. Journal of Automated Reasoning, 60(3), 257–277. [paper]
• Tan, G. and Morrisett, G. (2016). Bidirectional grammars for machine-code decoding and encoding. In 8th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), pages 73–89. [paper]
• Morrisett, G., Tan, G., Tassarotti, J., Tristan, J.-B., and Gan, E. (2012). Rocksalt: Better, faster, stronger SFI for the x86. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 395–404. [paper]. [webpage]

Sponsors