[cap-talk] Is "Authority" Subjective?

[Toby Murray]

On Sun, 2007-06-24 at 12:13 -0700, David Wagner wrote:

> I'm not persuaded.  Let me elaborate and maybe you can lay my concerns
> to rest.

> I still want to distinguish between "Alice", the name of an actor, and
> the instantiation of Alice (you can think of the latter as the code of
> Alice or the strategy that Alice will follow or the implementation of
> Alice; the crucial requirement is that it fully determines the behavior
> of Alice in response to events).  Think of an instantiation as a strategy,
> and before execution begins, Alice has to choose a strategy which she is
> then stuck with through execution.  Alice's "choices" are then all made
> up front, before execution is began, and thereafter execution proceeds
> according to the system's rules (and Alice's free will is restricted
> to her choice of a strategy).

Exactly. I agree completely.

All of these up-front choices of Alice (or whoever writes her code) are
represented by nondeterminism.

I said before that our predicates hold for all refinements of the
system. This means that however one chooses to resolve the
nondeterminism in the system, the predicates continue to hold.

For example, suppose we have the system

P = a -> b -> STOP |~| b -> STOP

where |~| represents a nondeterministic choice.

Now here one might rightly say that a doesn't cause b to occur, because
b is possible at the same point a is possible. However a real
implementation of this system might choose to resolve the nondeterminism
to the left, i.e. P might be implemented by a system equivalent to
Q = a -> b -> STOP.
Now in Q one would say that a can cause b to occur. Hence, we need a
predicate for P that detects that P has a refinement in which a causes b
to occur. 
The details are in the paper, but this is essentially what we've done.

> 
> I suspect the CSP process P above is intended to represent all possible
> traces that can arise from all possible instantiations of Alice and all
> possible instantiations of Bob and all possible message interleavings /
> all possible schedulings of Alice and Bob.  Is that right?

Yes, but normally one doesn't construct P by hand. I've perhaps been a
bit misleading by presenting P directly.

Usually (as is done in the paper) one builds processes to represent each
of Alice, Bob etc. and then composes these in parallel to produce the
whole system.

Any nondeterminism in each of the processes for Alice and Bob represent
different implementation strategies for Alice and Bob respectively --
what you refer to as the "up front choices" above.

<snip different strategies for Alice and  Bob>

> Does your framework allow Bimpl10 or Bimpl01 as an permissible
> strategy/behavior for Bob?  In any case, I am assuming that at least
> Bimpl00 and Bimpl11 are two possible instantiations of Bob.

Generally, no. Bob can't detect when Alice's events have occurred,
except by trying to perform b and see whether it is refused (in which
case he could infer that a1 has occurred but a2 has not yet occurred.)


The original process P, however, was built by hand. In order to come up
with separate processes whose parallel composition produces P we need to
extend the scenario a bit further.

Suppose we have three subjects, Alice, Bob and  Carol. Alice and Bob
will both try to invoke Carol and either may get in before the other.
Once invoked by one of them, the other has to wait until the first
invocation finishes. Bob invoking  Carol is always the final action of
the system.

the original events are renamed as:
a1 -> aliceInvokesCarol, a2 -> carolRespondsToAlice, b ->
bobInvokesCarol

then we can define each of our processes for Alice, Bob and Carol as
follows:

ALICE = aliceInvokesCarol -> carolRespondsToAlice -> STOP
BOB = bobInvokesCarol -> STOP
CAROL = aliceInvokesCarol -> carolRespondsToAlice -> CAROL  []
        bobInvokesCarol -> STOP


and we can combine them in parallel to form the entire system

SYSTEM = (ALICE ||| BOB)
[|{aliceInvokesCarol,carolRespondsToAlice,bobInvokesCarol}|] CAROL

The entire system has Alice and Bob interleaved, since they do not
communicate with each other. Then the interleaving of Alice and Bob is
put in parallel with Carol, where all events much be synchronised upon.

SYSTEM is semantically equivalent to the original P with the events
renamed.


> If yes, my concern with this framework is that the non-determinism
> in the CSP process P conflates several different kinds of choices or
> several different sources of non-determinism:
>   1) The choices that Alice has: i.e., the different actions that
>      Alice might take, depending upon how she is instantiated.
>   2) Any non-determinism inherent in Alice's instantiation, if you
>      allow Alice's strategy to itself be non-deterministic.
>   3) The choices that Bob has: i.e., the different actions that
>      Bob might take, depending upon how he is instantiated.
>   4) Any non-determinism inherent in Bob's instantiation, if you
>      allow Bob's strategy to itself be non-deterministic.
>   5) Non-determinism due to scheduling or message interleaving.

Yes that's correct, I believe.

> When I see a non-deterministic choice in the process P, it looks
> difficult to me to infer which of those 5 sources it might have
> come from.
> 
> Moreover, the framework combines all allowable instantiations of
> Alice with all allowable instantiations of Bob.  When we want to
> think about whether Alice has authority over Bob, we want to hold
> Bob's instantiation fixed, and vary how Alice is instantiated.

We want to check that for all instantiations of Alice and all
instantiations of Bob, does Alice have authority over Bob? Otherwise, a
real implementation of the system we're modelling might implement Bob in
such a way that Alice does have authority over him. If we hold Bob fixed
in our analysis then we can't be sure that his real implementation won't
behave differently to our fixed one.

I think our system does not suffer form what you describe. We produce a
check in the paper that can be carried out with a model checker to test
whether Alice has authority over Bob. The way the test works is to run
two copies of our system P. In the left-hand copy, we allow Alice's
events to be performed. In the right-hand copy, we prevent ALice's
events from being  performed. If the system can evolve such that the
left-hand can perform some Bob event but the right hand cannot, then we
conclude that the presence of ALice's events causes Bob's event to
occur.

However, both the left and right-hand copies are forced to perform the
same non-Alice events, so other than Alice's strategy, they both evolve
identically. Hence, if causation is detected, it has occurred when all
other objects in the system have been held constant, while the only one
that has varied is Alice. I think, therefore, that our automated test is
a direct embodiment of the strategy you've described.

> In other words, we want to vary Alice's behavior (this is the
> counterfactual part of the reasoning) and see how this affects
> things, but we want to hold the code that implements Bob fixed so
> that it doesn't confound our analysis.  How do we do that within a
> process P that includes behaviors due to all possible instantiations
> of Bob?

In our test, Bob's (and everyone else's) behaviours are the same between
both of the copies of P. The model checker explores all possibilities of
their choices however but when doing so, for each possibility, both
sides of the test must execute the same strategy modulo the occurence of
Alice's events in the left-hand copy.

> Perhaps I have missed some key part of your analysis.  I have to
> admit I didn't understand the reference to 'refinement'; perhaps that
> addresses these concerns somehow?

I hope I've clarified it a bit better.

> 
> If we follow my line of analysis, here are the conclusions I think
> we come to:

> 1. If Bob is instantiated by Bimpl00, then Alice has no authority
> over Bob -- or, more concisely, Alice has no authority over Bimpl00.
> (Reason: No matter what Alice does, Bimpl00's behavior is the same.)
> 
Yes. In either case Bob's behaviour is do nothing.

> 2. If Bob is instantiated by Bimpl11, then Alice may have some
> authority over Bimpl11, depending upon our notion of "equivalence".
> 
>   Example: If our notion of equivalence is "the set of possible behaviors
>   of Bob is identical", then Alice has some authority over Bimpl11.  Reason:
>   If Alice is instantiated by Aimpl0x, which always refrains from
>   performing a1, then Bimpl11's possible behaviors all involve performing b.
>   If Alice is instantiated by Aimpl10, then Bimpl11's possible behaviors
>   include the possibility of performing nothing (in case the scheduler
>   allows Alice to go first, in which case Aimpl10 deadlocks the system)
>   as well as the possibility of performing b (in case the scheduler
>   allows Bob to go first).  These two sets of possible behaviors are
>   not equivalent, at least under most notions of equivalence I can
>   think of.  The intuition is that Alice is able to prevent Bob from
>   reliably performing action b, and if Bob was relying upon his ability
>   to definitely perform b, then he is out of luck.
> 
>   Example: Suppose our notion of equivalence says that the set S1 of
>   behaviors is equivalent to the set S2 of behaviors if and if pre(S1)
>   = pre(S2), where pre(S) = {r : r is a prefix of s and s in S}.
>   (This notion of equivalence might be appropriate if we only care
>   about safety properties, i.e., if we don't care about the ability of
>   one party to mount denial-of-service attacks on the system, say by
>   deadlocking it.)  Then Alice does not have authority over Bimpl11.

This is precicely the equivalence used in CSP's /traces/ denotational
semantic model. Where behaviours are represented by a set of sequences
of events ( a trace set ) and all trace sets are prefix-closed.

This is the approach we take in the paper and is indeed only good for
detecting when one event causes another to occur. It can't be used to
tell when one event causes another to not occur.

Except usually when measuring Alice's effects on Bob, we consider only
the traces of Bob in the system and see whether they are different for
different strategies of Alice.  i.e. whether Alice's strategy modulates
Bob's behaviour, here represented by traces.

With Aimpl0x Bob's behaviours are {<>,<b>}. With Aimpl10, Bob's
behaviours are {<>,<b>}. So there is no difference. Hence, I'd argue the
opposite: Alice has no authority over Bob here when traces equivalence
is used.

However, if we use a stronger equivalence, then we can reason that Alice
can cause Bob to /not/ perform b. (This seems to be the difference in
Bob's behaviour you're picking up on.) Hence she has authority over Bob.
But in the original example, I was considering only whether Alice should
be considered to be able to cause Bob to perform b. Hence, to answer my
own question via your analysis,  I'd say she doesn't have authority over
Bob, for this definition of authority -- i.e. events causing other
events to occur, but not events causing other events to not occur.

> 3. If Bob is instantiated by Bimpl01, then Alice has authority over
> Bimpl01.  (Reason: With Aimpl0x, Bimpl01 never performs b.  With
> Aimpl11, Bimpl always performs b.)

Bimpl01 is  not a valid strategy, as said above.

> 
> 4. If Bob is instantiated by Bimpl10, then Alice may have authority
> over Bimpl10, depending upon our notion of "equivalence".  (Reason:
> This is basically the same as Bimpl11.)

Again, Bimpl10 is not a valid strategy.

> 
> Do you agree with these so far?

That seems fair, with the comments I've made above. So when a traces
equivalence is used, Alice has no authority over Bob -- i.e. she can't
cause Bob to perform b, is what I conclude both from your analysis and
from my own described in the paper. Do you agree?

> If this sounds right so far, then one has to think about what it means
> to say "Alice has authority over Bob".  I suspect this comes down to
> how we choose to use language.  I can imagine two language usages that
> might both make sense:
> 
> Usage #1: If we have a specific system implementation in front of us,
> and if in that system Bob is instantiated by BimplX, and if Alice has
> authority over BimplX, then we might say "in this system, Alice has
> authority over Bob."  If Alice doesn't have authority over BimplX, then
> we might say "in this system, Alice has no authority over Bob."
> 
> Usage #2: If we are trying to perform a local analysis of Alice
> (where we are looking only at the code of Alice but not the code of
> everyone else in the system), and if we determine that there exists
> a permissible instantiation Bimpl of Bob such that Alice has authority
> over Bimpl, then we might conservatively say "Alice has (may have)
> authority over Bob".  If there is no permissible instantiation of
> Bob that Alice has authority over, then we say "Alice has no authority
> over Bob".  (By permissible, I mean that we only consider instantiations
> that are consistent with the rules of the game as enforced by the
> underlying security monitor.  For instance, if we are analyzing E
> programs, we restrict attention to instantiations of Bob that can be
> expressed as legal E code, which implies that all instantiations must
> follow object capability rules.)
> 
We can do both in our model. In approach #1 we define a Bob's behaviour
in accordance with Bob's real behaviour in the real system. In the
second approach we define Bob's behaviour to be the most
nondeterministic permissible by the rules of the game. Since our test
checks for all refinements of Bob's behaviour, it will determine whether
for any implementation  of Bob (that plays by the rules) does Alice have
authority over that implementation. Hence, it will tell us could Alice
possibly have authority over Bob.

> The choice between Usage #1 and Usage #2 may be one that has to be made
> based on personal taste or pragmatic utility rather than because there
> is One Right Answer, and in some cases it may be more important to just
> agree on which usage we are using rather than argue over which is the
> best usage of language.
> 
> Does this sound right to you?

Yes. I can also imagine other definitions based on the different sort of
equivalence used in the testing. With a traces equivalence, we have
ALice has no authority over Bob if she can't cause him to perform any
action.

With a stronger equivalence, we have
Alice has no authority over Bob if she can't cuase him to, or not to,
perform any action b.

This is precisely the difference between different sorts of equivalence
used in the Non-Deducability on Compositions (NDC) information flow
tests. With Traces-NDC, we can only determine whether High can cause Low
to perform events it would not otherwise have performed. With say
Failures-NDC, which is stronger, we can also determine whether High can
cause Low not to perform any event it would otherwise have.

When our causation properties are strengthened to consider the
non-occurrence of events, it turns out a lack of authority is equivalent
to a lack of information flow as defined by the refinement-closure of
FNDC. When we consider only the occurrence of events, a lack of
authority is equivalent to the refinement-closure of TNDC.

> 
> I apologize that I haven't read your paper yet; I put it on my stack
> some time ago but my stack of papers to read keeps getting longer...

I know the feeling ;)

I hope I've clarified things a bit further and that you'll respond if
anything above seems dubious.

Cheers again,

this discussion has forced me to clarify my thoughts on this work a bit
and has been, therefore, really helpful.

Toby