Computer Scientists Close To Developing A Perfect, Hack-Proof Computer Code
As the world becomes more and more dependent on technology, it also becomes vulnerable to hacking.
In order to protect the devices against hacks, the engineers from the Defense Advanced Research Projects Agency (DARPA) have worked on a new kind of security mechanism— a software system that couldn’t be hijacked.
To test out the security mechanism, DARPA allowed “Red Team” hackers six weeks to try and take control of an unmanned military helicopter built by Boeing known as “Little Birds.” Further, they also gave the team additional to its computing network than actually the hackers could ever expect to attain. However, they couldn’t break through the defences of Little Bird.
“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.”
The computer code supporting the hardware was essentially unhackable with current technology, reports WIRED. The report notes the code is “as trustworthy as a mathematical proof.” The programming approach is known as formal verification, and which is written informally and assessed based mainly on whether it works. Each statement follows logically from the next. An entire program can be tested with the same confidence that 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, who does research on formal verification and security at Microsoft Research.
As most of the hacks are made by exploiting bugs and errors in code, it becomes essential to have formal verification that is hack-proof. With this approach, the codes that have undergone this process are supposed to be bug-proof. Since, the code just works, it leaves no holes for hackers to exploit.
The code is still in the initial stages and required a lot of work and testing for it to come through. However, once through, the benefits could be huge, as this coding technique could be used for the groundwork of things like home automation and public services, which always run the risk of being hacked.