Hardening attack surfaces with formally proven binary format parsers
Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael T. Tang, Omar D. Cardona, Arti Gupta
Abstract
With an eye toward performance, interoperability, or legacy concerns, low-level system software often must parse binary encoded data formats. Few tools are available for this task, especially since the formats involve a mixture of arithmetic and data dependence, beyond what can be handled by typical parser generators. As such, parsers are written by hand in languages like C, with inevitable errors leading to security vulnerabilities.
Topics & Concepts
ParsingComputer scienceInteroperabilityProgramming languageTask (project management)Binary numberLR parserSoftwareOperating systemArithmeticTop-down parsingMathematicsManagementEconomicsSecurity and Verification in ComputingAdvanced Malware Detection TechniquesLogic, programming, and type systems