formal verification

Can you imagine a system that could not be hacked? That repelled those who tried? This apparently impossible dream has been pursued by developers for decades, without much success. In theory, this is perfectly possible; in practice, however, it demands too much effort and program code would be too long.

However, the HACMS project has taken a very big step to fulfill that dream. According to information recently revealed to the public, in the summer of 2015 the U.S. Defense Advanced Research Projects Agency (DARPA) conducted an experiment consisting of subjecting an unmanned military helicopter equipped with a new kind of security mechanism to attack by a team of six hacking experts. The helicopter was impossible to hack into, despite the hackers had the advantage of having been given access to some parts of the drone’s computer system.

The security mechanism they were testing is based on an old concept that only recently is becoming a reality: formal verification, a style of software programming that ensures code integrity. With the technology that we have today, it was absolutely impossible to hack into key parts of the helicopter’s computer system, its code as trustworthy as a mathematical proof.

Writing such strong computer code has been the aspiration of every expert since the inception of computer science. For a long time it seemed hopelessly out of reach, but the technological advances made by military and academic institutions, in collaboration with large multinationals such as Microsoft and Amazon, have made the idea of creating hacker-proof code a closer reality.

 

The technological advances made by military and academic institutions, along with tech giants, 

have pulled hacker-proof code into a closer reality.

panda securityThe ongoing efforts towards developing unhackable code are being spurred by the need to strengthen security in our increasingly interconnected world, with the Internet of Things becoming a reality in households, cities and almost every object that surrounds us.

The promising results of the HACMS project have already been replicated in other areas of military technology, such as satellites and driverless trucks, and Microsoft is working on two projects based on similar techniques: one aimed at securing complex cyber-physical systems such a drones, and another one, codenamed Everest, to create a verified version of HTTPS that allows users to browse online safely.

It is difficult to think that we are witnessing the beginning of the end of hacking, but it is true that we are one step closer to making things much harder for cyber-criminals by designing programs which, with today’s technologies, are impossible to tamper with.