The Defense Advanced Research Projects Agency (DARPA) is implementing a new kind of computer security system that cannot be hacked. This system uses mathematical techniques which makes the codes looks like sentences that were logically arranged one after the other.
The technology used to create that hack-proof system is called formal verification, where every part acts like a mathematical proof. That means the program can be tested the same way mathematical theorems are proven.
According to Bryan Parno, a security and formal verification at Microsoft Research, says that with formal verification, the behavior of the program using a proof checker that will verify whether the statement is correct or not.
Jennifer Wing, the corporate vice president at Microsoft Research, added that they are not there to prove that the whole system is 100 percent correct and reliable.
Putting the Code to a Test
Little Bird, is a military drone that looks like military helicopters. While it was stationed at a Boeing facility in Arizona in 2015, a group of hackers tried to break into its system and take control of it. The hackers, however, got only as far as accessing one part of the drone's system.
Little Bird is a program of the High-Assurance Cyber Military Systems (HACMS). What the team did to the program of the military drone is to rewrite its software architecture using "high assurance building blocks." The purpose of those blocks is to make sure that the person who has access to one partition doesn't have the privilege to access other partitions. This way, they don't have full access of the system.
Since the beginning of computer science, there have been many attempts to create a formally verified software but was considered impossible. These days, however, a lot of giant tech companies like Microsoft and Amazon are collaborating with the U.S. military to do research on formal verification.
Researchers are still developing and creating different formal verification systems that are more ambitious than the last one.
