seL4 kernel is formally verified

[Nicholas Mc Guire]

On Mon, 17 Aug 2009, Gernot Heiser wrote:
> Hi,
>
> For those out there who missed the publicity (incl ./): NICTA
> announced last week that the formal verification of our seL4 kernel
> has been completed. This makes seL4 the first ever general-purpose OS
> kernel with a formal proof that the implementation is consistent with
> the specification.
>
> A paper on the project will appear in this year's SOSP.
>
> Details at http://ertos.nicta.com.au/news/home.pml#verified
>

This linke might help:
http://www.theengineer.co.uk/Articles/312631/Safersoftware.htm?nl=TE_NL&dep=webops&dte=140809

for some general comments (including this project) on complex software
and safety related verification - I would like to point you to
http://www.abnormaldistribution.org/ from Peter Bernard Ladkin as he raises
some interesting questions related to this work.

What did supprise me a bit is that: 

 7500 LoC yield 200k Lines of formal proof
 7500 LoC yield "more than 10k intermediate theorems

I wonder how scalable such an approach is... And of course raising (from a 
safety perspective) the question if the complexity and potential failures of
7.5k of Code were not replaced by a even higher complexity (of course its
a diverse representation - which takes out a lot of this imediately) - the
main concern I would have is that while this initial core might be very
reliable (see concerns raised at http://www.abnormaldistribution.org/) it
is a question of how changes to such a system can be handled and how the
interaction of the application/drivers can be handled in such a system. The
isolation of the core (microkernel) is not the issue (provided the full range
of the interface is covered in the formal proof) - but how far does that
actually help with respect to the actual safety related code, which is in
a user-space task/driver ? 

Neve the less this is a really impressive stunt - and I do hope more will be made available on the verification of this project !

thx!
hofrat