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

[steve jenkin]

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