From: "David Chizmadia" <>
Date: Sun, 8 Dec 2002 23:31:34 -0500
Subject: Re: [e-lang] Modelling Blindness (was: "Capability Myths Demolished" (was: Software security workshop))

Mark Miller wrote:
> Ah, now I understand the question. But I wouldn't say that SW is
> "inaccurate". SW includes certain things in the model and leaves out others,
> in order to make the confinement proof easier to carry through. So long as
> what's left in is accurate, and so long as the presentation of the model is
> clear that aspects of the real system are not represented in the model, I
> would avoid the term "inaccurate" to describe the situation.

I believe that the most precise characterization would be
"accurate, but incomplete". 

> Rather, I would say that SW is an accurate abstraction of EROS, even though
> this abstraction describes an ambient authority system. As to whether
> Lampson71 is an accurate model or CAL-TSS or any other actual capability
> system, I don't know.

As a general observation,  I think that shortly after Tyler
unleashes his paper arguing that Lampson had a "naive"
understanding of capabilities someone will have to produce
a paper semiformally* characterizing the "confused deputy"
threat. This characterization will then provide the metric
for formal analysis of both the Lampson Access Matrix and
proposed replacements. shap

The confused deputy characterization will also motivate
researchers to overcome the problem of modelling CLists 
as maps, since it will change the verification goal from
showing just confinement to showing both confinement and


* In my messages, I use the term "semiformal" to mean natural
language  (my preferred one being American English:) statements
of fact about a system that allow properties of the system to
be proven using symbolic logic. In the same way, I use the term
"formal" to mean mathematical statements of fact about a system
that allow the properties of the system to be proven using well-
defined combinations and transformations of the statements.

e-lang mailing list