[cap-talk] Capabilities and Freedom vs. Safety

[Jonathan S. Shapiro]

On Thu, 2007-07-26 at 13:31 +1000, James A. Donald wrote:
> Jonathan S. Shapiro wrote:
>  > The "safety property" is:
>  >
>  >    Given an initial configuration of a system, and an
>  >    arbitrary choice of right 'r', object 'o', and
>  >    subject 's', is it possible in principle to prevent
>  >    subject 's' from obtaining right 'r' on object 'o'.
>  >
>  > The answer (summarizing HRU's formal results):
>  >
>  >   In the general case this question is undecidable. It
>  >   is always
>  >     decidable if the system configuration is finite.
>  >
>  >   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.
>  >
>  >   In RBAC systems the answer is "yes, we can prevent
>  >   that". I do not
>  >     know (I haven't looked) whether the RBAC case is
>  >     decidable for infinite systems, but it is
>  >     certainly decidable for all finite systems, which
>  >     is good enough. I do not know the order statistic
>  >     on the decision procedure.
> 
> The proof assumes we cannot prevent subject s abusing
> right r in one system because one sort of thing could go
> wrong, but we can prevent that in another system because
> a slightly different sort of thing is assumed to never
> go wrong.

Umm. You seem to have completely missed the point. The proof does not
consider abuse of rights 'r' that a program is "supposed" to have. What
the proof shows is that the entire notion of "supposed" to have is silly
in most systems, because the set of rights obtainable by a program is
unrestricted.

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.

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.

None of this addresses the problem of programs that mishandle their
legitimate authority. I include "programs vulnerable to penetration and
hijacking" in this category, because being vulnerable to penetration is
entirely preventable using readily available technology today.

> Contrary to the proof, we cannot in fact prove that s
> can never abuse right r, because an entity x that
> rightfully has right r may well fail in ways that enable
> subject s to make x do what it wants - which is in fact
> the way that these attacks are usually conducted in the
> wild.

For many *current* programs this is correct. Not for all: there is a
subset of programs for which we can formally verify that no such abuse
occurs. Granted, that is a very specialized subset. There is a much
broader (and rapidly growing) set of programs in which buffer overrun
attacks are impossible (i.e. those written in safe programming
languages).

A couple of points about this issue:

 + Buffer overruns are a mess, but their continued existence today
   is a matter of pure negligence.

 + In the absence of buffer overruns, defensive programming is a matter
   of *design* and *architecture*. The question should then be asked:
   how do we engineer a development system and environment in which
   defensible designs are the most natural way to build things?

I believe that capability-based design is the best known answer to the
last question. I have only anecdotal support for that belief, but that
is why I work on this stuff.

shap
-- 
Jonathan S. Shapiro, Ph.D.
Managing Director
The EROS Group, LLC