  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.
