[e-lang] A broken brand?

[Toby Murray]

Hi all,

In March last year, David Wagner presented two attacks on
implementations of object-capability patterns that involved recursive
invocation of an object.

One of these [1] was against a sealer-unsealer implementation and
involved calling an unsealer with a purported box to unseal, which
I'll call 'Opener'. The unsealer would then call Opener, at which
point Opener would recursively call the unsealer passing a valid box
as argument.

The unsealer implementation in question is based on coercion, meaning
that it should successfully unseal a proxy to a box. Hence, I argued
that it is difficult to see exactly how this attack differs from the
situation in which an unsealer is rightly called with a proxy to a
box. The relevant part of this exchange follows.

I wrote:
> On Thu, 2008-03-13 at 12:04 -0700, David Wagner wrote:
> > Toby Murray writes:
> > >In the attack, the unsealer is being passed an object that has the
> > >authority to cause the box to divulge its contents. Hence, one might
> > >argue that the unsealer is being passed an object that is analogous to a
> > >proxy for the box and, hence, the attack might be viewed as valid
> > >behaviour in some cases.
> >
> > I'd say: This is an accurate description of the actual behavior of this
> > sealer/unsealer implementation, but it's not the desired or intended or
> > specified behavior for a sealer/unsealer.  If Viktor is relying upon
> > this Brand to behave like a brand ought to, then his security goals
> > can be violated.
>
> Could you expand on "like a brand ought to". Better yet, can we agree on
> a (formal) definition of the intended behaviour of a brand?

To which David and I agreed that a formal statement of the intended
property here was difficult to give.

I've been working on model-checking this pattern recently and think
I've made some progress towards a formal statement of the security
property of this pattern.

In a system in which this pattern is instantiated, producing an
unsealer 'u' and box 'b' whose contents is 'c':
1. an object that cannot acquire a proxy to b nor b itself, and cannot
acquire c from any object other than u should not be able to acquire
c.
2. an object that cannot acquire a proxy to u nor u itself, and cannot
acquire c from any object other than u should not be able to acquire
c.

We define an object p to be a "proxy to object o", if: p is not an
unsealer and p can call o in response to an invocation, or p can call
a proxy to o in response to an invocation.

David's attack scenario violates property 1. In his attack, the object
'Opener' is not a proxy for the box since while it calls the unsealer
which calls box, unsealer is not a proxy to box by definition.

I think this is getting close to a formal statement of the security
properties of this pattern. I'd be interested to get people's
thoughts.

Cheers

Toby

[1] http://www.eros-os.org/pipermail/e-lang/2008-March/012508.html