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