[Cryptography] Yet more formal methods news: seL4 to go open source

[Phillip Hallam-Baker]

On Mon, Jun 9, 2014 at 1:09 PM, Perry E. Metzger <perry at piermont.com> wrote:
> On Mon, 9 Jun 2014 12:42:32 -0400 Phillip Hallam-Baker
> <phill at hallambaker.com> wrote:
>> > Have you tried? Indeed, if you write your code in a dependently
>> > typed style within Coq or what have you, how does one
>> > meaningfully update the code *without* updating the proof? (There
>> > are quite interesting artifacts written with Coq itself --
>> > CompCert, for example.)
>>
>> Folk should remember that for the purposes of security, the most
>> important concern is not whether the algorithm is 'correct', it is
>> whether the code has buffer overrun, memory leak or access to
>> unallocated memory.
>
> My own current work is (largely) about things like mundane C safety
> issues, so I'm not about to deny the importance of fixing
> those. However, the OpenSSL bug of mere days ago was not of this form
> -- it was a failure to follow a complicated protocol correctly.
>
> If you want to know, really *know*, that your security protocol has
> been properly implemented, or that your kernel can be relied on to
> isolate hostile processes, or that your compiler will not take your
> carefully vetted code and mangle it, you need formal methods.

Agree

But the other reason to look at formal methods is that they stop the
protocol getting complicated.

Having learned formal methods I quickly discovered that the best way
to get to a proof was to start from a compact, well engineered
starting point. So I became rather intolerant of the 'five ways to do
everything' school of protocol design.

IPSEC did junk ISAKMP in favor of IKE in the end but if a formal proof
had been expected, ISAKMP would never have been suggested in the first
place.


At the moment we have TLS and IPSEC which both have a full set of key
exchange and PKI management interfaces. And we have Kerberos that does
it all again in symmetric key with the option of using 40 different
authentication floozles. And each of these has the option of 50
different algorithms, a half dozen different key management policies
and they still don't do what a lot of folk want because the protocol
designers assumed that the scheme would be used a certain way and
baked their assumptions into the protocol.

If we start from scratch and separate out the problem of security
context negotiation from the packaging we can use one key
establishment mechanism to support any layer in the protocol stack
from IP, through TCP to Messages/Transactions.