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

[Valerio Bellizzomi]

On 28/12/2006, at 19.00, Jonathan S. Shapiro wrote:

>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.


Can you expand on Observability ?
I will read your reply tomorrow, heading to bed now :-)


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