Formal methods can be applied at large scale

Formal methods can be applied at large scale
by Staff Writers
Washington DC (SPX) Mar 28, 2023

Engineering practices for software-reliant systems have evolved steadily over many decades, and so too have the assurance techniques that confirm systems' correctness and security.

Mathematically rigorous techniques, known as formal methods, have shown great promise to prove and provide continuous evidence of correctness for software systems. For example, DARPA's High Assurance Cyber Military Systems (HACMS) program demonstrated how these techniques could effectively secure Department of Defense (DOD) military systems.

Yet the majority of those techniques remain highly specialized and require a high level of expertise. Recently, revolutionary advances in tools, practices, and training within the formal methods community have facilitated the application of formal methods at greater scale. These advances indicate a tipping point that could result in increased access to affordable tools for traditional software developers and engineers lacking formal methods training.

Through a nascent discipline known as proof engineering, DARPA seeks to create higher levels of assurance that will help critical DOD software systems remain free of certain classes of defects and vulnerabilities.

Proof engineering will help developers construct software safely and ensure the software meets specified assurance requirements. DARPA's Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS) program will develop formal methods tools to guide software engineers through designing proof-friendly software systems and reduce the proof repair workload.

"The growing role of DOD software in warfighting, in the protection of national assets, and the safeguarding of human lives creates a diminishing tolerance for faulty assurance judgments," said William Martin, PROVERS program manager in DARPA's Information Innovation Office. "Ultimately, PROVERS aims to provide a pathway for national security systems to get ahead of cybersecurity threats, enabling high-assurance systems engineering and producing cyber-hardened, resilient systems and supporting infrastructure with verifiable security properties."

One of Martin's ongoing, related efforts helped lay the foundation for PROVERS. The Proof Engineering, Adaptation, Repair, and Learning for Software (PEARLS) AI Exploration project demonstrated how AI and machine learning could support and automate the generation and maintenance of proofs used in the formal verification of software at large scale.

Martin envisions the PROVERS program will 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. Furthermore, the tooling would integrate into a development pipeline enabling a continuous flow of capabilities over time while maintaining high levels of assurance.

PROVERS is a 42-month program spanning three phases that encompasses proof engineering, platform development, a red team to emulate potential adversaries' attacks, and a separate federally funded research and development center to provide quantitative evaluation and evidence curation.

A Proposers Day is scheduled for April 6, 2023; details can be found in the Special Notice at https://sam.gov/opp/bcf34cd2d80f4a109c5c15b75ed2063d/view.

This announcement will be updated once the Broad Agency Announcement is published.