DARPA touts ‘formal methods' for nipping cyber disasters in the bud

Yahoo

21-02-2025

Officials at the Defense Advanced Research Programs Agency have begun nudging Defense Department managers to utilize idling DARPA cybersecurity tools meant to preempt hacks and accidents in critical programs.
A series of high-profile incidents in recent years has highlighted a kind of passivity among defense officials in the face of the damage caused, according to Kathleen Fisher, the director of DARPA's Information Innovation Office. Believing that systems can't stave off catastrophic cyber incidents caused by software vulnerabilities, the department often focuses instead on reactive fixes, she said.
But proactive tools for building more resilient software already exist in the Pentagon's arsenal of countermeasures, she said at a demonstration day at the agency's Arlington, VA headquarters earlier this month.
'We have many critical mission systems that have these kinds of vulnerabilities in them, and the way we've learned to deal with them is after they've been attacked, after we've learned, 'OK, that's a bad one,' we then go and fix it,' Fisher said. 'We pay billions of dollars after the fact to go fix these problems.'
In 2017, Russia conducted a cyberattack against Ukraine that's now known as NotPetya.
While the attack targeted Ukraine's power infrastructure, it ended up spreading outside the country, affecting infrastructure and businesses across Europe, including a Danish logistics company, Maersk, which is responsible for about 20% of global container shipping. In seven minutes, the attack destroyed 50,000 of the firm's computers and nearly wiped out the active directory system tracking its container ships. The company estimated the damage at around $300 million.
Seven years later, in July 2024, faulty software from security firm CrowdStrike took millions of government and private sector computers offline, delaying thousands of commercial flights and canceling medical procedures as part of the global outage. The disruption was widespread, but the root cause was determined to be an accident — a software glitch that spread through a routine update.
Events like these — adversarial or accidental — have become more prevalent in recent years. And according to Fisher, they highlight troubling software vulnerabilities in critical infrastructure. In response, the Defense Department and the broader U.S. government have developed a sense of 'learned helplessness' when it comes to addressing software vulnerabilities.
Over the last 10 to 15 years, DARPA has proven that a software design approach called 'formal methods' can address these vulnerabilities before they're exploited by a coding error or an attack. Rather than validate the security of software code solely by testing it after it's already written, a formal-methods approach designs software through rigorous mathematical analysis, verifying its performance before and as it's being built.
Some of the tools DARPA has developed have made their way into DOD programs of record, but adoption has been limited. Now, as concerns grow about the cybersecurity of military weapon systems, the agency is trying to raise awareness in the defense acquisition community that these solutions exist and are available for use.
'We can imagine a world without these software vulnerabilities, where we can eliminate the sense of learned helplessness across DOD, where we can rapidly secure critical systems . . . and where we can create a sustainable ecosystem of formal-methods tools that are ready and off the shelf for people to use,' Fisher said.
One early DARPA program to showcase the utility of formal methods was the High-Assurance Cyber Military Systems effort, or HACMS. The program ran from 2012 to 2016 and culminated with two demonstrations, the first using a small quadcopter drone and then, in 2017, using Boeing's autonomous helicopter, the Unmanned Little Bird.
During the second demonstration, a red team of hackers tried unsuccessfully to infiltrate the aircraft, according to Darren Cofer, a principal fellow at Collins Aerospace, whose predecessor Rockwell Collins was a contractor on HACMS.
'In HACMS, we showed that formal methods could be used to eliminate important security vulnerabilities from embedded systems in real aircraft,' Cofer said during the DARPA demo day.
The agency has since pursued several other efforts to improve the usability of formal methods for DOD platforms. One of those programs, called SafeDocs, addresses vulnerabilities in parsers – software tools that convert data into a usable format. Another effort, Assured Micro Patching or AMP, provides a way to fix software bugs without the source code and ensure that the fix itself doesn't do more damage.
These tools have all transitioned to DOD programs in a limited capacity, and DARPA has several other ongoing efforts aimed at further improving formal methods. Fisher noted that because the problem hasn't been fully solved, there's a tendency for programs to hold off on adopting it. But DARPA sees potential for these technologies to be planted more widely now -- both to secure existing DOD software installed on legacy platforms and to design software for future systems.
'We have plenty of technology that's ready for prime time and we should go ahead and transition and use that technology now because it will dramatically improve the security of our systems,' she said. 'We can't afford to wait until we've solved the whole problem to use the technology that we've got now.'
How quickly and broadly the Defense Department adopts these tools depends on a number of factors — including funding and prioritization within the military services.
To help spread the word and address barriers to adoption, DARPA kicked off the Capstone program last year. Through a partnership with the Undersecretary of Defense for Research and Engineering and the Director of Operational Test and Evaluation, the agency is working with the services to identify platforms that could benefit from formal methods.
DARPA is providing some matching funds to make the tools available and, according to program manager Steve Kuhn, expects to identify the platforms by May. Once the Capstone programs are selected, the agency will help identify and fix software vulnerabilities within them and capture lessons learned to be compiled in a best practice guide that all programs will be able to access.
DARPA's hope, Kuhn said, is that the guide will help DOD program offices see how resilient software tools are being applied and offer a resource that helps with that implementation.
'Part of the strategy that we've been embarking on is really an adoption plan that brings these resilient software tools to both our defense industrial base, our partners and the services themselves,' Kuhn said. 'We're not going to fix everything, but can we really capture what it takes to bring these tools to the masses?'