seL4 kernel is formally verified
Nicholas Mc Guire
mcguire at lzu.edu.cn
Mon Aug 17 11:43:40 CEST 2009
On Mon, 17 Aug 2009, Gernot Heiser wrote:
> 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:
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 !
More information about the l4-hackers