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

[Perry E. Metzger]

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.

As it happens, we now have worked examples of proofs of all three in
usable, real world code -- artifacts like CompCert and seL4 are quite
real things.

As I noted in a parallel thread, the OpenSSL implementation bug from
days ago was found using formal methods. This should be a wake-up
call. If the bad guys are not already using formal methods to find
exploitable holes, they will be soon.

It would be a great shame if the good guys were not also using formal
methods to prevent them from being able to find holes to exploit.


Perry
-- 
Perry E. Metzger		perry at piermont.com