US Air Force Reaper Drones to Test New Anti-Hacking Software

The computer code that runs the MQ-9 Reaper drone will be overhauled in the next two years to test revolutionary new tools that would make its software “much, much harder to hack,” the Air Force says.  

Oren Edwards, chief engineer for the Medium Altitude Unmanned Aircraft Systems Division at the Air Force Life Cycle Management Center, made the announcement June 17. 

The new tools will analyze past versions of the Reaper’s operational software “all the way from the user interface to the flight control commands,” Edwards told Air & Space Forces Magazine.  

Analyzing these older versions with the new tools, collectively dubbed “formal methods,” will demonstrate that the new tools are better at finding software flaws than conventional testing, Edwards said. Hackers seek to exploit those vulnerabilities to gain control of the systems.   

Kathleen Fisher, director of the Information Innovation Office at the Defense Advanced Research Projects Agency, or DARPA, said the Reaper demonstration is the first of four in a campaign to promote the tools and to “significantly move the needle” on cybersecurity. The other three demonstrations, which will also be jointly funded by DARPA and their military service partners, will work with the Army, Navy, and a NASA-Space Force team, she said. 

Formal methods provide mathematical proofs of software capabilities, ensuring the programs perform as intended—and only as intended, Fisher explained. 

Conventional software testing verifies what software can do, but testing can’t prove a negative, she said: “It can never tell you what the system will never do.”  

It simply isn’t feasible to test all the possible ways a software program might behave, she said.

“You can never, ever get enough test cases to get a guarantee the system will never do ‘this,’” she said. “But with formal methods, you can get those guarantees.” 

She offered an analogy to physical security: “Right now, where we are with cybersecurity is, our doors are open, our windows are open,” she said. “We actually know how to close the doors and lock the windows. And we are choosing not to use that technology. We’re choosing to leave the doors open, leave the windows up and not use the locks.” 

Using formal methods won’t make software impervious to hackers, however. Locking doors and windows doesn’t make a house impenetrable, Fisher said.

“A skilled, well-resourced adversary can probably still break in,” Fisher said. “But it will make it much, much harder to hack, and it will give us more time to defend ourselves.” 

“Formal methods work when you’re talking about any kind of software systems or any kind of hardware systems,” she added. “They are very, very broadly applicable.”  

DARPA Deputy Director Rob McHenry said the new formal methods can break the so-called “iron triangle”—generally summed up as “Cheap, fast, good: Pick any two you want.” 

“Think about code development,” he said. “How much of the code development process is debugging? We write bad code informally, and then we spend a whole bunch of time trying to debug it and make sure it actually works as we want it to.”

Formal methods cost more up front in time and effort but eliminate the need for debugging because it mathematically proves the absence of bugs.  

“If you start with a slightly higher investment in time in the beginning to make [a] formal methods architecture, you practically eliminate the debugging piece of code development, and that’s a massive curtailment of the cost and time” of the whole project, McHenry said. 

DARPA has been working on formal methods for 13 years, since launching the High Assurance Cyber Military Systems (HACMS) program in 2012. But even within the cybersecurity field, the tools are poorly understood.  

Now that is set to change, McHenry said. Amazon Web Services, the cloud computing provider, “has embedded formal methods throughout their operations at scale,” he said. In an organization almost as large as the Department of Defense—Amazon employs more than 1.5 million people—the company is doing the experiment for DARPA, he said.  

“They have taken what was early technology coming out of the HACMS program. They have done the piloting within their organization, McHenry said.

“They have seen the successes, and now they’ve scaled it broadly and depend on it day in and day out,” for core functions like securing data and identifying users, he said.

“It is not a DARPA dream,” said McHenry. “We have evidence from real-world implementations that show us we’re ready to scale this across the Department of Defense.”