Re: A broken brand?

[Toby Murray-4]

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
_______________________________________________
e-lang mailing list
e-lang@...
http://www.eros-os.org/mailman/listinfo/e-lang

[Toby Murray-4]

2009/8/20 Toby Murray <toby.murray@...>:

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

Actually, more simply, that should be:

"An object that does not possess both u and a proxy to b, or b itself,
cannot have c returned to it by u."

This is nicer because it requires fewer assumptions about the other
objects in the system in order to test (e.g. that they won't pass an
object c etc.).

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

Boxes are also not proxies by definition.

This new property is equivalent to the old with respect to David's
original attack scenario.

Sorry for the confusion

Toby
_______________________________________________
e-lang mailing list
e-lang@...
http://www.eros-os.org/mailman/listinfo/e-lang

[Dave Chizmadia - Gmail]

Toby,

    Trying to have more testable and unambiguous statements of
requirement...

> Actually, more simply, that should be:
>
> "An object that does not possess both u and a proxy to b, or b
> itself, cannot have c returned to it by u."

    This is a constraint on u and should be stated that way...

    "u shall return the c iff an invoking object o satisfies the
    following preconditions:
    a) o invokes u using a valid capability, and
    b) the message from o invoking u provides a valid capability
       to either b or a proxy to b"

>
> This is nicer because it requires fewer assumptions about the other
> objects in the system in order to test (e.g. that they won't pass an
> object c etc.).
>
> > 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.
>
> Boxes are also not proxies by definition.

    I think that the "if:" in the definition for "proxy" should be
an "iff:", since in all cases that I can think of both conditions
must be satisfied.

    Happy modeling,

-DMC

_______________________________________________
e-lang mailing list
e-lang@...
http://www.eros-os.org/mailman/listinfo/e-lang

[Toby Murray-4]

2009/8/20 Dave Chizmadia - Gmail <davechiz@...>:

> Toby,
>
>    Trying to have more testable and unambiguous statements of
> requirement...
>
>> Actually, more simply, that should be:
>>
>> "An object that does not possess both u and a proxy to b, or b
>> itself, cannot have c returned to it by u."
>
>    This is a constraint on u and should be stated that way...
>
>    "u shall return the c iff an invoking object o satisfies the
>    following preconditions:
>    a) o invokes u using a valid capability, and
>    b) the message from o invoking u provides a valid capability
>       to either b or a proxy to b"

Exactly. Or, even stronger:
 "u shall return c in response to an invocation by an object o iff:
   a. o has passed a valid capability 'd' that is either b or, when
invoked by u, proxies to b.

where "d proxies to b" iff when invoked, d invokes b or d invokes an
object that proxies to b.

This condition has the disadvantage that it requires some knowledge of
how this pattern works. However, it doesn't require us to determine
wich objects may proxy to b a-priori since this is captured now in the
property being tested.

Thanks for you comments.

Toby
_______________________________________________
e-lang mailing list
e-lang@...
http://www.eros-os.org/mailman/listinfo/e-lang