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.