Several comments note that the headline is perhaps a little misleading; I agree, and I don't think any of us (I'm one of the cited people in the article) would've made such a strong claim.
Ignoring for a moment the fact that this is an alpha release (and that as such, a handful of minor proofs, e.g. mundane facts related to endianness conversions, have yet to be completed), there are several limitations of our work.
- Our tools themselves are not verified, so there could be a bug in F, z3, the kremlin F-to-C compiler; or a bug about the C compiler itself (unless one uses a constant-time fork of CompCert). We consider most of these to be theoretically unpleasant, but still an acceptable tradeoff.
- Specifications are extremely hard to get right: one might introduce a typo when reading an RFC, or, say, state an endianness conversion wrong. So, even before implementing an optimized version of anything, we audit and test the spec first. This is usually a good sanity check, but certainly not bulletproof (note that this is a general problem of software verification, not specific to us).
- As noted near the end of the article, our models do not account for Spectre and Meltdown; and there might be new classes of attacks that we can't guard against, for the simple reason that they haven't been found yet.
As to whether this is an attempt to get free security audits, I guess we weren't intentionally thinking of it! But we certainly would love it if people could test the code and give us feedback on what to improve to make this an even more compelling choice for whoever needs a good cryptographic library. I've written a bit about this here: https://jonathan.protzenko.fr/2019/04/02/evercrypt-alpha1.ht...
> there might be new classes of attacks that we can't guard against, for the simple reason that they haven't been found yet.
I've also puzzled about this phrase in the article. Why "class of attack haven't been found" necessarily leads to "we can't guard against this class of attack"?
I guess we need more definitions here to clarify what we're talking about... but you're doing that already, so maybe this statement can be made more precise elsewhere?
>Why "class of attack haven't been found" necessarily leads to "we can't guard against this class of attack"?
One thing I can think of is the practice of using multiple random number generators to generate a number that is random as long as any 1 generator is random. This guards against attacks on a specific generator even if those attacks are unknown. The class of attack is known, however, and protected against.
Moving past the silly headline, there is actually a pretty substantial achievement here. Using formal verification tools, the team proved the following properties for the library:
* Memory safety (no buffer overruns etc)
* Type safety (all compiler-visible interfaces/abstractions used as per spec)
* Functional correctness (all the crypto implementations are faithful to their algorithms)
* Side-channel resistance (all crypto is constant time)
This has been confirmed by fallible tools and is checked against human-made models which are also fallible, but this code is still likely to be about as close to bug-free as currently possible.
I think Barghavan's work in this area are the future of cryptographic coding in the medium term and likely all security-sensitive code long term.
One thing to think about might be that when we use the C output of this project in a non-formally-verified compiler (something other than CompCert), there might be compiler bugs that undo some of these guarantees. (The easiest one to see is that optimizers in the compiler could undo the constant-time guarantee -- I assume that the output or documentation indicates using keywords or pragmas or compiler options to disable some kinds of optimizations, but there could for example be a compiler bug where some optimizations can't be disabled this way.)
Basically the compiled code ends up using a run-time Windows library for 64-bit multiplication. That library decided to skip the upper 32-bit multiplication when the operands had 32 all zero MSBs. Oops.
ChaCha20 is also easy to implement in constant time. Which tends to be true. But most ChaCha20 implementations have other side channels. Turns out, when CPUs access non-register memory, the EM and power characteristics of that access are dependent on the bits of the data being accessed. Which means you can perform power or EM analysis on a CPU running ChaCha20 and extract the key. Oops. (Search for bricklayer attack)
In other words, become a cryptographer because you'll always have more work :)
I don't think there are any present, but fault injection mitigations (besides constant time execution, which does help) are something I'd be interested seeing their approach to.
I think it would be very useful if there were a way to formalize and prove that a particular mitigation was effective against a particular model of a fault. So if you assume a fault looks like X (single instruction skip, bit flips, multiple instruction skip, etc.) you could prove that a given SW mitigation was effective at retaining the other properties that are desired for the library.
This would be specific to a particular architecture of course.
>Functional correctness (all the crypto implementations are faithful to their algorithms)
You have to translate the human-written spec into the computer code that is used to validate the implemenation's code, right? And this point just means that this aspect is proven, yes?
So, doesn't that mean it's not proving an absence of errors in translating the human-readable version of spec into the validator code, right?
Usually there is a little bit more to it: the human-written spec (the mathematical description of the algorithm) is itself written in a format that can be validated. After the spec has been validated (i.e. finding a mathematical proof that the "platonic" version of the algorithm is "correct"), only then you do the second round of validation that confirms that the algorithm implementation is indeed equivalent to the platonic version of the algorithm.
It is validators all the way down. And at the very bottom there is a base piece of theorem-proving software that is only a few hundred lines of code that has been validated only by humans and self tests.
A caveat to this, which doesn't diminish your point but is interesting to consider, is that we prove the papers based on quite a lot of assumptions. For example, we may have 100% correct proofs that a given symmetrical encryption primitive is secure, but it's only secure under the common assumptions that A) the attackers are polynomial time, and B) that we don't care about any information the attacker may already have.
A is fairly obvious; we don't consider attackers who can perform infinite computation per second, because that's not practical. B is more subtly interesting. Most encryption systems reveal the length of the plaintext that's been encrypted, or at least some information about the length. But we don't consider that relevant in most of our proofs, because it's assumed to be information the attacker has a priori.
Of course in practice leaking length of the plaintext has sometimes made attacks on the overall system possible (encrypted VOIP calls can be partially decrypted because their packet lengths leak information about the speech being encoded).
We just ignore those problems in most of our proofs because building encryption primitives that don't leak that information is much, much harder and it's not _usually_ a problem.
Again, none of this detracts from the thrust of the arguments in this thread: formally verified code is objectively better than non-formally verified code; approaching the limits of our abilities today. The problems these assumptions may or may not introduce are universal to all implementations.
"And at the very bottom there is a base piece of theorem-proving software that is only a few hundred lines of code that has been validated only by humans and self tests."
Is it possible for that part of the system, to proof it's own correctness?
It's obvious that the danger with such a proof is that the code may think it's correct while it's incorrect in thinking it's correct.
But if I have learned one thing, then that Mathematicians can sometimes be really sly foxes.
You're right, but the comment you replied to covers that:
> This has been confirmed by fallible tools and is checked against human-made models which are also fallible, but this code is still likely to be about as close to bug-free as currently possible.
Well, as long as Intel does not devise a chip which chooses what to keep and what not to keep in the cache depending on the number of jumps executed and the name of the calling function... (just as way of example).
Also "optimized advanced heuristic multithreading" (for instance)...
I was thinking the only true way to prevent side channel information disclosure is to ensure x microseconds are spent encrypting/decrypting each byte in a message and using an external timer source as a reference clock to enforce the constant time interval.
Also, you never know what “side channel” may appear out the blue. Say, for instance, that Intel makes a chipnfor which 0’s spend less energy than 1’s in computations.
Reminds me of Steve Ballmer touting Windows XP as the "Most secure operating system ever" - on the day it was released. Claims that a code is unbreakable or hacker proof are big red flags.
First, the title of the article is typically from Quanta Magazine, which often uses editorialized clickbait titles to popularize scientific topics. Today, even Nature Communications seem to do it occasionally. If these claims are not directly from the official project, I don't see any red-flag here, it's an legitimate research project on formal verification.
On second thought, I think deliberately releasing a PR advertisement which claims a system is "unbreakable" can be a good way to receive free security audits.
So perhaps EverCrypt as a free and open source project who understands this point, the developers deliberately allowed Quanta Magazine to use this title, and so far, it has successfully received the attention of at least 5 HN users...
To be fair, formally proving that it contains no buffer overruns, timing differences, or memory access differences does make it immune to many/most of the standard hacking vulnerabilities.
There must be something in between right? Like... "secure"? Claiming "hacker-proof" isn't just an invitation, it's a challenge. Nothing triggers people like telling them something is %-proof.
The mathematical proof might be 100% solid and hacker proof. The implementation will probably never be.
Pretty secure compared to what? It had some security features that windows 95/98 didn't have so in comparison to windows 98 it was more secure. However windows XP had a large number of critical vulnerabilities and weaknesses.
A holiday sweater is more bullet resistant than a thin t-shirt, but no one would say a holiday sweater is "pretty bullet proof".
Protzenko noted there will always be attacks that no one has thought of before. EverCrypt can’t be proven secure against those, if only for the simple reason that no one knows what they will be.
Part of effective trolling is to actually get some credible folks to try and beat what you've created. I think the creators know saying things doesn't make it true. What makes it true is when you stick your neck out a little, troll a little, get people to take a few swings, and everyone sees they just keep on missing the mark. Or perhaps they land a punch, EverCrypt get a bloody nose, and we see whether and how they dust themselves off and try again.
I translate "hacker proof" into two things: this is something we all need; and we're ready, give us your best shot!
The Rust compiler does some limited "static analysis"* to determine if an array access is guaranteed to always be within bounds. But it doesn't do this universally. In other words, it's easy to write a program in safe Rust code that will attempt out of bounds accesses.
The saving grace is that in those cases the compiler just inserts a bounds check which panics at run-time.
That's a bit different from a formally verified OOB safe program which wouldn't require any compiler-injected bounds checking. All accesses are provably safe either because they are naturally so, or because the code explicitly performed a bounds check.
* IIRC what Rust's compiler actually does is just inject bounds checks on all array accesses and then depends on the underlying optimizations to remove them when possible. That's certainly a form of static analysis, but perhaps some wouldn't consider it as such.
Very true. Wouldn't it be possible to solve it to that standard using dependent types? I think I read that those are on a distant wishful thinking roadmap for Rust in some RFC. I really hope they get added some day, I find myself wanting them all the time.
Nice article! As a web developer though, I did a quick "View Page Source" on my browser and I saw a complete mess... I'm sorry Quanta Magazine, this is not good for your business.
They really need to rethink their website. Very low Pagespeed Insights score, very slow website and HTML/CSS is just a mess.
I understand that Cloudflare or their Minimize/Cache system is doing a lot of this mess, but this will definitely effect your Google results. For example:
Inside the Source code, search for the phrase "Programmers are human, but mathematics is immortal". Do you see that it appears two times? JS is doing some crazy things and this affects their actual HTML script.
The blog seems to be build with React. I don't understand why they need to reinvent the wheel and build Blogs from scratch. Just use WordPress.
Ignoring for a moment the fact that this is an alpha release (and that as such, a handful of minor proofs, e.g. mundane facts related to endianness conversions, have yet to be completed), there are several limitations of our work.
- Our tools themselves are not verified, so there could be a bug in F, z3, the kremlin F-to-C compiler; or a bug about the C compiler itself (unless one uses a constant-time fork of CompCert). We consider most of these to be theoretically unpleasant, but still an acceptable tradeoff.
- Specifications are extremely hard to get right: one might introduce a typo when reading an RFC, or, say, state an endianness conversion wrong. So, even before implementing an optimized version of anything, we audit and test the spec first. This is usually a good sanity check, but certainly not bulletproof (note that this is a general problem of software verification, not specific to us).
- As noted near the end of the article, our models do not account for Spectre and Meltdown; and there might be new classes of attacks that we can't guard against, for the simple reason that they haven't been found yet.
As to whether this is an attempt to get free security audits, I guess we weren't intentionally thinking of it! But we certainly would love it if people could test the code and give us feedback on what to improve to make this an even more compelling choice for whoever needs a good cryptographic library. I've written a bit about this here: https://jonathan.protzenko.fr/2019/04/02/evercrypt-alpha1.ht...