HR001120S0058-Amendment-01.pdf

Broad Agency Announcement Verified Security and Performance Enhancement of Large Legacy Software (V-SPELLS) Information Innovation Office

HR001120S0058

July 24, 2020

Amendment #1 Amended on August 3, 2020

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

HR001120S0058 V-SPELLS 2

Table of Contents Part I: Overview Information……………………………………………………………………...………3

Part II: Full Text of Announcement………………………………………………………………………..5

I. Funding Opportunity Description

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

IV. Application and Submission Information

A. Address to Request Application Package

B. Content and Form of Application Submission

C. Submission Date and Time

D. Funding Restrictions

E. Other Submission Requirements

V. Application Review Information

A. Evaluation Criteria

B. Review and Selection Process

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. Proposers Day

C. Submission Checklist

D. Associate Contractor Agreement (ACA)

HR001120S0058 V-SPELLS 3

PART I: OVERVIEW INFORMATION

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

Funding Opportunity Title: Verified Security and Performance Enhancement of Large Legacy Software (V-SPELLS)

Announcement Type: Initial Announcement

Funding Opportunity Number: HR001120S0058

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

Dates o Posting Date: July 24, 2020 o Proposal Due Date: September 9, 2020, 12:00 noon (ET) o Proposers Day: July 29, 2020

Anticipated Individual Awards: There are multiple technical areas for this solicitation.

Currently, DARPA anticipates multiple awards in Technical Area 1, Technical Area 2 and Technical Area 3; and a single award for Technical Area 4. DARPA anticipates making multiple awards under this BAA, which has a total anticipated funding amount of approximately $40 million.

Types of Instruments that May be Awarded: Procurement contracts or 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: V-SPELLS@darpa.mil o BAA Mailing Address:

DARPA/I2O

ATTN: HR001120S0058

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

HR001120S0058 V-SPELLS 4

PART II: FULL TEXT OF ANNOUNCEMENT

I. Funding Opportunity Description

DARPA is soliciting innovative research proposals in the area of software verification and assurance by enabling piecewise, compatible-by-construction enhancement of software components in legacy United States Department of Defense (DoD) systems, and creating methods and tools to recover succinct models of domain data abstractions and logic from the source code, adding enhancements at the level of these models, and converting them to performant new component implementations, which are verified to be compatible and secure.

Proposed research should investigate 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 grants and 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 posts BAAs on the System for Award Management, Contract Opportunities (Beta.Sam.Gov) website (https://beta.sam.gov/) and, when applicable, the Grants.gov website (https://www.grants.gov/).

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

Introduction

The DoD has a critical need for enhancing and replacing components of existing software with more secure and more performant code. This includes cases where a key performance or security benefit comes from moving parts of the software to new hardware, such as utilizing hardware accelerators, isolation enclaves, offload processors, and distributed computation.

However, introducing enhancements or replacements into large legacy code bases carries a high risk that new code will not safely compose with the rest of the system. Verified programming methodologies for creating software that is correct-by-construction are currently not effective for lowering this risk, because they focus on clean-slate software construction, assume an existing formal specification that is typically not available for a legacy system, and require formal methods expertise typically not accessible to developers.

The goal of the V-SPELLS program is to create a developer-accessible capability for piece-by-piece enhancement of software components with new verified code that is both correct-by-construction and compatible-by-construction, i.e., safely composable with the rest of the system.

V-SPELLS will create practical tools for developers to gain benefits of formal software verification in incremental software (re)engineering rather than only in clean-slate introduction.

V-SPELLS tools will enable developers to deliver assured incremental modernization of legacy systems in a manner that leverages verification technologies and reduces rather than raises risk.

V-SPELLS aims to radically broaden adoption of software verification by enabling incremental https://beta.sam.gov/ https://www.grants.gov/

HR001120S0058 V-SPELLS 5

introduction of superior technologies into systems that cannot be re-designed from scratch and replaced as a whole.

To accomplish these goals, the V-SPELLS program will leverage a combination of novel concepts in program understanding and verification, as well as recent developments in domain specific languages and composable system architectures for production systems at scale. The program seeks breakthroughs in and novel approaches to the following technical challenges, Including, but not limited to:

Automated program understanding to infer architectural structure, assumptions, and dependencies in a legacy source code base, enabling its decomposition into components with explicit modular structure, interfaces, dependencies, and constraints. Recovery of domain abstractions and models from legacy code bases, in succinct and expressive representations suitable for programming functional component enhancements or replacements that are safely composable with the existing systems.

Matching known and extracted domain abstractions and models with legacy code, lifting of legacy code to succinct, enhanceable, safely composable, and inter-operating representations, and automated specification inference leveraging such representation.

Provably safe composition of enhancements with the rest of the system.

Overcoming performance reduction due to added layers of abstraction with novel verified cross-layer optimization and distribution techniques (“verified stack flattening and distribution”). Development of non-brittle and granular rules for composable representation, packaging, and transformation of software verification proofs that support distribution and orchestration of verified programs.

Background Sustainers of today’s critical infrastructure and DoD code bases struggle to gain effective understanding of legacy code. Legacy code tends to entangle high-level application domain logic with low-level implementation detail and accumulated performance optimizations for past hardware that remain in the code despite being no longer useful. Code may also be difficult to comprehend due to “shortcut” paths unintended by software architects but expediently introduced by developers, and other developer deviations from the intended design and architecture. Often, component specifications aren't available and must be inferred from implementation, or the existing interface control documents do not account for differences between software and hardware versions. As a result, critical systems are locked into obsolete hardware and software components. Capability upgrades become increasingly difficult over time, with no capability for high assurance functional enhancement of legacy components.

Today’s focus on clean-slate methodologies limits applicability of verified programming to legacy systems. Today, verified software is written from scratch, starting with a formal specification. In recent scale-oriented approaches pioneered by DARPA’s High-Assurance Cyber Military Systems (HACMS) program and adopted by National Science Foundation DeepSpec, the specification is written in a proof assistant such as Coq or Isabelle in its respective functional language (e.g., Gallina for Coq), by a hybrid team of logic-focused formal methods experts and domain-focused requirements engineers. Domain expert programmers (e.g., network programmers, control system programmers, signal processing programmers, embedded systems programmers, avionics programmers, etc.) who implement this specification are typically not familiar with verified programming environments and conventions. They are provided with a Domain-Specific Language (DSL) or similar domain-focused model that imitates a programming

HR001120S0058 V-SPELLS 6

style familiar to them, e.g., a bespoke imperative DSL, but is designed by the domain logicians to be translated into the specification language. Domain specific models or codes are then proven to be equivalent to the specification, i.e., functionally correct. The structure of functional correctness proofs follows the structure of the system’s stack of abstractions, down to a formal description of the hardware if available (such as RISC-V).

Today, there are no technologies to effectively understand legacy code bases to reap the benefits of verification approaches for their incremental, assured enhancement, or to apply verification for safe composition of enhancements with large legacy systems. V-SPELLS will bridge this gap.

Desired assured enhancement scenarios and their respective challenges to overcome include but are not limited to the following:

• Significant performance gains are possible by shifting operations to modern hardware (packet processing, data stream reassembly, signal processing, etc.), but refactored software must have isomorphic functionality;

• A new memory-safe technology to replace legacy vulnerability-prone networking code is available, but legacy under-specified behavior must be replicated precisely;

• Side-channel vulnerability mitigation requires isolating parts of computation on dedicated CPUs, but distributing execution of software written for a single CPU is risky.

Insufficiency of Current Approaches Today, enhancing legacy software components or replacing them with technologically superior ones for performance or security faces high risk that the new code, despite being proven correct according to a specification, will not be fully compatible with the rest of the existing system.

System owners fear that they might need years of additional adjustments to new code (and its proofs, if any) to reliably interoperate with the actual behaviors of the system. The risk is concentrated towards the end of the effort, when the verified software is complete enough to be integrated, run, and tested, and is often further amplified by the need to preserve bug-compatibility of new components with the rest of the code in legacy systems.

Neither proof assistants nor any other part of today’s verified programming toolchains mitigate this risk. Crucially, these tools are not aware of the existing source code or binaries of the old component or of the other system components, and can’t examine such source code or binaries or draw on them in the course of the verified code development. Today, compatibility is a matter of getting the specification right and staying consistent with it.

Adjustments to the specification require costly combined effort of multiple mathematicians conversant in the proof assistant languages, besides the domain requirements engineers who formulate the system’s desired functional properties and the software engineers who actually implement the system. This inhibits the use of verification for enhancing or replacing parts of existing infrastructures.

Today’s software engineering tools and standards for composing software offer meager support for reasoning about software components at the implementation level, and thus enabling their seamless enhancement or replacement. For example, the designs of Application Binary Interfaces (ABIs)—the mechanisms that translate the abstraction of software libraries into binary linking and loading, and so underlie all code reuse—saw their last major advancement in late 1990. These advances enabled binary code relocation and runtime loading of binary libraries within a single address space, but offer no help for distributing code units across computing

HR001120S0058 V-SPELLS 7

nodes, reasoning about code unit dependencies, or for combining proofs. Shortcomings of native ABI library mechanisms led to an explosion in container-based solutions (e.g., allowing developers to maintain dozens of versions of a library dependency within a system), but these only increase technical debt, creating potential for avalanching flaws. Similarly, failure of ABIs to express known structure and properties of software doesn’t allow software orchestration to take advantage of such knowledge, requiring introduction of cumbersome additional levels of complexity to achieve desired decoupling and composability. ABI research needs new clearly posed challenges to advance.

Today, standard ABIs and other software engineering abstractions do not commonly offer first-class mechanisms and design patterns for safely composing new functional logic with the existing codebases and executable systems. Conversely, although examples of such safe composition patterns exist in systems programming practice, in the form of hook systems and DSLs recognized for their unprecedented stability, compositional safety, and ease of debugging—and delivering outstanding “return on investment” capability for safe, secure enhancements for production systems at scale—the root causes of these properties are not studied by program verification theory.

Finally, no metadata standards exist to support composition and translation of verification proofs.

For example, there is no support for granular, composable packaging of proofs with the binary code they prove correct, for automated translation of proofs between different hardware models, or for automated adaptation of proofs to distributed and orchestrated refactoring of code. The lack of standard, practical, and theoretically sound approaches to these tasks impedes proof engineering.

The V-SPELLS program seeks to address these gaps by combining novel concepts in verified programming with recent developments in domain specific languages and composable system architectures in production systems at scale.

Program Scope The V-SPELLS program will enable piecewise, compatible-by-construction enhancement of software components in legacy computer systems. To accomplish this, V-SPELLS will create methods and tools to recover succinct expressions and models of domain data abstractions and domain logic from source code, add enhancements at the level of these models and expressions, produce performant executable artifacts of these enhancements together with proofs of their safety and correctness, and safely compose these artifacts with the legacy system.

V-SPELLS tools will leverage iterative and interactive automated program understanding of a large code base to semi-automatically derive concise representations (such as DSLs, models, or specialized virtual machine operations) of the domain data structures and domain logic of a targeted component or subsystem. The tools will also concurrently infer the component’s specification within the larger environment. V-SPELLS tools will support safe and composable functional enhancements of the system using these representations, and then will generate, optimize, and distribute executable artifacts of these enhancements across the system, creating and validating relevant proofs.

V-SPELLS will combine novel concepts in verified programming that enable granularity and composability of proofs with recent developments in application of domain specific languages and systems architecture patterns for safe composition of functional software enhancements in production systems at scale.

HR001120S0058 V-SPELLS 8

Program Structure The program will produce theories, technologies, tools and formal proof methodologies leading to experimental prototype(s) that provide capabilities for piece-by-piece performance and security enhancement or replacement of legacy code in mission-critical systems. It is expected that these prototypes will provide a starting point for technology transition and assured incremental modernization of mission-critical software in cyber-physical system domains.

The V-SPELLS program is a 48 month program organized into three (3) phases: Phases 1 and 2 will be 18-months each, followed by a 12-month Phase 3, with milestones as described in Table

1. The program is divided into four Technical Areas (TAs):

TA1 Automated, iterative interactive program understanding TA2 Compositional DSL programming, component specification inference TA3 Verified layer flattening and distribution TA4 Demonstration and Evaluation

DARPA anticipates funding multiple technical approaches and performers across the V-SPELLS technical areas. Beyond Phase 1, subsequent phases will be considered options, and may or may not be exercised at the sole discretion of the Government. Funding of option phases will be based on demonstrated technical progress towards the goals of the V-SPELLS program and the availability of funds. There will be no forced down selects at the end of phases 1 and 2, but continued funding will depend on demonstrated progress in achieving program goals. It is desired that selected performers be funded through Phases 1, 2, and 3 of the program.

TA1 and TA2 performers should be prepared to work closely with each other in order to support integration of the TA1 tools for automated, iterative, interactive program understanding results with the TA2 environment for compositional DSL programming and component and interface specification inference, so that inferred specifications effectively inform further iterations of program understanding. In addition, TA2 and TA3 performers should be prepared to work closely with each other in order to support integration of the TA2 environment for compositional DSL programming results with the TA3 framework for verified layer flattening and distribution results, so that the enhanced code is performant, safely integrates with the code base, does not compromise the code base security, and can be suitably distributed among the hardware units, if needed for the enhancement.

To facilitate the open exchange of information, performers will have Associate Contractor Agreement (ACA) language included in their award. TA4 will be responsible for executing the V-SPELLS ACA. See Section VIII.D for more information regarding an ACA. While TA4 performers will be a party to the ACA, it is expected that TA4 outputs will be largely independent of TA1, TA2, and TA3 work.

Each proposal may address any one TA or any combination of TA1, TA2, and TA3. Proposals covering a combination of TA1, TA2, and TA3 must make the respective efforts and costs proposed on the different TAs clearly separable. Proposals covering combinations other that the full combination of the TA1, TA2, and TA3 should explain their rationale for the chosen TA combination and their collaboration plans with the TA not covered by their proposal.

Proposers may submit multiple proposals, and they may propose to multiple TAs or combinations of TA1, TA2, and TA3. In the case of submissions to multiple TAs or

HR001120S0058 V-SPELLS 9

combinations of TAs as above, the Government reserves the right to decide which, if any, to select for award. A proposer submitting proposals to TA1, TA2, and TA3 may be selected to perform on one, two, or all three of these TAs. When submitting separate proposals for more than one TA, and selected for more than one TA, significant cost reductions for the combined effort will be expected, through synergies of the proposed approaches. However, TA4 performers cannot perform on any other TA, to protect the integrity of program evaluation.

DARPA encourages proposers to consider the investigation and creation of open source and free software approaches and strongly encourages proposals that will provide an overall open source V-SPELLS framework that will result in open, modular tool architectures. Restricting technology transition of a proposed V-SPELLS technology may be considered a weakness of the proposal.

The Government will assess performer progress against target goals set for each phase, using a progression of technical use case challenges as outlined below in the Technical Areas. In addition, an advisory panel composed of participants from interested Government partners may participate in the meetings and in the informal challenges to provide feedback to the Program Manager.

Technical Areas

The program will enable piecewise, compatible-by-construction enhancement of software components in legacy DoD systems by creating methods and tools to recover succinct expressions and models of domain data abstractions and logic from the source code, add enhancements at the level of these expressions and models, and produce performant component implementations incorporating these enhancements that are verified to be compatible and secure, through progress in four key technical areas:

• Automated, iterative, interactive program understanding (TA1)

• Compositional DSL programming (TA2)

• Verified layer flattening and distribution (TA3)

• Demonstration and evaluation (TA4)

HR001120S0058 V-SPELLS 10

Figure 1: V-SPELLS Technical Areas (TAs) 1-3 Technical Area 1 (TA1) – Automated, iterative, interactive program understanding:

V-SPELLS TA1 performers will develop novel approaches that provide methods and tools for automated, iterative, interactive program understanding of software components in large code bases, based on extraction, matching, and application of domain-specific structures, expressions, and models.

In particular, TA1 tools will create the capability to interactively, iteratively extract domain abstractions and semantic models—such as concise descriptions of domain data structures and operations—and identify locations and paths in the code where these are instantiated. They will use this capability to infer architectural structure, composition patterns, assumptions, and dependencies in a legacy source code base, enabling its decomposition into components with explicit modular structure, interfaces, dependencies, and constraints.

TA1 tools will recover succinct expressions of the domain’s application logic—such as domain-specific semantic models (DSSMs) and domain-specific languages (DSLs). They will thereby untangle the targeted components’ application logic from low-level data representations and low-level implementations of notional operations of this data, performance optimizations driven by particular hardware choices, and similar detail incidental to the software components’ intended architecture, interfaces, and function.

A V-SPELLS TA1 capability will require research breakthroughs in convergent compositional verification, in which the specification of a component in the context of a larger system is inferred iteratively and interactively, through the effort of domain expert software developers supported by the appropriate code analysis tools, rather than primarily through the effort of software verification experts. V-SPELLS changes the role of the domain expert software developer from a mere implementer of a specification created by verification logic experts to the primary discoverer of the specification.

Strong TA1 proposals should discuss how the proposed effort will progress from effective methods of identifying and instrumenting all uses and operations on domain-specific data abstractions in legacy source code to replacement and enhancement of these operations with high-level DSL code, safely and usably composed with the rest of the legacy code base. The

HR001120S0058 V-SPELLS 11

Government desires this anticipated progression would be discussed in the context of a concrete open source software (or open software/hardware combination) solution that is commonly deployed in industry and has a known need for modernization. The discussion will clearly and quantitatively identify the challenges and obstacles to achieving safe composition and enhancement in this system, and present a compelling rationale for anticipated success of proposed approaches.

Proposals will present metrics and milestones for evaluating the progress of the proposed approaches in the context of the discussed use case, in line with the general program metrics in Table 1. For example, a strong TA1 proposal may argue that it will achieve refactoring of a significant open source software stack or its subsystem for safe instrumentation and functional enhancements such as protocol feature additions in months rather than years, and will automate code lifting to succinct enhanceable DSLs for the majority of the code rather than for isolated code fragments.

Strong TA1 proposals will present a review of the existing approaches, techniques, and challenges, emphasizing industry experience with and applications to large legacy systems, supported with appropriate literature citations.

The program will emphasize creating and leveraging open source technology and open source architectures. Strong proposals will offer metrics and benchmarks for evaluating the success of the existing and newly developed technologies, in open reproducible settings. Intellectual property rights asserted by proposers are strongly encouraged to be aligned with open source regimes. See Section VI.B.1 for more details on intellectual property.

Technical Area 2 (TA2) – Compositional DSL Programming:

V-SPELLS TA2 performers will focus on creating the capability for regular developers to quickly create new verified component replacements and enhancements that safely compose with the rest of the system.

TA2 performers will create a developer-usable integrated environment for compositional DSL programming and component specification inference in the context of a large existing code base.

This compositional DSL programming environment will enable developers to re-implement, re-engineer, and enhance a component of the system in a combination of DSLs and models derived for that component via TA1 tools, with automated assistance from the environment to ensure that the replacement is not only correct but also compatible-by-construction with the rest of the system. The environment will enable developers to incrementally re-implement and enhance application logic in the DSL, code unit by code unit, with continuous automated compatibility checking against the rest of the legacy code base and hardware interfaces.

Developers working with the TA2 integrated environment will receive immediate, interactive, and intelligible feedback on compatibility of DSL code they write with the old code and the rest of the code base. TA2 performers will develop ensembles of novel compatibility-focused program analyses, including static, dynamic, symbolic, concrete, and orchestrated combinations thereof, and the TA2 integrated environment will apply these analyses in a usable, automated, interactive, and iterative manner to guide the developers.

The TA2 integrated environment will communicate the results of its analyses to the programmer in a form accessible to a developer who is a domain application expert but not a program verification expert. Strong proposals will emphasize accessibility of this communication, HR001120S0058 V-SPELLS 12 preferring, e.g., iteratively refined counterexamples with suitable annotations to formal logic, type, or proof terms.

The TA2 implemented environment will also support extracting the specification of the components from the DSL created by the developers, for export to TA1 and TA3 tools.

Together with TA1, V-SPELLS TA2 changes the role of the domain expert software developer from a mere implementer of a specification created by verification logic experts to the primary discoverer of the specification. Additionally, TA2 enables the developer to produce code that is provably correct and safely composable, without exposing any of the proof machinery to the developers, and instead communicating with them by means of DSL constructs and counterexamples. Assurance evidence generated in TA2, such as proofs and specifications derived from the developers’ DSL code, is communicated to TA3 tools transparently and without developer intervention.

The integrated environment will take advantage of the existing specification (if any), interface control documents (if any), source code and related metadata, build chain, unit tests, and other information available for the legacy code base. It is assumed that the source code and the build process are available for the majority of the system, and that interface specifications are available for the hardware and those components of the system, if any, that are opaque and cannot be rebuilt. However, it is not assumed that these specifications are fully faithful, and strong proposals will discuss approaches for validating these specifications against the actual hardware or opaque components, combining automated inference and automated interface exploration and interrogation to support compatibility analysis and verification.

Creating this V-SPELLS TA2 capability will require research breakthroughs in compatibility-by-construction and design patterns for safe composition with existing systems at scale, where a new developer-accessible verified programming workflow will be created specifically to replace components of an existing infrastructure.

Strong proposals should discuss the developer's workflows for re-engineering a component of a legacy system, wherein novel, compatibility-focused program analyses provide timely interactive feedback to the developer, seeking to amplify workflow efficiency through automation and interactivity. The developers are assumed to be experts in the application domain and familiar with advanced debugging techniques, but not experts in program verification, program logics, or proof assistants. Strong proposals should discuss how these analyses and workflows incorporate and leverage the existing legacy code base, its build process and tests, the capabilities developed in TA1, and any sources of information reasonably available in industry practice.

Strong proposals should couch the discussion within the context of a concrete open source software (or open software/hardware combination) that is commonly deployed in industry and has a known need for modernization. The discussion should clearly and quantitatively identify the challenges and obstacles to achieving safe composition and enhancement in this system, and present compelling rationale for anticipated success of proposed approaches. Proposals should present metrics and milestones for evaluating the progress of the proposed approaches in the context of the discussed use case, in line with the general program metrics in Table 1.

HR001120S0058 V-SPELLS 13

Strong proposals should address the challenges of interfacing with hardware functions, and providing usable compatibility analysis for changing hardware components and replacing software functions with hardware functions specified to implement the same interface.

Strong TA2 proposals should consider solutions that build on the experience of recent DSL-based systems engineering successes, which enabled safe kernel-level enhancement of production systems at unprecedented scales, by regular application programmers rather than highly specialized kernel experts. V-SPELLS observes that such engineering successes can be accelerated and applied to other code bases and domains, by automating the distillation of DSLs and domain-specific semantics interactively and iteratively, and effectively enabling domain experts to produce the equivalent of an actionable specification of the system sufficient for safe composition of functional and performance enhancements.

Strong TA2 proposals should present a review of the existing approaches, techniques, and challenges in academia and industry, supported by appropriate literature citations, and drawing on the industry experience of recent DSL systems engineering successes at scale.

The program will emphasize creating and leveraging open source technology and open source architectures. Strong proposals are encouraged to offer metrics and benchmarks for evaluating the success of the existing and newly developed technologies, in open reproducible settings.

Intellectual property rights asserted by proposers are strongly encouraged to be aligned with open source regimes. See Section VI.B.1 for more details on intellectual property.

Technical Area 3 (TA3) – Verified layer flattening and distribution:

V-SPELLS TA3 performers will focus on processes, designs, standards, and tools for creating safe and performant executable artifacts for the composable DSL-based enhancements and replacements, to be created for legacy code bases with TA1 and TA2 tools. TA3 will leverage recovered higher-level domain abstractions and inferred specifications to optimize the resulting executable artifacts, prove their safe composability with the system, and improve their security.

It is expected that the knowledge of higher-level domain abstractions and explicit component dependencies will help to overcome potential performance reduction due to added layers of abstraction, while maintaining the system’s security guarantees. We refer to these novel verified cross-layer optimizations as verified flattening.

TA3 will also leverage recovered abstractions and inferred specifications, as well as any other suitable program analysis techniques, to restructure code among the target platform’s available processors, computing enclaves, nodes, or devices. This capability will address security or performance enhancement scenarios that call for distributing the execution of legacy code for security isolation, shifting it to modern hardware, or partially offloading its functions to specialized hardware accelerators.

Alongside with the above artifacts and transformations, TA3 tools will produce proofs of their compositional correctness and safety. To achieve TA3’s correctness-related goals, performers will develop non-brittle and granular rules for composable representation, packaging, and transformation of verification proofs that support distribution and orchestration of verified programs. Strong proposals should aim to achieve composability and granularity of proofs similar to or exceeding composability and granularity of executable binary code reuse enabled by the Application Binary Interfaces (ABIs).

HR001120S0058 V-SPELLS 14

Strong TA3 proposals will develop novel theories and approaches for compilation of TA2-developed DSL enhancements or replacements for platforms consisting of multiple distributed compilation targets. These compilation techniques should be tunable for the goals such as performance, security, diversity, or verifiability, and the proposal will discuss a progression of provable properties associated with these goals.

It is expected that strong TA3 proposals design and develop novel ABI extensions to enable multi-target composition and develop ways of capturing and maintaining dependencies and transformations for composable, granular proofs to support verification for such composition.

The TA3 capability will require research breakthroughs that will bridge the gap between program verification and actual code reuse, by creating a methodology and tools to explicitly and universally describe semantics of composability for existing major ABIs, and extending ABI mechanisms to include and enforce constraints for non-functional or intrinsic properties of the software, including timing-related constraints for real-time systems.

Strong TA3 proposals should discuss how the proposed effort will progress from overcoming potential performance overhead of a high-level DSL (e.g., due to a naïve virtual machine implementation of the DSL’s operational semantics) to achieving superior performance, reduced resource footprint such as the initial memory load and shorter load times, and verified safe composition transparent to the developers using V-SPELLS tools. Strong proposals should also discuss progression in the scope and kinds of properties for which the granular and composable representation of proofs is achieved. This anticipated progression will be discussed in the context of concrete open source software (or open software/hardware combination) that is commonly deployed in industry and has a known need for composable feature addition and security enhancements. The discussion will clearly and quantitatively identify the challenges and obstacles to achieving safe composition and enhancement in this system, and present a compelling rationale for anticipated success of proposed approaches.

Strong TA3 proposals should present a review of the existing approaches, techniques, and challenges in academia and industry, supported by appropriate literature citations, with emphasis on industry experience of relevant engineering successes based on principled designs.

The program will emphasize creating and leveraging open source technology and open source architectures. Strong proposals should offer metrics and benchmarks for evaluating the success of the existing and newly developed technologies, in open reproducible settings. Intellectual property rights asserted by proposers are strongly encouraged to be aligned with open source regimes. See Section VI.B.1 for more details on intellectual property.

Essential Interactions between TA1 and TA2 and TA3 TA1’s analysis tools are required to provide the extracted domain model and domain-tuned structures, as well as the architectural information recovered from the legacy code base, to TA2’s reasoning about the component specifications and DSL code enhancements, as well as for TA2’s compatibility and compositional safety analysis of the new DSL code. For example, TA1 tools should produce useful representations of the component boundaries, dependencies, interfaces, linking artifacts, and other relevant artifacts for TA2’s use. TA2 is required to provide TA3 with the higher-level abstractions and inferred specifications of components recovered via compositional DSL programming, with assurance evidence alongside the newly developed DSL enhancements, and with other analysis artifacts necessary for TA3 to accomplish verified layer flattening and distribution. For example, TA2 tools should produce useful representations of the

HR001120S0058 V-SPELLS 15

DSL, interfaces, linking artifacts, and other relevant artifacts for TA3’s use. Robust interaction is expected and should be planned for between TA1 and TA2, and between TA2 and TA3 in identifying the goals of the envisioned automated interactive verified enhancement via fast, secure DSLs.

V-SPELLS will require technological advances in comprehending and interrogating software and hardware interfaces at the lower layers of the computing stack. Strong TA2 proposals should demonstrate relevant technical capability and expertise, and plan to interact with TA1 and TA3 to effectively communicate the results of their analyses for the respective TA1 and TA3 needs.

Proposals will be strengthened by combining a fundamental research capability with a team capability for handling legacy DoD code.

Technical Area 4 (TA4) – Demonstration and Evaluation:

The TA4 performer will assist the Government team in the development of evaluations for the technological capabilities developed by the TA1, TA2, and TA3 performers, and in providing feedback to the TA1, TA2, and TA3 performers. The TA4 performer will be responsible for defining and executing a testing approach that enables the incremental development, demonstration, evaluation, and eventual DoD transition of V-SPELLS capabilities.

The TA4 performer will produce evaluation exercises of increasing difficulty for assessing developed capabilities, and identify and curate a variety of use cases suitable for fundamental research, each advancing in coverage, automation, and assurance guarantees through the program phases. The case studies may include but are not limited to network daemon and client programming, Operating System (OS) subsystems and drivers operating on a standard bus such as USB, digital radio firmware, boot loader and chipset firmware (in particular, in chain-of-trust scenarios), and/or cloud applications, such as load balancing and staged input processing and validation.

Strong TA4 proposals are encouraged to consider developing evaluation approaches with open-source components that are a critical part of the DoD supply chains, and curate and provision open source software and hardware case studies suitable for fundamental research conducted in TA1, TA2, and TA3. Some examples are large deployments in industry, with a known need for modernization despite common use, realistic hardware offload scenarios and software decomposition/distribution for cloud deployments. There will be no Controlled Technical Information (CTI) in the use cases provided to TA1, TA2, and TA3 researchers, to facilitate broad research community engagement.

Strong TA4 proposals are encouraged to provide open-source activity approaches that represent diverse, DoD-relevant use cases of legacy software understanding and hardware platform modernization. TA4 proposals should also identify platforms and use cases for DoD transition, and apply tools and methodologies developed by the TA1 and TA2 and TA3 performers to these use cases.

The TA4 performer will produce the testbed for demonstrating the V-SPELLS technological capabilities developed by TA1, TA2, and TA3 performers and will evaluate these capabilities against the program metrics. Evaluation will include both security testing of the V-SPELLS superior technologies and rigorous testing of the functional enhancements produced with these technologies, via a series of evaluation/challenge exercises of increasing complexity and difficulty. The challenges should be suitable for fundamental research, shared without limitations

HR001120S0058 V-SPELLS 16

with the TA1 and TA2 and TA3 fundamental research teams, and should not contain Controlled Technical Information (CTI).

The TA4 performer will provide the transition use cases and work with the services to establish a V-SPELLS technology transition plan. The TA4 performer will also work with the transition partner for any transition accreditations or certifications required for transition of the resulting V- SPELLS capability to the services. The Government will require the TA4 performer to include personnel cleared at the SECRET level to work with transition partner(s).

The program will be reviewed in its entirety at the end of each phase to realign resources and focus effort during the next phase, as evaluated by program metrics included but not limited to the metrics in Table 1.

Security Testing Activities TA4 proposals should describe methods for developing tactics, techniques, and procedures capable of demonstrating specific weaknesses in the TA1, TA2, and TA3 performers’ technologies. Strong TA4 proposals should address TA1, TA2, and TA3 performer technologies, and integrated system software security proofs/analyses after component enhancement and replacement.

Evaluation Testbed Development The series of evaluation/challenge exercises will progress in scale and complexity as detailed in Table 1, increasing the technical complexity of the challenges and the assurance guarantees that TA1 and TA2 and TA3 technologies must meet.

In each evaluation/challenge exercise, TA1 and TA2 and TA3 performers will receive software/firmware source-level or equivalent high-level representations of the code that needs to be enhanced or replaced. After the performers formulate and apply the enhancement, the enhanced code will be tested for desired functionality, robustness, and security.

Program challenge exercises will be conducted at the performer’s site over the course of the program. The events will determine whether TA1 and TA2 and TA3 technologies are meeting program metrics, thereby aiding the Government in determining the value added for additional V-SPELLS program phases. Specific V-SPELLS end-of-program goals will be used during the Phase 3 evaluation/challenge assessment exercises. Strong proposals should present detailed plans for organizing the evaluations, demonstrations, and hackathons/challenges for the TA1 and TA2 and TA3 performers using the testbed, as well as plans for allowing the performers suitable access to the testbed to prepare for these events.

Challenges should be drawn from but not limited to a cyber-physical mission-critical software domain such as Air Force legacy code or a similar domain of mission-critical systems. The challenges should be suitable for fundamental research, should be shared without limitations with the TA1 and TA2 and TA3 fundamental research teams, and should not contain CTI.

To aid the TA4 proposers, the following discussion of an exemplary evaluation testbed from the Air Force domain is provided below. Proposers are encouraged to enhance it with other relevant challenges, systems, and domains as needed to demonstrate safe and effective composition with the legacy code base capabilities.

HR001120S0058 V-SPELLS 17

Exemplary Evaluation Phase 1 will evaluate the capability to replace a known problematic driver in a large monolithic system, such as the Linux kernel or a real-time embedded system, in a subsystem currently lacking BPF-like instrumentation, with a correct and compatible DSL version, while creating such instrumentation for the subsystem.

Phase 2 will evaluate the capability to replace a component in a large distributed system. An example of a possible transition would be a software enhancement of an Air Force legacy embedded platform.

During Phase 3, with additional funding at a later date, accelerated transition could be undertaken involving an UAV hardware platform representative of the DoD incremental enhancement needs, provided that the Phase 2 evaluation is successful in its performance metrics.

Program Phases and Metrics The capability milestones and metrics for the V-SPELLS program, shown in Table 1 below, are related to the capability to incrementally enhance legacy systems. The specific metrics provided in the remainder of this section are indicative of the expected progress. Proposers should describe specific approaches that they will use for test and evaluation purposes during each of the program phases.

Table 1: V-SPELLS Metrics

The Government will assess individual performer efforts in terms of the viability of their technical approaches, the trend in the performance of their systems over time, and their overall progress toward V-SPELLS program objectives.

Schedule and Milestones For each year of the effort, there will be quarterly meetings with the Program Manager (PM), consisting of two site visits and two Principal Investigator (PI) meetings. During these reviews, the PM will assess progress toward the solution via performer briefings, technical discussions, demonstrations, and informal end-of-phase evaluation/challenge exercises based on the target goals of each phase.

PI meetings will focus on open technical exchange. Difficulties encountered and possible

HR001120S0058 V-SPELLS 18

solutions will also be discussed. The goals of the PI meetings will be to: (a) review and share innovations/accomplishments of the V-Spells program; (b) review and discuss plans and options for technology demonstrations and prototypes and V-Spells evaluation/challenge exercises; (c) review and discuss results from meetings and events conducted prior to the tests and evaluation/ challenge exercises; (d) demonstrate prototypes; and (e) plan for the next six-month period.

The Government will specify the locations for the technical interchanges and PI meetings.

Evaluation/challenge exercises will be held at the TA4 performer’s site. For budgeting purposes, assume the locations of the two PI meetings held each year will alternate between Washington, D.C., and San Diego, CA. For budgeting travel to the TA4 performer’s site, assume the location to be on the opposite coast from your location (or if regionally located in the Midwest, choose the more expensive coastal travel destination, San Diego, CA or Washington, DC). In addition to site visits, regular teleconference meetings are encouraged to enhance communications and collaborations, as required, among the performers. Should important issues arise between program reviews, the Government team will be available to support informal interim meetings.

In-person meetings, evaluations, and site visits may be replaced with virtual ones if necessary.

Figure 2 provides a tentative evaluation schedule.