Computer Security and Trust
Theme leader: Helge Janicke
In this research theme we are working on the identification and formalisation of classes of security requirements for Distributed Information Systems. We are specifically addressing access control, obligations, delegation control and information flow with respect to system or user behaviours. Our foundational work on controlling system behaviours using policy-based approaches and policy enforcement lead to wider research interests, including: end-to-end security in ad-hoc networks, behaviour modelling of malign software entities, social and analytical aspects of Information System Security and the management of Trust in collaborative systems. We are recently started to apply our expertise on behavioural modelling and analysis to Forensics.
Policy based managementUnder this research theme, we have been involved in the identification and formalisation of classes of security policies (initially, authorisation, obligation, delegation and privacy) for System of Systems (SoSs). Authorisation policies define what a system within an SoS is permitted or not permitted to do. They constrain the information made available to other systems and the operations they are permitted to perform on the managed information. Obligation policies define what a system must or must not do and hence guide the decision making process - the system has to interpret and validate policies (in terms of, e.g. conflict resolution) in order to achieve the overall objectives of an SoS. Fundamental to the model is that it allows for the dynamic change of policies in an SoS environment as well as integrating security requirement with both functional and temporal properties in a uniform fashion.. This permits it to adapt to evolutionary changes in the system, its environment and to new security policies. To ensure its soundness, the model is formalised using a logic-based approach.
In ITL a system is modelled as a set of behaviours. A behaviour is a (in)finite non-empty sequence of states, whereas a state is a mapping of variables to values. We defined a set of variables to model security. For example, authorizations are modelled as a boolean array autho, so that autho(s,a,o) is true if subject s is allowed to perform action a on object o. Then policies are expressed as safety formulas, stating how these variables are constrained over time. For example an authorization policy specifies how authorizations are granted over time. These contraints are formulated as (policy) rules.
Delegation is a mechanism that enables a subject to delegate some of its rights to another subject for it to act on its behalf. In discretionary access control whereby access restrictions are based on the identity of subjects, delegation of right is at the discretion of subjects. This means that the initiative to delegate is taken by subjects and not the security manager. However it should be possible to control delegations through access control policy to ensure security, especially in systems allowing cascaded delegations. In this respect, a delegation policy in our framework specifies the ability of subjects (grantors) to pass on some (or all) of their rights to other subjects (grantees) to perform actions on their behalf. Similar to authorisations, delegations are modelled as a boolean array.
Our framework has been successfully applied to healthcare systems in which delegations, for example, can be used to model the principal of patient consent. This principle stipulates that patient must consent to data sharing or any disclosure of personal health information. For example patients must be made aware that information may be shared between members of care team or different hospital departments such as Radiology, Surgery and Medicine.
Our framework also supports positive and negative authorisations/delegations. Positive authorisations specify permissions while negative ones specify denials. This provides an expressive model that can handle various kinds of policies such as open, closed and hybrid policies. The later, unlike the others, allows positive and negative authorisations/delegations within specifications. Therefore conflicting authorisations (delegations) might be derived from rules. Specific rules are provided to resolve conflicts within specifications. Furthermore, a security policy must determine at any time access rights of each subject with respect to any objects and any actions. Writing a complete specification to state this can be very complex and cumbersome. It is convenient to have a specification that contains only variables which are constrained to change eventually, other variables being assumed stable in the scope of the specification. Default rules have been used in some frameworks as a way to provide complete specification. The drawback of this approach is that defaults rules might not be conclusive. As a consequence the model can lead to a situation which an authorisation request has no answer. In this respect, we used the concept of default value which is conclusive compared to default rules. The idea is that when a variable is not explicitly assigned a value, it implicitly takes the default value.
Algebra for policy composition was developed, based on a rich set of operators including Boolean connectives and temporal modalities for building complex policies. The algebra specifies a simple policy as a collection of policy rules. A policy rule describes how new rights are inferred. The algebra provides operators for rule management (e.g. adding or removing rules from policies.) Then compound policies are devised by composing simpler ones using a rich set of operators, such as sequential composition, parallel composition, and nondeterministic choice. More importantly, some operators are introduced to model dynamic changes in policies. Sound algebraic laws for such operators are investigated and can be used to prove the equivalence and the refinement relationship among policies.
One advantage of our logical framework is that the properties of policies can be formulated and verified in the same logic. We have developed a set of compositional rules for policy verification and analysis. As an illustration, we formalise the concept of information flow permissible in an access control policy and analyse policies w.r.t. this property. We understand by permissible information flows those flows that are allowed by the security policy.
Based on the identification of security requirements we have designed
a linguistic constructs for expressing a sufficiently large class of
policies. A sound specification-oriented semantics for these
constructs has also been given. Continual Enforcement is a mechanism
that ensures an SoS satisfies a given set of security policies in
real-time. Further, it seamlessly adapts to changes in the environment
(e.g. changes in NGO policies/ battlefield strategies or the
occurrence of epidemic diseases w.r.t. healthcare). We have developed
efficient algorithms and heuristics for continual security
enforcement. Specifically, we have considered two types of
architectural design within the architecture-trajectory: Security
Enforcer and Vigilant SoS.