From: "Jonathan S. Shapiro" <>
Replying To: Mark Miller <>
Date: 11 Dec 2002 11:09:57 -0500
Subject: Re: [e-lang] Modelling Blindness (was: "Capability Myths Demolished" (was: Software security workshop))

On Sun, 2002-12-08 at 22:31, 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...

In modeling terms, the statement you want is "so long as the model is
strictly more powerful than the real system".  The model can be more
permissive than the real system (as is the case in SW). In the tech
report version of that work we took tremendous care to *ensure* that the
model was strictly more powerful. tyler

Actually, DimTake (the access model) truly does use ambient
capabilities, but the SW verification model does not.  The operation
semantics of SW elides the actual designator, but it requires for each
operation that there exists some specific capability in the set that is
the capability being invoked. The idea is that a process can invoke any
capability that it can designate. The information flow model must assume
that any capability that *can* be invoked *will* be invoked in some
possible hostile execution. Given this, the only useful constraint for
the information flow property is membership, not designation.

Once we introduce a notion of trusted code performing some mediation,
this ceases to be true because the feasibility of mediation depends on 
designation. In the SW system we took two shortcuts to "duck" this:

  We handled the space bank by integrating its primitives
  into the model. 

  We did not consider the fact that the real constructor
  permits unsafe capabilities.  The real implementation
  guarantees to identify the presence of such capabilities,
  not to prevent them. Tracking this correctly requires both
  designation and the ability to remove capabilities from C-lists.

The lampson model is not flawed in the sense that it is strictly more
powerful than a real capability system.  The *paper* is flawed in the
sense that it lends itself to a variety of misunderstandings. tyler


e-lang mailing list