[Cryptography] Formal Verification (was Re: Trust & randomness in computer systems)

[Henry Baker]

At 10:07 PM 3/16/2016, Christian Huitema wrote:
>Adding ASSERT statements liberally expresses a lot about code intent, and will catch potential issues during a debug break.
>
>Of course, true formal development if applicable will be somewhat better than C + SAL + ASSERT.
>
>ASSERT are too costly to be compiled in the production code.
>
>They are only activated in special debug builds, and thus can only detect issues encountered during debug runs.

IMHO, this is completely backwards.

ASSERT's should always be sprinkled *extremely liberally* all over your code.

The job of a theorem prover is merely to remove ASSERT's that it can prove are *always satisfied.*  I.e., a "theorem prover" is just a really good compiler optimizer for dead code elimination.

The ASSERT's that remain (i.e., can't be removed) attest to either:

a) the weakness of the theorem prover; or
b) an actual bug or misunderstanding.

In short: there is no such thing as "formal verification", only *(correct) compiler optimizations* that can remove provably dead ASSERT codes.

If you can't remove an expensive ASSERT with a compiler optimization(*), then you sure as hell shouldn't remove it from a production system!

(*) This brings up the need for easy ways to add ad hoc, but provably correct, compiler "peephole" (?) optimizations, since no compiler will ever be able to prove -- thanks to Goedel & Turing -- without the programmer's help -- all the lemmas and theorems it will need for every program.  I need to be able to enter into a dialog with my compiler, suggesting that such-and-such should be replace by such&other under certain conditions.  The compiler will ask me to prove that my optimization is correct, which may involve inserting additional ASSERT statements into the compiler optimization.

This type of compiler extension is *easy* (or at least easiER) in introspective languages like Lisp.