OK, I basically agree with what you say here.

On Sat, Jul 5, 2014 at 2:48 PM, Jonathan S. Shapiro <[email protected]> wrote:
> If you think about it, I think you'll conclude that ambient authority (which
> is what you call "undeniable authority") is the logical extreme of rights
> amplification gone amok.

Yeah, I see that. If you add axioms carelessly, you get a
contradiction, and then you're screwed. And it's not at all easy to
tell if a set of axioms is consistent in general. I didn't want to
strain the analogy though.

> The second one is much easier to describe. In PL terminology we might call
> it "de-encapsulating operations". These are operations that penetrate an
> explicitly represented abstraction boundary. An interface is an explicitly
> represented abstraction boundary.

Yes, in BitC.

> Where we use interfaces to implement
> security-enforcing encapsulations, I think it's fairly clear that we want to
> take great care about how those might get de-encapsulated.

Yes, that much is clear.

> Obviously, I'm dragging an idea from capability systems into the PL world
> here in a slightly different way than has been done previously. I'm probably
> not capturing all of this right, and we're going to have to learn (a) do we
> even need this, (b) is this the right place to embed this idea, and (c) if
> so, what are the idioms we want to teach and talk about. I don't yet feel
> that I have answers to those questions.

(a) Need the guarded open, assuming the rest of the BitC interface
semantics? I don't know.
When would there be an open or large set of amplified interfaces to
de-encapsulate into?

(b)
If you mean "Are wrapper-like interfaces the right way to provide
rights amplification?", well I'm not sure it's the best way to do it,
but it's a reasonable way to do it, and I don't have a fully worked
out alternative that's demonstrably better.

I was happy with Java/Joe-E's peer access for rights amplification. It
can easily implement seal/unseal. I think you can go the other way
too, by using a separate brand for each scope that uses peer access.
Peer access has no runtime overhead that I'm aware of.

(c) Based on the similarity to seal/unseal, couldn't you adapt use
cases from E's seal/unseal?

>> It sounds like you're still thinking of downcast as rights
>> amplification. That's pretty frustrating. Has nothing changed...?
>
> Downcast gives you more operations to perform. Therefore it is rights
> amplifying. This is purely a matter of definition. It's not an ideology
> debate.

Well then I think it's the wrong definition :)
It's misleading in the case of Java casts.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to