An official website of the United States government
Here's how you know
A .mil website belongs to an official U.S. Department of Defense organization in the United States.
A lock (lock ) or https:// means you’ve safely connected to the .mil website. Share sensitive information only on official, secure websites.

NEWS | April 3, 2023

SafeDocs: Safe Documents

Project Lead:  Dr. Sergey Bratus                                                            

Sponsoring Organization:  DARPA


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.