The Defense Advanced Research Projects Agency is so confident in the hack-proof software it developed for a remote-controlled quadcopter that it invited hackers at the recent DEF CON cybersecurity convention to try to break in and take it over.
None succeeded, according to Ray Richards, program manager of DARPA’s Information Innovation Office. Work on DARPA’s High-Assurance Cyber Military Systems, or HACMS, demonstration concluded in 2017, Richards told Air Force Magazine, but this was the first time DARPA had invited all comers to try to hack it.
A video presentation at the DEF CON Aerospace Village on Aug. 6 in Las Vegas—a-convention-within-a-convention focused on hacking air and space craft—demonstrated the vulnerability of conventional software architectures for flight control and the value of high-assurance software techniques such as HACMS.
In the video, a red team of hackers was able to break into a quadcopter’s mission control system by exploiting an unpatched software flaw in its video camera. Once inside the camera, the hackers were able to overwrite the encryption keys that protected the quadcopter’s command and control communications with its ground base, dramatically hijacking the craft and flying it back to their own base.
But using a technique called “formal methods,” HACMS software mathematically ensures the absence of software flaws that let hackers break into and take over computer systems. Boeing used HACMS in its Unmanned Little Bird autonomous helicopter project.
The formal methods-built software for the quadcopter turned out to be unhackable, even by the pros at DEF CON, because the architecture rigidly separated the different functions of the mission control system. Even though it was still possible to break into the video camera software, the “pivot” to command and control that hackers so often rely on couldn’t happen.
Just in case, though—and in accordance with flight safety regulations—the quadcopter that DARPA let hackers go at in the DEF CON Aerospace Village was flight disabled.
Hackers could do whatever they wanted with the video camera, explained Darren Cofer, a DARPA contractor from Collins Aerospace, in the presentation. “They can do anything”—such as crashing the camera software or crashing the quadcopter’s virtual machine, or VM—”and the quadcopter is able to continue flying without any impact on its command and control from the legitimate ground station.” In fact, the VM itself can be remotely restarted by the ground controllers to regain control of the camera, he added.
Formal methods as a technique for software assurance was first proposed in 1973 but has long been widely regarded as too expensive and laborious—but no longer, Richards told Air Force Magazine. “We have reached a tipping point for formal methods technologies. Commercial entities are applying formal methods at scale, where it provides them a benefit.” The journal of the Association of Computing Machinery, Communications of the ACM, reported in July that both Google and Firefox have installed formal methods-verified components in their Web browsers, and that Amazon Web Services has also employed the technique for key components in its critical cloud services.
As software grows ever more complex, testing—traditionally the baseline technique of choice for cybersecurity assurance—becomes more and more time consuming and less and less effective, Richards said.
“The ever-increasing focus on cybersecurity will increase the demand for large-scale application of formal methods,” he said.