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

[dj at deadhat.com]

> On 3/18/16 at 2:33 PM, perry at piermont.com (Perry E. Metzger) wrote:
>
>>Now, on the more general question, although it is true that
>>specifications can contain bugs as well, that's not a reason to think
>>formal verification isn't exceptionally useful.
>
> ...
>
>>And again, the big win is not perfection (which is difficult to
>>achieve) but rather the ratchet effect.
>
> Ignoring the ability of  formal methods to actually find bugs,
> they are valuable because they make you look at code and systems
> from a different prospective. This different view will be
> particularly valuable if the system was developed informally
> e.g. using agile methods. Another viewpoint has great value for
> finding bugs.
>

Formal verification of software is something I gave up hope on in 1991,
but formal verification of digital logic, in particular any moderately
complicated crypto implemented in digital logic is pretty much the only
hope and salvation. Digital logic is roughly equivalent to functional
programming, except the syntax is friendlier and people actually use it in
real products. However the conventional mix of directed and randomized
testing that is used to validate and verify digital logic designs is next
to useless checking moderately complex crypto algorithms with many input
states. However formal equivalence verification of hardware against a high
level model of a crypto algorithm (be it C, cryptol, or whatever,
preferably human readable) can do the job over all states in minutes.

FEV is traditionally used in digital logic to check the synthesizer did
its job in turning RTL into gates. This is exactly the same as having a
tool that would verify that compiled machine code is formally equivalent
to the C that the compiler translated it from. This is because in digital
logic, no one trusts the synthesizer, whereas in software, only the
security people seem to mistrust the C compiler.

If we wrote software with the same restrictions we write RTL (fixed state
with purely functional transitions), the tools for formally verifying
model equivalence would already exist.

My might want to make our network protocols a little less baroque to make
that feasible.

DJ