Formal specification, verification and correction of security policies based on the decision tree approach

  • Kamel Karoui
  • fakher ben ftima RIADI, ENSI, University of Manouba, Tunisia
  • Henda Ben Ghezala
Keywords: security policy, relevancy, anomalies detection, formal specification, formal verification, formal correction


Security components such as firewalls, IDS and IPS, are the mainstay and the most widely adopted technology for protecting networks. These security components are configured according to a global security policy.  An error in a security policy either  creates   security  holes  that will allow malicious  traffic to sneak  into a private  network  or blocks legitimate  traffic and  disrupts  normal business   processes,   which, in turn, could lead to irreparable consequences. It has been observed   that most security policies on the Internet are poorly designed   and have many misconfigurations.  In this paper, we propose a formal process to specify, verify and correct the security policy using the decision tree formalism, which consists of four steps. First, we define the security policy specifications and write it in a natural language. Second, the security policy will be translated into a formal language. Third, we verify the security policy correctness. If this latter is plugged with anomalies, we correct it in the last step.

To achieve these goals, we present a decision tree based formalism for security policy verification and propose a correction algorithm to guarantee the security policy correctness. A case study will demonstrate the usefulness of our approach.