[cap-talk] Non-safety vs. permission propagation -- HRU and IBAC ACLs

[David Hopwood]

Toby Murray wrote:
> On Mon, 2007-08-06 at 18:18 +0100, David Hopwood wrote:
>> To say that ACL systems fail to enforce the safety property, we only need
>> to argue that there may exist a right f, and a process P running as the
>> owner of f,

More precisely, "the owner of an object to which it has right f,"

>> such that P is not trusted to arbitrarily propagate f.
>> That's all. No other assumptions are needed.
> 
> But one can make exactly the same argument against cap systems.

Informally, the safety property asks the question, "For any generic
right, is it possible to set up a configuration in which some subject
initially has that right to any object, but is prevented from
propagating it (even temporarily) to another subject that does
not initially have it?"

In protected capability systems, if we want to prevent a subject from
propagating a right, we can confine the subject. The EROS confinement
proof demonstrates that this is feasible.

In ACL systems: for *any* subject P and generic right r, let O be *any*
object created by P, and let f be the right r to O. Since P created O,
it starts with right f, and since it is the owner of O, it can
propagate f to any other subject. Therefore the system does not have
the safety property.

> Jonathan's original point seemed to be that cap systems can do something
> that ACL systems cannot. (enforce the safety property.) This line of
> argument fails to make the necessary distinction.  Or am I missing
> something here?

In protected capability systems, objects do not have owners that can
propagate rights to the object to any other subject. Propagation of rights
is restricted by the connectivity of the object graph, and it is feasible
to set up this graph to prevent undesired propagation.

-- 
David Hopwood <david.hopwood at industrial-designers.co.uk>