[cap-talk] Capabilities and Freedom vs. Safety

[Jonathan S. Shapiro]

On Thu, 2007-07-26 at 14:01 +0100, Toby Murray wrote:
> On Thu, 2007-07-26 at 00:09 -0400, Jonathan S. Shapiro wrote:
> > Another way to look at this is that the safety property serves as a
> > litmus test. In a system that satisfies the safety property, it is
> > possible to know that some sensitive right is only accessible to some
> > particular (set of) programs. As a design matter, this allows you to
> > focus your attention on those programs when trying to manage that
> > sensitive access right.
> 
> By "right" I presume you mean "permission". If so, could we adopt that
> terminology. If you mean something  else, could you please clarify. 

I used the term "right" in this context because that is the term used in
most of the formal literature in this area, but yes, in the lexicon of
this list a "right" should be taken to mean a "permission".

> None of this helps when we move from considering perission to authority,
> however. The best work on the safety problem (such as Fred Spiessens'
> SCOLL) fails to adequately reason  about authority.

Yes and know. Failing the safety test tells us that authority control is
impossible. Passing the safety test tells us that authority control
*may* be possible. The confinement verification proof is a proof about
the upper bound of reachable permission, which is to say: authority.
 
> > Conversely, the proof shows that in all of the commodity systems in
> > current deployment, no such focus of attention is possible. It is silly
> > to worry about whether the behavior of some particular program w.r.t.
> > some right 'r' is sensible when *every* program is in a position to
> > abuse that right.
> 
> Could you elaborate on how the proof  (by which I presume you mean HRU
> but again if I've assumed wrong or lost the thread then please correct
> me) shows this? Current commodity systems certainly are more restrictive
> than those covered by the general HRU undecideability result.

Last point first: I disagree strongly that current systems are more
restrictive. The Windows access control model is modeled fairly
accurately in the HRU paper, as are classical UNIX permissions.

Modern linux is a more interesting beast because of the introduction of
SELinux. The *goal* of SElinux was to support RBAC, which is a
safety-enforceable scheme. The specific implementation of SELinux is
known to have significant holes and has never (to my knowledge) been
formally modeled.

In light of this, I believe that the conclusions of HRU hold very well
for current commodity systems. The HRU undecidability result isn't the
part that should worry us. The part that should worry us is that all
*finite* systems (which is to say: all systems observed in the real
world) are decidable, and for the access models used in current
commodity systems, the safety property is known to be false.


shap