Source-linked AI summary
The Mathematical Foundations for Mapping Policies to Network Devices (Technical Report)
Dinesha Ranathunga, Matthew Roughan, Phil Kernick, Nick Falkner
TL;DR
Manual configuration of heterogeneous networks is impractical, motivating high-level policies independent of device APIs. The paper develops an algebraic mapping framework and applies it to real SCADA networks, reporting zero incorrectly allocated firewall rules.
Problem
Manual, box-by-box configuration of heterogeneous networks is impractical, motivating high-level policy specifications independent of device-oriented APIs.
Source: §1 · p. 1Method
The paper proposes a generic algebraic framework for mapping policies to network devices, illustrating it with security policies and directed-firewall paths.
Source: §1 · p. 1, §4.1 · p. 7Results
Zero incorrectly allocated policy rules were found when mapping to SCADA firewalls; mapping averaged 53 seconds per case study.
Source: §6 · pp. 10–11Takeaways & Limitations
Mapping policies to the correct SCADA firewalls reduced network vulnerability to cyberattack and prevented catastrophic attack outcomes.
Source: §6 · p. 11Valid device paths must account for endpoint transit capability, since allowing transit can potentially expose grouped high-risk systems to cyberattacks.
Source: §3 · p. 4
Abstract
from arXiv · showhide
A common requirement in policy specification languages is the ability to map policies to the underlying network devices. Doing so, in a provably correct way, is important in a security policy context, so administrators can be confident of the level of protection provided by the policies for their networks. Existing policy languages allow policy composition but lack formal semantics to allocate policy to network devices. Our research tackles this from first principles: we ask how network policies can be described at a high-level, independent of firewall-vendor and network minutiae. We identify the algebraic requirements of the policy mapping process and propose semantic foundations to formally verify if a policy is implemented by the correct set of policy-arbiters. We show the value of our proposed algebras in maintaining concise network-device configurations by applying them to real-world networks.
1 INTRODUCTION
The introduction motivates top-down policy mapping as a way to derive device configurations from high-level specifications, then proposes algebraic foundations for mapping policies correctly and efficiently. It outlines application to real SCADA networks, including concise firewall configurations and what-if analysis.
1 INTRODUCTION
- Manually configuring heterogeneous network devices box by box is impractical; top-down configuration derives device settings from a high-level specification.The specification provides a single source of truth for determining who is permitted to access the network.Source: §1 · p. 1
- Accurate policy mapping is needed to enforce policies correctly and track device-level changes so redundant updates can be avoided.Source: §1 · p. 1
- Mapping must decouple policies from vendor and network details, support formal verification and complex node and link properties, and be efficient.Source: §1 · p. 1
- The paper proposes a generic algebraic framework for mapping policies to devices while preserving the semantics of sequential and parallel composition for correct deployment.The framework is also intended to make policy mapping efficient.Source: §1 · pp. 1–2
- The approach is applied to real SCADA networks to maintain concise firewall configurations and support what-if analysis of policy or topology changes.Administrators can observe which network devices would be required to implement the changes.Source: §1 · p. 2
2 BACKGROUND AND RELATED WORK
The section contrasts bottom-up network construction, where policies emerge from device and configuration decisions, with top-down specification of policy intent. It notes that existing languages offer this abstraction but still have limitations in network independence and provably correct device allocation.
2 BACKGROUND AND RELATED WORK
- Networks are often built bottom-up, so policy becomes implicit in interacting device purchases and configuration decisions; best-practice guides instead recommend designing policy first [Byres et al., 2005; ANSI/ISA-62443-1-1, 2007].Source: §2 · p. 2
- Top-down approaches in SDN and traditional networks maintain a high-level network-wide policy that captures intent rather than implementation details [Soulé et al., 2014; Anderson et al., 2014; Prakash et al., 2015; Bartal et al., 2004; Cisco Systems, 2014].Source: §2 · p. 2
- Although intent-focused policies can aid change management and compliance comparison, many still require hostnames or IP addresses as input [Bartal et al., 2004; Cisco Systems, 2014; Soulé et al., 2014].Source: §2 · p. 2
- Existing top-down languages support network-wide policies but lack a way to allocate them to devices provably correctly [Bartal et al., 2004; Prakash et al., 2015; Cisco Systems, 2014].Source: §2 · p. 2
- The authors’ earlier network- and vendor-independent firewall policy language motivates this paper’s focus on the requirements for mapping high-level policies to devices.Source: §2 · p. 2
3 ABSTRACT POLICIES
This section develops policy-to-device mapping around endpoint-pair/edge abstractions, with composition determined by topology and policy context. It applies those semantics to QoS, security, and traffic measurement, while accounting for endpoint transitivity and device-path constraints.
3 ABSTRACT POLICIES
- Parallel and serial routes compose policies differently; for traffic measurement, the examples use intersection for parallel routes and union for serial routes, with operator meanings depending on policy context.The symbols ⊕ and ⊗ denote parallel and serial composition, respectively.Source: §3 · p. 3
- Parallel routes require mapping to each arbiter, whereas serial routes may need only one; redundant paths and intermediate-endpoint transit capability also constrain valid deployment.Mapping to every serial arbiter may be inefficient or exceed device capabilities.Source: §3 · pp. 3–4
- Simple-edge mapping gives each edge one policy to track and treats endpoint-pairs as independently programmable network slices, avoiding hyper-edges’ imprecise one-to-many policy tracking.The paper associates the simpler graph with easier policy debugging and management by distinct policy subdomains.Source: §3 · p. 3
3.1 Quality of Service (QoS) Policies
- For QoS, parallel guarantees add while serial guarantees take the minimum; a route-dependent policy also requires intermediate endpoints to forward traffic.The examples express these operations as sum(B1,B2) and min(B3,B4), respectively.Source: §3.1 · p. 4
3.2 Security Policies
- Security composition uses the union of packets permitted by parallel filters and the intersection permitted by serial filters, while endpoint and edge definitions must capture security-specific grouping.The paper says a generic endpoint-pair/edge abstraction cannot capture such network-security concepts precisely.Source: §3.2 · p. 4
3.3 Traffic Measurement Policies
- For traffic measurement, parallel devices guarantee capture of the intersection of their captured packet sets, while serial devices capture the union.This is the converse of the security-policy composition examples in the preceding subsection.Source: §3.3 · p. 5
- Mapping must consider all feasible paths, excluding paths that repeat a physical firewall interface or traverse non-transit zones; directed conduits encode interface direction.The paper contrasts this with routing’s search for a best path and notes that relatively few endpoints can make centralized computation tractable.Source: §3.3 · pp. 5–6
- The Zone-Conduit model concretizes endpoint-pair/edge security policies: zones group systems by security requirements, conduits provide secure paths, and policy intent is separated from enforcement topology.The paper also notes that the original ISA model is extended for greater policy-specification precision.Source: §3.3 · p. 5
4 MAPPING ALGEBRA
The mapping algebra constructs valid device paths from policy edges and composes arbiter policies according to their context. A right-iteration algorithm computes paths while accounting for zone transitivity.
4.1 Firewall-path Construction
- Primary edges use policy arbiters, while secondary edges also traverse additional endpoints; valid firewall paths exclude repeated interfaces and non-transit zones.The path algebra treats union as order-independent but concatenation as order-sensitive.Source: §4.1 · pp. 6–7
4.2 Mapping Policy to Arbiters
- Mapping requires arbiter policies to compose into the intended high-level policy, with the meanings of sequential and parallel composition varying by policy context.For QoS, parallel composition sums and sequential composition takes the minimum; traffic measurement uses intersection and union, respectively.Source: §4.2 · p. 8
4.3 Computation of All Firewall-paths
- A right-iteration algorithm computes A∗, the matrix of valid primary- and secondary-conduit firewall paths, using an explicit zone-transitivity matrix.For bounded semirings, it iterates n−1 times, where n is the number of nodes in the Zone-Conduit model.Source: §4.3 · p. 8
- When zone 4 is non-transitive, the computed paths from zone 1 to 3 exclude paths through zone 4.The example identifies E14F43 and E14G43 as removed paths.Source: §4.3 · p. 9
5 IMPLEMENTATION
The implementation couples a high-level policy with a network topology, constructs zone and path representations, and computes a policy-to-device mapping. Its all-path calculation has O(n4) time complexity.
5 IMPLEMENTATION
- The mapping process takes a topology-independent high-level policy and a GraphML topology as inputs, then produces a policy-to-device map and verification output.The map breaks policy down by device, interface, and direction; the verification output is suited to identifying policy errors.Source: §5 · p. 9
5.1 Zone-transitivity Matrix and Adjacency Matrix Construction
- The system builds a Zone-Firewall model from the topology, defines primary conduits, compiles policy transitivity capabilities, and constructs the zone-transitivity matrix T and adjacency matrix A.Implicit mappings between primary conduits and firewall compositions support construction of A.Source: §5.1 · p. 9
5.2 A∗Calculation
- O(n4) is the algorithm’s time complexity; for SCADA networks with n < 25, mapping runs on average in 53 seconds per network on a standard desktop computer.The authors suggest grouping hosts, for example by subnet, to keep n reasonably low.Source: §5.2 · p. 10
- The calculation considers all valid paths between zones, supporting policy decisions along every possible communication path; other contexts may instead use a subset or a single path.The authors note that selecting shortest paths would yield O(n3).Source: §5.2 · p. 10
6 A SERIES OF CASE STUDIES
Seven real SCADA-firewall case studies show that the algebras mapped high-level policies to firewalls with no incorrectly allocated rules. The section also reports the configuration errors found in the existing cases, the small zone counts, and mapping runtime.
6 A SERIES OF CASE STUDIES
- Each network had at most 21 security zones despite a potential host count of up to 67580, making the zone-based mapping algorithm computationally tractable.Zones group hosts or subnets with identical policies.Source: §6 · p. 10
- Mapping high-level policy to network devices took an average of 53 seconds per case study on a standard desktop computer.The reported machine had a 2.7-GHz Intel Core CPU and 8GB RAM.Source: §6 · p. 10
- Existing configurations averaged 10 wrong-firewall, 8 wrong-interface, and 15 wrong-direction ACL allocations per SCADA case study.Wrong-interface means the correct firewall but an unsuitable interface; wrong-direction means the correct firewall and interface but reversed direction.Source: §6 · pp. 10–11
- Zero policy rules were incorrectly allocated across the seven SCADA case studies mapped with the proposed algebras.The case studies are summarized in Table 1.Source: §6 · pp. 10–11, Table 1 · p. 11
7 CONCLUSIONS
The conclusion identifies policy-network coupling and complex policy semantics as obstacles to precise device mapping. It proposes a mathematical foundation for mapping policies to network devices and using it to deploy real-world security policies to firewalls provably correctly.
7 CONCLUSIONS
- Precise mapping is hindered by policy dependence on network and vendor details and by semantics involving node and link properties.The conclusion highlights network decoupling as a central obstacle.Source: §7 · p. 11
- The paper proposes a mathematical foundation for mapping policies to network devices and applies it to real-world security policies on firewalls.The conclusion characterizes the deployment as provably correct.Source: §7 · p. 11
- The proposed approach is intended to give administrators confidence in the protection their network policies provide.Source: §7 · p. 11
Appendix
The appendix proves an iterative calculation for firewall-path matrices. Its recurrence extends paths by a hop while accounting for zone transitivity and self-paths.
Appendix
- Theorem 4 states that A* can be calculated using the right iteration algorithm.Source: Appendix · p. 12
- The induction handles non-transitive intermediate zones and corrects the diagonal case so a zone has its self-firewall path.The base case identifies A<1> with the valid single-hop paths represented by A.Source: Appendix · p. 12
- The recurrence A<n+2> = (A<n+1>T ∪ I)A extends valid firewall paths between zones to at most n+2 hops.T is the Zone-transitivity matrix and I is the multiplicative-identity matrix of the stated semiring.Source: Appendix · pp. 12–13