The early detection of potential threats during the modelling phase of a Secure Information System is required because it favours the design of a robust access control policy and the prevention of malicious behaviours during the system execution. This paper deals with internal attacks which can be made by people inside the organization. Such attacks are difficult to find because insiders have authorized system access and also may be familiar with system policies and procedures. We are interested in finding attacks which conform to the access control policy, but lead to unwanted states. These attacks are favoured by policies involving authorization constraints, which grant or deny access depending on the evolution of the functional Information System state. In this context, we propose to model functional requirements and their Role Based Access Control (RBAC) policies using B machines and then to formally reason on both models. In order to extract insider attack scenarios from these B specifications our approach first investigates symbolic behaviours. The use of a model-checking tool allows to exhibit, from a symbolic behaviour, an observable concrete sequence of operations that can be followed by an attacker. In this paper, we show how this combination of symbolic execution and model-checking allows to find out such insider attack scenarios.
Developing secure Information Systems remains an active research area addressing a wide range of challenges mostly interested in how to prevent from external attacks such as intrusion, code injection, denial of service, identity fraud, etc. Insider attacks are less addressed despite they may cause much more damage because an insider is over all a trusted entity. Intrinsically it is given means to violate a security policy, either by using legitimate access, or by obtaining unauthorized access. This paper deals especially with Role Based Access Control (RBAC) concerns with the aim to exhibit potential insider threats from a formal modelling of secure Information Systems. We are interested in finding attacks which conform to the access control policy, but lead to unwanted states. These attacks are favoured by policies involving authorization constraints, which grant or deny access depending on the evolution of the functional Information System state. This reveals, on the one hand, the need to link the security model to the functional model of the information system, and on the other hand, to build tools taking into account the dynamic evolution of the IS state.
Tools such as SecureMova [
This paper is organized as follows: section 2 gives an overview of our approach and its underlying methodology. In section 3 we present a simple example that illustrates our contribution. Section 4 defines semantics and technical aspects. In section 5 we propose a symbolic search that automates generation of attack scenarios and we discuss results of its application on the given example. Finally, we draw conclusions and perspectives. 2
Bridging the gap between formal (e.g. Z, B, VDM . . .) techniques and graphical
languages such as UML has been a challenge since several years. On the one
hand, formal techniques allow automatic reasoning assisted by proof and
modelchecking tools, and on the other hand, graphical techniques allow visualization
and better understanding of the system structure. These complementary aspects
are useful to ensure a software development process based on notations with
precise syntax and semantics and which allows to structure a system graphically.
Most existing research works [
In our work, we adopt a similar approach in order to graphically model
and formally reason on both functional and security models. We developed the
B4MSecure6 platform [
The functional B model on the left hand side of figure 1 is issued from a conceptual class diagram. It integrates all basic operations generated automatically 6 http://b4msecure.forge.imag.fr/ (constructors, destructors, setters, getters, . . .) and also additional user-defined operations which are integrated into the graphical model and specified using the B syntax. This functional specification can be further improved by adding invariants and carrying out proof of correction with the help of AtelierB prover.
The security model, on the right hand side of figure 1 is dedicated to control the access to functional operations with respect to access control rules defined in the SecureUML model. In our approach, we don’t deal with administration operations because we make the simplifying assumption that access control rules don’t evolve during the system execution. The security formal model allows to validate RBAC well-formedness rules such as no role hierarchy cycles, and separation of duty properties (SoD) such as assignment of conflicting roles to users. . .
This paper assumes that validation of both models in isolation is done:
operations of functional model don’t violate invariant properties, and the security
model is robust. Such validation activities are widely discussed in the literature
[
In this section we use a running example issued from [
The functional UML class diagram (presented in figure 2) describes a meeting scheduler dedicated to manage data about two entities: Persons and Meetings.
A meeting has one and only one owner (association MeetingOwner ), a list of participants (association MeetingParticipants), a duration, and a starting date. A person can be the owner of several meetings and may participate to several meetings. Operations notify and cancel are user-defined, and allow respectively to send messages to participants and to delete a meeting after notifying their participants by e-mail. Constructors, setters and getters are implicitly defined for both classes and both associations. 3.2
The access control model is given in Figure 3. It features three different roles: – SystemUser: defines persons who are registered on the system and then have permission UserMeetingPerm which allow them to create and read meetings. Deletion and modification of meetings (including operation cancel) are granted to system users by means of permission OwnerMeetingPerm, featuring an authorization constraint checking that the user who tries to run these actions is the meeting owner. – Supervisor: defines system users with more privileges because they can run actions notify and cancel on any meeting even if they are not owners. – SystemAdministrator: having a full access on entity Person, an administrator manages system users. Full access grants him the right to create a new person, remove or modify an existing one. Furthermore, a system administrator has only a read access on meetings. 3.3
This example is intended to be validated in [
Authorization constraint associated to OwnerMeetingPerm requires information from the functional model because it deals with the MeetingOwner association. In the rest of this article, we consider three users John, Alice and Bob such that user assignments are as defined by figure 4 and a given initial state in which Alice is owner of meeting m1, Bob is a participant of m1. In such a state, the above static query establishes that only Alice is allowed to modify or delete m1 because she is the owner of m1.
In [
In order to find malicious behaviours of an operational secure IS modelling, we rely on the set of finite observable traces of our B specifications. Indeed, B specifications can be approached by means of a trace semantics composed of an initialization substitution init, a set of operations O and a set of state variables V. We note val a possible state predicate allowed by the invariant and op an operation from O. A functional behaviour is an observable sequence Q
Q =ˆ init ; op1 ; op2 ; . . . ; opm such that ∀i.(i ∈ 1..m ⇒ opi ∈ O) and there exists a sequence S of state predicates which does not violate invariant properties:
S =ˆ val0 ; val1 ; . . . ; valm in which val0 is an initial state, and opi is enabled from state vali−1 and state vali is reached by opi, starting from state vali−1.
The security model filters functional behaviours by analysing access control premises which are triplets (u, R, c) where u is a user, R is a set of possible roles assigned to u, and c is an authorization constraint. An observable secure behaviour is a sequence Q, where for every step i, premise (ui, Ri, ci) is valid (expressed as (ui, Ri, ci) |= true). This means that roles Ri activated by user ui grant him the right of running operation opi and if a constraint ci exists, then it must be satisfied. The following premises sequence P must be valid for Q:
P =ˆ (u1, R1, c1) ; (u2, R2, c2) ; . . . ; (um, Rm, cm) 4.2
Model-checking and symbolic proof techniques are of interest in order to exhibit a relevant behaviour from an operational B specification. Proof techniques deal with infinite systems and can prove constraint satisfiability, or establish that some operation can be enabled from an abstract state predicate. Model-checking is based on model exploration of finite systems, and can be used to find a sequence of actions leading to a given state or property. In our approach, we combine both techniques in order to overcome their shortcomings: complexity of proofs for the first one, and state explosion for the second one. In this sub-section, we illustrate both tools.
Model checking and animation (the ProB tool). ProB [
In step 1, the tool animates operation personN ew which modifies variable
person (initially equal to emptyset) and this action was performed by user John
using role SystemAdministrator without need of authorization constraint. In
step 4, the tool adds participant Bob to the meeting m1 by animating operation
meetingAddParticipants, after validating that authorization constraint is valid
for Alice using role SystemUser. Indeed, Alice is the owner of m1.
Symbolic proof (the GeneSyst tool). ProB is useful to animate scenarios
identified during requirements analysis, or to exhaustively explore a finite subset of
state space. As we are interested in finding malicious scenarios that exhibit a
potential internal attack, the ProB technique may be useful only if it explores
the right subset of state space in the right direction, which is not obvious for
infinite systems. Symbolic proof techniques, such as that of GeneSyst [
In the generalized substitution theory, formula [S]R means that substitution S always establishes predicate R, and ¬[S]¬R means that substitution S may establish predicate R. Hence, proof (1) means that state F can be reached by actions of operation op, when operation precondition is true in state E. Proof (2) means that F is never reached by actions of operation op from state E. Finally, proof (3) means that F is always reached by op from E. Let us consider, for example, the functional operation meetingN ew: meetingN ew(m, p)=ˆ
EN D P RE m 6∈ meeting ∧ p ∈ person T HEN meeting := meeting ∪ {m} || meetingOwner := meetingOwner ∪ {(m 7→ p)}
This operation adds a new meeting m and links it to an owner p. If we define states E and F such that:
E =ˆ meetingOwner[{m1}] = ∅
F =ˆ meetingOwner[{m1}] 6= ∅ then proof obligation produced by GeneSyst for property (1) was successfully proved showing that operation meetingN ew when enabled from a state where m1 does not exist and there exists at least one person in the system, may lead to a state where m1 is created and has an owner.
Our work will be focused on proof (1) which states the reachability of a target state from an initial one, illustrated above, because it is sufficient to decide wether an operation is potentially useful for a malicious behaviour. Proofs (2) and (3) can be used if one would like to assume that a state can never be reached, or it is always reached, by an operation. 4.3
Based on the security requirements, several operations are identified as critical. For example, security requirements have identified the integrity of meeting information as critical. Therefore, operations which perform unauthorized modifications are identified as critical.
A malicious behaviour executed by a user u, regarding authorization constraints, is an observable secure behaviour Q with m steps such that: – opm is a critical operation to which an authorization constraint cm is associated. – user u is malicious and would like to run opm by misusing his roles Ru. – val0 : is an initial state where (u, Ru, cm) |= f alse – for every step i (i ∈ 1..m) premise (u, Ru, ci) |= true
In other words, malicious user u is not initially allowed to execute a critical operation, but he is able to run a sequence of operations leading to a state from which he can execute this operation. In our investigation we suppose that user u executes this malicious sequence without collusion. This problem will be tackled in a further work.
Section 3.3 gave an example where neither Bob nor John are allowed to run a modification operation, such as meetingSetStart which modifies attributes of class Meeting, from the initial state due to the authorization constraint. This initial state is: val0 =ˆ person = {Alice, Bob} ∧ meeting = {m1} ∧ meetingOwner = {(Alice 7→ m1)} ∧ meetingP articipant = {(m1 7→ Bob)}
In the following, we denote as init0 the sequence of operations leading to val0 such as that presented in table 1. We used the model-checking facility of ProB in order to explore exhaustively the state space and automatically find a path starting from val0 and leading to a state where operation meetingSetStart becomes permitted to John. We asked ProB to find a sequence where John becomes the owner of m1:
meetingOwner(m1) = J ohn After exploring more than 1000 states, ProB found a scenario in which John executes sequentially operations personNew, personAddMeetingOwner and meetingSetStart. Indeed, this dynamic analysis showed that John, as a system administrator, has a full access to entity Person. This permission allows him to create, modify, read and delete any instance of class Person. First, he creates an instance John of class Person that corresponds to him by running operation personN ew(J ohn). Then he adds meeting m1 to the set of meetings owned by John, by running operation personAddM eetingOwner(J ohn, m1) which is a basic modification operation of class Person. These two actions allowed him to become the owner of m1 and then he was able to modify the meeting of Alice. Like all model-checking techniques, when ProB explores exhaustively the state space, it faces the combinatorial explosion problem which depends on the number of operations provided to the tool and the state space size. In order to address this problem, our approach proposes a symbolic search which finds a sequence of potentially useful operations on which the model-checker should be focused.
The proposed symbolic search is performed by an algorithm that looks for an observable sequence Q =ˆ init0 ; op1 ; . . . ; opm executed by a user u, and where (u, Ru, cm) is not valid for a critical operation opm in the initial state val0 but becomes valid for state valm−1 where opm can be enabled. It is a backward search algorithm, starting from the goal state valm−1 from which the critical operation opm can be enabled: valm−1=ˆ cm ∧ P re(opm); and working backwards until the initial state val0 is encountered. The algorithm ends when sequence Q is found or when all operations are verified without encountering the initial state. We consider that val0 is a completely valuated state such as that where Alice is the owner of m1, and Bob is a participant to m1. This prevents the initial state from being included in both states valm−1 and valm−2, which would never verify the condition of the while loop. Note that each operation occurs at most once in a computed sequence, which ensures the termination of our algorithm. 1. Q =ˆ opm; 2. valm−1 =ˆ cm ∧ P re(opm); 3. valm−2 =ˆ ¬valm−1; 4. while val0 6⇒ valm−1 do 5. choose any oi ∈ O where 6. (u, Ru, ci) |= true ∧ 7. valm−2 ∧ P re(oi) ⇒ ¬[Action(oi)]¬valm−1 8. do 9. Q =ˆ oi ; Q ; 10. valm−1 =ˆ valm−2 ∧ P re(oi); 11. valm−2 =ˆ valm−2 ∧ ¬P re(oi); 12. else 13. raise exception: No sequence found 14. enddo 15. endwhile 16. Q =ˆ init ; Q ; 5.1
We take advantage of abstraction and step by step we refine the valm−2 symbolic state: 1. At the first step of the algorithm, the state space is represented by two symbolic states: the first one valm−1 includes all states where the authorization constraint cm is true and which are enabling opm, and the second one valm−2 is the negation of valm−1 which is then ¬cm ∨ ¬P re(opm). As they are two disjoint state predicates, we conduct proof (1) in order to find an operation oi that belongs to O and which possibly reaches the first state valm−1 from the second one valm−2 and such that premise (u, Ru, ci) is valid. If oi does not exist, then no sequence could be found for the expected attack and we can try proof (2) for each operation attesting that all operations never reach valm−1 from valm−2. 2. At the second step of the algorithm, if the proof (1) succeeds for some operation opm−1, then it may exist an observable sequence leading to the critical operation where access control premise (u, Ru, cm) is valid, and hence a potential symbolic attack scenario can be found. The algorithm looks inside state valm−2 in order to find out the previous operations that can be invoked in the attack scenario. State valm−2 is partitioned into two sub-states which are: valm−2 ∧ P re(opm−1) ≡ ¬(cm ∧ P re(opm)) ∧ P re(opm−1) valm−2 ∧ ¬P re(opm−1) ≡ ¬(cm ∧ P re(opm)) ∧ ¬P re(opm−1) Then, we look for operations that reach the first sub-state from the second one. 3. The algorithm proceeds iteratively by partitioning the second state into two sub-states until it finds a state that includes the initial state. In the best case, our algorithm gives some symbolic attack scenario, which consists of sequence (init0 ; opn ; opn+1 ; . . . ; opm) invoked by the same user u and where: valn−1=ˆ ¬(cm ∧ P re(opm)) ∧ ¬P re(opm−1) ∧ ¬P re(opm−2) ∧ . . . ∧ P re(opn) and such that val0 ⇒ valn−1 ∧ ∀i.(i ∈ (n..m) ⇒ (u, Ru, ci) |= true) 5.2
We apply our algorithm to the meeting scheduler example starting from the following initial state val0: val0 =ˆ person = {Alice, Bob} ∧ meeting = {m1} ∧ meetingOwner = {(Alice 7→ m1)} ∧ meetingP articipant = {(m1 7→ Bob)}
In this state user John is not allowed to modify meeting m1 because the authorization constraint allows modification only for the owner of m1. A malicious scenario would lead to a state where John becomes able to execute a modification operation such as operation meetingSetStart on meeting m1. In this state we have to verify:
P re(meetingSetStart(m1, start))=ˆ m1 ∈ meeting ∧ start ∈ N AT and (John, SystemUser, M eetingOwner(m1) = J ohn) |= true 1. First iteration: considering the following symbolic states valm−1 = (M eetingOwner(m1) = J ohn) ∧ m1 ∈ M eeting ∧ start ∈ N AT valm−2 = ¬valm−1 we have: – val0 6⇒ valm−1 because, in state val0, M eetingOwner(m1) = Alice, and – proof (1) succeeds for the operations meetingNew and personAddMeetingOwner. Then, we may go on the second iteration of the algorithm for each of these operations. 2. Second iteration: we partition state valm−2 into two sub-states: valm−2 = ¬valm−1 ∧ P re(opm−1) valm−3 = ¬valm−1 ∧ ¬P re(opm−1) – case 1: we choose opm−1 = meetingN ew, and then we have: – P re(meetingN ew) =ˆ m1 ∈ meeting ∧ J ohn ∈ person, and – val0 6⇒ valm−2 because J ohn 6∈ person In this case, the algorithm does not find an operation leading to a state where operation meetingN ew becomes enabled. Indeed, no operation satisfied proof obligation (1). Our algorithm concludes that it does not exist an attack scenario invoking meetingN ew at this step.
init0 meetingN ew meetingSetStart 3. Third iteration: we partition state valm−3 into two sub-states: valm−3 = ¬valm−1 ∧ ¬P re(personAddM eetingOwner) ∧ P re(personN ew) valm−4 = ¬valm−1 ∧ ¬P re(personAddM eetingOwner) ∧ ¬P re(personN ew) This stops normally the algorithm because in this case val0 ⇒ valm−3. Indeed, P re(personN ew) =ˆ J ohn ∈/ person and in the initial state John does not belong to set person. Figure 6 presents the full symbolic scenario that allows John to modify Alice’s meeting. personN ew personAddM eetingOwner meetingSetStart Technically, our approach applies the GeneSyst tool in order to produce proof obligations and then asks the AtelierB prover to discharge them automatically. As the resulting scenarios are symbolic and based on “possibly reached proofs”, the analyst can conclude that attacks may exist but he can not attest their feasibility for the concrete system. An interesting contribution of our proof-based symbolic sequences, besides the fact that they draw the analyst’s attention to potential flaws, is that they give useful inputs to the model-checker. Indeed, a model-checking tool can be used to exhibit, from a symbolic behaviour, an observable concrete sequence of operations that can be followed by an attacker. In order to reduce significantly the state space, we can ask ProB to explore only operations found in the symbolic malicious scenarios. For our example, when trying only operations personNew, personAddMeetingOwner and meetingSetStart, ProB exhibits a concrete attack scenario after visiting a dozen of states which shows a significant speed up with respect to our initial ProB attempts (involving more than 1000 states).
Our technique was able to extract another scenario (figure 7) which can be executed by user Bob from the same initial state, in order to steal the ownership of m1. In this scenario, Bob first cancels the meeting and then he recreates it before applying the critical operation.
init0 meetingCancel meetingN ew meetingSetStart
The first scenario, done by user John, is made possible by the full access permission to class Person, associated to role SystemAdministrator, which includes the right to modify association ends. This attack affects meeting integrity. One solution can be to add a SSD constraint between roles SystemAdministrator and SystemUser. John will then still be able to become owner of the meeting, but will not be able to log in as SystemUser in order to modify it.
The second scenario done by Bob was possible due to role Supervisor which gives him the right to cancel a meeting, and then, as a SystemUser he can recreate it in order to become its owner. This scenario does not point out a flaw since whenever a meeting is cancelled it should be legitimate that a user can start a new meeting with the same identifier as the cancelled one. 6
We described in this paper a symbolic search approach that can extract insider
malicious behaviours from a formal Information System modelling. The
meeting scheduler example was discussed in several articles [
Our approach is automated by exploiting tools B4MSecure8, GeneSyst9, AtelierB10 and ProB11. B4MSecure translates functional and security graphical models into B specification, from which we automatically produce proof obligations on reachability properties by taking advantage of the GeneSyst tool. Then, these proof obligations are discharged automatically using the AtelierB prover. When a symbolic scenario is found, ProB is used to explore concrete state space focusing on operations issued from the symbolic scenario. The main limitation of our work is that sometimes, when proof obligations are complex, AtelierB fails to prove them automatically. Interactive proofs are then required, but they may be pretty difficult for the analyst. One naive solution is to keep operations for which proofs don’t succeed automatically in order to be exploited further using the model-checker. A more interesting solution is to focus on other kinds of proof obligations. For example, one can try to prove that an operation o is never enabled from a state E and/or o never reaches a state F . Applying 7 http://lacl.univ-paris12.fr/selkis 8 http://b4msecure.forge.imag.fr 9 http://perso.citi.insa-lyon.fr/nstouls/?ZoomSur=GeneSyst 10 http://www.atelierb.eu/ 11 http://www.stups.uni-duesseldorf.de/ProB these proofs to the meeting scheduler example we were able to eliminate half of the operations after proving automatically that they cannot be involved in the attack scenario.
We believe that reachability properties can be expressed by means of LTL formula. We started exploring this direction basing on the LTL formula checking facilities of ProB and the first results are promising.