[mahemm]

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.

[schoen]

This is terrific stuff.

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.)

[fpgaminer]

Relevant stories:

Even though Curve25519 is built to be easy to implement in constant time, there was a non-constant time bug in a Curve25519 library: https://research.kudelskisecurity.com/2017/01/16/when-consta...

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 :)

[uxp100]

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.

[SilasX]

So, stupid question...

>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?

[krastanov]

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.

[fpgaminer]

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.

[Radle]

"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.

[taktoa]

It could prove its own correctness, but there is still the possibility that it has a bug that causes its proof of correctness to be meaningless :-)

[fpgaminer]

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.

[SilasX]

Fair point, I was too hasty in replying there.