[cap-talk] Another "core" principle - virtualizing memory

[Jonathan S. Shapiro]

On Tue, 2007-01-16 at 21:43 -0800, Charles Landau wrote:
> At 3:27 AM -0500 12/29/06, Jonathan S. Shapiro wrote:
> >The "traverse" right is conceptually equivalent to having a service S
> >that implements two facets A and B, will directly disclose some
> >capability to A, but will only wield it indirectly for B. The only
> >difference is that by reifying this right in the operational semantics
> >it becomes possible to do information flow analysis without analyzing
> >the code of S. We haven't exited the capability model at all here. It is
> >merely an optimization.
> 
> So, considering the kernel as a distinguished process, isn't the 
> protection model intact?

Yes. But this involves violating precisely the abstraction boundary that
the model is trying to guard, and it will leave us unable to do the
kinds of analysis that the model is designed to support. In consequence,
we will lose the entire chain of reasoning that the model was created to
support. The goal is to show that the kernel implements the restrictions
defined by the model. From the *user mode* perspective, traversal is
primitive and therefore needs to be modeled.

I don't think that this is difficult to do in the model. I see a number
of ways to handle it.

But it does raise a concern that we define the object-capability model
correctly.


shap