[e-lang] Thesis: Analysing the Security Properties of Object-Capability Patterns

[Toby Murray]

(Apologies for cross-posting.)

Hi all on cap-talk and e-lang,

I recently completed my D.Phil. (PhD) thesis that investigated how to
apply the process algebra CSP to model and formally reason about the
security properties of object-capability patterns (i.e. to prove that
reusable security-enforcing capability-based abstractions actually
enforce the security properties they claim to).

This thesis owes a great debt to many on these lists, so thanks to
everyone who has posted here since I've been following during the past
6 years. I've learnt so much from all of you. I certainly wouldn't
have done a doctorate on object-capability security if these lists
didn't exist.

The thesis is presently available here:
http://web.comlab.ox.ac.uk/publications/publication3612-abstract.html

The abstract follows this message.

It was examined in Oxford on March 22nd by Dr Fred Spiessens and Prof
Bill Roscoe, after which point it underwent some small but important
revisions in order to arrive at its current form. My thanks to each of
them, especially for the revisions that they suggested which have
helped make this thesis noticeably stronger.

Finally, since this thesis was examined, I've left Oxford and moved
back to Australia and am now working for NICTA on their Trustworthy
Embedded Systems project (http://ertos.nicta.com.au/), which is the
successor to their seL4 and l4.verified projects that last year
produced the world's first formally verified object-capability
microkernel. Future work on seL4 will focus, amongst other things, on
building a framework to produce formally verified application-level
software that runs atop the microkernel, as well as proving specific
security properties of the microkernel itself (that are not covered by
the current functional correctness proof), e.g. relating to how the
distribution of capabilities in a system affects the authority of each
application-level component.

Please feel free to reply to this message, or to send me a private
message, with any specific queries about the thesis.

Thanks again

Toby

---------------------
Analysing the Security Properties of Object-Capability Patterns
by Toby Murray
Oxford University Computing Laboratory

Abstract:

The object-capability model is an increasingly popular architecture for
building secure software systems. This model promotes the construction of
reusable patterns for enforcing security properties within object-capability
systems. In this thesis, we apply the process algebra CSP, and its
automatic refinement-checker FDR, to analyse object-capability patterns and
prove whether they uphold the security properties they are designed to
enforce.
    We show how CSP can accurately model object-capability systems and
patterns, and express their wide variety of features.
    We show that complex safety properties of object-capability patterns can
be reasoned about by encoding them as CSP refinement checks for FDR.
This enables one to detect vulnerabilities automatically in patterns due to
concurrent and recursive invocation.
    We show that CSP’s theory of data-independence can be applied to
allow one to generalise the results obtained from analysing small fixed-sized
systems, to systems of arbitrary size.
    We show how to reason about the information flow properties of object-
capability patterns. We argue that in order to do so sensibly, one must make
the assumption that objects can directly influence each other only through
their overt interactions together. We show how traditional noninterference
properties can be adapted to take this assumption into account, and how
they can then be tested with FDR.
    We consider how to reason about liveness properties of object-capability
patterns under necessary fairness assumptions. We prove that such proper-
ties cannot always be expressed as CSP refinement checks for FDR, making
them impossible for FDR to test precisely, but how FDR can be applied to
reason about them by testing sufficient conditions for them instead.
    To reason about authority, we develop a framework for expressing
general non-causation properties and show how it can capture various kinds of
authority, as well as the notions of defensive correctness and defensive
consistency. We show that, for deterministic systems, non-causation of safety
effects can be expressed as refinement checks in CSP models that FDR can
support. However, for nondeterministic systems, we prove that even certain
simple non-causation properties cannot be precisely captured this way.