[cap-talk] Another "core" principle - Brinkmann

[Jonathan S. Shapiro]

On Fri, 2006-12-29 at 00:44 +0100, Valerio Bellizzomi wrote:
> >My belief is that some form of fundamental access right describing a
> >right of opaque traversal must be introduced to account for this. I have
> >fumbled with such a right several times, and I have never managed to
> >build a completely satisfactory model for it.
> 
> The first thing that comes to my mind is a "seek"-like operation in the
> translation logic. It would have the power to address page table entries
> (like "seek" has the power to address file records or disk sectors), but
> NOT the power to alter the entries.

This is insufficient. In order to traverse the page tables you need to
read (i.e. TAKE) the entries. The trick is to account for why this does
not disclose the capabilities to the process performing the memory
reference.

I built a model at one point that introduced indirection rights and used
an accumulator-like traversal register. There was no operation
permitting a copy from the traversal register into the referencing
process, which ensures that the capability cannot leak that way. My
verification-oriented colleagues don't seem to like this formulation.

The real problem in this approach is that we need to deal with the fact
of observability, and I wanted to account for keeper invocation as well.
Observability is not quite read, and it is REALLY easy to drive the
model off the cliff when you introduce it. This is the part that I kept
screwing up in my attempts to write up DimTake.

> But I'm quite sure that I'm missing something..Probably capabilities must
> be read in order to perform address translation ?

Precisely. If the model ignores this, it's both non-believable and fails
to model observability correctly.

-- 
Jonathan S. Shapiro, Ph.D.
Managing Director
The EROS Group, LLC
+1 443 927 1719 x5100