[cap-talk] Authority vs. Information Flow

[Toby Murray]

On Sat, 2008-02-16 at 16:14 -0800, David Wagner wrote:
> Toby Murray writes:
> >It's worked pretty well so far. 
> >
> >In general, we can't know for sure whether *any* definition is
> >definitely appropriate.
> 
> I guess where I'm going is that if I simply refuse to accept this as
> the proper definition, the "paradox" evaporates.  Right now, that looks
> like the easier way out. :-)
> 
> The following work on causality might be of interest:
> 
> http://singapore.cs.ucla.edu/LECTURE/lecture_sec1.htm
> http://singapore.cs.ucla.edu/IJCAI99/index.html
> 
> The "firing squad" and "light switch" examples in the second talk
> seem closely relevant here.

I think I've read about those myself somewhere. When I did so,  I
remember thinking then that my intuitions disagreed with the authors'.
(I'm beginning to see a pattern here ;)

> 
> >Moreover, I can test for it in a CSP model checker,
> >which is very handy indeed.
> 
> Well, okay, but we do have to be careful of the "I'm looking for my
> keys under the lamppost because that's where the light is, not where
> I dropped them" effect.  I know this isn't the reason you chose that
> definition but I want to highlight that I don't find this a good reason
> to choose one definition over another.

Indeed. One must be careful to avoid choosing a definition because it is
convenient to apply. I agree totally.

> 
> >Yes, but this same system is also likely to have the traces:
> >
> >(Alice tries to press the button, the light turns on, Bob sees the light
> >turn on)
> 
> This is not a possible trace, since you stipulated that Dave's
> behavior is fixed and immutable and he will always try to press
> the button.

Yes. But we don't know *when* Dave will try to press the button. (This
comes back to the "level of abstraction" comment  I made earlier.) If
Alice gets in there first and all of these actions occur before Dave
tries to press the button, then I see this as a totally valid  trace.

I've been avoiding use of CSP in this thread so far because I thought it
would be helpful, but I see now that it may have made things more
difficult. The actual semantics in question that i've been trying to
describe are captured by the following process:

P = a -> b -> STOP [] d -> b -> STOP

Both "a" and "d" can initially occur. Neither Alice nor Dave will refuse
to perform their respective events. However, whoever gets in there first
locks out the other. (c.f. the E example in which the forwarder only
forwards one message.)

The CSP Traces denotational semantics states that the traces of P are

<>     -- empty trace
<a>
<d>
<a,b>
<d,b>

(Traces are prefix-closed. So if s is a trace of P, then all prefixes of
s are also traces of P. This is why we have not only <a,b> and <d,b> but
also all of their prefixes, incdluing the empty sequence.)

A more loose interpretation of the same scenario is this different
process:

P = (a -> b -> STOP ||| d -> b -> STOP)

The |||  operator is "interleaving" -- i.e. the two halves of P run in
parallel with no synchronisation between them so their events are
interleaved.  

Now the Traces  of P include those from before 

<>
<a>
<d>
<a,b>
<d,b>

but they also include all interleavings of the above. However, this
makes no difference because we still have that

e.g. <a,b> is a trace but <b> is not. (i.e. by performing a, Alice can
cause b to occur.)


> >> >I think it is dangerous to argue that Alice has no authority to cause
> >> >Bob to see the light turn on here.
> >
> >> I guess I don't see the danger yet.  Can you spell it out?  What
> >> harmful consequence might this have?
> >
> >Underestimating the authority of an untrusted subject is surely
> >dangerous. 
> 
> But suppose my contention is that I have not underestimated the
> authority of Alice; on the contrary, I have estimated it exactly
> accurately.  I'm suggesting we should take this one step further:
> what's the harmful consequence?  If you gave an example where my
> kind of reasoning led me to overlook a security vulnerability or
> make a decision we can all agree was poor, then I'd be concerned.
> So far, though, I don't see any negative consequences either way;
> it's just a disagreement over how we should use the word "authority".

I'll give you one. Let's take the prototypical confused deputy example.
Carol is a compiler, Alice is her user and Bill is her billing file.

The system is modelled by this process:

P = Alice.Carol.Execute?arg:{Alice,Bill,Carol} -> Carol.arg.Write ->
Carol.Bill.Append -> STOP

Events are of the form: o1.o2.oper.arg and represent object o1 invoking
object o2 with the message "oper" possibly passing the argument arg.

Initially Alice "Execute"s Carol, passing any argument from the set
{Alice,Bill,Carol}, indicating which object she wants the compilation
output written to. This gets bound to the free variable "arg". Carol
then "Write"s to this "arg", before "Appending" to Bill.

I say that, in-line with the understanding that Carol is a confused
deputy, that Alice has the authority to cause Carol to write to Bill. My
definition of causation detects this, (So does yours, I think), since

<Alice.Carol.Execute.Bill, Carol.Bill.Write> is a trace of the system
but
<Carol.Bill.Write> is not.

Now suppose we add another object to the system, e.g. Dave, that is in
an identical position to Alice. Now the system looks like:

P = Alice.Carol.Execute?arg:{Alice,Bill,Carol} -> Carol.arg.Write ->
Carol.Bill.Append -> STOP
     []
    Dave.Carol.Execute?arg:{Alice,Bill,Carol} -> Carol.arg.Write ->
Carol.Bill.Append -> STOP

Since they are in identical positions, Dave and Alice should have
identical authority. Hence, both Dave and Alice have the authority to
cause Carol to overwite Bill. (This is almost regardless of your
definition of causation, since we know they *ought* to have this
authority because Carol is a confused deputy.)

Hence, I argue that a good definition of causation should be able to
detect that both have the authority to cause Carol to overwrite Bill.

By my definition they do. By yours, neither has the authority to cause
Carol to overwrite Bill. This seems at odds with our (shared, I hope
this time) intuitions regarding the confused deputy scenario.


> 
> >This is the interesting thing about causation. Two people can have
> >wildly different intuitions. (This is also why agreeing on a definition
> >for it will be tricky ;)
> 
> Yes. :-)
> 
> >Even if Dave's behaviour isn't fixed. I'd still argue that Alice has
> >authority to invoke the light.
> 
> I'm arguing:
> 
>  * If Dave's behavior is fixed, Alice doesn't seem to have the authority.
>  * If Dave's behavior isn't fixed, Alice does have the authority
>    (or, if Dave's behavior is unknown, we must conservatively assume
>    that Alice may have the authority).
> 
> So it sounds like we agree on the second claim, and are disagreeing
> only on the first.
> 
> >I'd also like it to agree with people's intuitions.
> >
> >However, as this discussion has shown, people's intuitions  don't agree
> >with each other's anyway, so this last goal seems elusive indeed.
> >
> >The people on this list are perhaps the most qualified that I know of to
> >give their intuitions on authority; particularly in capability systems.
> >I was hoping that there would be a consensus one way or the other here,
> >but we still have some way to go to a shared definition of authority.
> 
> Yes, a good goal indeed.  It's always possible our intuitions are wrong
> and that we will need to revise our intuitions.  It's nice to preserve
> intuitions where ever possible but occasionally a careful analysis shows
> that our intuitions must be discarded -- so while we should strive to
> respect our intuitions, they aren't inviolable.
> 
> I'm glad that you are probing these issues carefully, because the notion
> of "authority" is a slippery one that has not (to my knowledge) been
> pinned down carefully but rather has been left to intuition.

My hope is to be able to formalise it (at least within the constraints
of a particular kind of model (in my case, CSP), in  order that we might
learn more about it than our intuitions can tell us.