Re: Contracts and communication channels in Shill [was Re: Shill: capability-based shell]

You might also be interested in another paper we wrote on using contracts
to control the flow of capabilities between components:
http://www.thinkmoore.net/csf14_capability_control.pdf

We look at how contracts can track and enforce restrictions on which
components have passed a component around. In some ways it is similar to
the Horton design pattern, but with a fixed interaction pattern and blame
assignment strategy.

On Friday, October 10, 2014, Scott Moore <[email protected]> wrote:

> Since Shill doesn't have channels, I'll rewrite this example as:
>
> foo(myfun, bar, buz) {
>   myfun(bar);
> }
>
> I'm going to specialize bar and buz to be directory capabilities to
> simplify the example.
> We'd like to prevent passing buz to myfun. You can do this by giving foo a
> *dependent* contract (I don't
> think we describe them in the paper):
>
> provide { foo : { myfun <- bar : { arg : and/c(dir?,fun (x) not(x == bar))
> } -> any },
>                   bar : dir?
>                   baz : dir? } -> any };
>
> This contract says that the first argument's contract depends on the "bar"
> argument, and in particular that
> the argument to myfun may not be the bar capability. Note that the
> contract also needs to say that the argument
> isn't a closure, otherwise I could close over bar to subvert the check.
>
> If foo has a weaker contract for the myfun argument, I can provide my own
> wrapper around myfun that either does this check,
> or just wraps it in the same contract.
>
> On Fri, Oct 10, 2014 at 2:17 PM, Anton Burtsev <[email protected]
> <https://urldefense.proofpoint.com/v2/url?u=http-3A__mailto-3Aaburtsev-40flux.utah.edu&d=AAMFaQ&c=WO-RGvefibhHBZq3fL85hQ&r=OO-QDw1vay4FMTJT3laIe8WvRDtiOvj1Sucsxf9k8cc&m=rfhaCQQ-OPqoyp_iPbE4-2u-CVdFvYiYhypbNPUOqaQ&s=IeW8UBuKoz0HaBI0vX4SieFAFN9zAXiLDOIy7e9e0lk&e=>
> > wrote:
>
>> I've meant something along the lines of
>>
>>   foo(channel c, capability bar, capability buz) {
>>
>>       c->send(bar);
>>   }
>>
>> In this code I would like to make sure that foo() doesn't send the "buz"
>> capability over the channel c. I guess, I can somehow express this with a
>> a contract.
>>
>> Anton
>>
>> On Fri, Oct 10, 2014 at 12:26:35PM -0400, Scott Moore wrote:
>> > I'm not sure if I addressed your question. Could you elaborate on the
>> kind
>> > of communication pattern you mean?
>>
>
>

_______________________________________________
cap-talk mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/cap-talk