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

[Toby Murray]

On Fri, 2007-07-27 at 17:03 +0100, Toby Murray wrote:
> On Fri, 2007-07-27 at 11:50 -0400, Jonathan S. Shapiro wrote:
> > On Fri, 2007-07-27 at 11:55 +0100, Toby Murray wrote:
> > > The question I was
> > > asking was whether the formal access control model (identity-based ACLs
> > > with so-called "discretionary" access control and the superuser) can
> > > enforce the safety property. Of course they can -- that was my point.
> > 
> > The answer is NO. Go re-read the HRU paper.
> 
> I will. But I don't remember anything in that paper to support your
> claim from last time I read it. I'm hoping that if re-reading the paper
> doesn't convince me you're right, that you could point to the relevant
> section in which this claim is proved.

I've now re-read that paper. 

(see a PDF here
http://www.cs.unibo.it/~babaoglu/courses/security/resources/documents/harrison-ruzzo-ullman.pdf )

Having done so, I see no evidence to support the claim that the safety
property cannot be enforced using identity-based ACLs with so-called
"discretionary" access control (i.e where the "owner" of an object can
control which subjects have permission to access it).

If anything, HRU demonstrates my position (rather than its negation, as
Jonathan claims.)

I'm hoping Jonathan will add some argument here to support his claim.
I've learnt a hell of a lot from his writing generally and particularly
his posts to this list. This may well be another example in which this
continues to occur. If I'm wrong, then it means I've failed to
understand one of the points that can be gleaned from this paper on a
number of separate occasions. I'd like to correct this, if it's the
case.

If I'm correct, I'd like the record set straight.

I suspect that the crucial part of the paper is Example 4, which appears
at the end of Section 3. Here, HRU model UNIX style access controls in
their formal model. They make no claim as to whether safety can be
assured in this model or not. At this point in the paper, the notion of
safety has yet to be covered in depth.

Figure 2 has some example commands for implementing simplified UNIX
access control semantics in their model. They define the following
commands:

-- subject s creates new file f
CREATEFILE(s, f)
  create subject f
  enter "own" into (s, f)

-- subject s grants the owner of f the permission to read f
LETOREAD(s, f)
   if "own" in (s, f)
   then enter "oread" into (f, f)

-- subject s grants everybody read permission to file f
LETAREAD(s, f)
   if "own" in (s, f)
   then enter "aread" into (f, f)

-- subject s attempts to read file f
READ(s, f)
   if either
      "own" in (s, f) and oread in (f, f)
   or
      "aread" in (f, f)
   then
      enter read into (s, f)
      delete read from (s, f)

The safety property is upheld by some initial configuration of the
sytem, there is no sequence of commands that can be executed from that
configuration, such that some right (like "read" or "oread" above) ends
up being held by an untrustworthy subject -- even if only temporarily as
it does during the execution of command READ above.

The authors (HRU) specifically say that in order to conduct a safety
analysis, we ought to first remove all trustworthy subjects from the
(model of the) system; since their ability to leak a permission doesn't
count as a violation.

So say we have a system of 2 subjects, s1 and s1, and one (file) object
f.

Say that s1 is the owner of f (i.e. "own" is in (s1, f) )
And we want to determine whether s2 (who is considered untrustworthy)
can obtain the right to "read" f. s1 is considered trustworthy, so we
remove it from the configuration, leaving a configuration with 2
entities (s2 and f) in which no entity has any permission to any other.

Clearly, s2 cannot obtain the permission to "read" f (without s1
granting it that permission.)

Hence, the controls represented by this model can indeed enforce the
safety property.

Again, the HRU paper supports this position and not its negation, as far
as I can see.

Have I missed anything here? Or is Jonathan's claim supported elsewhere
in this paper that I've overlooked?

Cheers

Toby