A Programmable Enforcement Framework for Security Policies

This thesis proposes the MAP-REDUCE framework, a programmable framework, that can be used to construct enforcement mechanisms of different security policies. The framework is based on the idea of secure multi-execution in which multiple copies of the controlled program are executed. In order to construct an enforcement mechanism of a policy, users have to write a MAP program and a REDUCE program to control inputs and outputs of executions of these copies. This thesis illustrates the framework by presenting enforcement mechanisms of non-interference (from Devriese and Piessens), non-deducibility (from Sutherland) and deletion of inputs (a policy proposed by Mantel). It demonstrates formally soundness and precision of these enforcement mechanisms. This thesis also presents the investigation on sufficient condition of policies that can be enforced by the framework. The investigation is on reactive programs that are input total and have to finish processing an input item before handling another one. For reactive programs that always terminate on any input, non-empty testable hypersafety policies can be enforced. For reactive programs that might diverge, non-empty downward closed w.r.t. termination policies can be enforced.