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

[Daniel Pittman]

steve jenkin <sjenkin at canb.auug.org.au> writes:

> Is this a "milestone event" or just some cute Academic result?

The later, probably.

> They've formally specified and 'proved' their ARM kernel (L4).
> It's intended for embedded devices. Possibly security, telecomms, ...

Ben Laurie is not so impressed[1]: http://www.links.org/?p=689

    Ian Brown asked “do you think a formally verified microkernel that
    enforces security controls within an OS is achievable/desirable?”

    I think this actually might be achievable, and perhaps even desirable. But
    I’m not so sure it would be truly useful. A microkernel architecture
    inherently punts on all the interesting security questions and simply
    enforces whatever incorrect decisions you have made outside the
    kernel. So, you are still left with all the real-world security problems,
    but at least you have a place to stand when you claim you are enforcing
    whatever security properties you think your code implements (that is, you
    can discount the microkernel as a source of problems and only have to
    worry about the other 99% of the code).

I am quite inclined to agree with him: L4 is about the most minimal kernel
possible, and doesn't include a lot of the features that actually, y'know, do
anything much.

So, like Ben I think this isn't a bad thing, and it means that you could use
that L4 microkernel implementation safe in the knowledge that you can trust it
to do everything it says it will do.[2]


Then you just have to worry about all the OS components you built on top of
L4, and the support software on top of those, and the applications on top of
those, and ...

        Daniel

Now, imagine trying to formally or informally prove a port of Erlang that ran
on L4, so you could apply the same trust to that part of your application
stack...

Footnotes: 
[1]  I can't identify if this is specifically the L4 result, or the principal
     and a case of coincidental timing.  I /think/ the later.

[2]  ...which is not to say that it will protect you from anything.  It could,
     for example, be formally proved to be absolutely insecure in the
     situation you wanted to use it in.  Hypothetically.  ;)

-- 
✣ Daniel Pittman            ✉ daniel at rimspace.net            ☎ +61 401 155 707
               ♽ made with 100 percent post-consumer electrons
   Looking for work?  Love Perl?  In Melbourne, Australia?  We are hiring.