[cap-talk] membrane implementations?

Mark S. Miller markm at cs.jhu.edu
Thu Jan 25 11:45:30 CST 2007

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.

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.

Text by me above is hereby placed in the public domain


More information about the cap-talk mailing list