[cap-talk] "A Contribution to Techniques for Building Dependable Software Systems"
kosik at fiit.stuba.sk
Sat Aug 13 03:35:43 PDT 2011
Thank you for reading and asking.
On 08/12/2011 11:28 PM, lists at notatla.org.uk wrote:
>> Interesting paper:
>> A Contribution to Techniques for Building Dependable Software Systems
>> by Matej Kosic and Jiri Safarik
> I'm sure I've missed understanding some details.
> Does the whole of this small OS compile to a single program?
((More precisely, the kernel has a form of a single ELF executable that conforms "multiboot specification".))
> If not I don't see how compile-time type checking is done on
> the capability interfaces between client and server components.
> For instance as in Section VI if the callback capability
> given by a client to a server (supposed to be used for upward
> responses) is actually a regular capability not allowing
> donating-send then at what point is it detected
It is automatically detected by the typechecker.
> and what happens?
The direct result is that the kernel is not compilable and triggers a need for audit.
(beyond examinging capabilities required by untrusted subsystems)
> The dc2 and p tarfiles contain a link to a file not provided:
> lrwxrwxrwx common.bib -> /home/kosik/doc/latex/common/common.bib
You are right. It is fixed now. The published archive
now includes an actual copy of that file.
Disclaimer: the whole thing is very incomplete so I do not try to actively hype it. I am trying to raise some money now. Then I need a holiday and then I will try to fix the most pressing issues (the P compiler generates shamefully verbose code, to start with. I have faith, but currently no energy.).
More information about the cap-talk