Download this article in PDF format.
The Department of Defense (DoD) knows that a strong military requires cutting-edge, resilient software to power every weapon and support system. It also understands the potential vulnerabilities of these applications and the proliferation of “threat actors,” or those individuals and groups that target critical infrastructure, steal sensitive military code and otherwise compromise national security.
To address these issues, the Defense Advanced Research Projects Agency (DARPA) says it’s developing tools that help eliminate “exploitable vulnerabilities” before software is even deployed. “Rather than testing software for vulnerabilities after it’s built, formal methods use mathematical proofs to verify software behavior as it’s developed,” the agency says. “This approach ensures software performs exactly as intended, making it inherently more secure.”
The ultimate goal is to accelerate the widespread adoption of “formal methods”—math-based software development practices—to make military systems inherently more secure. This approach uses mathematical proofs to guarantee software behavior, aiming to build stronger, more resilient systems capable of defending against current and future cyberattacks.
New Accelerator Program Rollout
DARPA is now calling on industry partners to assist with the cause, knowing that the innovation, tools and implementation capabilities of these partners can help the DoD use and scale advanced security solutions across the defense landscape. In June, DARPA introduced the Resilient Software Systems Accelerator Program with the goal of kickstarting the “widespread adoption of math-based software development practices to make military systems inherently more secure against cyberthreats.”
At a recent Resilient Software Systems Colloquium, 300 leaders converged to address the critical software challenges that the DoD is facing. There, DARPA’s Kathleen Fisher described formal methods as “mathematically based approaches” that allow the user to prove properties about software to obtain guarantees. These techniques are used to develop “high-assurance, verified software, where mathematical proofs are employed to demonstrate that software on a system will behave as intended,” DARPA explains.
Rather than testing software for vulnerabilities after the application has been built, formal methods use mathematical proofs to verify software behavior as it’s developed. DARPA says this approach ensures software performs exactly as intended, making it inherently more secure.
“Many of DARPA’s formal methods tools have already transitioned to military services for further development and operational deployment,” it adds. “Strong overall cyber resilience requires urgent, broader adoption.”
Fisher said DARPA is eager for industry partners to get involved via the new Resilient Software Systems Accelerator. DARPA says this program will provide seed funding to formal methods tool developers that partner with defense companies to apply formal methods tools and measure their level of effort to implement them.
“We are here to call you to action, to seize this opportunity and to...motivate you to listen and to think about where you have systems at home that might benefit from formal methods,” Fisher said. “DARPA is announcing today that we are going to offer funding to do a red team assessment of a system. You guys do this cyber retrofit and then do another red team to assess the difference, and then document what you did in the retrofit in a best practices standard format.”
Extending its Efforts
DARPA is also working with the Departments of the Navy and Army, and the National Aeronautics and Space Administration (NASA) on additional Capstone program platform experiments. The programs comprise jointly-funded projects on operational platforms aimed at assessing critical findings, including level of resiliency, cost, time and level of expertise required to adopt various formal methods capabilities.
Each project runs for about two years and is focused on four key goals: achieving inherently more secure software; accelerating the Authority to Operate (ATO) process; streamlining software developmental testing; and developing a “Best Practices Guide” to support broad adoption.
