[cap-talk] Capabilities and Freedom vs. Safety

James A. Donald jamesd at echeque.com
Wed Jul 25 23:31:35 EDT 2007


Jonathan S. Shapiro wrote:
 > 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.

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.

Observing actually existent attacks, they are almost all
of the form that the proof incorrectly assumes cannot
happen, and few if any attacks observed in the wild are
of the form that the proof correctly assumes cannot be
prevented.

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.


More information about the cap-talk mailing list