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

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.