Capbility Concepts

[Jonathan S. Shapiro]

> We believe that Mungi (http://mungi.org/) can do confinement (although
> we haven't done a formal proof -- I'm waiting for a student to do the
> work ;-).

Gernot, all:

My recollection from talks with Jerry Vochteloo is that mungi uses a
per-process or per-system XOR value (I don't recall which, but it doesn't
matter).

If this is correct, or a similar unforgeable transformation is used, then
Mungi can definitely do confinement subject to the assumption that the
inverse transform is unguessable. If so, then you don't actually need to do
a proof of confinement. You merely need to do an equivalence proof between
XOR application and capability/data partitioning. If you can do that then
you fall under the SW model proof.

The proof sketch I have in mind is:

1. Observe that the true capabilities are the post-XOR capabilities, which
are all partitioned. The pre-XOR capabilities are completely irrelevant.

2. Show that the XOR test operation has the effect of enforcing the
partition between capabilities and data, again subject to the unguessability
constraint.

3. Observe that if this partition exists then there is a direct equivalence
between the Mungi protection model and the SW model published in the latest
IEEE security symposium at http://www.eros-os.org/papers/oakland2000.ps ).
In point of fact, the SW proof only requires that users cannot invoke
capabilities as data. It is not compromised if the user can observe the
capability bits.

As far as Sam and I know, the SW model covers all capability systems
(including Mungi) that *can* enforce confinement, and excludes all the ones
that cannot.

Mungi definitely can do confinement.

I'll expect a citation of the SW paper in your publication :-)

While I'm thinking about it, would you consider adding an EROS link to your
related systems list? EROS has some of the feel of a single address space
system, and we've all certainly exchanged a bunch of ideas back and forth.


shap