[cap-talk] Authority vs. Information Flow

[Toby Murray]

On Sat, 2008-02-16 at 13:12 -0800, David Wagner wrote:
> Toby Murray writes:
> Alice has authority to cause Bob to see the light turn on iff:
> >
> >
> >   \exists s . s ^ <bobSeesLight> \in traces(System)
> >
> >( ^ is contatenation, <x> is the sequence of events containing the
> >single event x, traces(System) is the (prefix-closed) set containing all
> >sequences of events that System can perform )
> > [and]
> >
> >              s \ AliceEvents ^ <bobSeesLight> \nin traces(System)
> >
> >( s \ X is the sequence s with all events from the set X removed )
> 
> How do we know whether this is the appropriate definition of causality?
> Perhaps the apparent paradox arises because the definition you are using
> isn't a great one, rather than due to any inherent contradiction.

It's worked pretty well so far. 

In general, we can't know for sure whether *any* definition is
definitely appropriate. Some definitions will work better with some
models, however. All we can do is to try to find a definition that
matches a certain sort of model well that doesn't have any known
counter-examples. In fact, since we want to err on the side of caution,
we want the *weakest* definition of causation that doesn't have any
"obvious" counter-examples (i.e. counter-examples that everyone can
agree are instances of causation that this property doesn't detect).

The sorts of models I've been using are CSP processes. This definition
has worked well so far for this kind of model. However, more examples
are required in order to increase my confidence in it.

There may yet be a better definition out there. But this one seems
pretty good so far. Moreover, I can test for it in a CSP model checker,
which is very handy indeed.

> 
> This definition of causality seems somewhat fragile, because the result
> of the analysis will depend heavily upon how you define the set of events.

Indeed. The level of abstraction at which you choose to model your
system will affect this as well.

> Suppose the trace is
> 
>    (Alice tries to press the button, Dave tries to press the button,
>     the light turns on, Bob sees the light turn on)
> 
> Then when we delete Alice's action (the first event), Bob still sees
> the light turn on.  If this was how we modelled the system, we'd
> conclude Alice did not cause Bob to see the light go on.

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)

and

(Dave tries to press the button, the light turns on, Bob sees the light
turn on)

When we remove Alice's events from the first, we see that
(the light turns on, Bob sees the light turn on) is not a valid trace of
the system. Hence, we can conclude that Alice can cause the light to
turn on.

Symmetrically for Dave with the second trace.

> 
> It also seems odd to remove only Alice's actions.  What if some
> subsequent part of the trace depended upon the presence or absence of
> Alice's actions?  Seems like you may need to fix up the rest of the
> trace as well.

If some subsequent part of the trace depended on Alice's actions, then
Alice (probably) caused that part of the trace. If the final action in
the trace depended on those other actions, then (transitively) Alice
caused the final event. Since Alice caused the intermediate events,
removing Alice's events means that these intermediate events can't
happen initially. Hence the sequence with Alice's events removed won't
be a valid trace. 

This is another reason the definition is good. It's transitive -- i.e.
if a causes b and b subsequently causes c, then (by this definition) a
will cause c, which is what you expect.

> 


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

> 
> >Surely, you would agree that both of the Alice and Dave objects have the
> >authority to invoke Bob's "observeLight()" method? 
> 
> Why?  What's wrong with saying that, if the behavior of Dave truly
> is known and immutable and fixed, then (subject to that constraint)
> Alice does not have authority to invoke observeLight()?  It seems like
> a viable position to take.  Does that create some kind of absurdity?  

No. I guess I mean that it doesn't fit with my intuitions is all.

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 ;)

> I'd say that that your observeLight() example is not representative of
> how we usually reason about systems, because it assumes that we know
> somehow that Dave's behavior is fixed and immutable.

Even if Dave's behaviour isn't fixed. I'd still argue that Alice has
authority to invoke the light. So long as

(Alice presses button, light turns on, Bob sees light)

is a trace of the system but

(light turns on, Bob sees light)

is not, then I say Alice has authority to cause Bob to see the light
turn on. Dave's behaviour is irrelevant in this case.

>   In practice we will
> often review the code of Alice in isolation, without looking at the code
> of Dave.  In that case we will conclude conservatively that Alice might
> have authority to invoke observeLight().  (When looking at only part of
> the system, it's typical that we can only make conservative upper bounds
> on the authority that particular components might have.  We might often
> say "Alice has authority to invoke observeLight()" but that is really
> shorthand for "Alice might have authority to invoke observeLight(),
> so we'd better be prepared for the possibility that she does".)

Indeed. That's why I want a definition of caustion that, if anything,
will overestimate a subject's authority but never underestimate it.

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.