Analysing the Security Properties of Object−Capability Patterns
Toby Murray · 2010
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 renement-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 renement 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 xed-sized systems, to systems of arbitrary size. We show how to reason about the information ow properties of objectcapability patterns. We argue that in order to do so sensibly, one must make the assumption that objects can directly in uence 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 properties cannot always be expressed as CSP renement checks for FDR, making them impossible for FDR to test precisely, but how FDR can be applied to reason about them by testing sucient 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 con- sistency. We show that, for deterministic systems, non-causation of safety eects can be expressed as renement 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.