[cap-talk] Announcing "Analysing Object-Capability Security" Paper and Authodox v. 0.2.0

[Jonathan S. Shapiro]

On Fri, 2008-05-30 at 16:53 +0100, Toby Murray wrote:
> 2006: the first formal model for reasoning about capability-systems,
> cognizant of the ideas of the OCap model is produced [5]. This formal
> model allows one to reason about the behaviour of trusted entities
> within a system, in order to reason effectively about the system's
> security properties.

Your chronology is consistent with the work that I know about, with one
addition: Scott Doerrie is currently working on automating the
formalization of the 2000 confinement verification work.

I consider automation significant, and I'm sure that Fred and Toby will
agree. Where we may possibly differ (I have not discussed with them) is
on why, and in consequence on how to go about the automation.

First, let me back up some. As my dissertation work progressed, several
things became apparent to me:

  1. The opaqueness boundary at the OS/application layer is a problem,
     because it forces the OS to make mostly static, conservative
     assumptions about program behavior. For most programs this is fine,
     but there are two classes of important programs for which it is
     a problem:

     A  Trusted programs -- though the question here is "by whom". The
        underlying problem in OS-based capability systems is that the
        primitive capability weakening operations don't have enough
        information to weaken entry capabilities to trusted programs
        sensibly.

     B  Memoryless programs. There is a class of programs that require
        state for realistic implementations, but none of that state
        remains live when the program returns from a given request.
        The OS cannot see this. Functional programming doesn't help,
        because the compiled realization of a functional program is
        generally stateful.

  2. Reasoning about the correctness of the capability runtime (in my
     case, the OS) requires a formal model.

  3. Maintainability of security properties in evolving systems is
     a huge problem. If you cannot automate almost all of the property
     verification, you are pragmatically doomed. As supporting evidence,
     consider that only one A-1 system went through multiple certified
     versions.

  4. Given a formal model, it really ought to be possible to connect
     the capability invocation layer (which occurs at the level of
     application semantics) to the behavior within the OS (which occurs
     at the layer of the cap runtime formal model).

  5. Given that isolated operational semantic machines are composable,
     it should be possible to engage in modular reasoning in a
     capability based system.

Point [4] was still fairly inchoate in my mind at that time. It took a
comment by MarkM years later to bring it into clear focus: capability
semantics is the semantics of lambda calculus with side effects. There
are other semantic calculi that one might prefer; the key point was that
the point of connection between the program semantics and the abstract
machine semantics was unearthed by his statement. As with so many
flashes of clarity, I wondered how I could possibly have failed to see
it so completely for so long.

MarkM would later point out that the absence in the 2000 model of
designation was a significant shortcoming if the goal was to connect the
two layers. One of the very early models that Sam and I built still had
it. It was removed at some point as a simplification. The consequences
of that removal weren't relevant to our immediate goal, and probably
shrunk the paper enough to make the difference between published and not
publishable, but I'm pleased to say that Scott Doerrie's work has
preserved the indexing of capabilities in his model with no substantive
effort required.


In any case, the kind of formalization that I am really interested in
here is the kind that lets us reason about the composition of
operational machines and the analysis of real programs in source (or at
least AST) form. CSP is a fine modeling tool, and it has its place, but
it doesn't really fit my objectives. With CSP, I can analyze an abstract
model of a program, but I cannot really analyze the program itself.

Further, I am interested in models that support systems programming
languages, because I do not anticipate Haskell (or whatever) taking over
this part of the world in my reasonably expected lifespan.



shap