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

[Toby Murray]

On Fri, 2008-05-30 at 10:23 -0400, Jonathan S. Shapiro wrote:
> On Fri, 2008-05-30 at 01:02 +0100, Toby Murray wrote:
> > On Thu, 2008-05-29 at 23:09 +0100, lists at notatla.org.uk wrote:
> > > Toby Murray <toby.murray at comlab.ox.ac.uk> wrote:
> > > 
> > > > [The OCap model is totally Mark Miller's creation, btw. Hopefully he'll
> > > > chime in if I've messed up any of the above.]
> > > 
> > > So that only dates from ~2006 and is totally different from the work
> > > in KeyKOS etc?
> > >  
> > 
> > The OCap model dates from as early as 2003, if not before. It was first
> > described properly in "Paradigm Regained: Abstraction Mechanisms for
> > Access Control", although the term may be older than that.
> 
> The OCap model is an outgrowth of many years of work, and I think it is
> safe to say that it is heavily influenced by systems like KeyKOS.
> Earlier attempts to capture this model:
> 
>   Shapiro, Weber. "Verifying the EROS Confinement Mechanism",
>      2000 IEEE Symposium on Security and Privacy, 2000
> 
>   Lawrence Snyder. "On the Synthesis and Analysis of Protection 
>      Systems", 6th ACM Symposium on Operating Systems Principles, 1977
> 
> Each of these differs in some particulars from the OCap model as it
> stands today. The OCap model is a refinement of the earlier work, with
> some significant new ideas.

The OCap model differs significantly from the earlier work cited in that
it is an informal model. In contrast, the other models are formal models
with rigorously defined semantics. The OCap model, on its own, cannot be
used to formally reason about OCap systems. In order to reason about
OCap systems, one needs to embed the OCap model in another formalism.

Fred Spiessens created his own formalism, Knowledge-Behaviour Models, in
order to do this. I'm using an existing one, namely CSP.

Note that I'm not arguing for the formalisation of the OCap model, since
I think it would be very difficult to formalise in a way that would make
everyone happy. I prefer having it as an abstract, informally defined
concept that can be reliably formalised in many different ways, each of
which has its own advantages and disadvantages. For instance, in CSP I
can reason about causation, but can only consider finite-state systems.
KBMs cannot (at present) reason about causation but have their own
advantages.

Cheers

Toby