A Principled Approach to Policy Composition for Runtime Enforcement Mechanisms

Runtime enforcement mechanisms are an important and well-employed method for ensuring an execution only exhibits acceptable behavior, as dictated by a security policy. Wherever interaction occurs between two or more parties that do not completely trust each other, it is most often the case that a runtime enforcement mechanism is between them in some form, monitoring the exchange. Considering the ubiquity of such scenarios in the computing world, there has been an increased effort to build formal models of runtime monitors that closely capture their capabilities so that their effectiveness can be analysed more precisely. While models have grown more faithful to their real-life counterparts, is- sues concerning complexity and manageability (a common concern for software engineers) of centralized policies remains to be fully addressed. The goal of this thesis is to provide a principled approach to policy construction that is modular, intuitive, and backed by formal methods. This thesis introduces a class of policy combinators adequate for use with runtime en- forcement policies and analyses a particular instance of them called Static Committee Com- binators (SCCs). SCCs present a model of policy composition where combinators act as committees that vote on events passing through the monitor. They were conceptualized in collaboration with Jay Ligatti and Daniel Lomsak. The general class of combinators are called Static Decision Combinators (SDCs), which share key features with SCCs such as allowing combinators to respond with alternative events when polled, in addition to re- sponding with grants or denials. SDCs treat the base-level policies they compose as black boxes, which helps decouple the system of combinators from the underlying policy model. The base policies could be modelled by automata but the combinators would not maintain their own state, being static . This allows them to be easily defined and understood using truth tables, as well as analysed using logic tools. In addition to an analysis of SDCs and SCCs, we provide useful examples and a reusable combinator library