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.
This linke might help: http://www.theengineer.co.uk/Articles/312631/Safersoftware.htm?nl=TE_NL&...
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