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.
Here's the interesting bit about what they actually did:
The platform needed the capacity of a traditional software language like C++ and the logical syntax and structure of proof-assistant programs like Isabelle and Coq, which mathematicians have been using for years. No such all-in-one platform existed when the researchers started work on EverCrypt, so they developed one — a programming language called F*. It put the math and the software on equal footing.
“We unified these things into a single coherent framework so that the distinction between writing programs and doing proofs is really reduced,” said Bhargavan. “You can write software as if you were a software developer, but at same time you can write a proof as if you were a theoretician.”
Couldn't help but notice the code is built with a compiler named "KreMLin". Isn't that interesting.
It's possible to be mathematically perfect...in fact, mathematically is pretty much the only way to be "completely" or "perfectly" anything.
The basic problem with mathematical proofs is that math is an abstraction (the model), and the perfect-and-complete nature of the proof can *only* ever apply to the abstraction. The degree of fidelity to which the model reproduces your particular real situation is another story. Mathematically proving your solution is perfect not meaningful by itself.
It's a huge red flag the the vendor in this ad is directing our attention to a meaningless mathematical proof of perfection in their product. This strongly suggests to me that there is no valid reason to trust their design.
Even if we stipulate a "perfect" set of cryptographic algorithms implemented in a mathematically "perfect" set of code, the solution is meaningless without proper implementation and user procedures.
For example: I've got a great VPN (it uses OpenVPN), but when it fails, all my traffic is suddenly exposed. So I adjust my firewall rules so the only traffic allowed besides that needed to establish the vpn link must go through through tun0. Or use wireguard instead. Until next week when I'm in a factory and I need to talk to some PLCs or I/O modules to configure them, then I turn off the firewall or use the "factory" instead of the "office" setting. Now I have to remember to turn it on again or I won't be protected. etc. etc. etc.
There are no "magic bullets", and somebody claiming to have one has just saved you the trouble of evaluating them any further.
"Reality is that which, when you stop believing in it, doesn't go away." - Philip K. Dick
It' impossible to prove that your crypto library is invulnerable to side-channel attacks. It is possible, however, to prove it's not vulnerable to common side-channel attacks. That's not nothing.
Their marketing hyperbole is so over the top, however, that I wouldn't trust them with anything.
A big problem in general in software crypto is that it's impossible to prove that the random/entropy source provided by the processor is good. There's no software work-around to that - oh, you can try to use I/O timings and so on, but those can be manipulated. Even if the code that generates the mask that is used in the fab is proven correct, we know the NSA is capable of tampering with the mask between code and fab.
After the Snowden revelations were understood, paranoid crytpo guys reached the point of "I can't only trust a hardware entropy source that I build myself from components I bought myself in person from a random store." That's not exactly productizable, but it's a fair assessment of the threat of the NSA.
Socialism: a lie told by totalitarians and believed by fools.