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

[Jonathan S. Shapiro]

On Fri, 2008-05-30 at 10:35 -0700, Charles Landau wrote:
> I'm getting confused between formal models, informal models, and 
> non-models.
> 
> KeyKOS clearly had no formal model. If it was an informal model, then I 
> have to disagree with the above. For example, KeySafe [1] was a subject 
> operating outside the kernel, so it had limited authority, and it 
> further limited the authority of others.
> 
> So is KeyKOS a non-model that contributed to later models?

Charlie:

You're getting confused because it really is confusing. Let me try first
to define terms, and then try to answer your question about KeyKOS.

  informal model:  A model that is expressed in natural language (e.g.
     English). This type of model can be very useful, but it is rarely
     comprehensive and it is very hard to maintain. The root problems
     are:

        Comprehensive modeling is hard (this is equally true for formal
        models)

        Natural language just isn't very well suited to expressing
        mathematically precise concepts.

  formal model: A model that is expressed using some mathematical
     formalism, or perhaps in some facilitating modeling language
     (e.g. CSP) that is itself directly and umambiguously reducible
     to one or more mathematical formalisms. The root problems here
     are:

        Programs are bloody difficult things to make precise.

        Mathematics is an alien notation in the eyes of most people,
        and even in the eyes of most programmers.

        Formal models are often abstractions of real systems, and
        the abstraction is usually specific to the question you are
        asking at any given time. This introduces the likelihood that
        two variant abstract models of the same system which are
        constructed for two different questions may not be consistent
        with each other.

  automated formal model: A formal model that has been captured in 
     some form of automated theorem proving infrastructure.

So on to your question about KeyKOS.

At a minimum, KeyKOS is a model in the trivial sense: every programming
language is a mathematical formalism, and therefore every program is a
model (and, in fact, a formal model) of itself.

In a more useful sense, KeyKOS implicitly embodies a model in the sense
that there is a (relatively) straightforward state space and operational
semantics associated with the KeyKOS object layer (as seen by the
kernel). This model was captured formally in the paper I wrote with Sam
Weber. To my knowledge, the only "important" thing that we abstracted
out was capability indexing, and that was actually included in an early
version of the model.

KeyKOS+KeySafe is *not* a model, because (a) the combined artifact has
never been expressed as a model in unified form, and (b) the individual
artifacts (and their supporting programs, e.g. space bank) have not been
expressed individually in any form where their composition (i.e. their
interactions) could be examined.

In my characterization of models as "part of the platform" vs. "modeled
as subject", I was sloppy. I was referring there entirely to formal
models and formal modeling techniques (to date).

In my opinion, the part of KeyKOS that has contributed (so far) most
strongly to later models is the object system and the atomicity proper.
Because these were so straightforward in the KeyKOS design, it was
possible to extract a formal model for general capability systems by
starting from the model implicitly defined within KeyKOS.

I say "implicitly" in the formal modeling sense. The KeyKOS design was
clearly very explicit and very well thought out, but it wasn't the
purpose of KeyKOS to define a general formal model for capability
systems.


I'm not sure if this answer makes your confusion better or worse... :-)



shap