From: "Jonathan S. Shapiro" <shap@eros-os.org>
Replying To: Mark Miller <markm@caplet.com>
Date: Fri, 06 Dec 2002 19:17:51 -0500
Subject: Re: [e-lang] "Capability Myths Demolished" (was: Software security workshop)

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

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

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. There
is a non-monotonic convergence problem lurking within the ability to
overwrite capabilities. markm

Some security properties require explicit consideration of designation
to verify. Others do not.  The models reflect the problems that the
researcher was trying to solve rather more than they reflect the
realities of the systems. Properly done, this does not render the
models, the systems, or the concepts in any way contaminated.

shap 

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