[cap-talk] Capability propagation - e.g. Horton (was: Comparing identity-based and capability-based designs)

Mark S. Miller erights at google.com
Wed Nov 23 10:14:51 PST 2011

On Wed, Nov 23, 2011 at 7:27 AM, Thomas Leonard <talex5 at gmail.com> wrote:


> OK, I tried this. It did spot one slightly-interesting case: if b and
> c collaborate, then
> b may be able to get a direct reference to c if c can throw one back
> in an exception.
> (SAM assumes that every object has a direct reference to itself, which
> is true in Java and in E)

Hi Thomas, this is a very encouraging result. Horton is one of the more
complex ocap patterns I've tried to code. I'm glad you assume that objects
always have a reference to themselves. It is not a necessary part of the
ocap model, but I have never seen much utility in being able to deny an
object a reference to itself. Besides E and Joe-E, SES (Secure EcmaScript)
objects should also be assumed to have a reference to themselves.

Regarding the thrown exception, E and Joe-E both enforce that anything
thrown must be transitively immutable (DeepFrozen and Immutable,
respectively). So your addition to the TCB here violated E semantics.
Nevertheless, your result is very relevant. SES does not, since SES-on-ES5
cannot enforce this. I will keep this in mind when I recode Horton in SES.

Kevin's implementation of CapTP in E is probably the ocap program with the
most complex and subtle security properties[1]. It's security is critical,
and due to its complexity, I can't say we currently have high confidence
we've gotten in right. Do you think SAM might be able to model it?

[1] Consider my CapTP-on-Java as just a prototype, since it uses Java
serialization rather than CapTP.

> For example, this modified form of the Horton example shows b invoking
> c.bye() without the call being logged:
> def makeUnknownAnnotationValueException :=
> <unsafe:javax.lang.model.element.makeUnknownAnnotationValueException>
> def c {
>    to hi(_) {
>        throw(makeUnknownAnnotationValueException(null, c))
>    }
>    to bye() {
>        println("bye")
>    }
> }
> def b {
>    to foo(c) {
>        try {
>            c.hi(c)
>        } catch ex {
>            def realC := ex.leaf().getArgument()
>            realC.bye()
>        }
>    }
> }
> prints
> ...
> Carol said:
> > Bob asks me to:
> > > hi/1
> bye
> The example isn't very convincing though, because I had to import
> UnknownAnnotationValueException using <unsafe> (which is not available
> to unconfined code in E).
> --
> Dr Thomas Leonard        http://0install.net/
> GPG: 9242 9807 C985 3C07 44A6  8B9A AE07 8280 59A5 3CC1
> GPG: DA98 25AE CAD0 8975 7CDA  BD8E 0713 3F96 CA74 D8BA
> _______________________________________________
> cap-talk mailing list
> cap-talk at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/cap-talk

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.eros-os.org/pipermail/cap-talk/attachments/20111123/d1c0e815/attachment.html 

More information about the cap-talk mailing list