[cap-talk] Is "Authority" Subjective?

[Jonathan S. Shapiro]

On Fri, 2007-06-22 at 15:08 +0100, Toby Murray wrote:
> On Fri, 2007-06-22 at 09:37 -0400, Jonathan S. Shapiro wrote:
> > Toby:
> > 
> > I'm not familiar with CSP, but I think that your question derives from
> > an oversimplified model.
> > 
> > If I understand your CSP model (remember: I don't know CSP), it is
> > describing a DFA. There are four system states as follows:
> > 
> >   S1: a1 -> S2
> >       b -> STOP
> >   S2: a2 -> S3
> >   S3: b -> STOP
> >   STOP: <>
> > 
> > What you have here is actually an operational semantics where each
> > operation is preconditioned on the system being in the correct state.
> > 
> > The problem with your question is that Alice and Bob cannot, by
> > definition, be distinct subjects, because their actions are updating the
> > same system state variable.
> 
> I don't see why this precludes them being distinct subjects. Can you
> explain further?

I can try. My note earlier was confused. Let me start over.

First, you *may* have a terminology problem. I am not clear if by
Alice/Carol/Bob you mean processes (subjects) or people (principals).
Which is it? Aside: this confusion is why I ABSOLUTELY DETEST the
Alice/Carol/Bob naming convention.


Assuming you mean subjects (processes) the problem is simple: your model
doesn't have subjects anywhere. If you want to model subjects, you need
to introduce a set of subjects. The resulting model will look very
different.

In SW, there is a universal set P of processes (subjects). To simplify
the model, all objects are subjects in SW. There is a universal set R of
access rights. There is a universal set C of capabilities, each of which
has the form (p,r), where p is a process in P and r is a member of the
2^R (the power set of R. That is: r is a set of rights conveyed by the
capability). Finally, there is a relation CAPS : P -> C describing the
set of capabilities {c} held by a subject p. [This last was correct for
our purposes, but in a real system it should be an indexed vector rather
than a set so that we can tie the model to a PL-level
lambda-environment.]

In SW, system states are mutable. That is, all transitions proceed from
the current state S to a new state S' which becomes S in the next step.
The state of the system, by definition, consists of P, C, and CAPS.

The operational semantics (which describes what effects are possible in
any step from S to S') has preconditions for each step. For example,
the 

   write-page(p, c)

operation has the preconditions:

   c in CAPS(p)
   write in RIGHTS(c)

and the effect that target(C) (a process) is mutated.



I have omitted many details here. My point is to demonstrate that this
kind of model is qualitatively different from the kind of model you are
writing. It may be that CSP can handle this sort of thing -- I do not
know. What I do know is that if your model does not admit subjects as
entities in the model, it is semantically meaningless to talk about the
behavior or impact of subjects w.r.t. the model.

> What if the system has a third subject, Carol, and we rename the events
> as follows so that P becomes:
> 
> P = aliceInvokesCarol -> carolRespondsToAlice -> bobInvokesCarol -> STOP
> []
>     bobInvokesCarol -> STOP
> 
> This models Bob being unable to invoke Carol while she is invoked by
> Alice. Alice's events are now shared with Carol and likewise for Bob's
> events. 
> 
> Does that remove the problem you raise above, which I'll admit I don't
> grasp. My question still remains valid for the modified example but is
> now rephrased as  "Should we say that Alice can cause Bob to invoke
> Carol?"

I still think that this model is too weak to say much along the lines
you are trying to explore, but to answer your last question above: no,
the most we can say is that "Alice causes the preconditions to exist
that might *permit* Bob to invoke Carol". My recollection is that a CSP
model is non-deterministic, so there is no guarantee that the
'bobInvokesCarol' event ever happens.

> While I see a difference, yes, I can't see how it precludes Alice and
> Bob being distinct subjects on my model.

Alice and Bob cannot be distinct subjects in the model because the model
does not incorporate any notion of subjects. In the absence of a notion
of subjects, there can be no notion of distinct subjects.

shap