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

I have put some notes about TCB size.
http://altair.dcs.elf.stuba.sk:60001/mediawiki/upload/2/2b/Backwater.pdf
to Section 1.7.

(237 lines of Pict code in untrusted modules + some main kernel module
 719 lines of C code of the whole Pict runtime
 some OSKit code for initializing the processor and hooking up the IRQs
)

Such numbers arised after reorganization I recently made. Some primitives were rewritten in Pict. All the primitives are now concentrated in four untrusted modules. The rest of the system (modulo the main kernel module that is also trusted) is considered untrusted.

This is present state and some changes are anticipated. For example if I succeed to to implement some mechanisms for enforcing some policy with respect to how much memory and how much CPU can various untrusted components use, the size of the runtime will grow up. But that is necessary.

When it will have sense, I will try to make similar tests as Singularity people with respect to efficiency of message delivery. I do not think they can beat Pict.

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


-- 
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/20070512/3da0bf35/attachment.bin