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

[Charles Landau]

Mark Miller wrote:
> 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. All earlier models, including those Shap cites above, force
> the modeler to choose, for each component of the system, whether it is
> 
> a) modeled as part of the platform -- in which case its authority
> limiting behavior can be relied on, but its own authority is
> unlimited, or
> 
> b) modeled as a subject operating within the rules created by the
> platform, in which case its own authority can be limited, but it is
> presumed hostile.
> 
> The authority limiting behavior of #b cannot be modeled in these
> systems, and so these models cannot account for security arrangement
> in which one relies on their behavior -- except by promoting these
> subjects into category #a.
> 
> By forcing the modeler to chose between #a and #b, these models
> effectively hid the possibility (and the practice) of unprivileged
> access control abstractions.

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?

[1] http://www.cis.upenn.edu/~KeyKOS/agorics/KeyKos/keysafe/Keysafe.html