[cap-talk] Analyzing Authority with CSP - link broken (was: Backwater: some small progress)

[Toby Murray]

Indeed. Sorry about that.
I was going to wait until we heard back from the FCS-ARSPA reviewers
until I pointed to the current draft, which is what we submitted there.

You can find it here:
http://web.comlab.ox.ac.uk/oucl/work/toby.murray/papers/analysing_authority.pdf

The analysis technique described in this newer version is quite
different from that described in the original paper. The original
version  tried to extract causal relationships from Finite State
Automata. We used CSP as a means of describing such automata.

The new version works on the CSP denotational semantics directly. This
obviously makes the technique less applicable to other modelling
formalisms. However, this has a number of advantages:
  + we can use a standard CSP model checker like FDR to do the analysis
rather than having to hand craft our own tool
  + the new definitions handle nondeterminism correctly, while the old
ones didn't.
  + we can more easily compare our technique to other sorts of analyses
such as information flow analyses, that are fairly well understood in
the context of CSP.

The second point above is crucial. Nondeterminism is extremely useful
for building abstract models of systems. 

The third point is also very useful. I've suspected for a while now that
standard notions of information flow like non-interference ought to be
viewable as some sort of special case of authority analysis. (The
special case being that we're restricting our attention to systems of
just two subjects: High and Low, and we're interested in finding out
whether High has absolutely no authority over Low.)

However, it probably does require a bit of familiarity with CSP and its
standard semantic models.

The basic idea is this:

suppose we're trying to determine whether some objec, o, in our system
has the power to cause some event, e, to occur.  For example, o might be
Alice and e might be Carol overwriting Bill. Hence, we're trying to
determine whether Alice can cause Carol to overwrite Bill.

We look at all sequences of actions that our system as a whole can
perform. In particular, we're interested in all sequences leading up to
the event e. Using standard CSP sequence notation, we're interested in
all sequences 
   s ^ <e>

each s ^ <e> represents one of the ways in which the event e can occur
within our system.  for each s ^ <e>, s is the sequence of events that
precedes this particular occurrence of e.

for some particular occurrence of e, represented by s ^ <e>, we can
conclude that the object o has caused e to occur if o was involved in s,
and had o not been involved in s, e wouldn't have occurred.

ie. if we remove all of o's events from s (to produce some sequence s')
and if e can't follow s', then we conclude that o causes this occurrence
of e and hence, that o has the authority to cause e to occur.

Unfortunately, in the face of nondeterminism the above breaks down. We
might have some (nondeterministic) system in which o can't cause e to
occur, but depending on how we resolve the nondeterminism, in practice o
might be able to cause e to occur. Therefore, we need a definition of
causation that holds if and only if there is some way to resolve the
nondeterminism in a system such that when the nondeterminism is
resolved, causation holds for the deterministic system.

We go on to show that there is such a property and describe how one can
use a standard CSP model checker like FDR to test for this property. It
gets a bit involved at times, but the above is the general idea.

Please feel free to pester me about any of the details or general ideas
contained in that paper. 

MarkM: I have a feeling that you've thought about causation and
authority a bit before. I came across the 'causation' page on
erights.org the other day. This work is a first attempt to try to build
a formal notion of authority from causation. It's scope is perhaps a bit
restricted, given how deeply wedded it now is to CSP. But I can't see
why a similar  approach couldn't be taken with the semantics of other
process algebras (although I'm unfamiliar with them so could be
completely wrong here.)

Thanks for the interest, btw. It's exciting to know someone else is
interested in this work.

Cheers

Toby

On Sat, 2007-04-28 at 23:04 -0700, Mark Miller wrote:
> On 4/28/07, Mark S. Miller <markm at cs.jhu.edu> wrote:
> > [...] Toby Murray's
> > <http://web.comlab.ox.ac.uk/oucl/work/toby.murray/analysing_authority.pdf>
> > uses another process algebra, CSP, to reason about authority. [...]
> 
> Oops. I just tried that link, and it's broken. Toby, where can this
> paper be found?
> 
>