Re: A broken brand?

On Thu, Mar 13, 2008 at 2:56 PM, Toby Murray
<[email protected]> wrote:
>  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.

One one hand, I don't believe that Fred's SCOLL system can reason
about this code, and distinguish the correct from the incorrect
implementations, because SCOLL doesn't understand about stacks. But I
do believe a SCOLL-like system could provide the means to specify the
desired behavior with sufficient precision that it would forbid the
attack. (Good specifications forbid. Good implementations prevent the
forbidden.) The real test of any such specification language is
whether a specification written in ignorance of the attack would have
been written tightly enough to forbid the attack.

When thinking about (my broken adaptation of) MarcS' sealer/unsealer
pattern and David's attack in the context of SCOLL, the issue that
jumped out at me is the need to specify the authority provided by the
innocent wrapper that's wrapping the box. It is this innocent wrapper
that David is abusing. If this innocent wrapper intended to provide
its clients the authority to obtain the box contents (given the
unsealer), then David would indeed simply be utilizing authority he
was intentionally given. However, the innocent wrapper's specification
should be that it doesn't provide (to a client possessing the
unsealer) the authority to obtain the box contents.

This implies that the specification of the sealer/unsealer system
should include that a relied-upon wrapper can be written that will
obtain and utilize the box contents itself in a limited manner, but
will not provide its unrelied-upon caller the authority to obtain the
box contents. Even with SCOLL, I admit that it's unlikely that a
specification written in ignorance of this attack would think to
specify this.

It seems this issue is a great simple concrete example just beyond the
bleeding edge of our ability to reason about authority. Research
opportunity!

-- 
Text by me above is hereby placed in the public domain

 Cheers,
 --MarkM