The U.S. Defense Advanced Research Projects Agency (DARPA) has awarded BAE Systems’ FAST Labs research and development organization a $6 million contract as part of the Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS) program. This initiative aims to enhance the security and correctness of critical Department of Defense (DoD) software systems through more efficient and accessible formal methods tools.
Current formal methods tools, a type of software verification, provide high levels of assurance through mathematical proofs that certain properties hold, but can be time-consuming and difficult to learn and use. These proofs also need to be re-written at every code or specification change, which fails to scale.
The goal of PROVERS is to make formal methods accessible to non-experts (e.g., traditional software developers and systems engineers) while minimizing the impact on their existing processes and performance.
“Engineering practices for software-reliant systems continuously evolve, and so too must the assurance techniques that confirm systems’ correctness and security,” said Daniel Mitchell, technical manager at BAE Systems’ FAST Labs™ research and development organization. “With PROVERS, proof engineering will create higher levels of assurance – helping critical Department of Defense software systems remain free of certain defects and vulnerabilities.”
Under the terms of the contract, BAE Systems will provide a Department of Defense (DoD)-relevant system to demonstrate how formal methods tools can integrate into the development and certification process and provide assurance of correctness. The company’s software engineers will also provide feedback to developers on how to ensure formal methods tools are applicable to DoD systems and how to make those tools accessible to them.
Work on this program will take place at BAE Systems’ facilities in Merrimack, New Hampshire; Burlington, Massachusetts; and Arlington, Virginia.
