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

[Toby Murray]

On Fri, 2008-05-30 at 08:11 -0700, Mark Miller wrote:
> On Fri, May 30, 2008 at 7:35 AM, Toby Murray
> <toby.murray at comlab.ox.ac.uk> wrote:
> >> 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.
> 

For posterity's sake, the two quoted lines above were written by shap,
as are the following lines:

> >> 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.
> 
> Certainly. The OCap model owes a tremendous debt to these earlier works.

I wrote this:
> > The OCap model differs significantly from the earlier work cited in that
> > it is an informal model.

> Toby, I agree with everything you're saying, but I'd also like to call
> attention to the issue that I consider the most important innovation
> in the OCap model: The ability to explain the authority limiting
> behavior of subjects that are themselves operating within limited
> authority. 

[I know you know this but for others following this discussion] Fred
Spiessens' work perhaps makes the best arguments for the need for better
formal models that capture this fundamental new idea that the OCap model
embodies informally.

In this sense, the OCap model is strange in that it is one of the most
important influences on formal models for capability systems, despite
being informal itself.

My own take on the development of formal models for reasoning about
capability-based systems is something like this:

Late 70s: the first formal model is introduced, namely the Take-Grant
model [1]. This saw a lot of refinement throughout the coming decades
and variants of it are still being used today [2].

2000: the first real-world application of a (new, decidable) formal
model to an existing capability system to verify a critical security
property is performed, specifically in the context of verifying the EROS
confinement mechanism [3]. While showing the usefulness and viability of
these kinds of formal models, this work provided the first decidable
formal model able to reason not only about capability propagation in an
OS but also about "indirect" access that arises when
capabilities-to-pages are used to define a process's address space.

2003: the informal object-capability model is proposed [4]. The idea
that reasoning about the behaviour of entities is vitally important in
order to properly reason about security properties in capability-based
systems is explicitly recognised. The paradigm of "security enforcing
abstractions" has been regained.

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.

Each of the events in this timeline is influenced by those that came
before it.

I'd be curious to know how this lines up with others'?

This discussion has been great since before it took place, I'm not sure
I could have written such a useful timeline as the one above. Certainly,
this has clarified my own thinking on the relationship between the OCap
model and the formal models and how each influenced the other.

Thanks heaps

Toby