[cap-talk] Authority vs. Information Flow
toby.murray at comlab.ox.ac.uk
Mon Feb 18 04:34:10 EST 2008
On Sun, 2008-02-17 at 17:50 -0800, David Wagner wrote:
> Toby Murray writes:
> >But the CSP process I gave didn't model *what* was written to the file.
> >Hence, it cannot make these sorts of distinctions.
> Well, I'd call that a flaw of the model. I'd suggest that if we get
> misleading conclusions about whether Alice has the authority, maybe
> it's because of flaws in the model, not because of problems with my
> notion of authority. If we correct the flaw in the model, then I think
> my notion of authority does not generate misleading conclusions about
> Alice's authority.
But that's (part of) my point. I don't believe that the conclusions my
test are drawing are misleading. I firmly believe that both Alice and
Dave have authority to turn on the light.
(More on this below.)
> I think I see where the apparent paradox is coming from. It
> looks like neither Alice nor Dave has the authority to cause the
> light to turn on, yet turn on it does.
> But I'd frame it another way. I think that authority depends upon
> where we draw the boundary around what part of the system we're
> analyzing and what is left unanalyzed -- i.e., what part of the system
> we consider fixed and what part we consider "free to change".
> There are four cases:
> (i) Dave if fixed and Alice can be changed. (i.e., we've examined
> the code of Dave but not the code of Alice)
> (ii) Alice is fixed and Dave can be changed. (i.e., we've examined
> the code of Alice but not Dave)
> (iii) Neither Alice nor Dave is fixed. (i.e., we haven't looked
> at the code of either of them)
> (iv) Both Alice and Dave's behavior is fixed. (i.e., we've
> examined both of their code)
> In case (iv), I'm not sure it makes sense to even talk about
> authority. What will happen, will happen; there is no room for
> any other alternative.
Ahh. I don't understand this at all. I think this must be the root of
where we diverge.
(When Carol is invoked, she invokes Bob who invokes Alice.)
We've analysed the code for all three entities. We know this is what
will happen. Yet I argue that Carol can cause Alice to be invoked.
Apparently you would disagree, no?
Could you explain why that is the case. To me, reasoning that Carol can
cause Alice to be invoked is the most natural thing in the world.
Notions of what is fixed etc. do not come into it.
In terms of my own work, when modelling code that is fixed (i.e. we
assume how it will behave) we tend to model it as a deterministic
process. e.g. the above would be modelled as
P = c -> b -> a -> STOP
which is deterministic.
Note that both of our definitions of authority (when applied to the
model P) would agree that c causes a.
I don't see how it makes sense to say "trusted (i.e. code about which we
know how it will behave) code has no authority". I don't understand at
> In case (iii), both Alice and Dave have authority to turn on the
> It's cases (i) and (ii) where it gets tricky. In case (i), I'd
> say Alice doesn't seem to have the authority, since no matter what
> she does, the light will be turned on either way. In case (ii),
> I'd say Dave doesn't seem to have the authority, since no matter what
> he does, the light will be turned on either way.
> This illustrates that, if you accept my notion of authority, then
> the amount of authority depends upon what parts of the system we
> consider fixed and what we don't. Is that too weird to be useful?
Could you explain how you reached the conclusions in each of the four
cases. That might help me to understand.
> Am I thinking about this in the wrong way? I don't know. That's
> why it would be nice to have a good definition of authority that we
> can all agree upon. It's hard to see what that would look like, though.
That's precisely the same question I wanted to find out when I started
this thread ;)
More information about the cap-talk