Directed Security Policies: A Stateful Network Implementation
This solves the problem of ensuring security policy compliance in stateful network implementations for network administrators and security engineers, representing a strong incremental improvement with automated verification.
The paper addresses the problem that stateful network implementations of security policies (like firewalls) can create unintended backflows from B to A when A connects to B, potentially violating the original policy. It provides compliance criteria to verify lack of side effects in linear time, algorithms to automatically construct correct implementations, and demonstrates scalability in a real-world case study with correctness guaranteed by the Isabelle/HOL theorem prover.
Large systems are commonly internetworked. A security policy describes the communication relationship between the networked entities. The security policy defines rules, for example that A can connect to B, which results in a directed graph. However, this policy is often implemented in the network, for example by firewalls, such that A can establish a connection to B and all packets belonging to established connections are allowed. This stateful implementation is usually required for the network's functionality, but it introduces the backflow from B to A, which might contradict the security policy. We derive compliance criteria for a policy and its stateful implementation. In particular, we provide a criterion to verify the lack of side effects in linear time. Algorithms to automatically construct a stateful implementation of security policy rules are presented, which narrows the gap between formalization and real-world implementation. The solution scales to large networks, which is confirmed by a large real-world case study. Its correctness is guaranteed by the Isabelle/HOL theorem prover.