A theory of constructive and predictable runtime enforcement mechanisms

Nowadays owners and users of software systems want their executions to be reliable and secure. Runtime enforcement is a common mechanism for ensuring that system or program executions adhere to constraints specified by a security policy. It is based on two properties: the enforcement mechanism should leave legal executions without changes(transparency) and make sure that illegal executions are amended (soundness). From the theory side, the literature proposes the precise characterization of legal executions that represent a security policy and thus is enforced by mechanisms like security automata or edit automata. Unfortunately, transparency and soundness do not distinguish what happens when an execution is actually illegal (the practical case). They only tell that the outcome of an enforcement mechanism should be "legal", but not how far the illegal execution should be changed. In this thesis we address the gap between the theory of runtime enforcement and the practical case. First, we explore a set of policies that represent legal executions in terms of repeated legal iterations and propose a constructive enforcement mechanism that can deal with illegal executions by eliminating illegal iterations. Second, we introduce a new notion of predictability, that puts a restriction on the way illegal executions are modified by an enforcement mechanism. Third, we propose an automatic construction of enforcement mechanisms that is able to tolerate some insignificant errors of the user and we prove it to have a sufficient degree of predictability. The main case study of this thesis is a business process from a medical organization. A number of discussions with the partners from this organization shows the validity of the approaches described in this thesis in practical cases.