The Defense Advanced Research Projects Agency (DARPA) has launched a new collaborative effort with U.S. military services to improve the resilience and cybersecurity of defense software systems through math-based development practices.
Through its Resilient Software Systems Capstone program, DARPA is working alongside each military branch to promote the adoption of formal methods – software engineering techniques that use mathematical proofs to verify code correctness during development.
The initiative comes amid growing concern over the Department of Defense’s (DoD) reliance on outdated IT infrastructure and security policies, which experts say leaves critical systems vulnerable to cyberattacks.
“A strong, lethal military depends on secure, modern software,” Stephen Kuhn, DARPA Capstone program manager, said in a statement. “The current patch-and-pray approach to software development for DOD systems is simply unacceptable when lives depend on those systems.”
The Resilient Software Systems Accelerator will support the transition of formal methods tools to military and industrial partners. Many of these tools, developed under earlier DARPA programs, have already moved into service use. Now, the agency is seeking to speed up and scale adoption, citing the growing threat from adversaries targeting critical infrastructure and reengineering sensitive military technologies.
The program includes jointly funded projects focused on operational platforms and aim to assess the effectiveness and feasibility of formal methods. These assessments will consider resiliency outcomes, cost, implementation time, and the expertise required for adoption. Each project will run for about 24 months.
The U.S. Air Force is the first military branch to pilot a Capstone project, selecting the MQ-9 Reaper drone program as its testbed. Project goals include improving software security, accelerating the Authority to Operate process, streamlining developmental testing, and producing a best practice guide for industry-wide use.
To support broader transition, DARPA will provide seed funding to formal methods tools developers who will team with defense contractors to apply and evaluate these tools in real-world contexts. The agency is also offering funding for “red team” cyber assessments before and after formal method retrofits to quantify improvements in system resilience.
“DARPA’s transition approach through the Capstone brings resilient software tools to both the services and industry partners and will allow us to capture the lessons learned to drive broad adoption of correct-by-construction,” Kuhn said. “This effort will serve as a template that can be used by others to help jumpstart their efforts to incorporate DARPA’s resilient software tools into their platforms and development pipelines.”
Historically, DOD software development has leaned on standardized controls and static code analysis to catch human coding errors. But legacy systems often require extensive updates and prolonged testing cycles, with some upgrades taking more than a year to pass security and performance validation.
“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,” Kathleen Fisher, director of DARPA’s Information Innovation Office, said in a statement.
“Our goal today is to inspire widespread adoption of high-assurance formal methods, whether developed by DARPA or not,” Fisher added. “Through use cases, lessons learned and best practices, we’ve shown how this strengthens cyber resiliency, reduces costs and simplifies processes like securing authority to operate.”