HR001123S0020.pdf

Broad Agency Announcement

Pipelined Reasoning Of Verifiers Enabling Robust

Systems (PROVERS)

INFORMATION INNOVATION OFFICE

HR001123S0020

March 29, 2023

TABLE OF CONTENTS

PART II: FULL TEXT OF ANNOUNCEMENT

I. Funding Opportunity Description

A. Introduction B. Program Structure C. Technical Areas D. Program Assessments/Schedule E. Government-furnished Property/Equipment/Information F. Intellectual Property

II. Award Information A. General Award Information B. Fundamental Research

III. Eligibility Information A. Eligible Applicants B. Organizational Conflicts of Interest C. Cost Sharing/Matching D. Other Eligibility Criteria

IV. Application and Submission Information A. Address to Request Application Package B. Content and Form of Application Submission

V. Application Review Information A. Evaluation Criteria B. Review of Proposals

VI. Award Administration Information A. Selection Notices and Notifications B. Administrative and National Policy Requirements C. Reporting D. Electronic Systems E. DARPA Embedded Entrepreneur Initiative (EEI)

VII. Agency Contacts VIII. Other Information

IX. APPENDIX 1 – PROPOSAL SUMMARY SLIDE

PART I: OVERVIEW INFORMATION

Federal Agency Name – Defense Advanced Research Projects Agency (DARPA), Information Innovation Office (I2O) Funding Opportunity Title – Pipelined Reasoning Of Verifiers Enabling Robust

Systems (PROVERS) Announcement Type – Initial Announcement Funding Opportunity Number – HR001123S0020 Catalog of Federal Domestic Assistance Numbers (CFDA) – 12.910 Research and

Technology Development Dates o Posting Date: Monday, March 29, 2023 o Proposers Day: Thursday, April 6, 2023 o Abstract Due and Time: Friday, April 14, 2023, 12:00PM Eastern Time (ET) o FAQ Submissions Due and Time: Friday, May 12, 2023, 12:00PM ET o Proposal Due Date and Time: Friday, June 2, 2023, 12:00PM ET o BAA Closing Date: Monday, September 25, 2023, 12:00PM ET

Concise description of the funding opportunity – The Defense Advanced Research Projects Agency (DARPA) is soliciting innovative research proposals in the area of proof engineering, to include proof development, maintenance, deployment, and management.

Proposals should drive advances in proof engineering, providing for the development of knowledge, methods, and tools enabling integration of capabilities into a continuous software development pipeline accessible to traditional software developers and engineers, ensuring that critical DoD systems remain free of categories of defects and vulnerabilities.

Total amount anticipated to be awarded – Multiple awards are anticipated. See Part II.

Types of instruments that may be awarded – Procurement contract, grant, cooperative agreement, or other transaction Cost sharing requirements – Not applicable Agency Contacts o Technical POC: Brad Martin, Program Manager, DARPA/I2O o BAA Email: PROVERS@darpa.mil o BAA Mailing Address:

DARPA/I2O

ATTN: HR001123S0020

675 North Randolph Street Arlington, VA 22203-2114 mailto:PROVERS@darpa.mil

PART II: FULL TEXT OF ANNOUNCEMENT

I. Funding Opportunity Description

DARPA is soliciting innovative research proposals in the area of proof engineering, to include proof development, maintenance, deployment, and management. Proposals should drive advances in proof engineering, providing for the development of knowledge, methods, and tools enabling integration of capabilities into a continuous software development pipeline accessible to traditional software developers and engineers. The goal of this effort is to ensure that critical defense systems remain free of entire categories of defects and vulnerabilities. The term pipeline is meant to imply a continuous flow of enhanced capabilities with no decline of confidence with regard to cyber risks.

This publication constitutes a Broad Agency Announcement (BAA) as contemplated in Federal Acquisition Regulation (FAR) 6.102(d)(2) and 35.016 and 2 C.F.R. § 200.203. Any resultant award negotiations will follow all pertinent laws and regulations, and any negotiations and/or awards for procurement contracts will use procedures under FAR 15.4, Contract Pricing, as specified in the BAA.

DARPA BAAs are posted on the System for Award Management (SAM) website (https://sam.gov/content/home), and when applicable, on the Grants.gov website (https://www.grants.gov).

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

A. Introduction Formal methods for systems assurance have a rich history spanning half a century. Even in the early days of computing, there were efforts directed at mathematical specifications and proof of properties of programs. Motivated by emerging uses of computing software and hardware in critical systems (e.g., space or aircraft flight control, communication security, or medical devices), several US agencies invested in research in formal methods. For decades, however, formal methods tools and ecosystems could operate only on problems and systems of modest scale. Recently, there have been revolutionary advances in tools, practices, training, and ecosystems that have facilitated the application of formal methods at larger scales, pointing to the existence of a tipping point for the scalability and usability of formal methods in a manner that is affordable and accessible to traditional software developers and engineers.

The goal of Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS) is to develop formal methods tools fully integrated into pipelined software development and maintenance processes to enable higher levels of assurance that software systems are free of certain defects or security issues. These formal methods tools will be designed for software engineers who are not formal methods experts in verifying a system’s properties. Tooling will be integrated into a development pipeline, enabling a continuous flow of capabilities over time while maintaining high assurance.

https://sam.gov/content/home https://www.grants.gov/

B. Program Structure PROVERS is organized to advance proof engineering technologies and integrate these technologies into software development pipelines where they become more accessible to traditional developers without formal method backgrounds. Well-specified use cases, proposed by PROVERS performers, will provide the context for experts to advance program verification and proof repair technologies. Under PROVERS, changes will be made to use case specifications that will motivate repairs to supporting verification evidence. Computational and human effort to develop a proven implementation for the revised use case will be measured and assessed.

Specification changes and proof adaptations will occur in several cycles throughout the program as a means for technology developers to improve and refine their approaches. To assure the developed techniques are usable, the program will engage an increasing proportion of software developers/engineers without prior background in formal methods tools as it moves through three phases. In phase 1, planned use cases are open (unclassified) and activities will largely engage performers with substantial formal methods backgrounds. In phase 2, additional use cases will be introduced, along with some programmers without substantial backgrounds in formal methods tools. This personnel mix will be tasked with adapting software in four specification change cycles throughout phase 2. In phase 3, additional changes to established use cases will be handled largely by programmers without formal methods backgrounds.

A federally-funded research and development center (FFRDC), not solicited by this BAA, will handle quantitative assessments and evidence curation. They will help identify appropriate measurements and then collect/assess measurement results. An independent red team will assess the cybersecurity vulnerabilities of each PROVERS platform use case at kick-off and at the end of each phase. The FFRDC will combine red team assessment results with the evidence collected continuously over the course of each phase to inform end-of-phase evaluations. The FFRDC will also curate the systems produced and evidence collected.

C. Technical Areas PROVERS has three (3) technical areas (TAs), as shown in Figure 1, and a Quantitative Evaluation & Evidence Creation (QE/EC) activity that an FFRDC will perform. TA1 focuses on advancing proof engineering technologies and integrating these technologies into modern software development processes. TA2 focuses on providing platform use-cases for assessing TA1 capabilities.TA3 focuses on assessing the cybersecurity vulnerabilities of the TA2 platform use cases.

Figure 1. PROVERS Overview

TA1: Proof Engineering TA1 has three (3) sub-areas: scalable automation (TA1.1), workflow integration (TA1.2), and continuous feedback (TA1.3). TA1 performers will leverage their developed capabilities in concert with TA2 performers and associated use cases. TA1 performers should have exceptional expertise in formal methods including proof development, repair, and maintenance. Performers will have experience in deploying practical and scalable formal verification and program analysis tools across government and industry partners. Performers should have experience developing and deploying continuous assurance solutions, providing for automated analyses per pull request and reporting within traditional developer workflows. TA1 performers should have expertise in usability and human factors.

TA1.1 Scalable Automation should develop proof engineering tools to guide software engineers through designing proof-friendly software systems and to reduce the proof development and repair burden. Developed capabilities should address challenges of scalability and usability as well as increasing the range of properties that can be proven using formal methods tools. Proof engineering tools should help engineers design systems that are more amenable to verification.

Tools should automatically identify relevant proof design principles and help guide engineers through designing software systems to use those principles with a goal of automating proof repair. Proof engineers often use abstractions to make proofs that are less likely to break.

Promising related work includes information hiding techniques1, developing deep specifications to ease large system verification2, and developing specific domain design principles3.

1 G. Klein, “Proof engineering considered essential,” in Proc. 2014 - Formal Methods 19th Int’l Symp. May 2014, Springer LNCS 8442.

2 R. Gu, et. al “CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels,” in Proc. 12th USENIX OSDI, Nov. 2016. https://www.usenix.org/system/files/conference/osdi16/osdi16-gu.pdf 3 B. Aydemir, et. al., “Engineering Formal Metatheory,” POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages.

https://www.usenix.org/system/files/conference/osdi16/osdi16-gu.pdf

Proof repair tools developed within PROVERS will support scalable automation so that changes to code that are orthogonal to a verified property result in automatic updates to associated proofs.

Towards this end, tools that support breaking down large changes into smaller pieces should encourage scalable automation. Promising recent work includes the securing of an open-source implementation of the transport layer security (TLS) network encryption protocol by integrating continuous verification and leveraging tooling for analyzing cryptography4. Other work has demonstrated the feasibility of automating the repair of broken proofs5. Research efforts in identifying changes6, and factoring those changes into smaller parts, also provide encouraging steps in support of proof repair automation.7 8 9

TA1.2 Workflow Integration will integrate new and existing TA1.1 tools with widely-used tool chains consistent with common defense industrial base (DIB) workflows, providing for a continuous flow of enhanced capabilities. The aim of TA1 is to design and develop user interfaces and tools to match the intuition and expectations of traditional software developers rather than proof engineers. Tools are expected to be engineered so that as software is developed or updated, (re)assessment effort is comparable to the effort of maintaining the software.

Promising developments allow for continuous checking to ensure that properties remain true after software updates with re-established proofs and without extensive interaction from developers. Such developments in the domains of cryptography10 and static analysis11 have transitioned from research into commercial practice and should serve as a guide for PROVERS efforts. Leveraging these developments, TA1 proposers are encouraged to take a developer/analyst-oriented approach where formal reasoning methods adapt to help developers and analysts. A PROVERS goal is to provide for the seamless integration of formal methods into modern engineering workflows including the aforementioned (semi) automated repair and long-term proof maintenance in both models and code.

Proof engineering tools are expected to naturally integrate with traditional software engineering tools, making such tools accessible to DIB-developers by designing and developing user interfaces and tools to match the intuitions and expectations of software engineers rather than

4 A. Chudnov, et. al., "Continuous Formal Verification of Amazon s2n," in International Conference on Computer Aided Verification, 2018. https://link.springer.com/chapter/10.1007/978-3-319-96142-2_26 5 T. Ringer, Proof Repair, Seattle: University of Washington, 2021.

https://homes.cs.washington.edu/~djg/theses/ringer_dissertation.pdf 6 D. Hutter, "Management of change in structured verification," Proceedings ASE 2000. Fifteenth IEEE International Conference on Automated Software Engineering, Grenoble, France, 2000, pp. 23-31, doi:

10.1109/ASE.2000.873647.. https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=873647 7 I. Whiteside. Refactoring Proofs. Ph.D. Dissertation, School of Informatic, University of Edinburgh, 2013.

https://era.ed.ac.uk/bitstream/handle/1842/7970/Whiteside2013.pdf 8 R. Mitchell and L. de Moura. “Automation and Computation in the Lean Theorem Prover,” 2016. http://aitp-conference.org/2016/slides/RLslides.pdf 9 R. Selsam and L. de Moura. Congruence Closure in Intensional Type Theory. International Joint Conference on Automated Reasoning (IJCAR) 2016. https://arxiv.org/pdf/1701.04391.pdf 10 A. Chudnov, N. Collins, B. Cook, J. Dodds, B. Huffman, C. MacCárthaigh,, S. Magill, E. Mertens, E. Mullen, Tasiran, S. Tasiran, A. Tomb and E. Westbrook, "Continuous Formal Verification of Amazon s2n," in International Conference on Computer Aided Verification, 2018. https://link.springer.com/chapter/10.1007/978-3-319-96142- 2_26 11 D. Distefano, et. al. “Scaling Static Analysis at Facebook,” Communications of the ACM, August 2019, Vol. 62 No. 8, Pages 62-70 https://cacm.acm.org/magazines/2019/8/238344-scaling-static-analyses-at-facebook/fulltext proof engineers. These tools will help software engineers interactively generalize tests to specifications for writing proofs, or infer specifications from program analyses. Tools should check relevant specifications for correctness and integrate with debuggers to help software engineers fix incorrect programs or specifications. Tools should prove as much as possible automatically, then prompt software engineers with only the relevant questions needed to complete proofs. Promising activity on robustness and trustworthiness that allows proof assistant users to harness satisfiability modulo theories (SMT) solvers in a trustworthy way12 suggests an opportunity of using proofs as auditable certificates for communicating about formal guarantees (regulatory standards/security practices) of system assurance. Recent efforts also allow proof authors to automate reasoning procedures at a more familiar level of abstraction13.

PROVERS TA1 performers should adapt proof engineering methods specifically to developers and analysts with the seamless integration of proof engineering into modern software engineering workflows with feedback delivery in step with developer workflows. Advances may allow developers to recognize and resolve issues themselves by providing them with accurate and actionable feedback. Developments could provide for gentle, timely, and effective prompting to aid developers in improving the security of the systems they are developing. Software analysis results should be delivered within processes focused on the modified software, allowing developers to easily triage issues without disrupting their workflow. Capabilities will integrate with proof repair tools to automatically adapt those proofs in response to changes. A natural place for such proof engineering integration is in the continuous integration/continuous delivery (CI/CD) pipeline, where analyses can automatically be adapted in response to software changes14 15.

TA1.3 Continuous Feedback will ensure that TA1.1 and TA1.2 capabilities continually adapt and improve based on engineer feedback. Program capabilities will be instrumented by TA1.3 to collect usage data16. Insights drawn from usage data, as well as studies that may be performed by TA1.3, will be leveraged by TA1.1 and TA1.2 performers17 18 to continuously improve performance and user acceptance within the program. Additionally, models that predict the costs and benefits of using formal methods should be developed based on this collected data.

12 B. Ekici, et. al., “SMTCoq: A plug-in for integrating SMT solvers into Coq,” Int’l Conf. on Computer Aided Verivifaction (ICAV) 2017, LNCS 10427. https://homepage.divms.uiowa.edu/~tinelli/papers/EkiEtAl-CAV-17.pdf 13 D. Matichuk, T. Murray, M. Wenzel. “Eisbach: A Proof Method Language for Isabelle.” Journal of Automated Reasoning Vol. 56, Issue 3, March 2016 pp 261–282.

https://trustworthy.systems/publications/nicta_full_text/8465.pdf 14 Travis CI, Travis-CI, Leverkusen, Germany. https://docs.travis-ci.com/user/tutorial/ 15 MuseDev, "MuseDev Readme," 5 Dec 2019. [Online]. Available: https://github.com/Muse- Dev/MuseDev#readme.

16 T. Ringer, et. al., "REPLica: REPL instrumentation for Coq analysis," in CPP 2020: Proc. 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, New Orleans, 2020.

https://dependenttyp.es/pdf/analytics.pdf 17 P. O'Hearn, "Experience developing and deploying concurrency analysis at Facebook," 9 July 2018. [Online].

Available: https://research.facebook.com/publications/experience-developing-and-deploying-concurrency-analysis-at-facebook/.

18 L. Dennis, R. Monroy and P. Nogueira, "Proof-Directed Debugging and Repair," in Seventh Symposium on Trends in Functional Programming (TFP06), Nottingham, 2006.

https://personalpages.manchester.ac.uk/staff/louise.dennis/pubs/proofddebugging.pdf

Strong proposals would include mechanisms for instrumenting tools to log user information and time (amongst other metrics). This tool instrumentation will be a means of collecting user data via non-intrusive techniques, thus reducing potential research load on the TA2 developers. The data should support quantitative evaluations, particularly regarding usability, efficiency, and cost metrics. Instrumentation data collected from TA2 human participants (engineers), may involve Human Subjects Research (HSR). Refer to Section 3e below for procedures on HSR.

TA2: Platform Development Strong TA2 proposals should nominate System(s) Under Test (SUTs) that have the characteristics of high-consequence national security systems. Preference will be given to SUT(s) that require the analysis of a composition of components over the course of the PROVERS program, as opposed to those that require analysis only of a single component. An ideal SUT would have a rich set of security requirements and safety requirements. TA2 performers will have responsibility to provide modifications/updates of the SUT within each of the three phases. TA2 proposals should include SUTs to be used throughout all three program phases. TA2 should provide SUT change requests (i.e., requirement changes) to TA1 and QE/EC that will notionally occur twice in phase 1, four times in phase 2, and twice in phase 3.

Additionally, TA2 SUTs are required to be open (unclassified) in phase 1. Following phase 1, TA2 proposers may propose to continue the use of the open phase 1 SUT into phases 2 and 3, or may propose to transition to use of a sensitive SUT for phases 2 and 3, to include national security systems.

A key question for the PROVERS program is the extent to which TA1 proof engineering tools can be used by non-expert software developers/engineers without unduly disrupting their existing software development processes and performance. TA2 performers will be required to demonstrate the use of TA1 developed capabilities on initial and updated SUT(s). TA2 performers are anticipated to utilize a mix of personnel with different degrees of experience with formal methods in software development. In early phases of the program, the TA2 personnel mix will likely include a greater proportion of developers with proof engineering experience; as the program progresses that proportion should diminish so that at the end of the program the developers involved would represent a population of software developers with minimal proof engineering experience. These TA2 performers will collaborate with TA1 performers throughout all three program phases, in the manner described below in "Interfaces Among Technical Areas and QE/EC."

Strong TA2 performers are expected to have experience and expertise in architecting, developing, and testing systems of national security relevance. Specifically, TA2 performers should have deep subject matter expertise relative to the proposed SUTs and provide this expertise to TA1, TA3, and QE/EC to facilitate their understanding of the SUT and the evolution of the SUT over the program phases. TA2 performers will have direct access to proposed platform artifacts and provide the collaborating TA1 performer team, TA3, and QE/EC access to relevant SUT artifacts to demonstrate PROVERS technologies throughout the program.

Collaborating TA1 and TA2 performers will provide each end-of-phase SUT to the TA3 red team for the security assessment.

TA2 roles also include:

• Providing details of TA2 performer software development workflow processes.

• Providing details of systems security and safety properties of SUT relevance;

TA2 will provide the collaborating TA1 performer, TA3, and QE/EC performers with access to SUT digital development artifacts listed below:

• SUT design artifacts, to include system/subsystem design description;

• SUT requirement artifacts, to include systems engineering descriptions of requirements and systems behavior in a format representative of the current state of the art in systems engineering;

• SUT implementation artifacts, to include software that satisfies requirements and implements functional system behavior specifications;

• SUT test artifacts, to include software test description, and;

• Change-sets that represent the SUT evolution during the course of the PROVERS program.

TA3: Red Team TA3 will provide the state of the art in security assessment: a high-quality red team that conducts baseline assessments before any modifications and then reexamines each high-assurance version at each phase boundary. TA3 will provide assessment results to the QE/EC team, in support of the quantitative evaluation. Additionally, TA3 will share the assessment results with the TA1 and TA2 performers. TA3 performers should have considerable experience with penetration testing, finding vulnerabilities via static and dynamic analysis, and formal methods-based vulnerability discovery. Strong performers are expected to have expertise in evaluating system designs and identifying vulnerabilities by adopting varying adversarial perspectives. TA3 performers should also have practical experience analyzing systems for security strengths and weaknesses, and identifying potential vulnerabilities that could lead to system compromise.

TA3 is focused on assessing the security of the targeted use-case systems, to include SUTs provided by TA2 performers and the Government. To that end, the Red Team will conduct static and dynamic baseline assessments of all SUTs at the initiation of phase 1, as well as at the initiation of phase 2 for TA2 proposers who do not continue the use of the open phase 1 SUT into phase 2. At the conclusion of each phase, the Red Team will conduct static and dynamic assessments of the verified systems produced during that phase. TA3 assessments will be conducted independently from the QE/EC activities and will be reported to the QE/EC team on completion of each phase.

Quantitative Evaluation & Evidence Curation (QE/EC) The QE/EC support is not solicited under this BAA. The following information is provided for program planning purposes.

In support of both program and TA metrics, a FFRDC will carry out a quantitative technology assessment. The QE/EC team will be responsible for conducting assessments throughout the program, capturing and quantifying progress made by all TA performers against their individual assessment goals. The QE/EC team will also provide for the curation of artifacts and evidence, such as structural entities (e.g., source files, libraries, build tools) and evidential entities (e.g., test and proof suites, test and proof results) of PROVERS TA2 use cases.

The envisioned QE/EC Government team member will have deep formal methods and security expertise in support of defense program efforts. They will have experience in the development and verification of safety/security-critical systems, and wide-ranging security expertise in diverse operational contexts. The QE/EC team will have deep experience in conducting assessments in a variety of technical areas and have the ability to draw upon specialized cyber expertise from across their organization. The QE/EC team will have experience tailoring assessments to the sponsor’s specific needs and adversarial concerns.

The QE/EC team will provide guidance for the performers (TA1, TA2, and TA3) to promote compatibility and measurability of their processes, and will use the artifacts generated by the performers to evaluate the effectiveness and usability of those processes. As the PROVERS program progresses, the QE/EC team will receive and curate the evidence from TA2’s use of the TA1 formal methods workflows to harden the platforms. The QE/EC team will also receive and curate the TA3’s red team evaluation of the platforms before and after hardening. This evidence will be used to measure the overall value and applicability of the formal tools and workflows developed in PROVERS, using objective and subjective metrics that may include the range of formal properties proven, comparative red team findings, developer productivity relative to time or other costs, and ease of use (including ease of updating proofs as the implementation changes). The QE/EC team will include subject matter experts in verification & validation, formal methods, systems engineering, and human factors.

Evidence Curation The QE/EC team will be responsible for curating evidence throughout the program as a basis for evaluation. From TA2 performers, this evidence will include artifacts from the system development workflow, repositories to track the development process, measurements taken, and such additional evidence as may be identified during the program. From TA3, this evidence will include outputs from Red Team exercises. Within the scope of the program, these outputs will help determine assessment metrics and milestones.

The overarching goal of PROVERS is to make formal methods accessible to non-experts (e.g., software developers and systems engineers) while minimizing impact on their existing processes and performance. Thus, in addition to code-focused metrics (e.g., defect rate, code quality, etc.), evaluation metrics developed by the QE/EC team will include elements of efficiency (of defect detection, overall development process, tool integration, and code base sharing) and cost (of scaling, use, adoption, and maintenance). Along with a baseline understanding of the TA2 workflow, the QE/EC team will use these metrics to characterize differences between traditional approaches of formal verification and continuous reasoning pipelines. Note that some metrics, such as usability, efficiency/performance, and adoption could include data from humans (including data collected from the backend of the TA1 tools), and thus could result HSR. Section IV.B.3.e below refers to HSR procedures.

Quantitative Evaluation Results of TA3 red team security assessments and evidence collected from the TA2 system development process will provide the basis for evaluation. The QE/EC team will collect evidence continuously from TA1 and TA2 performers over the course of each phase, with the collected evidence being evaluated at the end of each phase to coincide with red team exercises. In addition to the core evaluation metrics (see Table 1 in Section D), the QE/EC team will evaluate the relative cost and efficiency of using, adopting, and maintaining the TA1 tools within TA2 workflows. The QE/EC team will use judgment to determine which TA3 findings beyond the core evaluation metrics (see Table 1 in Section D below) will be shared with TA2.

Interfaces Among Technical Areas and QE/EC

Technical Area 1

TA1.1 develops capabilities and tools that will be integrated into modern workflows by TA1.2. TA1 capabilities and tools are instrumented through TA1.3 activities in support of analyses on usability, scalability, and user acceptance of capabilities.

TA1 performers will collaborate strongly with paired TA2 performers. These pairings, made at time of proposal submission by the proposal offeror or by the DARPA PM after the Scientific Review Official’s selections, will ensure TA1 performer capabilities and workflows are a strong fit for proposed TA2 workflows and use case artifacts. TA1 and TA2 performer selection, and necessary negotiation, will ensure technical alignment of TA1 performer technology capabilities and workflow concepts with TA2 platform providers and associated workflows. Performer selection will ensure that the TA2 platforms are relevant to PROVERS’ intent and are tractable to the proof engineering tasks and expertise of TA1. TA1 and TA2 performers will collaborate with one another to incorporate TA1 proof engineering tools into TA2 systems engineering workflows for development of the representative defense platform. TA2 will provide a description of the representative platform and of a representative systems engineering plan based upon TA2 subject matter expertise and experience in development of systems of relevance from a national security perspective.

TA1 performer team members are to be leveraged into TA2 system updates/change requests and will collaborate with TA2 performer team members. For phase 1, TA1 performer team members will collaborate in an unconstrainted manner with TA2 performer team members. For phase 2, and more so for phase 3, TA1 performer team member collaboration with TA2 performer team members will be constrained to emphasize the usability of TA1 tools by TA2 developers/engineers without formal methods expertise.

TA1 and TA2 performers will interact with QE/EC performer assessment team members as detailed by TA4 assessment needs. TA1 will provide for delivery of associated TA capabilities to the QE/EC team for curation.

Technical Area 2

TA2 provides platform use-cases in support of the PROVERS program, supporting artifacts, associated threat models and properties relevant to the system. TA2 platform and related artifacts are provided to the QE/EC team for curation, and for use by other PROVERS performers.

TA2 performers interact with TA1 performers as outlined previously.

TA2 will put forward updates/change requests to exercise maintenance/repair capabilities of TA1 throughout each of the phases, and as dictated by the phase schedule.

TA2 will interact with TA3 in support of communicating TA2 expertise related to the TA2 supplied use case.

TA2 interacts with QE/EC performer assessment team members as detailed by TA4 assessment needs.

Technical Area 3

TA3 ensures TA2 use cases are able to build both at initiation and end of phase.

TA3 provides a baselining and end of phase assessment of each TA2 use case for each phase, with assessments being factored into QE/EC assessments.

D. Program Assessments/Schedule

PROVERS is a 42-month program divided into three phases. The first phase will be 12 months, the second phase will be 18 months and the third phase will last 12 months. There will be four assessments to measure the technical progress over the course of the program: at the completion of phase 1, interim and final assessments in phase 2, and a concluding assessment in phase 3.

Continuation into phases 2 and 3 will be at the sole discretion of the Government program manager and will depend upon performer progress and funding availability.

For planning purposes, proposers should assume all meetings are two (2) days in length and alternate between the East and West coast. Table 1 shows the tentative goals and metrics for the assessments. Program Principal Investigator (PI) meetings are scheduled to help coordinate program activities, facilitate the assessment process, prepare evaluators for assessments, and disseminate results after assessments. Highlighted program events, including program kick-off, semi-annual PI meetings, and evaluations occurring in each phase, are depicted in Figure 2 below.

For the Government to evaluate the effectiveness of a proposed solution in achieving the stated program objectives, proposers should note that the Government hereby promulgates the following program metrics that may serve as the basis for determining whether satisfactory progress is being made to warrant continued funding of the program. Although the following program metrics are specified, proposers should note that the Government has identified these goals with the intention of bounding the scope of effort, while affording the maximum flexibility, creativity, and innovation in proposing solutions to the stated problem.

Proposals should cite the quantitative and qualitative success criteria that the proposed effort is anticipated to achieve by the time of each phase’s program metric measurement.

Phase 1:

Preparation

Phase 2:

Hardening

Phase 3:

Maturation

Capability Metrics Low complexity Expert developer

Moderate complexity Journeyman developer

High complexity Traditional developer

Hardened artifact assessment

Percentage of serious findings by Red Team remaining

Less Than 25% Less Than 10% Less Than 5%

Provide for broad range of property verification

Number of classes of system properties proven

5 10 Greater than 10

Provide increments of assurance during system update and maintenance

Percentage of lines of proof requiring manual change following software update and maintenance

20% 10% 1%

Table 1. Program Goals and Metrics

TA1: Proof Engineering TA1.1: Scalable Automation

TA1.2: Workflow Integration TA1.3 Continuous Feedback

Meetings

TA2: Platform Development

TA3: Red Team

FFRDC: Quantitative Evaluation & Evidence Curation

Phase 1 (12 months) Preparation (Low complexity)

Phase 2 (18 months) Hardening (Medium complexity)

Phase 3 (12 months) Maturation (High complexity)

Continuous Integration Events Continuous Integration Events Continuous Integration Events

Open source systems of DoD interest

Sensitive applications/security appliances

Evaluation to what extent high assurance has been achieved without impacting development efficiency

Pipelining versions of new and existing TA1.1 techniques, to include integration with widely-used tool chains

Open source systems of DoD interest

Sensitive applications/security appliances

Open source systems of DoD

Sensitive applications/security

Continued analysis of efficiency metrics in comparison with conventional T&E, model coverage

Kick-off

PI Mtg

PI Mtg Phase I

Exercise / Eval PI Mtg

Phase II Exercise / Eval

PI Mtg

Capstone Eval (DEFCON)

Automation and scaling of diverse techniques for proof engineering, Maturation of existing automation techniques to increased scaling

Hardening tool integration

Integration exercises and evaluations on both open ecosystems and national

Tool integration demonstration with open and closed ecosystems

Continued tool maturation and Integration with modern software development infrastructure

PI Mtg PI Mtg

Figure 2. Program phasing and milestones A proposer should submit no more than one proposal as a prime contractor. Such a proposal may cover TA1, TA2, TAs 1 and 2, or TA3. However, proposers selected for TA3 red team cannot be selected for any portion of the other two TAs, whether as a prime, subcontractor, or in any other capacity from an organizational to individual level. This restriction is to avoid organizational conflict of interest situations between the TA and to ensure objective test and evaluation results.

If an organization is proposed at any level under both a TA3 and another TA proposal whose selections would create a conflict, the decision to de-conflict this matter is at the discretion of the Government. If a proposal is submitted for a TA 1 and 2 combination, the decision as to which

TA(s), if any, to consider for award is at the discretion of the Government.

Refer to Section III.D. for DARPA guidance on performer security clearance requirements.

E. Government-furnished Property/Equipment/Information Performers should not anticipate access to government-furnished property/equipment/ information except wherein a use case put forward by the Government calls for such access.

F. Intellectual Property A primary focus of PROVERS is developing capabilities within the program into the hands of traditional developers. The Government encourages Performers to open-source and democratize the capabilities developed under PROVERS. This focus should maximize transition success. The program would like to emphasize creating and leveraging open-source technology and architecture. Intellectual property data rights asserted by proposers are strongly encouraged to align with open-source regimes.

A key program goal is to establish an open, standards-based, multi-source, plug-and-play architecture that allows for interoperability and integration. This goal includes the ability to easily add, remove, substitute, and modify software and hardware components. This ability will facilitate rapid innovation by providing a base for future users or developers of program technologies and deliverables. Therefore, it is desired that all noncommercial software (including source code), software documentation, hardware designs and documentation, and technical data generated by the program be provided as deliverables to the Government, with a minimum of Government Purpose Rights (GPR), as lesser rights may adversely impact the lifecycle costs of affected items, components, or processes.

II. Award Information

A. General Award Information

Multiple awards are anticipated for TA1 and TA2, a single award is anticipated for TA3The resources made available under this BAA will depend on the quality of the proposals received and the availability of funds.

The Government reserves the right to select for negotiation all, some, one, or none of the proposals received in response to this solicitation and to make awards without discussions with proposers. The Government also reserves the right to conduct discussions if it is later determined to be necessary. If warranted, portions of resulting awards may be segregated into pre-priced options. Additionally, DARPA reserves the right to accept proposals in their entirety or to select only portions of proposals for award. In the event that DARPA desires to award only portions of a proposal, negotiations may be opened with that proposer. The Government reserves the right to fund proposals in phases with options for continued work, as applicable.

The Government reserves the right to request any additional, necessary documentation once it makes the award instrument determination. Such additional information may include but is not limited to Representations and Certifications (see Section VI.B.2., “Representations and Certifications”). The Government reserves the right to remove proposers from award consideration should the parties fail to reach agreement on award terms, conditions, and/or cost/price within a reasonable time, and the proposer fails to timely provide requested additional information. Proposals identified for negotiation may result in a procurement contract, grant, cooperative agreement, or other transaction, depending upon the nature of the work proposed, the required degree of interaction between parties, whether or not the research is classified as Fundamental Research, and other factors.

Proposers looking for innovative, commercial-like contractual arrangements are encouraged to consider requesting Other Transactions. To understand the flexibility and options associated with Other Transactions, consult http://www.darpa.mil/work-with-us/contract-management#OtherTransactions.

In accordance with 10 U.S.C. § 4022(f), the Government may award a follow-on production contract or Other Transaction (OT) for any OT awarded under this solicitation if: (1) that participant in the OT, or a recognized successor in interest to the OT, successfully completed the entire prototype project provided for in the OT, as modified; and (2) the OT provides for the award of a follow-on production contract or OT to the participant, or a recognized successor in interest to the OT.

In all cases, the Government contracting officer shall have sole discretion to select award instrument type, regardless of instrument type proposed, and to negotiate all instrument terms and conditions with selectees. DARPA will apply publication or other restrictions, as necessary, if it determines that the research resulting from the proposed effort will present a high likelihood of disclosing performance characteristics of military systems or manufacturing technologies that are unique and critical to defense. Any award resulting from such a determination will include a requirement for DARPA permission before publishing any information or results on the program. For more information on publication restrictions, see the section below on Fundamental Research

B. Fundamental Research

It is DoD policy that the publication of products of fundamental research will remain unrestricted to the maximum extent possible. National Security Decision Directive (NSDD) 189 defines fundamental research as follows:

‘Fundamental research’ means basic and applied research in science and engineering, the results of which ordinarily are published and shared broadly within the scientific community, as distinguished from proprietary research and from industrial development, design, production, and product utilization, the results of which ordinarily are restricted for proprietary or national security reasons.

As of the date of publication of this solicitation, the Government expects that program goals as described herein may be met by proposed efforts for fundamental research and non-fundamental http://www.darpa.mil/work-with-us/contract-management#OtherTransactions research. Some proposed research may present a high likelihood of disclosing performance characteristics of military systems or manufacturing technologies that are unique and critical to defense. Based on the anticipated type of proposer (e.g., university or industry) and the nature of the solicited work, the Government expects that some awards will include restrictions on the resultant research that will require the awardee to seek DARPA permission before publishing any information or results relative to the program.

University or non-profit research institution performance under this solicitation may include effort categorized as fundamental research. In addition to Government support for free and open scientific exchanges and dissemination of research results in a broad and unrestricted manner, the academic or non-profit research performer or recipient, regardless of tier, acknowledges that such research may have implications that are important to U.S. national interests and must be protected against foreign influence and exploitation. As such, the academic or non-profit research performer or recipient agrees to comply with the following requirements:

(a) The University or non-profit research institution performer or recipient must establish and maintain an internal process or procedure to address foreign talent programs, conflicts of commitment, conflicts of interest, and research integrity. The academic or non-profit research performer or recipient must also utilize due diligence to identify Foreign Components or participation by Senior/Key Personnel in Foreign Government Talent Recruitment Programs and agree to share such information with the Government upon request.

i. The above described information will be provided to the Government as part of the proposal response to the solicitation and will be reviewed and assessed prior to award. Generally, this information will be included in the Research and Related Senior/Key Personnel Profile (Expanded) form (SF-424) required as part the proposer’s submission through Grants.gov.

1. Instructions regarding how to fill out the SF-424 and its biographical sketch can be found through Grants.gov.

ii. In accordance with USD(R&E) direction to mitigate undue foreign influence in DoD-funded science and technology, DARPA will assess all Senior/Key Personnel proposed to support DARPA grants and cooperative agreements for potential undue foreign influence risk factors relating to professional and financial activities. This will be done by evaluating information provided via the SF-424, and any accompanying or referenced documents, in order to identify and assess any associations or affiliations the Senior/Key Personnel may have with foreign strategic competitors or countries that have a history of intellectual property theft, research misconduct, or history of targeting U.S. technology for unauthorized transfer. DARPA’s evaluation takes into consideration the entirety of the Senior/Key Personnel’s SF-424, current and pending support, and biographical sketch, placing the most weight on the Senior/Key Person’s professional and financial activities over the last 4 years. The majority of foreign entities lists used to make these determinations are publicly available. The DARPA Countering Foreign Influence Program (CFIP) “Senior/Key Personnel Foreign Influence Risk Rubric” details the various risk ratings and factors. The rubric can be seen at the following link:

https://www.darpa.mil/attachments/092021DARPACFIPRubric.pdf https://www.darpa.mil/attachments/092021DARPACFIPRubric.pdf

iii. Examples of lists that DARPA leverages to assess potential undue foreign influence factors include, but are not limited to:

1. Executive Order 13959 “Addressing the Threat From Securities Investments That Finance Communist Chinese Military Companies”:

https://www.govinfo.gov/content/pkg/FR-2020-11-17/pdf/2020-25459.pdf

2. The U.S. Department of Education’s College Foreign Gift and Contract Report: College Foreign Gift Reporting (ed.gov)

3. The U.S. Department of Commerce, Bureau of Industry and Security, List of Parties of Concern: https://www.bis.doc.gov/index.php/policy-guidance/lists-of-parties-of-concern

4. Georgetown University’s Center for Security and Emerging Technology (CSET) Chinese Talent Program Tracker:

https://chinatalenttracker.cset.tech

5. Director of National Intelligence (DNI) “World Wide Threat Assessment of the US Intelligence Community”: 2021 Annual Threat Assessment of the U.S. Intelligence Community (dni.gov)

6. Various Defense Counterintelligence and Security Agency (DCSA) products regarding targeting of US technologies, adversary targeting of academia, and the exploitation of academic experts: https://www.dcsa.mil/

(b) DARPA’s analysis and assessment of affiliations and associations of Senior/Key Personnel is compliant with Title VI of the Civil Rights Act of 1964. Information regarding race, color, or national origin is not collected and does not have bearing in DARPA’s assessment.

(c) University or non-profit research institutions with proposals selected for negotiation that have been assessed as having high or very high undue foreign influence risk, will be given an opportunity during the negotiation process to mitigate the risk. DARPA reserves the right to request any follow-up information needed to assess risk or mitigation strategies.

i. Upon conclusion of the negotiations, if DARPA determines, despite any proposed mitigation terms (e.g. mitigation plan, alternative research personnel), the participation of any Senior/Key Research Personnel still represents high risk to the program, or proposed mitigation affects the Government’s confidence in proposer’s capability to successfully complete the research (e.g., less qualified Senior/Key Research Personnel) the Government may determine not to award the proposed effort. Any decision not to award will be predicated upon reasonable disclosure of the pertinent facts and reasonable discussion of any possible alternatives while balancing program award timeline requirements.

(d) Failure of the academic or non-profit research performer or recipient to reasonably exercise due diligence to discover or ensure that neither it nor any of its Senior/Key Research Personnel involved in the subject award are participating in a Foreign Government Talent Program or have a Foreign Component with an a strategic competitor or country with a history of targeting U.S.