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.

Complex software-security policies are dicult to specify, understand, and update. The same is true for complex software in general, but while many tools and techniques exist for decomposing complex general software into simpler reusable modules (packages, classes, functions, aspects, etc.), few tools exist for decomposing complex security policies into simpler reusable modules. The tools that do exist for modularizing policies either encapsulate entire policies as atomic modules that cannot be decomposed or allow ne-grained policy modularization but require expertise to use correctly. This dissertation presents a policy-composition tool called PoliSeer [27, 26] and the PoCo policy-composition software-security language. PoliSeer is a GUI-based tool designed to enable users who are not expert policy engineers to exibly specify, visualize, modify, and enforce complex runtime policies on untrusted software. PoliSeer users rely on expert policy engineers to specify universally composable policy modules; PoliSeer users then build complex policies by composing those expert-written modules. This dissertation describes the design and implementation of PoliSeer and a case study in which we have used PoliSeer to specify and enforce a policy on PoliSeer itself. PoCo is a language for specifying composable software-security policies. PoCo users specify software-security policies in terms of abstract input-output event sequences. The policy outputs are expressive, capable of describing all desired, irrelevant, and prohibited events at once. These descriptive outputs compose well: operations for combining them satisfy a large number of algebraic properties, which allows policy hierarchies to be designed more simply and naturally. We demonstrate PoCo's capability via a case study in which a sophisticated policy is implemented in PoCo.

Student mobility in the area of Higher Education (HE) is gaining more attention nowadays. It is one of the cornerstones of the Bologna Process being promoted at both national and international levels. However, currently there is no technical system that would support student mobility processes and assist users in authoring educational curricula involving student mobility. In this study, the problem of student mobility programmes generation based on existing modules and programmes is considered. A similar problem is being solved in an Intelligent Tutoring Systems field using Curriculum generation techniques, but the student mobility area has a set of characteristics limiting their application to the considered problem. One of main limiting factors is that mobility programmes should be developed in an environment with heterogeneous regulations. In this environment, various established routines and regulations are used to control different aspects of the educational process. These regulations can be different in different domains and are supported by different authors independently. In this thesis, a novel framework was developed for generation of student mobility programmes in an environment with heterogeneous regulations. Two core technologies that were coherently combined in the framework are hierarchical planning and policy-based management. The policy-based planner was designed as a central engine for the framework. It extends the functionality of existing planning technologies and provides the means to carry out planning in environments with heterogeneous regulations, specified as policies. The policy-based planner enforces the policies during the planning and guarantees that the resultant plan is conformant with all policies applicable to it. The policies can be supported by different authors independently. Using them, policy authors can specify additional constraints on the execution of planning actions and extend the pre-specified task networks. Policies are enforced during the planning in a coordinated manner: situations when a policy can be enforced are defined by its scope, and the outcomes of policy evaluation are processed according to the specially defined procedures. For solving the problem of student mobility programme generation using the policy-based planner, the planning environment describing the student mobility problem area was designed and this problem was formalised as a planning task. Educational processes valid throughout the HE environment were formalised using Hierarchical Task Network planning constructs. Different mobility schemas were encoded as decomposition methods that can be combined to construct complex mobility scenarios satisfying the user requirements. New mobility programmes are developed as detailed educational processes carried out when students study according to these programmes. This provides the means to model their execution in the planning environment and guarantee that all relevant requirements are checked. The postponed policy enforcement mechanism was developed as an extension of the policy-based planner in order to improve the planning performance. In this mechanism, future dead-ends can be detected earlier during the planning using partial policy requests. The partial policy requests and an algorithm for their evaluation were introduced to examine policies for planning actions that should be executed in the future course of planning. The postponed policy enforcement mechanism was applied to the mobility programme generation problem within the descending policy evaluation technique. This technique was designed to optimise the process of programme components selection. Using it, policies for different domains can be evaluated independently in a descending order, gradually limiting the scope for the required component selection. The prototype of student mobility programme generation solution was developed. Two case studies were used to examine the process of student mobility programmes development and to analyse the role of policies in this process. Additionally, four series of experiments were carried out to analyse performance gains of the descending policy evaluation technique in planning environments with different characteristics.

Organisations such as governments and healthcare bodies are increasingly responsible for managing large amounts of personal information, and the increasing complexity of modern information systems is causing growing concerns about the protection of these assets from insider threats. Insider threats are very difficult to handle, because the insiders have direct access to information and are trusted by their organisations. The nature of insider privacy breaches varies with the organisation’s acceptable usage policy and the attributes of an insider. However, the level of risk that insiders pose depends on insider breach scenarios including their access patterns and contextual information, such as timing of access. Protection from insider threats is a newly emerging research area, and thus, only few approaches are available that systemise the continuous monitoring of dynamic insider usage characteristics and adaptation depending on the level of risk. The aim of this research is to develop a formal framework for an adaptive early warning and response system for insider privacy breaches within dynamic software systems. This framework will allow the specification of multiple policies at different risk levels, depending on event patterns, timing constraints, and the enforcement of adaptive response actions, to interrupt insider activity. Our framework is based on Usage Control (UCON), a comprehensive model that controls previous, ongoing, and subsequent resource usage. We extend UCON to include interrupt policy decisions, in which multiple policy decisions can be expressed at different risk levels. In particular, interrupt policy decisions can be dynamically adapted upon the occurrence of an event or over time. We propose a computational model that represents the concurrent behaviour of an adaptive early warning and response system in the form of statechart. In addition, we propose a Privacy Breach Specification Language (PBSL) based on this computational model, in which event patterns, timing constraints, and the triggered early warning level are expressed in the form of policy rules. The main features of PBSL are its expressiveness, simplicity, practicality, and formal semantics. The formal semantics of the PBSL, together with a model of the mechanisms enforcing the policies, is given in an operational style. Enforcement mechanisms, which are defined by the outcomes of the policy rules, influence the system state by mutually interacting between the policy rules and the system behaviour. We demonstrate the use of this PBSL with a case study from the e-government domain that includes some real-world insider breach scenarios. The formal framework utilises a tool that supports the animation of the enforcement and policy models. This tool also supports the model checking used to formally verify the safety and progress properties of the system over the policy and the enforcement specifications.

Code modularization provides benefits throughout the software life cycle; however, the presence of crosscutting concerns (CCCs) in software hinders its complete modularization. Traditional modularization techniques work well under the assumption that code being modularized is functionally orthogonal to the rest of the code; as a result, software engineers try to separate code segments that are orthogonal in their functionality into distinct modules. However, in practice, software does not decompose neatly into modules with distinct, orthogonal functionality. In this thesis, we investigate the modularization of CCCs in software using two different techniques. Firstly, we discuss IVCon, a GUI-based tool that provides a novel approach to the modularization of CCCs. We have designed IVCon to capture the multi-concern nature of code. IVCon enables users to create, examine, and modify their code in two different views, the woven view and the unwoven view. The woven view displays program code in colors that indicate which CCCs various code segments implement, while the unwoven view displays code in two panels, one showing the core of the program and the other showing all the code implementing each concern in an isolated module. IVCon aims to provide an easy-to-use interface for conveniently creating, examining, and modifying code in, and translating between, the woven and unwoven views. Secondly, we discuss LoPSiL, which is a location-based policy-specification language. LoPSiL is Turing-complete and provides users with language constructs that enable them to manipulate location information; hence, LoPSiL can be used to specify and enforce generic policies that might involve location-based constraints. We have implemented a LoPSiL compiler using AspectJ, and we observe and discuss how the use of traditional units of modularization---aspects in this case---help modularize functionally orthogonal CCCs such as security and auditing.