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

[Steve McInerney]

Without having read TFA:
The cheaper part - and logically how they did so - is interesting.
The usefulness of it? Not so much.

TCSEC had similar "proof" requirements ... heh... decades ago now. eg A1
systems.
http://en.wikipedia.org/wiki/Trusted_Computer_System_Evaluation_Criteria

As with any formal approval don't assume it covers everything a stock
system would. eg NT4's C2 cert meant you had to rip out networking;
posix layer etc etc etc etc.

Or the one I hit & debugged about 2-3 years ago; where email with a
wrong format message ID in the headers would get bounced by the
"approved" gateway firewall - "NO! Of course you can't disable that
option! Else it'd be running different to the approved spec!!!".
Yet sending multiple forged emails with identical message ID's would
pass happily. Which was the "threat" they were trying to stop.

Yay for brainless security where performing a deliberate Denial of
Service is more important then having business emails pass thru.


So yeah, fascinating, but....


Cheers!
- Steve


On Wed, 2009-08-19 at 10:11 +1000, 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.
> 
> "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