[Cryptography] The Case for Formal Verification

[Tim Newsham]

> The CompCert people are claiming a formally verified compiler and I
> think this claim is very misleading to say the least.

I don't find it misleading at all and I think perhaps the
confusion is your notion of what formally verified means.

>> And to suggest that such a project is misguided because it places
>> blind trust in coq (and because it is written in ocaml?!) shows a
>> misunderstanding of the proof tools. There is a very small core of
>> trust that you need to have faith in and it is backed by solid theory
>
> Yes, the axioms.  These need to be small in number and 'obviously'
> correct; something that cannot be said of the source code of coq.
> The nearest I can think of is the Lisp subset written in itself in
> under a 100 lines (my memory is vague on this point)

What I am saying is that you do not need to trust the coq code.
There is actually very little of the coq tool that you do need to
trust. That is the part of coq that performs type checking. The
type checker is what verifies proofs.  It is a small part of coq and
most of coq is not trusted and generates terms that still must
pass the type checker. Neither do you need to put a lot of faith
in the ocaml compiler, the cpu or spend a lot of time worrying about
cosmic rays flipping the bits during computation.  Yes, some flaw
could potentially lead to an incorrect computation on a certain cpu
or a certain memory bit in a certain machine during a certain computation.
But the coq type checker has been compiled on many machines and
with many versions of the ocaml library and the odds of a random error
behaving in a way that just happens to validate an invalid proof term
more miniscule (as in, I would be more worried about your spontaneously
tunneling into my livingroom due to quantum effects to resume the rest
of this conversation).

There is a small part of coq that you DO have to trust. If this part
is incorrect it could invalidate all of the proofs. However, this part
of coq is backed by strong theory and has had many eyes on it.
And while it is possible that an error here could lead to a bad proof,
it is by no means assured.

> Derek M. Jones                  tel: +44 (0) 1252 520 667

-- 
Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com