[cap-talk] What sustained interest in capabilities

[Toby Murray]

On Sun, 2009-01-11 at 20:49 -0800, Mark Miller wrote:
> On Sun, Jan 11, 2009 at 12:46 AM, ross mcginnis
> <ross_mcginnis at hotmail.com> wrote:
> >
> > Are there actually any top-to-bottom projects out there?
> > By that I mean a single project that claims it is going to integrate or produce everything from a kernel all the way to a user's desktop environment based on caps with at least all the lower system level being verified.
> 
> I'm curious why you're tying the top-to-bottom security question to
> verification. AFAIK, Coyotos is the only low level ocap system that
> has verification as an explicit goal.

seL4 [1] is also a "low level ocap system that has verification as an
explicit goal". Jonathan Shapiro has described seL4 as a "tour de force"
of verification [2]. To my knowledge, at the current time, it represents
the most formally verified and specified ocap system that has ever been
developed.

[1] seL4 is a project of NICTA to built a secure (ocap) microkernel. 
http://ertos.nicta.com.au/research/sel4/

It has close links with L4.verified, which is the NICTA project to
formally verify it. 
http://ertos.nicta.com.au/research/l4.verified/

The kernel API is described here
http://ertos.nicta.com.au/research/sel4/api.pml

Most accessible of the verification work, perhaps, is the high-level
isolation proof
http://ertos.nicta.com.au/publications/papers/Elkaduwe_GE_08.pdf


[2] http://www.bitc-lang.org/docs/bitc/bitc-origins.html