Synthesizing optimal security configurations for enterprise networks : a formal approach

In this paper, we present NetSecSlider, an automated framework for synthesizing network configurations exploring various security and safety design alternatives. The design alternatives include distribution of different level of isolations (firewall, IPSec, etc.) and safety enforcement process (e.g. tampering of network flow) in the network. NetSecSlider takes the network topology, organizational security and safety requirements and business constraints as input, and synthesizes a correct and optimal security configuration. Finally, it determines the optimal placement of enabling devices in the network. The framework uses (i) a SMT solver for finding the correct and optimal security configuration and (ii) a method for determining the optimal placement of devices. The framework is evaluated on different networks with varying security and safety requirements.