[cap-talk] Authority vs. Information Flow

[Toby Murray]

On Thu, 2008-02-14 at 00:41 -0800, David Wagner wrote:
> Toby Murray writes:
> >Example 2: In which Authority exists, but perhaps not Info Flow
> >---------------------------------------------------------------
> >

> (I assume you mean that _Dave_'s behavior is fully specified, and
> that Alice and Dave will both race to push the button and surely at
> least one of them will succeed in pushing the button.  I assume that's
> a typo above.)

Yes. Sorry for the confusion.

> 
> I'll assume that Bob cannot using timing channels (or anything
> case) to distinguish the case where both Alice and Dave try to push
> the button from the case where only Dave tries to push the button.
> 
> In that case, where Dave's behavior is fully specified, I'm not convinced
> that Alice has authority to turn the light on.  MarkM's thesis defines
> authority as causation through overt channels.  If I understand the
> standard scientific notion of causation, we imagine two experiments:
> 
>   Experiment 1: Everything is as you specified above.
> 
>   Experiment 2: Same as Experiment 1, except that Alice's behavior
>   is modified so that she does not try to push the button.
> 
> Notice that the definition of Experiment 1 and 2 are identical except
> for Alice's behavior.
> 
> Now, Bob cannot distinguish between Experiment 1 vs Experiment 2.
> Therefore Alice's push of the button does not cause Bob to see the
> light, because Bob sees the light whether Alice pushes it or not.
> Consequently it seems to me that Alice does not have authority to
> cause Bob to see the light.

I think that this is too coarse grained. In my work so far, I consider
single traces of execution rather than entire behaviour of the system.
Now, Alice has authority to cause Bob to see the light turn on iff:

1. There is a sequence of events in which Alice acts and Bob sees the
light turn on (i.e. the sequence ends with the evnt "Bob sees the light
turn on" and contains some event(s) that Alice performed.)

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

2. When we remove Alice's actions from that sequence of events, "Bob
sees the light turn on" does not directly follow. (i.e. without Alice
acting -- but with NO other changes to the sequence -- Bob can't see the
light turn on).

              s \ AliceEvents ^ <bobSeesLight> \nin traces(System)

( s \ X is the sequence s with all events from the set X removed )

I think it is dangerous to argue that Alice has no authority to cause
Bob to see the light turn on here. Consider an analogous example framed
in more familiar object-cap terms:

Two vats hosting two objects,  Alice and Dave. Both Alice and Dave have
a (remote) reference (capability) to the object Light that has a method
"poke()". 

Each of Alice or Dave can do

light <- poke()

and they will race to do so.

Light in turn has a capability to Bob that allows it to call Bob's
"observeLight()" method. Light looks like this:

def light {
   to poke() :any {
      bob.observeLight()
   }
}


Alice and Dave's capabilities are really to a proxy that forwards the
invocation to Light, but once it has forwarded a single invocation, it
refuses to forward any more. e.g.

var keepForwarding := true
def target := light
def forwardOnce {
   match [verb, args] :any {
      if (keepForwarding){
         E.call(target, verb, args)
         keepForwarding := false
      }
   }
}

Alice and Dave really have a remote reference to "forwardOnce(light)"

This basically captures the scenario I described earlier. Alice and Dave
can each invoke Light which will in turn invoke Bob's "observeLight()"
method. 

Surely, you would agree that both of the Alice and Dave objects have the
authority to invoke Bob's "observeLight()" method? 


> 
> This notion of causation is one where Dave's behavior is presumed
> to be known and fixed, and the only question is how Alice chooses
> to behave.  I'm inclined to think that is probably the right notion.
> What do you think? 

I agree. In my definition of causation, this manifests itself in that
the only change we make to the trace s is to remove Alice's actions. All
other actions stay as they were.

>  (Of course, there could be some other configuration
> or some other definition of Dave under which Alice _did_ have authority
> to cause Bob to see a light, but that'd be a different question.)
> 
> I realize I didn't answer your question of whether this counts as
> information flow (and my answer to that would also be "No"), but by
> denying the premise, hopefully I have resolved the paradox.  Do you
> buy it?

Unfortunately not. I can see how by your definition of causation, Alice
has no authority. But I see this definition as being too strong.

> Caveat: I haven't thought carefully about causation or authority,
> so it's possible that I may have stepped into some pitfall.  What
> I'm writing might well be total nonsense.
> _______________________________________________
> cap-talk mailing list
> cap-talk at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/cap-talk