[cap-talk] Announcing "Analysing Object-Capability Security" Paper and Authodox v. 0.2.0

[Toby Murray]

On Thu, 2008-05-22 at 23:57 +0100, lists at notatla.org.uk wrote:
> Toby,
> 
> > For anyone who's interested, I'd love to get feedback on the paper
> > before the final version is submitted on June 1st. It's available here:
> > http://web.comlab.ox.ac.uk/people/toby.murray/papers/AOCS.pdf
> 
> I have a few newbie comments.

No such thing. Thanks for the comments and sorry for taking so long to
respond -- I've been meaning to write this email for almost a week now.

> 
> In Figure 1 b):
> 
> TheReadOnlyFwdr seems to hold a {read,write} capability on Fred
> when I expected it to hold only {read}.

There are a few unstated assumptions here. (I had to cut the whole thing
down tremendously to get it to fit into the Workshop's page limit.)

One assumption is that Fred is an object supporting the both read() and
write() operations/methods. Any (direct) reference to Fred will thus be
a {read, write} capability. 

Technically, the names of operations in braces, e.g. {read, write} are
the operations that the object to which the arrow points supports. Since
we are dealing directly in the object-capability model, there is no
notion of capabilities supporting specific "permissions". A capability
is just a reference to an object that allows you to invoke (all of) its
methods. If you want a capability that allows invoking only a subset of
the methods, you need to create a proxy (or /AttenuatingForwarder/ as
the paper describes it) that forwards only that subset.

>    I realise that Alice
> trusts TheReadOnlyFwdr (and probably created it), but since
> there is only {read} from TheRevocableFwdr to TheReadOnlyFwdr
> I found that part of the diagram odd.

There is only {read} from TheRevaocableFwdr to TheReadOnlyFwdr because
{read} is the only message that TheReadOnlyFwdr understands. Hence, it
is the only operation one can perform if one has a reference
(capability) to TheReadOnlyFwdr. This applies no matter who it is that
holds a capability to TheReadOnlyFwdr since all capabilities to that
object support the {read} operation (only) since capabilities here allow
one to invoke all of an object's methods.
 
> 
> The same goes for TheRevocableFwdr holding {get,set} on
> the flag variable "Forward?" .

Again, the same reason here. The Forward? object understands get() and
set(). All references to it allow the invocation of both methods. One
needs to create a proxy to allow access to just a subset of those
methods.

> 
> TheRevocableFwdr presumably could have been given a read capability
> direct to Fred, making this a diagram of one pattern rather than two.

That's just the point. In the object-capability model, one cannot create
a "read"-only capability to Fred. One instead needs to construct a proxy
that forwards only "read" messages to Fred. TheReadOnlyFwdr is just such
a proxy and its job is to mimic a "read"-only capability to Fred.

Of course, in many real capability systems, one can create "read"-only
capabilities to files, particularly OCap operating systems. However, the
same is not true for OCap languages, like E and Caja. The
object-capability model must be generic enough to accommodate both
styles. Since one cam mimic the OS style by using proxies, the
object-capability model chooses to adopt that approach to make it
compatible with both kinds of system (i.e. to allow it to be used to
model both kinds of system).

[The OCap model is totally Mark Miller's creation, btw. Hopefully he'll
chime in if I've messed up any of the above.]
 
> Was it made in these two stages to match the limited alphabets of the
> modelling in later sections?

Sort of. It was made in two stages to match the semantics of the OCap
model. The limited alphabets used in later sections are the minimum
required for me to model the OCap patterns in the paper to some level of
accuracy.

> 
> The description that goes with Figure 1 b) uses verbs rather like
> telling a story as opposed to merely describing an established layout.
>    "We instantiate the ReadOnlyForwarder ... We then instantiate
>    the RevocableForwarder ... Finally, we also give Alice
>    a direct reference to Fred."
> But if this is in story form I would have thought that the order is
> backwards (direct access to the file coming last etc) and Alice
> should be doing the work while "we" watch.

Possibly. I was purposely trying to leave it ambiguous as to who might
be creating these abstractions.

As Mark pointed out in another cap-talk message:
> I had a similar reaction to the story. I would have had Alice start
> with full authority, and then explain how Alice can dispense
> attenuated authority to the other players.

While the text tends to suggest that Alice would create these
abstractions since they serve her interest, this need not necessarily be
the case. Alice and Bob might have signed a contract that governs the
terms of their collaboration. This pattern might be the instantiation of
that contract in the form of security-enforcing code -- what Nick Szabo
refers to as a "Smart Contract". In this case, the objects might have
been created by the party that wrote the contract. This might be Alice,
Bob or someone else entirely, such as the person for whom they are
cooperatively building whatever it is Alice the architect has designed.

Leaving it ambiguous allows these other possibilities. It also allows
those from a "system administrator defines the security policy" mindset
to more easily map the ideas of security-enforcing abstractions into
their world view, since I suspect that for some of them, they might
imagine that it is system administrator who created the abstractions.

At any rate, both you and Mark came to the conclusion that it is most
likely that Alice would be creating these abstractions. Hence, the
current text still naturally implies this while still leaving room for
other interpretations. 


> I've only made it to the end of 2.2 so far.

Please let me know how you go with the rest. CSP is nothing if not
arcane and hairy. 

Thanks again for the comments so far and for taking the time to read the
paper.

Cheers

Toby