A Formal Framework for Network Security Design Synthesis

Due to the extensive use of Internet services and emerging security threats, most enterprise networks deploy varieties of security devices for controlling resource access based on organizational security requirements. These requirements are becoming more fine-grained, where access control depends on heterogeneous isolation patterns like access deny, trusted communication, and payload inspection. However, organizations are looking to design usable and optimal security configurations that can harden the network security within enterprise budget constraints. This requires analyzing various alternative security architectures in order to find a security design that satisfies the organizational security requirements as well as the business constraints. In this paper, we present ConfigSynth, an automated framework for synthesizing network security configurations by exploring various security design alternatives to provide an optimal solution. The main design alternatives include different kinds of isolation patterns for traffic flows in different segments of the network. ConfigSynth takes security requirements and business constraints along with the network topology as inputs. Then it synthesizes optimal and cost-effective security configurations satisfying the constraints. ConfigSynth also provides optimal placements of different security devices in the network according to the given network topology. ConfigSynth uses Satisfiability Modulo Theories (SMT) for modeling this synthesis problem. We demonstrate the scalability of the tool using simulated experiments.