Directed Security Policies: A Stateful Network Implementation

Cornelius Diekmann
(Technische Universität München)
Lars Hupel
(Technische Universität München)
Georg Carle
(Technische Universität München)

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.

In Jun Pang and Yang Liu: Proceedings Third International Workshop on Engineering Safety and Security Systems (ESSS 2014), Singapore, Singapore, 13 May 2014, Electronic Proceedings in Theoretical Computer Science 150, pp. 20–34.
Published: 3rd May 2014.

ArXived at: https://dx.doi.org/10.4204/EPTCS.150.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org