DARPA HACMS employed Formal Verification Methods to develop hack proof unmanned vehicles , weapons , satellites, and command and control systems

In 2011, Iran claimed to have downed a sophisticated American stealth drone, and unveiled what it alleged was a reverse-engineered copy of the futuristic looking RQ-170 Sentinel UAV, produced by defense giant Lockheed Martin. The drone was brought down by the Iranian Armed Forces’ electronic warfare unit which commandeered the aircraft and safely landed it, Iran’s Tasnim News Agency announced.

“Many things have computers inside and those computers are networked to talk to other things. Whenever you have that situation, you have the possibility for remote vulnerabilities where somebody can use the network connection to take over and get the device to do what the attacker wants instead of what the owner wants,” according to Kathleen Fisher, a professor of computer science at Tufts University and the founding program manager of the High-Assurance Cyber Military Systems (HACMS) project.“A lot of the ways attackers take over programs on machines and the Internet is by exploiting security vulnerabilities, and there are many kinds, such as the buffer overrun vulnerability, to which safe languages are just immune,’’ notes Andrew Appel, professor of computer science at Princeton University, who is considered an expert in the program verification field.

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 in August 2021  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.

DARPA, introduced a new unmanned drone with secure software that protects the control and navigation functions of the aircraft from a systems hack. During the summer of 2015 a team of hackers attempted to take control of an unmanned military helicopter known as Little Bird. Even though the Red Team was given six weeks with the drone and more access to its computing network than genuine bad actors could ever expect to attain, they failed to crack Little Bird’s defenses.“They were not able to break out and disrupt the operation in any way,” said Kathleen Fisher, a professor of computer science at Tufts University and the founding program manager of the High-Assurance Cyber Military Systems (HACMS) project.

The software was developed under Defense Advanced Research Project Agency (DARPA)’s High Assurance Cyber Military Systems (HACMS) program whose goal is to demonstrate the feasibility of using formal verification to improve the software security for complex cyber-physical systems. The researchers turned to formal methods, that programmers can use to create ultra-secure, ultra-reliable software. 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. The mini drone is made with software that is mathematically proven to be invulnerable under large classes of cyber attacks, said Kathleen Fisher. The goal of HACMS is to enable high-assurance military systems ranging from unmanned vehicles (e.g., UAVs, UGVs, and UUVs), to weapons systems, satellites, and command and control devices.