Security automation for stateful firewalls

Stateful functions are functions that keep some internal state across invocations, allowing them to retain information from previous executions. This is in contrast to stateless functions, which do not preserve any information between calls and always behave in the same way regardless of how many times they are called. In networking, stateful functions play a crucial role in ensuring proper communication, security, and efficient data transfer. They are used to monitor connections, manage active sessions, and maintain information about the status of network activities. This helps provide continuity, reliability, and control over traffic and resources. This thesis focuses on stateful firewalls, a key application of stateful functions. Stateful firewalls are crucial for network management because they enhance the control and monitoring of data traffic by maintaining the state of active connections. This capability allows the firewall to make informed decisions about whether to allow or block traffic based on the state of each session. By preserving connection states, stateful firewalls significantly improve system security, as they can more effectively detect and block potential attacks. This work specifically focuses on enhancing the functionality of VEREFOO, a framework designed to automatically allocate and configure packet filtering firewalls within a service graph, meeting the security and connectivity requirements specified by the user. As first thing, a series of verification tests were conducted to evaluate the correctness of the Verification Problem within the framework, which had not been fully tested previously. These tests use a Service Graph, representing the network configuration, and a set of Network Security Requirements (NSRs) that the network must adhere to. Various scenarios were tested, all involving stateful firewalls that were already deployed in the network and configured with their respective rules. The objective of these tests was to determine whether the NSRs were met under the given configuration. The test cases were written in XML files and provided to the platform for analysis. Following these tests, the analysis shifts to the Refinement Problem, where the framework automatically generates and optimally allocates firewalls in the network based on the input Network Security Requirements (NSRs). To model this problem with stateful firewalls, several Boolean logic formulas were defined. These formulas aim to describe the behavior of a stateful firewall, specifying when traffic should be blocked or permitted, and when to consider the connection state in making these decisions. In the final part of this work, a set of translators for stateful firewalls was implemented in Java. These translators process XML files containing network configurations and the security policies to be applied. The XML content is translated into configuration files used by specific firewall technologies, including Iptables, IpFirewall, and Open vSwitch. The resulting configuration files are tailored to each chosen technology and include all the commands necessary to recreate the network configuration described in the XML files. Executing these configuration files will set up a network with the configured security policies in place.