[cap-talk] "A Contribution to Techniques for Building Dependable Software Systems"

[Matej Kosik]

Hello,

Thank you for reading and asking.

On 08/12/2011 11:28 PM, lists at notatla.org.uk wrote:
> 
>> Interesting paper:
>> http://www2.fiit.stuba.sk/~kosik/doc/ecbs-eerc-2011.pdf
>> 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?

Yes.
((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
http://www2.fiit.stuba.sk/~kosik/tar.gz/dc2.tar.gz
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.).