Firewall configuration policies for the specification and implementation of private zones

We introduce and discuss two case studies where a complex network is modeled as a set of zones interconnected by routers or firewalls. To address the problem in full abstraction, we defined PDLz, an extension of the PDL event-condition-action language that supports the specification of firewall routing policies. PDLz allows the modelling of computer networks based on the concept of zone, i.e., a TCP/IP subnet where internal traffic remains unconstrained. PDLz policies are enforceable thanks to a direct translation to the IPtables firewall configuration language. At the same time, PDLz has a declarative semantics thanks to translation to logic programs. The logic programming translation also supports, by adding extra rules, the formal verification of properties of the network, viz. off-line reachability testing across firewalls. We describe the application of PDLz to the case studies.