–
Project Lead: Dr. Sergey Bratus
Sponsoring Organization: DARPA
Website: https://www.darpa.mil/program/safe-documents
Project Synopsis: SafeDocs will develop novel verified programming methodologies for building high-assurance parsers for extant electronic data formats, and novel methodologies for comprehending, simplifying, and reducing these formats to their safe, unambiguous, verification-friendly subsets (“safe sub-setting”). SafeDocs’ multi-pronged approach will combine: extracting the extant formats’ de facto syntax (including any non-compliant syntax deliberately accepted and substantially used in the wild); identifying a syntactically simpler subset of this syntax that can be used in verified programming while preserving the format's essential functionality; and creating software construction kits for building secure, verified parsers for this syntactically simpler subset, and high-assurance translators for converting extant instances of the format to this subset. The parser construction kits will be usable by industry programmers who understand the syntax of electronic data formats but lack the theoretical background in verified programming. The tools also will guide the syntactic design of new formats by making verification-friendly format syntax easy to express.