[cap-talk] Capabilities and Freedom vs. Safety

[Jonathan S. Shapiro]

On Wed, 2007-07-25 at 17:46 +0100, Toby Murray wrote:
> On Wed, 2007-07-25 at 12:37 -0400, Jonathan S. Shapiro wrote:
> > The difference between James and the community is that James doesn't
> > understand the math. He therefore tries to reason about this stuff
> > informally. Then he gets upset when people who *do* understand the math
> > tell him that he has it wrong.
> 
> Could you elaborate on this "math"? The arguments presented about the
> merits of protected caps over caps-as-data have been anything but
> formally stated. I recall seeing no formal proofs of these arguments
> (although I don't believe they're needed to substantiate them.)

The math is not needed, but it is helpful. English is often sufficient,
but when the English becomes convoluted you rapidly discover that
English is not very good as a language for discussing precise
mathematical things. At that point, switching to math can be very
helpful.


You ask a good question. My statement above was intended to refer to the
math that differentiates ACL and Cap systems.

Concerning ocaps vs. caps-as-data, the math distinction is very simple.
Any "caps-as-data" system has all of the deficiencies attributed by Kain
+Landwehr and/or Boebert. Caps-as-data are data, and if modify the SW
model to allow operations to be based on data of any sort, you will find
that the "safety property" (defined by Harrison Ruzzo and Ullman) cannot
be enforced. You will *probably* discover that you cannot say anything
at all about the safety of the system without formally reasoning about
the properties of the trust-enforcing programs. This is, in effect, the
price of introducing dependency on user-mutable data into the
operational semantics. [Caveat: I haven't attempted that verification.]

The reason that kernel-decrypted caps dodge the bullet about dependency
on user data is tricky, and if anybody cares I will take it up in
another message.

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.

  For all other known protection systems, the problem is decidable in
    the finite case and the answer is "no, we cannot prevent that."

It is clear that if *both* the decrypt and the encrypt key are held by
the kernel, then the encrypted form is merely an index for the
(supervisor protected) decrypted form, and the system should be viewed
as a protected cap system.

The interesting question that has been raised on the list over the last
few weeks is whether cryptographic capability systems wherein the
*encrypt* cap is held by user code may also be arranged in a way that
yields a protected cap system. Jed has made a pretty convincing case
that the answer is probably "yes".


shap