[cap-talk] Backwater: some small progress

[Mark S. Miller]

Matej Kosik wrote:
> Hi,
> 
> There is a lot of work to be done, but I have made small progress with my
> Backwater project.
> [...]
> That gave me the possibility to add (very simple versions of) device drivers for
> - the keyboard (8741/8742 chips)
> - the timer (8253/54 chips)
> E.g. the Timer driver is given the authority to
> - reset the observer of IRQ 0 to any channel
> - write to the I/O port 43
> - write to the I/O port 40
> Nothing more. That is enough authority for it.
> 
> http://altair.dcs.elf.stuba.sk:60001/mediawiki/upload/0/01/Iitsrc2007-poster.pdf

HI Matej, I hadn't realized before that you've been working on getting all 
this running on the bare metal. That's very interesting! The other projects I 
know about to try to use language-based security as a replacement for OS 
security are SPIN (based on Modula-3) and Singularity (Based on .NET). Your 
approach looks it could produce a much more minimal TCB than theirs. Aided 
further by Pict's very clean semantics, perhaps this could result in higher 
confidence.

On <http://wiki.erights.org/wiki/Object-capability_languages> I have changed
[https://altair.dcs.elf.stuba.sk/~kosik/tmp58/Harmless.pdf Harmless Pi]
to
[http://altair.dcs.elf.stuba.sk:60001/mediawiki/index.php/Backwater Backwater]

Is this right? Does Backwater replace Harmless Pi?


> I like the idea that applications (in my case untrusted modules) should
> declare the authority they need in order to be able to what is expected from
> them. I would like to evaluate SCOLL, whether it can be used for these
> purposes, if it can bring something that is not obvious.


I know that Fred, in his search for a good formalism for reasoning about 
authority, spent some time examining Pi Calculus before deciding to base SCOLL 
on take-grant systems. Also, Toby Murray's 
<http://web.comlab.ox.ac.uk/oucl/work/toby.murray/analysing_authority.pdf> 
uses another process algebra, CSP, to reason about authority. (I have easily 
understood Occam and Orc, and I have briefly understood Pict, but I don't 
understand CSP. I'm not sure why some simple process algebras seem so much 
easier to understand than others.)


> I am far from that
> now yet, because the two problems I mentioned in my previous mail
> - I need to modify the Pict runtime in a way that untrusted modules
>   will not be able to consume arbitrary amount of free heap of memory
> - I need to modify the Pict runtime so that untrusted modules
>   will not be able to consume arbirary "CPU bandwidth"
> These problems are immediate.

They are also hard for language-based systems to address. It is especially 
hard to address at object granularity (or, for Pict, process granularity). The 
knobs needed are just too much to express at fine grain within program logic. 
Perhaps you could make do if you had a very well thought out defaulting 
strategy for the knob settings.

An alternative is to explicitly bring in some larger-grain vat-like unit of 
aggregation as unit of resource budgeting and preemptive eviction. This is the 
approach we'd always planned to take with Joule and E. Java is now planning 
something like this for their "isolates" proposal. (But their resource 
allocation API looks to me to be too complex.)

I do not yet understand Backwater well enough to give advice specific to it.

-- 
Text by me above is hereby placed in the public domain

     Cheers,
     --MarkM