Confirmed! Researchers Are Close To Creating A Hack-Proof Code

More and more things are getting connected to the internet. Apart from its advantages, it also raises a concern regarding these things becoming prone to hackers. A DARPA-led project HACMS is aimed at developing the formal verification technology. The software is designed in accordance with the formal specifications that make them hack-proof.

The rise of the technology and the internet has been a doorway to sophisticate security breaches. For advanced hackers, jumping into complex systems is like a child’s play. A single bug gets caught in the software code and puff–You have been hacked!
So, the matter of concern for the security researchers is the process used to write the software code. In general, programs are written in an informal way and testing is done to get assured that the code is working and producing the desired output.

Last year, an unmanned version of the military helicopter Little Bird was tested by a Red Team of hackers. The task was to take control of the helicopter. The team was granted access to part of Little Bird’s system and it was not a big deal for them to penetrate further into the system. But the real motive was not to test the existing software of the helicopter.

The task was a part of HACMS (High-Assurance Cyber Military Systems), a DARPA-funded project. DARPA developed a completely new security system for the Little Bird. The team failed to hack Little Bird’s security in 6-weeks even though it had more access to it than an actual attacker.

“They were not able to break out and disrupt the operation in any way,” said Kathleen Fisher. “That result made all of DARPA stand up and say, oh my goodness, we can actually use this technology in systems we care about”. Fisher is the founding program manager of the HACMS project and a computer science professor at Tufts University.

The new system was based on formal verification, a buzzword from the past that is gaining popularity among the security community. Formal verification is a technique of testing a software code like a mathematical proof. Each statement in a proof is logically derived from the preceding one. The same way mathematicians prove theorems.

“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, formal verification and security researcher at Microsoft Research.

The process involves the cross-checking of the fact that the code adheres to a predefined formal specification. So, basically, a formal specification defines what a program does.

“To see how this works, imagine writing a computer program for a robot car that drives you to the grocery store. At the operational level, you’d define the moves the car has at its disposal to achieve the trip — it can turn left or right, brake or accelerate, turn on or off at either end of the trip. Your program, as it were, would be a compilation of those basic operations arranged in the appropriate order so that at the end, you arrived at the grocery store and not the airport.”

The software installed on the Little Bird by HACMS is divided into partitions. The system is designed in such a way if a hacker manages to access a single partition, he won’t be able to access others. As it was in the case of Red Team which was granted to Little Bird’s camera system but failed to hack the helicopter.

DARPA has plans to use formal verification in various military techs like self-driving trucks and communication satellites. It’s not only defense organizations like DARPA who have been working on formal verification technologies. Tech companies like Microsoft and Amazon are also investing their efforts in creating such products.

Redmond’s Microsoft Research division is working on Everest, a project aimed at achieving formal verification for secure connections by creating a verified version of HTTPS. Another project in the works is to create a formal specification.