Specifying a security policy (SP) is a challenging task in the development of secure communication systems since it is the bedrock of any security strategy. Paradoxically, this specification is error prone and can lead to an inadequate SP regarding the security needs. Therefore, it seems necessary to define an environment allowing one to “trust” the implemented SP. A testing task aims verifying whether an implementation is conforming to its specification. Test is generally achieved by generating and executing test cases. Some automated testing tools can be used from which model checkers. In fact, given a system modeling and a test objective, the model checker can generate a counterexample from which test cases can be deduced. The main proposition of this chapter is then a formal environment for SP test cases generation based on a system modeling, a SP specification (test purpose), and the use of a model checker. Once generated, these test cases must be improved in order to quantify their effectiveness to detect SP flaws. This is made through the generation of mutants.
Top1. Introduction
The need for security is driven by the increasingly proportion of losses caused to the organizations due to various security incidents. One reason of this can be a lack of a global security environment that differentiate between the actions to authorize and those to deny trough a set of rules, generally grouped in a document referred to as security policy (SP). SP development is unfortunately, a sensitive task because it may contain errors, or may be generated by wrong decisions or wrong evaluations of the security organization needs. In order to avoid such problems a validation process is necessary before any deployment. SP validation consists in checking if the policy matches all the security needs i.e. are we building the right SP? In recent works, we proposed a three-step process allowing the validation of a SP (Abbassi & El Fatmi, 2008b, 2009). In the first step, we proved that the SP is consistent. The second step dealt with proving the completeness of the SP according to the initial requirements while in the third step, we proved the preservation of the security properties. However, validation is not enough to ensure that the SP is correctly enforced. In fact, once the SP is formally and correctly specified, it is essential to prove that it is correctly implemented in the system, too. This can be done by testing the enforced SP.
Moreover, we have found that the theory developed for this aim in the software engineering domain can be adapted for SP because several similarities exist between the expressions of the needs in the two domains as mentioned in several studies. In the software engineering domain, testing entails the execution of the software system in the real environment, under operational conditions (Belli & Guldali, 2004). It is used in order to verify whether an implementation is conforming to its specification (supposed correct) i.e. checking that the behavior of a real implementation is correct with respect to a specification (Calame, 2005). Such testing is carried out by test cases, i.e., ordered pairs of test inputs and expected test outputs (Felli & Guildali, 2004). By analogy, testing a given network configuration for compliance with a stated SP is a kind of conformance testing.
Furthermore, since testing task needs the use of automated tools, model checkers can be used. In fact, given a system model and a test criterion, the model checker can generate a counterexample from which test cases can be deduced. A model checker visits all reachable states of the model and verifies whether the expected system properties, specified as temporal logic formula, are satisfied over each possible path. If a property is not satisfied, the model checker attempts to generate a counterexample in the form of a trace as a sequence of states.
In this paper, we propose a framework to model a SP, to formally specify it and to test its implementation regarding some security exigencies and thus, using the model checking technique. This framework is based on the concept of Executable Security Policies (ESP), that we introduced in Abassi and El Fatmi (2008a, 2008b, 2009) in order to model the behavior of a given SP before its actual implementation. More precisely, we take as input: (1) a formal model of a network together with its embedded ESP. This model is expressed in S-Promela, a Promela based language handling security aspects. (2) Some Test Purposes (TP) describing desired behaviors. TP are expressed by the Linear Temporal Logic LTL (Kroger, 1987). As output, we generate Test Cases (TC) in order to verify that the desired SP is correctly enforced in the considered network.