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

[Alex Satrapa]

On 19/08/2009, at 11:15 , Daniel Pittman wrote:

> 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]

... and nothing that it doesn't say it will do.

That's the important part of the spec & proof. Once you read the spec,  
you know exactly how it's supposed to behave, the proof is the logic  
that says yes, the implemented system exactly conforms to the spec.

ie: no nasal demons*.

> 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 ...

Baby steps.


Alex

* right up until you ask "what happens when cosmic rays or Dr  
Manhattan happen to our computer hardware?"
-------------- next part --------------
A non-text attachment was scrubbed...
Name: PGP.sig
Type: application/pgp-signature
Size: 220 bytes
Desc: This is a digitally signed message part
URL: <http://lists.samba.org/pipermail/linux/attachments/20090819/c80224a0/attachment.pgp>