[cap-talk] membrane implementations?

[Toby Murray]

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.
> <http://www.eros-os.org/papers/oakland2000.ps>
> 
> 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.
>