Are you thinking of types as capabilities or object references as
capabilities? If object references, then casting should not be thought
of as affecting the authority provided by a reference. If types are
capabilities, then you have a very static system for access control
and yeah, downcasting is dangerous. But you're proposing some weird
cross breed where a token object reference makes it OK to use
something at a different type. Why do you need that? If you want to
use object references for authority, then an abstract type is not a
means to attenuate authority; for that you use a wrapper. At least
this is what I thought I learned about object-capability security. Is
the problem that the wrapper might be too much overhead?

On Tue, Jul 1, 2014 at 12:33 PM, Jonathan S. Shapiro <[email protected]> wrote:
> I've been really negative about checked downcast in my mind, without quite
> putting my finger on why. It finally occurred to me that downcast is an
> operation that amplifies rights. Assuming the check passes, you get back an
> object that has a bigger API (therefore more authority) than the original.
> If you look at that from the capabilities perspective, that raises some real
> concerns.
>
> The seal/unseal pattern suggests a possible resolution. What I'm about to
> describe definitely needs to be refined,  but I want to get a first
> reaction.
>
> We're looking at an expression "X as Y". The question is: under what
> conditions can this be performed? Two sensible answers are:
>
> 1. Whenever X is a subtype of Y, because the operation is strictly reducing
> authority.
> 2. Whenever X implements a method "as() -> Y"
>
> Now the second one is kind of interesting, because it seems like the right
> place to implement the unseal pattern. Suppose we replace it with:
>
> 2. Whenever X implements a method "as(guard: T) -> Y"
>
> and make the requirement be that the caller must present proof of authority
> to unseal in the form of an value of type T.
>
> If T is some global type (e.g. bool or unit), then anybody can fabricate a
> guard value, and the "as" operator can then be called by anyone. But if T is
> an opaque type it cannot be instantiated by anyone, and we can think about
> programs in which the possession of a suitable guard value serves as proof
> of authority.
>
> And incidentally, a dependent type system makes this more powerful than it
> looks, because T can be a dependent type that is conditioned on a particular
> instance of an interface...
>
>
> Jonathan
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to