[cap-talk] Backwater: some small progress

[Matej Kosik]

Mark S. Miller wrote:
> 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 Mark

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

If I add mechanisms for constraining untrusted modules in time and space such comparison will be perhaps fair. The Pict runtime most probably gets more complicated. That is not a good news but it seems to me essential.

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

Yes. Roughly. Backwater is an unfinished kernel. As such it is composed from many programs. The `Harmless' I have mentioned earlier was only a tamed version of (part of) the standard Pict library. Now it is part of Backwater under a different name (public trusted modules).

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

What bothers me on Backwater is that not a science. It is an art or engineering. There are many useful statements that are obviously true, for example "the ClockMorph has the authority to change 8 characters on the screen whose coordinates are: (7,5), (8,5), (9,5), ... , (14,5). If someone were able to prove that, that would be a science. I know that it is true but I cannot prove it. I do not need the proof in this case very much (the truth is so "obvious") but it may be handy if I wanted to persuade others about my opinion.

I view Occam as Pict as programming languages and CSP, pi-calculus and other formalisms as a possibility to do proofs. I would like to learn such capabilities. There are people who are better in this area than me.

> 
> 
>> 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 agree with you about introducing coarser grains. Although they go against "united view" (everything is a process) but they are unavoidlable.

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

I have to learn all details of Pict runtime and compiler and then I will hopefully be able to come up with proper modification of Pict.
-- 
Matej Kosik

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
Url : http://www.eros-os.org/pipermail/cap-talk/attachments/20070430/cfa52912/attachment.bin