[clug] New from UNSW, formally specified and verified ARM kernel.
alexsatrapa at mac.com
Tue Aug 18 22:19:42 MDT 2009
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.
... 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 ...
* 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...
Size: 220 bytes
Desc: This is a digitally signed message part
More information about the linux