Idea Transcript
Specifying a Security Policy: A Case Study Fr´ed´eric Cuppens and Claire Saurel ONERA-CERT 2 Av. E. Belin 31055, Toulouse Cedex France email: cuppens,saurel @cert.fr fax: +(33) 62 25 25 93
Abstract The objective of this paper is to assist the security administrators, in their attempt to specify, define and formalize security policies suited to a given high risk environment. It is then possible for the administrators to automatically derive consequencies of these policies. In particular, we want to provide users with the following functionalities:
system against any threat of its security properties (confidentiality, integrity and availability). Not surprisingly, several successive steps are necessary for a security methodology:
Query a given security policy.
The first one consists of a risk analysis: which are the threats we want the system to be protected against? What are their characteristics? This first work is generally not an easy task: a lot of information may be implicit and informal, so that it may be quite long and fastidious to extract an exhaustive set of threats.
Verify that properties such as consistency and completeness are enforced by a given policy.
Verify that a given situation does not violate the security policy. Investigate interoperability problems between several security policies.
In this paper we more precisely focus on the problem of security policies formalization. We want to get a generic approach, being as much domain-independent as possible. In order to achieve the above goals, we have chosen a logicbased approach. It combines a deontic logic to model the concept of permission, obligation and prohibition with a modal logic of action. It also includes the possibility to deal with additional concepts such as role, responsibility and delegation. We shall illustrate this approach through a case study: a regulation whose purpose is to define means to protect secret data related to the National Defense.
1. Introduction Given a system to be designed, the final issue is to provide the security administrators with security policy specifications, in order to efficiently and sufficiently protect the
Given a set of threats, the second step consists in specifying a security policy to combat them. A security policy may have various abstraction level according to ITSEC classification [6]: it may be a Corporate Security Policy, a System Security Policy, or a Technical Security Policy. All organizations generally have security standards that apply to all systems within the organization and define the security relationship between the organization and the outside world. Using the ITSEC terminology, these standards represent the Corporate Security Policy. The System Security Policy then specifies the security measures that regulate how sensitive information and other resources are managed, protected and distributed within a specific system. These security measures are to be defined in a way which is consistent with the Corporate Security Policy. Finally, the measures of a System Security Policy that apply to the hardware and software of an Information Technology system may be separated from the remainder of the System Security Policy and defined in a separate document: the Technical Security Policy.
The work related in this paper focuses on the second step, especially the formalization and analysis of an already defined security policy. We want our methodology to be as much domain-independent as possible, and reusable. We
also want it to fit with all levels of abstraction a security policy may have. In particular, it should be applied to specify a Corporate, a System or a Technical Security Policy. In our approach, we assimilate a security policy to a specific case of regulation. A regulation may be viewed as composed of agents, events and objects of the system to be regulated; it aims at defining what actions the agents are permitted, obliged or prohibited to do. We distinguish between two classes of constraints:
natural language. Our illustration only deals with the information protection part. What are the main concepts used to specify this security policy? Actually, as the document uses a quite large subset of natural language, its expressiveness is very rich. Most of classical deontic concepts, such as obligation, permission and prohibition, are present. We give some examples:
1. The constraints to be enforced by the agents when they perform actions on the system objects.
The transmitter of a classified document is obliged to update the document classification as soon as it is possible, i.e. immediately after the transmitter estimates the document classification is obsolete (that means, the result of its classification evaluation does not fit with the classification of the document).
2. The constraints to be enforced by agents when they interact with other agents. In this case, the regulation may use various concepts such as the concepts of responsibility, delegation, hierarchical authority and so on...
Any agent who is not the transmitter of a classified document is prohibited to change the classification of this document.
In order to meet all former constraints, we choose a logicbased approach because of the following triple advantage:
It represents a universal formal language, useful for expressing any kind of knowledge and data. We shall illustrate how it may be used in the case of a regulation.
The possibility of formal calculus methods it may support, useful to help users to reason about the regulation.
The holder of a classified document is permitted to ask the transmitter to revise the classification of this document.
The instruction uses other organizational concepts such as the concepts of responsibility and delegation. For instance:
The existence of running tools which support a logical theory (several kinds of PROLOG and other theorem provers).
Every organization which holds some secret documents is obliged to designate an agent who is responsible for preserving these documents.
The remainder of this paper is organized as follows. We first introduce a case study we shall use to illustrate our approach. We define the deontic language we use to formalize policies, and show how our case study is formalized within it. We then present several types of practical applications that can be developed using such a formalism. We finally propose a comparison with other related works and a discussion of some difficulties that raised along this work of formalization, and which represent further work that remains to be done.
If it is decided to send a classified document, then the sending office is obliged to establish a consignment note of this document. The head of this office is obliged to sign this note. The head of this office is permitted to delegate the obligation to sign the note to one of his representatives.
We also have to represent the concepts of actions and events. In our model, the execution of an action is associated with the occurrence of an event, in the sense that, by performing an action, an agent causes an event to occur, which in turn will possibly cause other events to also occur. For instance:
2. A case study Our approach is illustrated with a case study which may be viewed as an example of Corporate Security Policy. It applies to the context of the multilevel security policy, deals with protection of both sensitive information and people cleared at a given security level having a need to know of some sensitive information. It is quite a large set of paragraphs which defines various concepts necessary for the protection, and gives rules to be applied in order to protect vulnerable people or information. Its size is about 60 pages in
Every time a document classified at the secret level is destroyed (action), the holder of this document and a witness of the destruction (corresponding event) are obliged to sign the destruction minutes. When a meeting is finished (event: meeting), its organizer is obliged to incinerate all the preparatory documents of the meeting.
One can also notice that a temporal representation is necessary: we have to represent temporal structure to represent
intervals such as before, during, and after the execution of an action. For instance:
Before every meeting, the organizer of this meeting is obliged to establish a list of all participants in this meeting.
may inherit from another class. By doing so, we can represent different abstraction levels. A class of objects is defined by: its name,
the names of the classes it possibly inherits from,
During the time an agent is elaborating a document classified at the secret level, he is obliged to work in a protected area.
its attributes; attribute values are objects (so that we can define structured objects), and a set of methods one can apply to the objects, in order to manipulate the object or to create another object.
After a secret document is destroyed, the document holder is obliged to notify the document author of this destruction.
Finally, there are rules in our case study which deal with situations of violation. For instance:
In our logical language, a class of objects is represented as follows:
If the organizer of a meeting does not incinerate all the preparatory documents of this meeting when the meeting is finished, then this organizer is obliged to bring it about that these documents are kept in a safe.
This last rule corresponds to a situation where the above primary obligation to incinerate the preparatory documents is violated.
3. Language definition This section describes the language we propose to deal with all the notions we found in our case study and their associated axiomatics. Due to space limitation, we do not develop a semantics for this language in this paper but it is partially described in [8]. Our language is based upon a first order modal logic. To represent a regulation, we have to represent objects, events, actions and agents. We also need to introduce the concept of delegation. Then we have to represent the deontic concepts of obligation, permission and prohibition. For this purpose, we propose to use a deontic logic because of its advantage on other logical formalisms, for instance alethic logic (necessary and possible) or temporal logic, to reason about a situation where a rule is violated. The last rule of section 2 provides an example of such rules. They are generally called contrary to duty norms (see for instance [17, 4]).We actually found many examples of this type of rules in our case study and deontic logic was well suited to model them.
We take our inspiration from the object-oriented concepts. An entity is represented by an object. Any object belongs to a “class of objects” which is an abstraction of it. The set of classes is structured in a hierarchical way; a class
name: a predicate symbol,
attribute: a function; its signature provides the type (i.e. the object class) of the attribute value, method: an action; its signature provides the types of input and output parameters of this method.
Given a regulation, we shall represent its agents and objects as entities. For instance, we give the (partial) definition of the class Classified Document: Class: Classified Document Inherits : Document Attributes : Classification : Level Consignment Note : Note Methods : Change Classification : Classified Document Establish Consignment Note : Classified Document Note
Level
Level and Note are supposed to be two already defined object classes. In our language, a particular entity will be represented by a constant symbol. For instance, if D337 is a particular classified document, then we have: Classified Document(D337).
! " $#% &('*) +," -./,+102,02+, The concept of event is often used in the domain of natural language analysis. We follow Allen [1] and take the position that events are primarily linguistic or cognitive in the sense that the world does not really contain events. An event may be viewed as a means to classify how the world may change, i.e the different ways to update the state of the world. As a consequence, any execution of an action may be viewed as an event.
In our language, events are represented as objects. There is a predefinite class 3541687:9 which describes the characteristics common to every event. In particular, this class 3;4@?19A6 whose value is an interval of time. Therefore, if 6 is an event, then >B?,9A6WVUFXY7 Z and [\S9A68U – with the following axioms, where 6 is considered to be an event:
^] 16 MLQ_6/S TFUF6@?19A6@?19A6Rfg9LK ^] 61ML>@VhUFXY7 Z CD6/E!` a 9 K MN9 O MF>B?,9A6@?19A6 k 9 O ^] 61ML[ S9A68U@?19A6@?19A6
d VhUFU/687:9 >@?19A6 is supposed to be a predefinite object; its value represents the actual date. Let us notice that we consider that the evaluation of any formula is related to d VhUFU/687:9 >@?19A6 . Similarly to entities, the set of events is associated with a hierarchical structure, the class 3;4 and associate with this class two attributes [.op9ATFU and >@6/q=9 to respectively represent the agent who causes the n occurrence of the event 35[.> and the entity read during the occurrence of this event. J*rs,tu) 2 Actions are applied to objects or agents of the regulation. They are actually associated with methods in an objectn oriented environment. For instance, if 6F?1v is the name of n an unary action and if v is a document, then 6F?@?19A6 is previous to the time of the execution of w by ? (this means, ? has not yet executed w ). >WVU8XY7 Z 3;xh6FoCD?hMyw!E is true during the execution of w by ? .
3;x68oC?MLwE
is true after ? has executed w . actually an abbreviation for [ S9A6=U 3;x6Fo .
3;xh6Fo
is
Actions and events are connected through these temporal predicates. For instance, for the predicate QR6/S TFU/6 3;xh6Fo , n n the action 6F? , we have the following axiom:
n ^] ?M ] vhMLQR6/S FT U/6 5 a 3 xhn 6FoC?M 6F?@TC?MDEcl>@TC?MyE$>@TCD?hMD_clE This axiom says that if ? brings it about that and brings it about that , then ? actually brings it about the conjunction of and . $|8 = 5$ |8 N i.e. if l is a tautology, then bringing it about that is equivalent to bringing it about that .
® /85® /8 i.e. if @ is a tautology, then the obligation to do should imply the obligation to do .
3.
4.
° CªRc~E¦² ° _c °
This axiom says that the permission to do and should imply the permission to do and the permission to do . Notice that the converse is generally not true. For instance, if you have your driving licence, you are permitted to drive a car. You may also be permitted to drink a bottle of wine. However, it is prohibited to drive a car and to drink a bottle of wine, at the same time.
° Rc ¨ R²h ° Cª_c~E
This axiom says that if it is permitted to do and obligatory to do , then it is permitted to do the conjunction of and . In particular, this axiom implies that:
¨ B °
i.e. the obligation to do should imply the permission to do .
° l ¯ i.e. if is explicitly permitted, then
should not
be prohibited.
³ /=5³ /= i.e. if ¥j is a tautology, then the permission to do should imply the permission to do . J´µsh'*) 2tu ¦tY-YtD=¶%"§ $#·#¦-u§":,tu)! 5.
In order to formalize the organizational concepts of responsibility and delegation, we must first define a special object class ¸¹XAqFqXTF7 with the following structure: Class Mission Attributes: Responsible : Agent Controller : Agent Obligations : set of Action Methods: Designate Responsible : Mission
Agent
Therefore, if º is a mission and ? and are two agents, n then 6FqLTF7§qXApD6B6Fq=XuZ@T/opVºe6=7:9 æ½U/6/q86=UF4