K.: Transformational approach to facilitate monitoring of high level policies

We present a method for specifying high level security policies that can be en-forced by runtime monitoring mechanisms. The method has three main steps: (1) the user of our method formalizes a set of policy rules using UML sequence diagrams; (2) the user selects a set of transformation rules from a transforma-tion library, and applies these using a tool to obtain a low level intermediate policy (also expressed in UML sequence diagrams); (3) the tool transforms the intermediate low level policy expressed in UML sequence diagrams into a UML inspired state machine that governs the behavior of a runtime policy enforce-ment mechanism. We believe that the method is both easy to use and useful since it automates much of the policy formalization process. The method is underpinned by a formal foundation that precisely defines what it means that a system adheres to a policy expressed as a sequence dia-gram as well as a state machine. The foundation is furthermore used to show that the transformation from sequence diagrams to state machines is adherence preserving under a certain condition.