[cap-talk] Is "Authority" Subjective?

[Valerio Bellizzomi]

On 22/06/2007, at 13.27, Jonathan S. Shapiro wrote:

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

I agree, this naming convention is confusing. I have the same problem, I
am not clear what Alice/Carol/Bob are. I said it already in the past, but
no one seems interested in revising the issue.


>
>
>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
>
>_______________________________________________
>cap-talk mailing list
>cap-talk at mail.eros-os.org
>http://www.eros-os.org/mailman/listinfo/cap-talk