Subject: Re: [e-lang] "Capability Myths Demolished" (was: Software security workshop)

From: Mark Miller <markm@caplet.com> · Date: Sat, 07 Dec 2002 11:27:47 -0800

At 04:17 PM 12/6/2002 Friday, Jonathan S. Shapiro wrote:
>On Thu, 2002-12-05 at 19:35, Mark Miller wrote:
>> Even if all actual capability systems are lambda-capability systems, since 
>> most formal models of capabilities (including Lamport and SW) to date have 
>> been ambient-capability models, and since most people learn capabilities by 
>> learning these models, I return to thinking we should draw a line between 
>> capability systems...
>
>These models do not claim to faithfully model real systems, nor do they
>claim to faithfully model capabilities. Instead, they claim to model the
>portions that are relevant **to a particular verification problem.**
>
>For example, the EROS confinement verification says explicitly that the
>real system does not use sets, and that we use sets to simplify the
>mathematics. We in fact had to argue in the TR version why this
>simplication was sound.

So far, we're in complete agreement, as should be clear from the email 
you're quoting. 

>Picking a new name won't help. It will simply lead to the publication of
>appropriately simplified models of lambda capabilities too. The fact
>that verification models invariably elide details that are not relevant
>to a particular verification (and invariably document the fact that they
>do so) does not in any way contaminate the "capability" term.

So long as the models are not mistaken for complete descriptions of the 
capability-ness of the systems themselves,  then there isn't any 
contamination. That would be a much nicer world than the one we've all 
been living in the last 31 years. In this world, several generations learned 
from Lampson's model, or learned from those who learned from Lampson's 
model, and mistook its properties to be an accurate statement of the 
properties of capabilities.

(Despite the fact that there wasn't anything wrong that I know of with 
Lampson's own capability OS design, CAL-TSS,  Norm's sense is that Lampson 
proceeded to make the same mistakes as everyone else, by taking his model 
more seriously than his system. I am much more ignorant of the history than 
Norm, but from what I know, I concur.) tyler

>I invite you to revise the verification proof in either our paper or the
>earlier TR to re-express the verification in terms of indexed arrays
>instead of sets. You'll shortly see why we didn't do it that way, and
>why it is unlikely that any verification of this kind ever will. [...]

Again, as you'll see in the email you quote,  I think it's great for a model 
to abstract away detail in order to serve the purpose for which the model 
was constructed. I have no problems with SW used for the purpose you created 
it for.

I do have a problem when a model is mistaken for the terrain,  such that 
people conclude that an inadequacy in the model implies a corresponding 
inadequacy in the systems being modelled. This type of mistake is the root 
cause of the accumulation of a 31 year legacy that we must now somehow unwind.

On this list, I've already been on both sides of the question.  For me, the 
definitive point was

At 04:25 PM 12/5/2002 Thursday, David Wagner wrote:
>If we'd like to criticize
>this concept, then it would help to have an unambiguous name to use when
>referring to this concept.

Note that earlier, you yourself wrote: 

At 08:14 AM 12/4/2002 Wednesday, Jonathan S. Shapiro wrote:
>One of
>the key differences in various capability system designs is whether
>C-lists are sets or maps

If you yourself would even consider admitting C-lists-as-sets systems into 
the category "capability system",  then I know I need a narrower term to 
describe the kinds of system I'm advocating.

----------------------------------------
Text by me above is hereby placed in the public domain

        Cheers,
        --MarkM

_______________________________________________
e-lang mailing list
e-lang@mail.eros-os.org
http://www.eros-os.org/mailman/listinfo/e-lang