EverCrypt: Snake oil or a major break-through in Computer Security … Provable safe code?

EverCrypt: Snake oil or a major break-through in Computer Security … Provable safe code?

Sometimes it feels like there is very little in the way of a proper foundation in computer security, and where little can actually be truly trusted. We define that RSA is secure for 4K keys, and where our computers would have to boil all the oceans on the planet to crack a single key. But this is hardly a strong mathematical base to build a future world on. Our coding methods, too, are often flawed and where we introduce bugs which can be exploited. So how do we make sure that a program does what it is meant to do?

And so, Karthik Bhargavan and his team, have introduced a coding infrastructure and which has in-built proof of its operation. For this they have released EverCrypt, and which is a cryptography library. This library contains code which is provable safe. EverCrypt is part of Microsoft’s Project Everest, and which aims to build the next generation of the HTTPs protocol:

Well, as someone who has investigated side channels in cryptography, it will be interesting to see if this is “snake oil” or a major breakthrough.

The proof, though, relates to the known attacks, and not to ones which it has not been tested against. If the methods prove successful, it would mean that a tester would not have to test the code for its behaviour, as it was provable, and in the same way that that area of rectangle is its length times its breath.

The code then makes sure it only does what it is suppose to do, and nothing else. This leads to a formal verification of the code. This should overcome the weakness in the integration of cryptography libraries, as these can be slow and buggy. Within EverCrypt, we see the integration of proof that the cryptography is actually working how it should be.

In order to make EverCrypt work, the research team needed the power of C++ and the proving methods of Isabelle and Coq. So, they came up with a new programming language called F*.

Conclusions

So with F*, you can write code, and prove it, all at the same time. It should be free of buffer overflows, and all of the common flaws that code brings. But can it to side-channels? … No! Can it guard against new threats? … No! But, at least, it will run code as it was meant to run, and, in many cases, that will be a major step forward for many applications.