[clug] New from UNSW, formally specified and verified ARM kernel.
sjenkin at canb.auug.org.au
Tue Aug 18 18:11:20 MDT 2009
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, ...
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
More information about the linux