[cap-talk] Capabilities and Freedom vs. Safety

[Jonathan S. Shapiro]

On Wed, 2007-07-25 at 20:28 +0100, Toby Murray wrote:
> On Wed, 2007-07-25 at 13:04 -0400, Jonathan S. Shapiro wrote:
> >   In cap systems it is decidable in O(|S+O|) (that is: in linear time)
> >     and the answer is "yes, we can prevent that". This is true even if
> >     the system is infinite.
> 
> Is this second result from SW or from take-grant systems or what
> formalism? Certainly, HRU didn't examine restricting their semantics so
> as to match those for capability systems.

The HRU work did not look at this case specifically, but there was work
by Jones, Lipton, and Snyder published at about the same time that did.

The SW result should be viewed as confirming this, since confinement
cannot be enforced if safety cannot be enforced.

> >   For all other known protection systems, the problem is decidable in
> >     the finite case and the answer is "no, we cannot prevent that."
> 
> Where does this last result come from? That seems like a pretty bold
> claim.

Hmm. Yes. I should be more careful. What I should have said is that
there is no other known system that has been subjected to formal
analysis that supports the safety property for finite instantiations.
The HRU paper looked at several. There were subsequent follow-on papers.

To be clear: there *are* some subsequent papers that claim to have
verified such security properties for other systems. In all of the cases
I know about, the ground assumptions of the system model were either
transparently absurd or obviously failed to capture some critical aspect
of the systems that they modeled.

The other failure mode I have seen is results that make no sense in the
real world. For example, there is one paper claiming that ACL and
Capability systems are equivalent provided the implement the same access
rights. This paper had two flaws:

  (1) The two classes of system *never* implement the same access
      rights. For example, the "own" right is nonsense in a capability
      system.

  (2) Ignoring that, the verification was wrong.

All of the above, by the way, is paraphrased intentionally so as to make
the particular publication that I have in mind non-obvious. The authors
have learned some things since then, and there is no point beating up on
them about an early, mistaken result.

shap