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

From: "Jonathan S. Shapiro" <shap@eros-os.org> · Date: Wed, 11 Dec 2002 22:26:26 -0500

On Wed, 2002-12-11 at 15:55, Tyler Close wrote:
> Wow, this is really bad jargon. The interpretation of the sentence
> in plain English is completely misleading. The Lampson model is
> susceptible to the Confused Deputy and does not support
> confinement, but is "more powerful" than a real capability system.
> 
> Can you suggest a textbook that defines this modeling jargon?

I think it's just really *unfamiliar* jargon. When you see the
definition it will make perfect sense.  A model is "strictly more
powerful" than the system it models if the legal states and transitions
in the real system are a strict subset of the legal states and
transitions in the model. norm tyler

The idea is that if you can prove the property for the supersystem  (the
one actually modeled) then you know that *removing* operations won't
break any security property that holds for the model. You therefore know
that the real system is safe because the operations it permits are a
subset of those permitted by the model.

The basic Lampson access matrix based formalism *does* support
confinement,  though other parts of the paper were unfortunately stated
in ways that you and Alan Karp have already enumerated. tyler

I caution, however, that you seem to still be insisting on conflating
some things and that this is getting in your way.  There is no one
universal verification model for a system. When doing a verification,
you build a model that is (a) well suited to the particular property or
properties that you are trying to analyze and (b) strictly more powerful
(as defined above) than the real system. For the confused deputy problem
(which, aside, is a policy quite hard to formally state), you would use
a completely different *kind* of model and a completely unrelated set of
proof techniques. In principle, no one model is going to be appropriate
to both confinement and confused deputy. In fact, the two verifications
occur at completely different layers of abstraction in the system.
Showing that the deputy isn't confused is basically a value/control flow
analysis at the source code level. tyler

The SW and DimTake models were developed to analyze a *particular* set
of information and authority flow properties.  The properties we were
trying to analyze did not include the confused deputy property. The fact
that these models don't address the confused deputy issue is completely
irrelevant to anything. tyler

I think much the same confusion is happening in the discussion here
about the Lampson paper.  The Lampson model was not attempting to address
many of the issues that this group finds important. It was nonetheless a
reasonable attempt at a model for the problems that it was trying to
solve. It was flawed, and in consequence some of the people here have
spent a considerable amount of energy crapping on Butler. I have to say
that this is exceptionally disrespectful. This stuff is **bloody hard**.
It took Sam and I three years to get that verification right, and most
of the work was in arriving at the right model. We surely would not have
gotten it right without the benefit of seeing how Butler (and several
others) got it wrong. tyler

In short,  I think people here may be ignoring the degree to which
science is a process in which partial progress and semi-flawed results
are both proper and necessary. tyler

shap 

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