[clug] New from UNSW, formally specified and verified ARM kernel.

[Grant Baldwin]

http://ertos.nicta.com.au/research/l4.verified/

Specifically:

"We chose an operating system kernel to demonstrate this: seL4. It is a
small, 3rd generation high-performance microkernel with about 8,700 lines of
C code."

This and other quotes strongly suggest the primary research outcome for the
l4.verified project was being able to prove formal correctness for a
microkernel of this size (subject to assumptions laid out). This has been
completed. This has interesting implications for proving formal correctness
of larger programs.


There is another project to actually develop the seL4 microkernel, which,
being in the same organization has a degree of people overlap in the
publications. They don't yet claim to have completed their project, but
assuming they someday do, it has some interesting commercial applications
and implications from design experience.

Different projects, different research & commercial outcomes.




> -----Original Message-----
> From: linux-bounces at lists.samba.org [mailto:linux-
> bounces at lists.samba.org] On Behalf Of steve jenkin
> Sent: Wednesday, 19 August 2009 10:11 AM
> To: CLUG List
> Subject: [clug] New from UNSW, formally specified and verified ARM
> kernel.
> 
> Is this a "milestone event" or just some cute Academic result?
> 
> They've formally specified and 'proved' their ARM kernel (L4).
> It's intended for embedded devices. Possibly security, telecomms, ...
> 
> cheers
> steve
> 
> An article:
> <http://www.theengineer.co.uk/Articles/312631/Safer%20software.htm>
> 
> 
> Their website:
> <http://ertos.nicta.com.au/research/l4.verified/>
> <http://ertos.nicta.com.au/research/sel4/>
> 
> The L4.verified project
>   A Formally Correct Operating System Kernel"
> 
> They found 166 bugs in the code.
> * proved 7,500 LOC 'C', not assembler and boot code (600 & 700 LOC)
> * 200,000 proofs, machine-checked.
> 
> They estimate its an order of magnitude cheaper than EAL-6 verification
> & testing. 12ppl, 4 years (~$7M) vs $10k/LOC normally (~$75M)
> 
> 
> "Our proof statement in high-level natural language is the following:
> 
> "The C code of the seL4 microkernel correctly implements the behaviour
> described in its abstract specification and nothing more.
> 
> "This doesn't sound like much, but it is a very strong formal
> statement,
> called functional correctness.
> 
> --
> Steve Jenkin, Info Tech, Systems and Design Specialist.
> 0412 786 915 (+61 412 786 915)
> PO Box 48, Kippax ACT 2615, AUSTRALIA
> 
> sjenkin at canb.auug.org.au http://members.tip.net.au/~sjenkin
> --
> linux mailing list
> linux at lists.samba.org
> https://lists.samba.org/mailman/listinfo/linux