[cap-talk] membrane implementations?
toby.murray at comlab.ox.ac.uk
Fri Jan 26 04:50:54 CST 2007
On Thu, 2007-01-25 at 09:45 -0800, Mark S. Miller wrote:
> Pierre THIERRY wrote:
> > Scribit Jonathan S. Shapiro dies 25/01/2007 hora 11:20:
> >> Aside: it is somewhat flattering the number of times people have said
> >> "the o-c model says X" and sure enough that was exactly what the
> >> formal model said. The flattering part is that everybody forgets to
> >> acknowledge the formal model, but its characterization of the o-c
> >> model seems to have entered the ethos of ideas. I can live with that.
> > Is there somewhere a comprehensive description of the obj-cap model?
> The formal model Shap refers to above is the SW model of
> Jonathan S. Shapiro and Samuel Weber. Verifying the EROS Confinement
> Mechanism. In Proc. 2000 IEEE Symposium on Security and Privacy, pages
> 166--176, 2000.
> As Shap and I have discussed, the SW model describes an abstraction which
> includes objcap systems; but it also includes systems which are not objcap
> systems. As I wrote earlier on cap-talk:
> > Also, various prior models of objcap systems, like take-grant and Shap's SW,
> > also throw all capabilities held by a given subject into an undifferentiated
> > bag. As an abstraction of actual systems, it is valid to drop information.
> > This simplification in indeed safe and valid for the purposes for which these
> > models are designed -- which treat all subjects as, in Shap's phrase,
> > "presumptively hostile". They are not able to describe relied upon subjects,
> > such as deputies or access abstractions, but they were not meant to.
I would have thought that the fundamental issue is not that a subject's
capabilities are grouped into an undifferentiated bag. Instead isn't the
issue that the models don't allow a subject to *choose* which cap they
want to use.
One can construct a model that groups all of a subject's caps into a set
and then enforce the constraint that the cap a subject is choosing to
exercise is a member of that set, for example.
> Chapter 9 of <http://erights.org/talks/thesis/> presents an *informal* model
> that includes the treatment of "index"es (c-list indexes or lambda-calculus
> names) needed to account for how deputies may avoid confusion.
> I eagerly anticipate Fred's soon-to-be-finished thesis, which presents a
> formal model able to describe unconfusable deputies.
More information about the cap-talk