Re: A broken brand?

On Mon, 2008-03-03 at 02:30 -0800, Mark Miller wrote:
> On Sat, Mar 1, 2008 at 11:38 PM, David Wagner <[email protected]> wrote:
> > I've been reading the Caja spec.  It includes an example of a brand
> >  implemented in Caja, using an implementation technique attributed to
> >  Marc Stiegler.  I think I may have found an attack on it, and I was
> >  curious whether this was well-known. 
> >
> >  Does this attack look correct to you?
> 
> Yes.

I'd like to throw in an aside:

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. But on to the main point of this email...

> 
> 
> > Is it well-known?
> 
> It is not. 
>
> I'd be curious if Fred's SCOLL system or Toby's CSP-based authority
> analysis frameworks would have been able to catch this.

Not sure about SCOLL. But regarding whether one could detect this
vulnerability using a CSP model of the code:

It's funny this should come up now since I've recently been looking at
modelling the MarcS brand in CSP to analyse its security properties.

No, I didn't find this attack. The reason is basically that CSP is not
well suited to modelling systems in which objects may invoke each other
recursively. CSP is best suited to modelling systems in which each
object has its own thread of control, with synchronous invocation
between objects. In order to try to model a single-threaded system like
an E vat, one needs to model the call-stack for the thread. As the
maximum size of the call-stack grows, so does the state-space of the
model.

Furthermore, when expressing the behaviour of the unsealer, it hadn't
occurred to me to account for the possibility that, while waiting for
the invocation of the given box to complete, the unsealer might be
recursively invoked.  Hence, my model didn't allow for the behaviour
that gives rise to this attack.

This gives some good insight into how one should go about trying to
express models of these sorts of systems in CSP. However, in most cases,
the model will continue to grow as one increases the maximum size for
the call-stack. Being able to say "no attacks for max call stack of N"
isn't nearly as nice as being able to say "no attacks for call stack of
any N" would be much nicer, but I fear that this may be out of reach of
the current approach I'm taking.


> Altogether, between this and your attack on the Cajita Mint, it's
> clear we need better tools for this kind of programming to become
> adequately robust. (Not that there's any known better alternative.)
> Between auditors, SCOLL, and Toby's work, I figured we were advancing
> towards having such tools. Now I'm not so sure.

Nor am I. But I'm glad, therefore, that David has so aptly shown the
limitations of these current approaches. It has certainly given me some
food for thought about the practical effectiveness of my work here to
date. ;)