The Mathematical Foundations for Mapping Policies to Network Devices (Technical Report)

TL;DR

This paper develops a formal mathematical framework for mapping high-level network policies to specific devices, ensuring correctness and security in network configurations.

Contribution

It introduces algebraic and semantic foundations for policy mapping, enabling formal verification and vendor-independent policy implementation.

Findings

Formal semantics for policy mapping are established.

Application to real-world networks demonstrates effectiveness.

Supports verification of correct policy deployment.

Abstract

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.