[cap-talk] Is "Authority" Subjective?

[David Wagner]

Toby Murray writes:
> Suppose we have a system represented as the following CSP process:
>
> P = a1 -> a2 -> b -> STOP [] 
>     b -> STOP
>
> Now suppose that actions a1 and a2 are performed by some object Alice
> and b is performed by another object Bob. Does Alice have authority to
> cause Bob to perform b?
[...]
> All traces of the system represent possible behaviours. If there is some
> trace s after which one of Alice's events can follow, i.e. for some
> event e in Alice's alphabet s^<e> is a trace of the system, then Alice
> has the choice to perform e after s.

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

I presume you mean that if for some events e1, .., en in Alice's alphabet
such that s, s^<e1>, ..., s^<en> are all traces of the system, then
at the point just after trace s occurs, Alice has n+1 options she can
choose among: do nothing, perform e1, .., or perform en.  Yes?

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

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?

For instance, one possible instantiation of Alice (that is
consistent with your process P) would be:
  Aimpl10:
    When given the chance to perform a1, do so
    When given the chance to perform a2, refrain
It looks to me like there are 4 possible instantiations of Alice that
appear to be consistent with P, assuming we restrict our attention to
deterministic strategies.

How many possible instantiations are there of Bob?  I think I can
see between two and four (again, restricting attention to
deterministic strategies):
  Bimpl00: Never perform b.
  Bimpl11: Always perform b, whenever given the chance to do so.
  Bimpl10: If in the initial state of the process and given the
     chance to perform b, do so; but if in the 2nd state of the
     top line of the P, do not take the opportunity to perform b.
  Bimpl01: Don't perform b in the initial state of P, but do
     perform b if in the 2nd state of the top line of P.
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.

Am I understanding your setup correctly?  Have I got all that right
so far?

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

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?

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

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.

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

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

Do you agree with these so far?

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

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?

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