[cap-talk] Authority vs. Information Flow

[David Wagner]

Toby Murray writes:
>David Wagner writes:
>> 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.

Then I think you need to add a notion of time to your model.
The model is already a bit sketchy without it, and I think you've
just found a place where it is needed.  Either that, or you've
found a problem with your "delete from the trace" model of causality.

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

I don't think this situation is analogous to "Will Bob see the
light?"  The reason is that the caller of Carol gets to control
the contents of what Carol writes into the file.  Therefore, the
situation where Dave writes and then Alice writes is not equivalent
to the situation where Dave writes and Alice does not.  Therefore,
if we model this accurately, I think my definition would say that
Alice *does* have authority in this situation, even though she
does *not* have the authority in the "Will Bob see the light turn
on?" example.

Also I think to fully model this situation you may need a notion
of time, and then you might find that Alice does have authority
because she can control the timing at which the change to the file
is visible to others.

However if you set up this situation so that it is exactly identical
to the "Will Bob see the light turn on example?" then I think we'll
indeed conclude that Alice has no authority.  For instance, suppose
we know that the contents of the output file is not visible to anyone
until time T (no matter when it is written), suppose we know that
Dave will always call Carol.Execute(Bill) before time T, suppose
that the caller of Carol cannot control what is written to the file,
suppose the file keeps no record of when or how many times it is
written, and suppose that Alice's access to Bill is revoked at or
before time T.  In that kind of crazy situation, I think we could
indeed (under my definition) conclude that Alice does not have authority
to modify the contents of the file -- and I think that conclusion
would be safe.