DARPA’s SafeDocs initiative

The US Defense Advanced Research Projects Agency (DARPA) is starting a project to improve detection of invalid or maliciously crafted data in electronic documents.

It may safely be assumed that PDF, while already meeting many of the project's objectives, will also be one of the program's key targets.

The "SafeDocs" program is intended to facilitate safety checks in documents, images or messages, and provide a means for untrustworthy files to be converted into safer formats without loss of functionality.

There are three basic avenues for development. To paraphrase the DARPA project description:

1. extraction of de facto syntax (including any non-compliant syntax deliberately accepted and substantially used in the wild);
2. identifying a simpler subset of this syntax that yields itself to use in verified programming while preserving the format's essential functionality; and
3. 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.

DARPA's background information further states:

The parser construction kits developed by the program will be usable by industry programmers who understand the syntax of electronic data formats but lack the theoretical background in verified programming. These tools will enable developers to construct verifiable parsers for new electronic data formats, as well as extant ones.

As the PDF Association has already developed technologies at least partially aligned with these objectives in the form of veraPDF

The PDF Association will be represented at the project's "proposer's day" by Executive Director Duff Johnson, who will report back to members on his impressions.

More information on this project is available from the organizer's website for this purpose. The DARPA solicitation is also available.