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

[Shayne Flint]

steve jenkin wrote:
> 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.
>
>   

But who says the specification is correct?

> "This doesn't sound like much, but it is a very strong formal statement,
> called functional correctness.
>
>