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

[Perry E. Metzger]

On Wed, 11 Jun 2014 01:36:11 +0200 Lodewijk andré de la porte
<l at odewijk.nl> wrote:
> I'm very excited about this. This might finally open up the
> possibility to have a truly secure system!
> 
> Or at least, it's a mayor, mayor, mayor step in the direction.

Presuming you're referring to the seL4 news:

I'm enthusiastic, but within limits.

We have yet to see the license, and also, there is no POSIX style
multiserver available for the L4 microkernel platform at this point.
(Minix 3, which should not be confused with earlier versions of
Minix, is to my knowledge the only actively developed POSIX
microkernel+multiserver.)

Also, it isn't clear that the proof technology used for seL4 is as
flexible as some of the things that have come after. The Isabelle/HOL
infrastructure described in the papers the researchers published
sounds quite brittle.

However, yes, this will probably be something of a milestone. I was
somewhat surprised no one else commented on it before now.

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