Why do we need formal representation of Security policies

Resource: Wissam Mallouli, Fayc ̧al Bessayah, Ana R. Cavalli, and Azzedine Benameur. Security rules specification and analysis based on passive testing. In Proc. of the Global Communications Conference on Exhibition and Industry Forum Co-located with WTC (GLOBECOM’08), New Orleans, LA, USA, pages 2078–2083. IEEE, November-December 2008.

"A security policy is a set of rules that defines the desired behavior of users within an information system. Its main goal is to describe how data and other critical system resources are protected. If a security policy is written in a natural language specifying for example: ‘file F is only accessible from terminal T in the context C’, it will be very difficult to verify its correct implementation using an automatic testing approach because it is a completely informal specification. Consequently, if such verification is not performed, there is no guarantee that the security rules of the system are properly implemented".

"To guarantee that the system respects its security policy, we can rely on formal testing based methods. The main ones are (i) the active testing which validates a system implementation by applying a set of security test cases and analyzing its reaction and (ii) the monitoring (or passive testing) that consists in observing, during the execution, whether the system behavior is conform according to its functional and security formal specification".

"To perform this analysis, we rely on a dedicated formal language to describe the security requirements of the system. Then, we check using well adapted algorithms whether these security rules are verified on the collected traces to deduce the appropriate verdict about the system security conformance".

W. Mallouli, J.-M. Orset, A. R. Cavalli, N. Cuppens-Boulahia, and F. Cuppens. A formal approach for testing security rules. In V. Lotz and B. M. Thuraisingham, editors, SACMAT, pages 127–132. ACM, 2007. 

To ensure that a certain level of security is always maintained, the system behavior must be restrained by a security policy. A security policy is a set of rules that regulates the nature and the context of actions that can be performed within a system, according to specific roles. As an exam- ple, such policy can tackle the interactions between a network infrastructure and Internet or manage accounts and rights toward an operating system or a database. Generally, a security policy is written by the mean of a natural lan- guage specification, containing statements such as “this file must be accessible only to authorized users” or “all ports are closed except for 21 (ftp), 22 (ssh) and 80 (www)”.

The main problem is that it is quite difficult to verify whether a system implementation conforms to its policy. However, if one can not ensure this conformance, the global security can not be guaranteed anymore. Most current work only concentrate to define meta-languages in order to ex- press security policies and provide unambiguous rules. Once the security policy is formally specified, it is essential to prove that the target system imple- ments this policy by (1) injecting this policy in the system considered or (2) specifying formally the target system and generating proofs that this system implements the security policy or (3) by considering several strategies of formal tests.

Completeness of policy refinement

Source: N. Damianou, A. Bandara, M. Sloman, and E. Lupu. A Survey of Policy Specification Approaches. Technical re- port, Department of Computing, Imperial College of Science Technology and Medicine, London, 2002.

The objective of policy refinement is to transform high-level policy specifications into more specific policies that would be better suited for use in different execution environments.

Definition: (Policy Refinement) If there exists a set of policies Prs:p1, p2, .. pn, such that the enforcement of a combination of these policies results in a system behaving in an identical manner to a system that is enforcing some base policy Pb, it can be said that Prs is a refinement of Pb. The set of policies Prs:p1, p2, .. pn is referred to as the refined policy set.

A policy refinement can be said to complete iff all the following properties hold:
1.    Correctness: a refinement is said to be correct if there exists a subset of the refined policy set such that the conjunction of all the members of that subset is also a refinement of the base policy.
2.    Consistency: refinement is said to be consistent if there are no conflicts between any of the policies in the refined policy set.
3.    Minimality: a refinement is said to be minimal if it is correct and if removing any policy from the refined policy set causes the refinement to be incorrect.

Handling Conflicts between policies

Source: N. Damianou, A. Bandara, M. Sloman, and E. Lupu. A Survey of Policy Specification Approaches. Technical re- port, Department of Computing, Imperial College of Sci-
ence Technology and Medicine, London, 2002.


Jajodia et al. 1997, proposes that a conflict, once detected could be handled in one of three ways. The most obvious and simplest one is for the system to declare an error condition whenever a conflict arises. However, this solution is not particularly interesting since it does not allow for the system to automatically recover from the conflicting scenario. Other solutions are to allow the positive policy to override; or to let the negative policy override. The latter strategy is adopting an approach of ‘‘do no harm’’, based on the assumption that the negative policy (i.e. the one that prevents an action being performed) has a more benign effect on the system than its conflicting counterpart. As would be expected, the positive policy override strategy is the exact converse of the negative override approach described.

In addition to the negative and positive override strategies mentioned above, [Lupu and Sloman 1999] also identifies some alternatives. One approach suggested is to assign explicit priorities to every policy. This way when a conflict arises the agent enforcing the policy could simply compare the priority values and enforce the policy that has the highest priority. However, this approach could easily lead to inconsistent behaviour of the system if, as is common in distributed systems, multiple people are responsible for defining policies and assigning their priorities. Other strategies suggested include giving priority to the policy that is ‘closest’ to the managed object; or using the specificity of the policy definition to determine the priority.

[Moffet and Sloman 1993] introduces the idea of policy hierarchies and the application of policy refinement to derive lower-level, more specific policies from high-level ones.
policy refinement is to transform high-level policy specifications into more specific policies that would be better suited for use in different execution environments.