[cap-talk] Another "core" principle - e.g. re purpose capabilities in dist. documents.

[Kevin Reid]

On Dec 19, 2006, at 13:21, Jonathan S. Shapiro wrote:
> On Tue, 2006-12-19 at 12:30 -0500, Kevin Reid wrote:
>> On Dec 19, 2006, at 11:56, Jonathan S. Shapiro wrote:
>>
>>>   someCap->deepCopy(sourceOfStorageCap) -> dataSpaceCap
>>
>> This case can be handled by using a different protocol. In your
>> notation:
>>
>>    sourceOfStorageCap->subdivide() -> fragmentCap
>>    someCap->deepCopyInto(fragmentCap) -> completion
>>
>> When the deepCopyInto is complete, fragmentCap, which was created
>> locally and so is not membraned, has a copy of the data someCap
>> provided by writing to its wrapped-fragmentCap through the membrane.
>
> I see that this pattern will work, but I have to say that from the  
> "can
> developers maintain this idiom" perspective I am suspicious that it is
> not an idiom that programmers can be relied on to build correctly.
> Recall that this pattern is going to be common. It's not something  
> that
> "just" the security experts need to know how to do.

Without claiming that this is in fact adequate, some points that come  
to mind:

- My protocol has an advantage in non-membrane conditions: the  
programmer is not relying on someCap to return a dataSpaceCap which  
really is from sourceOfStorageCap.

- Under the "membranes will be common" scenario, it would be  
reasonable to expect programmers to test their program's behavior in  
membranes, insofar as they test at all.

- The design of the space bank protocol might affect which of these  
protocol comes naturally for "give me some data in my storage"  
scenarios like this.

>> In Mark Miller's most recent posting of a membrane program, the
>> equivalent function, passing passive permissionless objects
>> irrevocably, is handled by this part:
>>
>> def makeMembrane (target) {
>>      ...
>>      def wrap(wrapped) {
>>          if (Ref.isData(wrapped)) {
>>              # Data provides only irrevocable knowledge, so don't
>>              # bother wrapping it.
>>              return wrapped
>>              ...
>>
>> Ref.isData provides the knowledge needed to pass information through
>> the membrane. It is implemented by the capability to be wrapped
>
> I think I had misunderstood this example then, because I had assumed
> that isData() was somehow primitive.

The method Ref.isData is itself part of the primitive Ref object, but  
it is equivalent to querying the separate Data/DeepPassByCopy guard- 
and-auditor.

> That is: I had originally read this to mean that the argument in  
> question was a data argument as opposed to a capability argument  
> (which made sense, but I see that in E this cannot be what is going  
> on, because all arguments are capabilities).

(Another way to look at it is that all arguments are objects, which  
might be like either what you call data or what you call  
capabilities. Or: a capability to data is the same as data.)

The Data test verifies that the subgraph it is given contains only  
objects which behave like data. Specifically, either:

   - the object is an immutable leaf, such as null, 1, "hi", or  
false, or

   - the object is Selfless (which means that it is immutable and  
willing to present a complete description of itself) and all the  
components of that description are data.

Selfless is an ordinary guard/auditor; objects may choose to be  
audited by Selfless. It is special only in that many primitive  
objects use it.


If one wished to reproduce this subsystem separately as unprivileged  
code ('CarolsSelfless'), the only part which would not be identical  
to the primitive one would be a mechanism for allowing preexisting  
objects not audited by CarolsSelfless (such as primitive lists, etc.)  
to be approved.


> Why is it that the membrane policy can trust the answer provided by
> isData()? I would appreciate some detail here, because I'm looking to
> understand how we might go about duplicating that effect in an OS- 
> based
> system.

It is not that it /can trust/ the answer, but that it /does rely/ on  
the answer, just as much as it relies on being executed by a correct  
E evaluator. If you evaluate the membrane maker providing it a  
correct definition of Data; it operates correctly; if not, not.

-- 
Kevin Reid                            <http://homepage.mac.com/kpreid/>