HR001118S0054-Amendment-01.pdf

Broad Agency Announcement Safe Documents (SafeDocs)

HR001118S0054

August 23, 2018

Amendment 1

Amended on September 19, 2018

Defense Advanced Research Projects Agency Information Innovation Office 675 North Randolph Street Arlington, VA 22203-2114

HR001118S0054 SAFEDOCS 2

Table of Contents

PART I: OVERVIEW INFORMATION

PART II: FULL TEXT OF ANNOUNCEMENT

I. Funding Opportunity Description

A. Background

B. Insufficiency of Current Approaches

C. Program Description/Scope

C.1 TA1: Extant Syntax Recovery, Simplification, and Safe Sub-setting

C.2 TA2: Constructing secure parsers

C.3 TA3: Testing and Evaluation

C.4 TA4: Instantiation

D. Program Structure

E. Program Evaluation and Demonstration

F. Demonstrations, Exercises, and Hackathons

G. Deliverables to DARPA

H. Intellectual Property

II. Award Information

A. Awards

B. Fundamental Research

C. Disclosure of Information and Compliance with Safeguarding Covered Defense Information

Controls

III. Eligibility Information

A. Eligible Applicants

B. Organizational Conflicts of Interest

C. Cost Sharing/Matching

D. Other Eligibility Requirements

IV. Application and Submission Information

A. Address to Request Application Package

B. Content and Form of Application Submission

C. Submission Dates and Times

D. Funding Restrictions

E. Other Submission Requirements

V. Application Review Information

A. Evaluation Criteria

B. Review and Selection Process

HR001118S0054 SAFEDOCS 3

VI. Award Administration Information

A. Selection Notices

B. Administrative and National Policy Requirements

C. Reporting

VII. Agency Contacts

VIII. Other Information

A. Frequently Asked Questions (FAQs)

B. Collaborative Efforts/Teaming

C. Proposers Day

D. Submission Checklist

E. Associate Contractor Agreement (ACA)

HR001118S0054 SAFEDOCS 4

PART I: OVERVIEW INFORMATION

Federal Agency Name: Defense Advanced Research Projects Agency (DARPA), Information Innovation Office (I2O)

Funding Opportunity Title: Safe Documents (SafeDocs)

Announcement Type: Initial Announcement

Funding Opportunity Number: HR001118S0054

Catalog of Federal Domestic Assistance Numbers (CFDA): 12.910 Research and Technology Development

Dates o Posting Date: August 23, 2018 o Proposers Day: August 24, 2018 o Abstract Due Date: September 7, 2018, 12:00 noon (ET) o Proposal Due Date: October 19, 2018, 12:00 noon (ET) o BAA Closing Date: October 19, 2018, 12:00 noon (ET)

Anticipated Individual Awards: DARPA anticipates multiple awards for technical areas 1 and 2; and single awards for technical areas 3 and 4.

Types of Instruments that May be Awarded: Procurement contracts, cooperative agreements or Other Transactions (grants will not be awarded)

Agency Contacts o Technical POC: Dr. Sergey Bratus, Program Manager, DARPA/I2O o BAA Email: SafeDocs@darpa.mil o BAA Mailing Address:

DARPA/I2O

ATTN: HR001118S0054

675 North Randolph Street Arlington, VA 22203-2114 o I2O Solicitation Website: http://www.darpa.mil/work-with-us/opportunities http://www.darpa.mil/work-with-us/opportunities

HR001118S0054 SAFEDOCS 5

PART II: FULL TEXT OF ANNOUNCEMENT

I. Funding Opportunity Description

DARPA is soliciting innovative research proposals in the area of secure processing of untrusted electronic data. Proposed research should investigate innovative approaches that radically improve software's ability to recognize and safely reject invalid and maliciously crafted input data, while preserving essential functionality of legacy electronic data formats. Proposals should build on an existing base of knowledge of electronic document, message, and streaming formats and the nature of security vulnerabilities associated with these formats.

DARPA is interested in innovative approaches that enable revolutionary advances in science, devices, or systems. Specifically excluded is research that primarily results in evolutionary improvements to the existing state of practice.

This Broad Agency Announcement (BAA) is being issued, and any resultant selection will be made, using procedures under Federal Acquisition Regulation (FAR) 6.102(d)(2) and 35.016.

Any negotiations and/or awards will use procedures under FAR 15.4 (or 32 CFR § 200.203 for cooperative agreements). Proposals received as a result of this BAA shall be evaluated in accordance with evaluation criteria specified herein through a scientific review process.

DARPA BAAs are posted on the Federal Business Opportunities (FBO) website (https://www.fbo.gov/) and the Grants.gov website (http://www.grants.gov/).

The following information is for those wishing to respond to this BAA.

A. Background

Electronic documents are ubiquitous and essential to all aspects of modern life. Individuals and organizations must routinely engage with electronic documents received from a variety of unauthenticated or potentially compromised sources, comprising a growing variety of electronic data formats. Even if the immediate provider of the data can be authenticated, the data may derive from an untrusted source.

We expect pictures, charts, spreadsheets, maps, audio, video, as well as rich messages potentially including any and all of these, to be received with a click of a button. However, the complexity of managing such electronic data results in software vulnerable to attack. This situation is unsustainable.

Current software that processes electronic data such as documents, messages, and data streams is error-prone and vulnerable to exploitation by malicious inputs. According to MITRE's Common Vulnerability Enumeration data, over 80% of yearly reported vulnerabilities occur in code that handles input data. Such code converts a given bit stream representing the data into memory objects and validates that these objects have expected structure and relationships.

Exploitation of input-handling vulnerabilities leverages inaccurate programmer assumptions regarding the extent to which input data has been validated by input-handling code. Code that behaves correctly under certain assumptions (and may even be proven correct under these https://www.fbo.gov/ http://www.grants.gov/

HR001118S0054 SAFEDOCS 6

assumptions) will typically not behave correctly if any of these assumptions do not hold.

Attackers can induce incorrect behaviors by presenting vulnerable software with maliciously crafted input data that violates unchecked assumptions. The programmer assumes that validated input data contains certain objects in certain relationships, and writes code under these assumptions. However, should any of these assumptions not hold, the code will not behave correctly. A single missing or incorrect check can create a vulnerability, as was the case with the Heartbleed vulnerability (CVE-2014-0160), in which code acting on an unchecked assumption exposed sensitive memory content to remote attackers.

Parsing or checking code itself contains exploitable flaws and behaviors. Such flaws are particularly insidious, as they require little or no human interaction for the attack to succeed or lead to pre-authentication vulnerabilities.

B. Insufficiency of Current Approaches

Today, code for input data validation is typically written manually in an ad-hoc manner. For commonly-used electronic data formats, input validation is, at a minimum, a problem of scale whereby specifications of these formats comprise hundreds to thousands of pages. Input validation thus translates to thousands or more conditions to be checked against the input data before the data can be safely processed. Manually writing the code to parse and validate input, and then manually auditing whether that code implements all the necessary checks completely and correctly, does not scale.

Moreover, manual parser coding and auditing typically fail even for electronic data formats specifically designed to be easier to perform such tasks, e.g., JSON and XML. A variety of critical vulnerabilities have been found in major parser implementations for these formats.

Widely deployed mitigations against crafted input attacks include (a) trying to prevent the flow of untrusted data to vulnerable software; and (b) testing of software with randomized inputs to find and patch flaws that could be triggered by maliciously created inputs.

Unfortunately, neither of these approaches offers security assurance guarantees.

Mitigations for preventing the flow of untrusted data to vulnerable software, which can be implemented via network or host-based measures such as firewalls, application proxies, anti-virus scanners, etc., neither remove the underlying vulnerability from the target, nor encode complete knowledge of document or message format internals. Attacker bypasses of such mitigations exploit incompleteness of the mitigations' understanding of the data format to exploit the still-vulnerable targets.

The effectiveness of fuzzing methods for testing of software with randomized inputs to find and fix flaws depends on whether randomly generated inputs can emulate maliciously crafted inputs closely enough to trigger all relevant code flaws. Although modern fuzzing methods incorporate feedback from tracing the execution of the code as it consumes crafted inputs, they also employ symbolic and concolic execution of code in their exploration of the space of potential crafted inputs. As a result, these methods are still essentially heuristic. There is no guarantee that attackers, who also use fuzzing to locate and develop vulnerabilities, will not cover a more substantial and more productive portion of the input space with a different set of heuristics.

HR001118S0054 SAFEDOCS 7

In contrast, approaches based on automatic generation and analysis of code (and, potentially, formal verification of such code to be functionally correct) offer security assurances. Such approaches produce code that is significantly less error-prone and vulnerable. Some of this code can even be automatically verified and proven to be correct, as was demonstrated, e.g., by the DARPA High-Assurance Cyber Military Systems (HACMS) program.

However, these approaches are typically not applied to code that parses and validates the dominant electronic data formats. Automatic code generation tools and code verification tools cannot function without a precise specification, which also must be of reasonable complexity to enable verification. Regrettably, the application of formal methods is impeded by the ambiguity and complexity of the formats.

Ambiguity: Even though electronic data formats such as Portable Document Format (PDF) have published specifications approved by standards bodies such as the International Organization for Standardization, dominant implementations of these formats extend the standards by deliberately accepting non-compliant inputs without any indication to the users that the document contains malformations silently presumed benign. Actual populations of electronic documents (referred to as extant in this BAA) contain many such malformations, which are not documented, but for all practical purposes have been allowed to become a part of the de facto format syntax. Being undocumented, these silent “fixing” behaviors have led to phenomena such as strikingly different interpretations of the same document or message by different implementations.

Complexity: Existing standards, even when fully complied with, do not seek to limit the syntactic complexity of the data. As a result, they allow constructs that, although never used in benign documents, make formal reasoning about code that would validate such constructs very hard or even undecidable.

C. Program Description/Scope

The Safe Documents (SafeDocs) program 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 will address the ambiguity and complexity obstacles to the application of verified programming posed by extant electronic data formats. SafeDocs’ multi-pronged approach will combine:

a) extraction of the extant formats’ de facto syntax (including any non-compliant syntax deliberately accepted and substantially used in the wild);

b) identifying a syntactically simpler subset of this syntax that yields itself to use in verified programming while preserving the format's essential functionality; and

c) 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 developed by SafeDocs 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

HR001118S0054 SAFEDOCS 8

electronic data formats as well as extant ones. The tools will guide the syntactic design of new formats, by making verification-friendly format syntax easy to express, and vice versa.

SafeDocs will distinguish between electronic data formats for documents understood as static, self-contained content, and formats for streaming electronic data from external devices such as Internet of Things (IoT) endpoints or sensors. This distinction reflects two modes of parsing and validation for security purposes (discussed in more detail below in TA2). Documents can be examined as a whole, in an early phase of their processing, validated, judged as “safe” at that particular point in time, and remain “safe” from that point onwards. By contrast, streaming data requires continual low-latency validation of incoming data.

Electronic document formats are understood to contain formatted text, images, and allow a limited amount of user interaction, but do not include general-purpose executable functionality or continual external updates (compare common uses of PDF for electronic office workflows and archiving). Data streaming formats are understood to provide machine-to-machine real-time data exchanges such as, e.g., streams encapsulated by the Data Distribution Service (DDS), up to and including video and sound streams.

SafeDocs will focus on flaw-free processing of input syntax. Cryptography-based approaches are not in scope for the SafeDocs program. Parsing failures and syntactic ambiguities of cryptographic formats are a known source of weakness in implementations of cryptographic systems, exploited to bypass their theoretical guarantees. SafeDocs aims to protect cryptographic constructs along with other kinds of data objects.

The SafeDocs program consists of four Technical Areas (TAs):

TA1: Extant Syntax Recovery, Simplification, and Safe Sub-setting.

TA2: Constructing Secure Parsers TA3: Testing and Evaluation TA4: Instantiation

C.1 TA1: Extant Syntax Recovery, Simplification, and Safe Sub-setting

TA1 will develop methodology, formalism, and tools to capture and describe de facto syntax of electronic data formats in human-intelligible, machine-readable form, combining as sources of information the published specifications of the format, a large corpus of extant instances of the format (such as electronic documents or messages in the wild), and the binaries (or source code, where available) of existing dominant software implementations. This methodology will recover the ground truth of an extant electronic format, creating a basis on which the use and abuse of the format's features in the wild may be evaluated. In doing so, TA1 will produce the first effective metrics and comprehensive analysis of the format’s ambiguity in actual use.

TA1 will identify syntactic complexity obstacles that extant formats present to automated verification methods. TA1 will also develop methodologies and tools for the selection of a simpler ‘safe’ syntactic subset of a format that, while preserving the format's essential functionality, is free of these obstacles. TA1’s human-intelligible, machine-readable description of the format will be used by TA2 to build high-assurance and verifiable parsers for the format.

HR001118S0054 SAFEDOCS 9

These goals will require breakthroughs in the theory and practice of automated comprehension of electronic data formats.

Outcomes of TA1

TA1 will produce an automated methodology for comprehending an extant data format, as described below, resulting in a machine-and-human-readable formal description of a simplified unambiguous subset (“safe subset”) of the de facto format syntax that is suitable for defining and verifying:

a. a secure functionally correct parser for the data language, and

b. a high-assurance translator from the de facto syntax (including malformations presumed benign, allowed syntactic ambiguities, syntactic exuberances, and syntactic redundancies) to the simplified unambiguous subset of the format.

The automated methodology for comprehension of an extant electronic data format will draw upon its published standards, its dominant implementations, and a large (at least 106 – 109 samples) corpus of its extant instances such as documents or messages (for evaluation purposes, TA3 will provide reference corpora for selected formats). This methodology will allow format subject matter experts to quickly review the “ground truth” of the de facto format syntax, and to make determinations of which features or malformations presumed benign can be allowed in the simplified format or can be converted to this format canonically and composably to yield the functionally correct translator as described above.

Strong proposals for TA1 will show capability to collect the data needed to recover the ground truth of extant electronic data formats and to identify security-relevant format phenomena (see the following section titled “Empirical Exploration of Extant Format Phenomena”), but should also plan to work with TA3 to refine their understanding of the extant formats’ challenges.

TA1 Theory Challenges

Specifications of extant electronic data formats, with few exceptions, can be characterized as:

ambiguous or imprecise (being written in natural language);

not machine readable (similar but not quite the same as above);

de facto redefined or extended by permissive implementations; and divergent (due to multiple, non-specified kinds of permissive handling of non-compliant data by implementations).

Syntactically, extant electronic data formats are sets of dialects that purport to have the same syntax and semantics, and agree on it in their large core part, but also diverge syntactically and semantically in ways that impact security.

Current theory lacks convenient abstractions for describing syntactic phenomena associated with extant electronic data formats. For example, existing formal language theory abstractions:

do not describe the phenomena of divergent dialects of a language;

do not offer the simplest notional description of the assumed syntactic properties of data;

do not account for permissiveness and ambiguity effects; and

HR001118S0054 SAFEDOCS 10

do not provide a way to compositionally reason about transformations between syntactic expressions meant to be equivalent.

Formal devices currently used to capture data format syntax, e.g., Backus-Naur Form (BNF), Extended Backus-Naur Form (EBNF), etc., in such standards specifications that use them, share the above drawbacks.

Strong proposals will outline the current state of the art in regard to the challenges of describing extant electronic data formats, identify weaknesses of current approaches, and plan to address them with a comprehensive formal approach that enables reasoning about the format and its implementations.

The approach must enable creation of high-assurance parsers for the formats that exhibit phenomena such as diverging concepts of allowable syntactic malformation, divergent interpretations of syntactic validity and equivalence of syntactic constructs, as well as the existence of a core language on which multiple implementations agree.

The formalism will describe ways in which occurrences of equivalent syntactic expressions can be converted to a preferred simplest form, and provide means of reasoning about composing such local syntactic transforms. The formalism should not assume global syntactic consistency, i.e., that all such transforms are compatible or composable.

TA1 proposals that explore several competing or complementary formal approaches should describe each approach as a separate statement-of-work task and provide sufficient costing details for such tasks to be separable.

Empirical Exploration of Extant Format Phenomena

Strong TA1 proposals will recognize the need to explore empirical properties of extant data formats, such as syntactic features that often result in unintended execution (a.k.a. exploitation), the existence of “polyglot” files (files that simultaneously conform to several unrelated published standards or de facto format syntax at the same time) and the so-called “schizophrenic” files.

Schizophrenic files fit several divergent de facto dialects of the same data format, and whose syntactic structure is interpreted differently in these dialects, and, as a result, are understood differently by different interpreters of the format. Strong proposals will maintain this awareness through all layers of syntax down to the bit-level data representation.

Strong proposals will offer systematic ways of exploring, describing, and excluding these phenomena where they can lead to vulnerabilities and unintended execution.

Strong proposals should recognize that format-related domain expertise is a sparse, expensive resource, and that exploring security phenomena of a complex format may require multiple experts with non-overlapping areas of expertise. TA1 proposers should discuss how they will gain sufficient access to enough of these individuals to ensure robust, accurate results. Proposals should design processes and interfaces to use the domain experts' time in the most efficient manner, by creating capabilities to automatically digest large corpora of format samples and to promptly validate or disprove hypotheses about the use (or abuse) of particular format features in the wild (as well as take TA4-developed requirements into account).

HR001118S0054 SAFEDOCS 11

Note on Format Nesting

SafeDocs considers all data parsed within a process to be within the scope of the above definitions. For example, when an electronic data format allows inclusions of another format, to be parsed with a plugin or a library, the included format must receive the same treatment of de facto allowed syntactic analysis and simplification to allow parser verification, or be excluded from the simplified format if such exclusion does not affect the format's essential functionality.

C.2 TA2: Constructing secure parsers

Existing approaches to validation of electronic data inputs appear to be lacking a constructive theory of security. Theoretically compelling approaches, such as defining an electronic data format via a formal grammar, fail to address popular extant formats (due to their complexity and ambiguity), whereas approaches used in practice lack theoretical cogency (and, often, actual efficacy). As a result, security risks of interacting with untrusted complex inputs lack a theoretical basis on which they could be evaluated, while empirically these risks appear to approach those of running untrusted code.

SafeDocs requires a breakthrough constructive theory that connects input validation and security.

The scope of TA2 proceeds from the following assumptions:

1. Secure handling of untrusted inputs means predictable execution driven by consumption of these inputs.

2. Input validation means automatic, static reasoning about the execution an input will produce.

3. For many models of computation driven by inputs–e.g., when the inputs are general-purpose programs or equivalents thereof, to be executed by the receiving entity–static reasoning about non-trivial properties of execution is undecidable, thus making the security of these models of input consumption in the sense of (1) and (2) undecidable.

Such models are outside of the SafeDocs scope if their properties that lead to undecidability are intentional. For example, intentional interpretation (or compilation and execution) of inputs that are general-purpose programs or deliberate equivalents thereof is outside of SafeDocs’s scope.

4. Deserialization, parsing, and validation of structured electronic data should not be one of the models in (3).

When a computation model associated with consuming an electronic data format exhibits undecidable characteristics unintentionally, SafeDocs views this property as an obstacle to constructing verified parsers, and seeks to remove it via safe sub-setting of the format, as discussed above. Note that well-known vulnerabilities resulted from the common anti-pattern of passing string inputs to full-featured execution environments such as command shells or general-purpose programming language interpreters, typically under the assumption that the passed strings were filtered or “sanitized” to allow only the intended command(s) and none others.

SafeDocs regards general-purpose code injection and execution resulting from this anti-pattern as unintentional and calls for identifying and eliminating all of its instances in the electronic data formats under scrutiny. This phenomenon is one of many that underscore the importance of

HR001118S0054 SAFEDOCS 12

empirical format exploration involving domain experts. Strong proposals should address this phenomenon.

Consistent with the TA1 note on format nesting, SafeDocs regards all electronic data formats that can be contained in a format and are parsed within the same process to be within scope as defined by assumptions 1-4 above.

SafeDocs thus requires the co-design of electronic data formats and the code that parses and validates these data formats to allow static reasoning about the effects of consuming inputs. For extant formats, it calls for principled safe sub-setting of the format’s syntax to allow such reasoning.

Outcomes of TA2

This technical area of SafeDocs will produce:

a) constructive theories of security for parsers;

b) secure parser construction kits usable by industry programmers who understand the format but lack the theoretical background in verified programming;

c) verified parsers for selected extant electronic data formats, given their simplified verification-enabling subset definitions developed in TA1, and produced with the use of the secure parser construction kits (b); and

d) for electronic data formats subject to de facto syntax extensions, high-assurance translators from the de facto syntax to the simplified syntax, based on the transformations developed in TA1.

More specifically, SafeDocs poses the following theory, design, and instantiation challenges.

Theory Challenge: A Theory of Input Validity

Strong TA2 proposals will present a formalism to capture the idea of input validity understood as a decidable property of the input (and of the input-checking code) that can be checked efficiently, by code that can be proved correct, and, having been checked, provides security guarantees to the rest of the program's code modules. These security guarantees should amount to preclusion of unintended computation due to consumption of inputs both while their validity is being checked and after it has been checked (and the input has not been rejected as invalid).

For example, should the modules of a program downstream of the input checker be verified in turn, the input checker will provide preconditions for their verification, sufficient to show that no unintended computation will occur due to consumption of successfully validated inputs.

The theory of input validity will offer insights on the complexity of input validation and of verifying implementations of input validation. It will warn of flawed designs where the validity of inputs offers no security value in the sense of precluding unintended computation, or implies that effective validation of inputs means solving undecidable problems.

TA2 proposals that explore several competing or complementary formal approaches should describe each approach as a separate statement-of-work task and provide sufficient costing details for such tasks to be separable.

HR001118S0054 SAFEDOCS 13

Bringing Secure Parsing Development Kits to Industry Developers

SafeDocs will develop approaches and tools for creating high-assurance parsers. These tools will be accessible to industry developers, and will make secure, succinct, and efficient parsing code faster to write, to test, and to run. These tools will build on the recent advances in parser programming, leveraging programming language constructs familiar to developers, and making use of intelligible, constructive, and prompt feedback from the development tool chain components (such as an Integrated Development Environment (IDE)) to guide the developers.

Parser code should make it immediately clear which syntactic element of input is being consumed by any particular line of the code, and which properties of input have been checked, are being checked, and are yet to be checked at every line. Answering these questions, e.g., during a code review or a security audit, should not require a static analysis tool – the answers should be obvious from the code itself, to a human or a machine.

A strong TA2 proposal should outline the current state of the art in regard to at least the following challenges, identify weaknesses of current approaches, and plan to address them.

Usability: Developer's learning curve for the new programming idioms should be minimized, maximizing their productivity. Using the proposed style of parser programming should make parsers faster to write and easier to read than “rolling one’s own parsers.”1

Intelligibility: If using a DSL to automatically generate parser code, the proposers are encouraged to keep the generated code readable and idiomatic, so that reading the syntactic specification of valid or expected data off of the generated code remains a simple non-heuristic task for both humans and machines.

Performance: Compiled code should not run significantly slower or require significantly more memory than legacy parser code.

Semantic Actions Safety: Although the user should be allowed to supply semantic action code to compose with the parser, this composition should not be allowed to compromise the parser security guarantees (as established by the input validity theory). The acceptable semantic action code can be limited, but the limitations must be made easy for the user to grasp.

Feedback: While expressive enough to capture most useful syntactic features, the declarative style should discourage security pitfalls in programming and design by giving feedback to the programmer in the form of readable warnings, instant hints from the IDE, or a combination thereof. Problematic code should be reported to the user as early as possible. The lack of a simple way to express a syntactic property should clearly signal to the user that this syntactic property is problematic.

Stability: The developers' workflow should not be brittle with respect to versions of verification tools involved “under the hood.”

1 Thus pointer-stepping parsing code such as *hbtype = *p++; is severely discouraged, and no one who implements a parser should have to write it ever again.

HR001118S0054 SAFEDOCS 14

A strong TA2 proposal should consider means of steering industry developers towards the style of programming that is both intuitive given the understanding of the data format and provides maximum benefit for verification of the resulting code. Industry developers should receive intelligible, actionable feedback on the preferred idioms to accomplish the task.

Theory Outcomes of TA2 for Analysis of Electronic Data Formats

A common problem in practical security is to distinguish legacy technologies that present insurmountable security risks and must be discontinued from those for which applying mitigations may be sufficient. Recent decisions by major vendors to disable support for legacy web technologies such as Java applets or Flash suggest that the security risk-benefit analysis may no longer be always in favor of backward compatibility. However, to date, such risk-benefit analysis lacks a theoretic foundation. TA2 will help establish such foundations for data formats.

In particular, a successful input validity theory will connect validity with predictability of execution driven by inputs. The theory will distinguish between the concepts and designs of input where such predictability of computation is driven by the inputs. For example:

Predictability cannot be achieved because the input is meant to describe general purpose computation (i.e., the input is deliberately used as a programming language for a Turing-complete computing environment, and thus automatic validation of the execution's non-trivial properties including termination is undecidable).

Predictability cannot be achieved with the input language as described because it is accidentally Turing-complete on the accepting environment, but can, in fact, be achieved for a subset of the language and with changes to the environment.

Predictability can be achieved, but further sub-setting of the language or the environment as above will make the checker or the verification of the checker much more efficient.

Predictability can be achieved without changes and is, in fact, optimal among competing input formats.

Strong TA2 proposals should address metrics for complexity of new formats (a “complexity tax”) and extant formats (a “security debt”) that facilitate risk-benefit analysis of their security.

C.3 TA3: Testing and Evaluation

TA3 will evaluate assurance provided by parsers and translators developed in TA2 against best-of-breed exploitation methods, and will develop general methodologies for systematic testing of parser implementations. TA3 will test essential content and functional equivalence of documents transformed by high-assurance translators to a syntactically simpler safe subset of the format (as produced by the methodology developed in TA1).

TA3 proposals will outline the state of the art in parser testing, identify weaknesses of current approaches, and plan to address them, also planning to utilize the insights developed in TA1 and

TA2.

TA3 will work with TA4 to select the appropriate electronic data formats for evaluating the progress of TA1 and TA2 performers, to ensure that the theories and technologies developed are relevant to the safe information exchange requirements established by TA4. The formats selected should represent both electronic document and data streaming use cases.

HR001118S0054 SAFEDOCS 15

Strong TA3 proposals should outline methods for collecting and synthesizing extant data content sufficient to exercise both the static and streaming use cases for TA1 and TA2. This includes creating large (106 – 109 samples) reference corpora for selected static and streaming electronic data formats and frameworks for testing against these corpora. The reference corpora will scale with time to match the progression of program evaluation metrics (see Table 2). Reference corpora will be provided to TA1 and TA2 performer for white-box testing of their systems for correctness and coverage. An initial reference corpus of no less than 105 instances will be provided early within Phase 1 of the program.

In addition, TA3 will produce static and streaming testing corpora, not shared with the TA1 and TA2 performers, to test their systems for robustness with synthetic data instances during evaluation exercises.

As a key part of its mission, TA3 will orchestrate empirical exploration of the extant data formats, by engaging format exploitation and reverse engineering experts, and working with TA1 performers to ensure the discovered phenomena are accounted for in their analysis of the format.

Strong TA3 proposals should demonstrate knowledge of the empirical data exploration domain and activities, and the ability to quickly and efficiently engage format experts, including non-traditional performers.

TA3, in collaboration with TA4, will produce a workbench of representative platforms on which the performance of tools developed in TA1 and TA2 will be evaluated, and will make this workbench available to the TA1 and TA2 performers within the first six months of Phase 1.

TA3 will design and implement scenarios and software for the evaluation exercises.

A successful TA3 proposal should include, at a minimum, the following:

develop automated ways to compare security assurance of parsers and translators created in TA2 against leading commercial products and open source solutions in format security;

develop corpora, use cases, hackathon scenarios, and testing frameworks for selected extant electronic data formats, to test TA1 and TA2 solutions;

develop automatic means of testing content equivalence between extant electronic data instances and their syntactically simplified versions as produced by TA2 translators; and develop automated ways of testing for parser differentials, i.e., differences in syntactic interpretations of the same message between different implementations of the same format, which generalize to classes of messages differently interpreted and manipulable by attackers.

TA3 will lead the demonstrations, the hackathons, and the exercises as described in the Program Evaluation section. The TA3 performer will submit plans for these events to the Government team at least two months prior to each event. TA3 proposers should discuss how they will facilitate these events, including the acquisition and provisioning of appropriate event facilities and resources.

Additionally, TA3 will design and implement yearly contests open to the public at information security conferences such as DEFCON, in which the developed technologies from TA1 and TA2

HR001118S0054 SAFEDOCS 16

as well as a variety of current commercial products and open source solutions will be exposed to contestants, to gauge the progress of the SafeDocs technologies.

C.4 TA4: Instantiation

TA4 will collect business requirements for enterprise/ Internet of Things (IoT) electronic data formats, the industry development process for the code handling these formats, and for the acceptance testing of such code. TA4 will collaborate with TA1 and TA2 performers to ensure that the theories and the resulting systems developed can meet the requirements, and that the requirements are relevant to the safe information exchange needs of the public, the enterprise, and the U.S. Government agencies including the Department of Defense (DoD).

TA4 will identify industry partners interested in the eventual adoption of SafeDocs technologies, and facilitate their interaction with TA1 and TA2 performers to inform their theories. TA4 will ensure that TA1 and TA2 performers’ risk-benefit analysis of electronic data format features is informed by the industry requirements, e.g., inform TA1 and TA2 of the value of risky features to industry.

TA4 will identify electronic data formats in the areas of documents, messages, and data streams that are of high security concern, and will analyze these formats using tools developed in TA1.

Using tools developed in TA2, TA4 will implement prototypes of secure enclave gateways that translate these formats to their respective safe subsets, in a variety of use cases. TA4 will work with industry partners to ensure that the use cases are realistic, and the safe subsets and the gateways match the identified requirements.

TA4 performers will be expected to perform the custom programming tasks needed to adapt the tools developed in TA1 and TA2 to particular use cases of the secure enclave prototypes. TA4's feedback on usability of the tools will be the means of evaluating progress of TA1 and TA2 performers on these TA’s respective usability requirements.

Using theory insights and formalisms developed in TA1 and TA2 and the experience of the use cases, TA4 will develop methodologies for code and data review suitable for use in enterprise/IoT software acceptance testing. Feedback from this effort will inform the theories developed in TA1 and TA2. TA4 performers will collaborate with TA1 and TA2 performers to produce metrics for evaluating the risks associated with legacy electronic data formats data and legacy code for handling these data formats.

In particular, TA4 will develop practical metrics for a “data complexity tax” applicable to new protocols and systems, and for the “data technical debt” applicable to legacy systems, to reflect the risks of electronic data format complexity on security of systems, and prioritize mitigations for risky legacy systems.

A strong proposal should include, at a minimum, the following:

A plan for working with industry vendors to collect their security requirements for electronic data formats and parsers deployed in development and operational environments, and for the development toolchains used to develop data specifications and input-handling code.

HR001118S0054 SAFEDOCS 17

A plan to identify, design, and implement use cases of secure enclaves for the selected formats that are of interest to industry partners and match the identified requirements.

A plan to experimentally evaluate the impact of SafeDocs tools for safe sub-setting electronic data formats and their parsers within enterprise/IoT environments.

A plan to facilitate adoption of SafeDocs methodologies within these environments.

In the option Phase 3, TA4 will work with industry to standardize the simplified safe formats and will transition the components to identified government partners.

D. Program Structure

The program is anticipated to run 48 months and has been organized into three (3) phases. Phase 1 (base) will be 18 months and will explore selected electronic data formats. Phase 2 (base) will be 18 months and will scale prototype implementations that instantiate the theories. The program will conclude with a 12-month Phase 3 (transition phase option), which will be contingent on the success of the previous phases.

In Phase 1, performers will target the core structure and functionality of selected document and streaming formats, without restrictions on the platform's resources. In Phase 2, performers will target commonly associated data formats and extensions of the selected document, and address challenges of scale and performance, such as processing the selected streaming format on a resource-constrained embedded platform. In option Phase 3, performers will transition their methodologies and tools to industry and government partners.

In Phase 1, there will be two integration/demonstration events and a final evaluation exercise at the end of the phase. Exercises will feature test corpora not provided to performers a priori.

Phase 2 and the option Phase 3 will have two demonstration events each to identify and correct any weaknesses, and provide ample time to address any shortcomings before mid-phase and final evaluation exercises. (See Figure 1.)

Figure 1 - Tentative evaluation schedule

Each abstract and proposal submitted against this solicitation shall address only one TA.

Organizations may submit multiple abstract/proposals to any one TA, and they may propose to multiple TAs. For example, a proposer submitting a proposal to TA1 and another to TA2 may be selected to perform on both TAs. This rule applies to TA1, TA2, and TA4. However, TA3 performers cannot perform on any other TA as either a prime or sub. A proposer submitting a proposal to TA1 and another to TA2 may be selected to perform on both TAs. However, TA3 and TA4 performers cannot perform on any other TA.

HR001118S0054 SAFEDOCS 18

There are multiple points of expected and potential collaboration among TAs, and the Government expects that all performers producing software will interact closely with the TA3 (evaluation) and TA4 (instantiation) performers. Additionally, TA1 and TA2 performers are expected to collaborate closely, as described below. Proposers should read the descriptions of all TAs and the Program Evaluation and Demonstration section to ensure a full understanding of the program context, structure, and anticipated relationships required among performers. To facilitate the open exchange of information, all program performers will have an Associate Contractor Agreement (ACA) language included in their award.

TA4 will lead the development of the ACA for the program. See Section VIII.E for more information regarding the ACA.

There will be no forced downselects in phases 1 and 2, but continued funding will depend on demonstrated progress in achieving program goals.

Efforts in the four technical areas of this program run concurrently, with ramp-up and ramp-down for specific tasks, as described below. Relationships between the technical areas change from phase to phase, as described below.

Phase 1: Explore

In phase 1, TA1 performers will focus on creating the tool chain and methodology for comprehending an extant electronic data format (the “challenge format”). In the meantime, TA2 performers develop the theory and build up tools for their verified parser construction kits using a series of simpler format descriptions, already formulated in machine-readable form, which approximate the initial output of TA1 efforts in this phase.

The TA1 toolchain will include tools for:

a) representing the format specification in a machine-readable form;

b) recovering the de facto language(s) allowed by implementations, from source code or binary (this includes effective automation for exploring differences between (a) and the implementation); and

c) enumerating format features and their uses in a large corpus of documents and effective automation for checking whether any properties encoded in (a) and (b) hold for the documents in the corpus, and effectively summarizing where and how they are violated if not.

It is anticipated that these tools will be developed in parallel with comprehending the challenge format, co-evolving with the comprehension effort, and, by the end of Phase 1, will produce comprehensible, machine-readable description of the format syntax used to express the core format functionality, and this syntax will be suitable for verified programming use in TA2.

Throughout Phase 1, and especially in its second sub-phase, TA1 performers are expected to collaborate with TA2 performers to assure suitability of their output to TA2.

The syntax and semantics of the TA1-produced human-and-machine-readable specification are expected to largely settle by the end of Phase 1, although its further evolution is expected

HR001118S0054 SAFEDOCS 19

through Phase 2; it is expected to reach beta state in the middle of Phase 2. At the start of Phase 3, it is expected to reach the release candidate state (and meet with approval by TA4 performers).

Meanwhile, TA2 performers are expected to start developing infrastructure for building verified parser construction kits, to take advantage of the data format specifications being developed in

TA1.

The goal for TA2 performers in Phase 1 is to build up the capability to construct provably correct parsers for simple data formats described by an unambiguous and human-intelligible specification that is also machine-readable. TA2 performers will build on this capability in Phase 2, to construct and verify more complex parsers for more complex formats, as machine-readable specifications for these are created in TA1.

Usability of the parser construction kits will be a focal point for TA2. TA4 and TA3 performers will provide continuous feedback to TA2 performers. Performance optimization (so long as the overhead of the kit-based parsers is within the allowed percentage of the metrics for Phase 1) will become a focal point in Phase 2.

TA3 performers will evaluate parsers produced in TA2 and specifications produced in TA1 for the metrics of Phase 1.

TA4 performers will collect requirements defining enterprise/IoT use of electronic document, message, and streaming formats, ensuring that the instantiation of data validity and verified code theories developed in TA1 and TA2 address these requirements.

Phase 2: Scale

In Phase 2, the TA2 focus shifts to developing verified parsers using the de facto format specification being recovered in TA1. TA1 continues to refine its toolchain, and, in this phase, applies it to a variety of formats to complete the recovery of the ground truth in the challenge suite of extant, populated electronic data format, to scale its performance to larger corpora of extant documents, and to improve its accuracy, as per Phase 2 metrics.

In this phase, the fitness of specifications produced in TA1 for the verified parser programming approaches being developed in TA2 is put to the test. Although TA2 performers are expected to provide feedback on the format of the TA1 outcomes throughout Phase 1, it in Phase 2 that TA2 performers receive a synthesized “ground truth” description of a complex format and must accommodate it with their verified parser construction kits (or push back with rigorous arguments of why such accommodation is not possible, so that TA1 tools could be modified to allow it).

Usability of TA2’s verified parser construction kits remains a concern in Phase 2, but performance of the produced code becomes a focus. TA2 performers are expected to release their secure parser construction tool kits to the TA4 performer “early and often,” to seek TA4’s feedback.

TA3 will continue developing and testing the means of evaluation of security and performance of the parsers.

HR001118S0054 SAFEDOCS 20

TA4 will ramp up work to instantiate the prototype of a secure enclave entry gateway, combining machine-readable format descriptions produced in TA1 with tools being developed in TA2.

Phases 1 and 2 are expected to explore competing approaches to their technical areas, since the current state of theory does not allow pre-selecting them. In fact, one of the desired outcomes of TA1 and TA2 should be the creation of such theories.