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

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