Slashdot Mirror
A Suite of Digital Cryptography Tools, Released Today, Has Been Mathematically Proven To Be Completely Secure and Free of Bugs (quantamagazine.org)
By making programming more mathematical, a community of computer scientists is hoping to eliminate the coding bugs that can open doors to hackers, spill digital secrets and generally plague modern society. From a report: Now a set of computer scientists has taken a major step toward this goal with the release today of EverCrypt, a set of digital cryptography tools. The researchers were able to prove -- in the sense that you can prove the Pythagorean theorem -- that their approach to online security is completely invulnerable to the main types of hacking attacks that have felled other programs in the past. "When we say proof, we mean we prove that our code can't suffer these kinds of attacks," said Karthik Bhargavan, a computer scientist at Inria in Paris who worked on EverCrypt.
EverCrypt was not written the way most code is written. Ordinarily, a team of programmers creates software that they hope will satisfy certain objectives. Once they finish, they test the code. If it accomplishes the objectives without showing any unwanted behavior, the programmers conclude that the software does what it's supposed to do. Yet coding errors often manifest only in extreme "corner cases" -- a perfect storm of unlikely events that reveals a critical vulnerability. Many of the most damaging hacking attacks in recent years have exploited just such corner cases.
EverCrypt was not written the way most code is written. Ordinarily, a team of programmers creates software that they hope will satisfy certain objectives. Once they finish, they test the code. If it accomplishes the objectives without showing any unwanted behavior, the programmers conclude that the software does what it's supposed to do. Yet coding errors often manifest only in extreme "corner cases" -- a perfect storm of unlikely events that reveals a critical vulnerability. Many of the most damaging hacking attacks in recent years have exploited just such corner cases.
Generally, you fall back to some very axioms that everyone agrees on. That's the way math works.
"First they came for the slanderers and i said nothing."
Proving the code that USES their library is yet another thing.
That's the rub. There will be some wrapper written to make parameter exchange automatic, or facilitate finding a VPN gateway, or whatnot, and it'll undo all the hard work in a few lines of hastily coded VB.
There's a hard and fast requisit for establishing a MITM-proof crypto channel: you have to exchange some keying material safely... whether that's through a CA system or a preshared key or whatever, it simply must be done... and the users will choose the software which skips that step because someone assured them it is taken care of automagically, and well heck, that's much easier.
Someone had to do it.
I can imagine a mathematical formalism where every instantiation of a secret key must result in calling a destructor that securely zeroes the key.
I don't think it makes it as far as being compiled before it loses it's provability. The article says a new language, F* was built that is verifiable. But did they also verify the F* compiler?
My guess is that their library is only provably correct on a theoretical machine like a turning machine. But once the rubber hits the road, it could have a bunch of problems.
Still, some formal verification is better than many existing cryptographic libraries.
If you extend that reasoning further, then absolutely nothing is secure, because even secure hardware will be used by humans who do not practice perfect security. 2048-bit RSA running on a dedicated and verified FPGA is now insecure as well because some idiot human is capable of giving out the key. If there are flaws or vulnerabilities in other layers, it says absolutely nothing about the security of the software. You could argue that perhaps their proof is incorrect, but unless they've made some obvious mistake, we'd have bigger problems were that the case.