The U.S. Defense Advanced Research Projects Agency (DARPA) said they've successfully concluded a real world experiment where hackers were unable to remotely seize control of the code of a test system despite being given advantages that would have allowed them to do this.

DARPA said the hack proof code that withstood this hack attack was based on a style of software programming known as "formal verification." Formal verification can also be defined as the process of checking if a design satisfies some requirements.

Like Us on Facebook

 DARPA explained that formally verified software reads like a mathematical proof, meaning each statement follows logically from the preceding one. An entire program can be tested with the same certainty that mathematicians prove theorems.

It's worth remembering most computer codes is written informally and evaluated based mainly on whether it works. Not so for formal verification.

"You're writing down a mathematical formula that describes the program's behavior and using some sort of proof checker that's going to check the correctness of that statement," said Bryan Parno, who does research on formal verification and security at Microsoft Research.

To test formal verification as a hack proof process, DARPA  in late 2015 commissioned a team of hackers to take control of an unmanned military helicopter known as the Unmanned Little Bird H-6U made by Boeing.

Little Bird H-6U is the unmanned variant of the AH-6i manned scout helicopter used in U.S. special operations missions. The "Red Team" hackers were given several advantages.

At the time they began the operation, they were given access to one part of the drone's computer system. Now all they needed to do was hack into Little Bird's onboard flight-control computer, and the drone was theirs.

They failed to do so thanks to formal verification that formed the basis for a new kind of security mechanism developed by DARPA.

Key parts of Little Bird's computer system were unhackable with existing technology. The code remained trustworthy as a mathematical proof.

Even though the Red Team was given six weeks with the drone and more access to its computing network than genuine hackers 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.

"That result made all of DARPA stand up and say, 'Oh my goodness, we can actually use this technology in systems we care about'."

TagsDefense Advanced Research Projects Agency, DARPA, formal verification, Unmanned Little Bird H-6U, Boeing