[cap-talk] Is "Authority" Subjective?

[Toby Murray]

On Sun, 2007-06-24 at 09:39 -0700, David Wagner wrote:
> 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?
> 
> I'm not convinced this provides a suitable framework for thinking
> about authority.
> 
> Reasoning about authority requires reasoning about counterfactuals.  
> More specifically, it requires reasoning about what would have happened
> had Alice made a different choice.  For instance, we ask: What happens
> if we Alice chooses to perform action X?  What happens if Alice chooses
> not to perform action X?

David, this is precisely what we have done in CSP. If you're
interested, see the paper: "Authority Analysis for Least Privilege
Environments"
http://web.comlab.ox.ac.uk/oucl/work/toby.murray/papers/AALPE.pdf

> If we can identify some action X, such that (a) if Alice chooses to
> perform X, then Y inevitably ensues, and (b) if Alice chooses not to
> perform X, then Y cannot follow, then I think at that point we might
> be in a position to declare that Alice has authority to cause or not
> cause Y.  This requires reasoning about both a real-life Alice that
> will choose to perform X and an imaginary counterfactual Alice' that
> will refuse to perform X.

You're using a definition of causation equivalent to that proposed by
Lewis in his 1970 paper, "Causation".  We use precisely this definition
to characterise causation in the CSP semantics of a system.

> 
> However, it looks to me like your framework does not provide any way
> to reason about Alice's "choices" or what freedom Alice does and does
> not have.  Your framework does not provide the ability to reason about
> counterfactual imaginary Alices, or to characterize the scope of what
> Alice can and cannot choose to do. 

On the contrary (unless we mean different things) it does.
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.

>  Alice's actions are constrained by the
> underlying system and by what the security monitor will allow her to do,
> but as long as she plays "within the rules of the game", our framework had
> better account for the fact that Alice can choose among many strategies
> for playing this game.  But that doesn't show up in your framework.

Of course it does show up. See the example in Section 5 of the paper
where we model confused deputy. Each of those processes have many
"choices" which they can make. Of course the choices are constrained by
the access control model and policy under consideration, but what good
would our model be if it couldn't account for all possible choices that
can be made by each actor?

We also account for all possible ways in which a given system, described
in CSP, might actually be implemented in practice. This is done by
ensuring that our causation properties continue to hold for
all /refinements/ of a system. (See the paper.)

I'm pretty sure that, despite a few similar comments from this list, our
framework is expressive enough -- the example and work in the paper
demonstrate this, as far as I can see. I would urge you to read the
paper and if you still have concerns, I'd love to discuss them.


> 
> I wonder if the non-determinism in CSP might be confusing things.
> Thinking about causality -- even coming up with a satisfactory definition
> of causality -- is harder when non-determinism is floating around, and
> it's harder to get a good intuition on this.

Absolutely. Nondeterminism makes things harder -- but we deal with this
OK. The trick is to ensure that you're predicates continue to hold under
refinement.

> 
> It looks to me like you're trying to use the non-determinism in CSP
> as a way to model the actors' choices, but I have doubts about whether
> it is the right approach to that.

Nondeterminism is used to model different implementation possibilities
for a particular model. 

>   At the heart of the matter is *who*
> chooses which of the many non-deterministic paths will be followed.
> When we reach a non-deterministic choice point, who should we think of
> as choosing which transition to take?  I suspect that in your intuition
> you are tempted to think "Alice chooses whether to take the a1 transition
> or not", but that isn't supportable by CSP, because CSP doesn't allow
> you to make distinctions about who is choosing which transition to take.

> I think in CSP we have to think about this as though the Environment
> is making these choices, and the Environment is a fourth actor who
> you haven't accounted for.
> 
Normally. But the way we construct our models (eg in the paper) external
(deterministic) choices represent choices to be made by actors, rather
than the environment. Actors may resolve these choices and the choices
represent the different decisions they may make in practice. 

> If you ask me, I would suggest starting from a different framework.
> Let me sketch one that might support the kind of investigation I think
> you are interested in taking.  Suppose the actors are Actors={A,B,C,...}.
> Treat A as the name of an actor, not as the specification of a process
> itself.  Introduce a map I : Actors -> Processes, where Processes might
> be the set of CSP processes or the set of all finite-state automata
> or you name it (the framework will need to choose one).  I(A) is A's
> implementation.  Also, model the security restrictions imposed by the
> underlying system as a set of admissible values of I.  The admissibility
> constraints determine which "moves" are allowable by "the rules of the
> game", and I(A) models A's strategy.  (For instance, in an ACL system, the
> admissibility constraints ought to model that I(A) cannot access resource
> R unless A appears in R's ACL; in a capability system, the admissibility
> constraints should require that I(A) can only invoke a capability C if
> I(A) received C from some other process or if I(A) created C.)
> 
> Then you need to introduce some way to model communication between
> the actors.  For instance, you might specify: there are n^2 communication
> channels, one for every pair (A,B) of actors; each channel is a queue of
> elements from some alphabet \Sigma; I(A) can append an element to the
> end of any channel ch(A,.), and I(B) can pop an element from the front
> of any channel ch(.,B), but not vice versa; and channels are in-order
> and reliable.
> 

> Now we can use the semantics of the process and communication model
> to assign a semantics to each choice of I.  In other words, the map I
> determines the behavior (or possible behaviors) of the composed system.
> 

This is very close to (if not exactly) what we've done already. Perhaps
I should have provided more details.


> We need a notion of "equivalence" of behaviors; write I ~_B I* if
> the behavior(s) of B in the system I is "equivalent" to the behavior(s)
> of B in the system I*.  For instance, we might consider them
> "equivalent" if the set of possible traces of B in I is equal to
> the set of possible traces of B in I*, or we might consider them
> "equivalent" if there is a bisimulation between the B-part of I
> and the B-part of I*.  The choice of our notion of "equivalence"
> is another paremater of this family of frameworks; the framework
> will need to choose one.  The key part is that equivalence only looks
> at the behavior(s) of B, and ignores the behaviors of all other
> components of the system.
> 
> Suppose we want to determine whether A has any authority over B.
> In what follows, let I,I* denote two admissible maps that differ
> only at A: i.e., I(X)=I*(X) for all X!=A (but possibly I(A)!=I*(A)).
> Say that A has no authority over B if for all I,I*, we have
> I ~_B I*.  Say that A has some authority over B if there exists
> I,I* such that I ~_B I* does not hold.  (Note that in the latter case
> A's authority might be partial, such as the case where A's influence
> over B is subject to C's approval.  Also we will be heavily reliant
> upon choosing a good notion of "equivalence".)

This sounds a hell of a lot like the various information flow properties
defined for CSP and associated process algebras.

In some (as yet unpublished work) I've been able to extend the work in
AALPE and show that an extended definition of non-caussation corresponds
to some well known information flow properties. Hence, a lack of
authority corresponds  to a lack of info flow.

This gives me great confidence that we are indeed on the right track and
have probably taken a route very close to that you describe above.

> 
> I have a gut feeling this kind of definition might more or less coincide
> with our intuition about what we mean by authority, though that hypothesis
> remains to be explored.  What do you think?

I think I agree. I think I'm  already there in terms of the work that's
been done.

> 
> One aspect of authority this definition doesn't encompass is secrecy.
> It doesn't allow us to formalize statements like "A has authority to
> learn the secret key K"; it only allows us to formalize statements about
> side effects.

Indeed. It can tell us whether A has no authority to pass information
(ie. affect) B, but it doesn't directly tell us whether B has authority
to be affected by A -- one has to make that inference by implication
from A's lack of authoirty over B.

> 
> This definition does have the benefit of being objective, so if we agree
> that this comes close to matching what we intuitively mean by authority,
> then maybe that helps answer your question about whether authority is
> objective or subjective.

Absolutely. 

Cheers for all of the insights. I hope we can continue this a bit
further.