Validation of Security Solutions for Communication Networks: A Policy-Based Approach

Typically, security solutions are defined to meet the requirements of security policies, and are configured to implement some of their rules. Approaches proposed so far in the literature to validate security solutions have merely taken interest to the need of: a) describing the security policy used to define and configure these solutions b) generating executable description of attack scenarios targeting the secured system and c) verifying whether the secured systems react as expected. In this paper we develop a logic-based approach for the modeling of security policies and solutions based on the concept of observations, and the generation of executable scenarios of attacks. This approach provides a unified formalism for the specification of security policies, security solutions, library of legitimate actions and attacks, and correctness rules in the form of predicates over executions. We propose a modeling of two types of security solutions, namely passive and active solutions. We develop a Model Checker to generate executable scenarios of attacks, verify the security state of the system, and test whether the solutions react as expected to security attacks. A case study is proposed to illustrate the proposal.