Re: A broken brand?

On Thu, 2008-03-13 at 12:35 -0700, David Wagner wrote:
> Toby Murray writes:
> >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? 
> [...]
> >I am uncomfortable, however, that the definition of "correct behaviour"
> >here seems rather fuzzy.
> 
> Nope.  I can't give you a careful, complete specification of the desired
> behavior of a brand.  But I would say that the behavior exposed in my
> attack seems unexpected and undesirable.  My intuition is that you should
> only be able to get at the contents of a sealed box if you have both the
> box and the unsealer, and my attack violates that intuition.

This is indeed the intuition that I think we all share. However, suppose
I have an object that is a proxy for the box. The brand implementation
can unseal the proxy just fine. My intuition is that this does not
violate the intuition that I "have both the box and the unsealer".

How might we state this formally? In particular, what does it mean to
"have the box"? Clearly it is not just that one has permission to the
box (i.e. a direct capability to it), since in the case of holding a
proxy for the box, one has authority to invoke the box, but not
permission.

Hence, we might say that one "has the box" if one has authority to cause
the box to be invoked. But this is too broad if your attack is to be
considered a violation of the brand's intended behaviour. In your
attack, the attacker has authority to cause the box to be invoked (since
he can invoke the go() method which causes the unsealer to invoke the
box.)

Hence, "having the box" here is neither "having permission to the
box" (too narrow) nor "having authority to invoke the box" (too broad,
since it makes your attack a valid behaviour).


>   Can I make
> this intuition precise?  Can I provide a full specification of a brand?
> Nope.  The intuition is indeed fuzzy.  But (in my opinion) I think this
> intuition is enough to conclude that my attack is a successful violation
> of the security goals of a brand, even if I can't specify all of those
> security goals carefully and even if I cannot fully specify the desired
> behavior for a brand.

The problem here is that we have two situations that we cannot really
distinguish. One of them is considered valid (holding the unsealer and a
proxy to the box) and the other is considered invalid (holding the
unsealer and a reference to an object that, when invoked, can cause the
box to be invoked). We have no way to state what the fundamental
difference between these two cases is, since the first is an instance of
the second. Yet we consider one valid and the other invalid.

More precisely, we consider some instances of the second case invalid.
But the instances that correspond to the first case are valid. But what
distinguishes those valid instances (like holding the unsealer and a
proxy to the box) from the invalid ones (like as in your attack)?

Your comparison with crypto protocols is useful here in order to
highlight the undesirability of this situation. Crypto protocols are
hard to get right. But at least with cryptographic protocols, it is
possible to state the properties that a protocol is to enforce and to
determine reliably when an attack is valid (i.e. violates one of the
properties the protocol is meant to enforce).

Our goal should be to bring similar precision to the design of
fundamental object-cap abstractions. If we cannot precisely state what
an abstraction is supposed to be achieving, how on earth can we
determine when an implementation is valid? 

(I expect you agree with what I'm saying here; I'm just trying to make
the argument explicit. Hopefully I'm not ranting too much ;)


>   Such a spec sure would be nice to have, though.

I fear that without one, object-cap engineering cannot be taken
seriously. My understanding is that work in crypto protocols really
blossomed once formal statements of their security properties were able
to be written and their (abstract) implementations verified against
these properties (under standard e.g. Dolev-Yao assumptions about the
abilities of an attacker). It would be nice to be able to do likewise to
object-cap patterns.