A firewall algebra for OpenStack

An algebra is proposed for constructing and reasoning about anomaly-free firewall policies. Based on the notion of refinement as safe replacement, the algebra provides operators for sequential composition, union and intersection of policies. The algebra is used to provide a uniform way to specify and reason about OpenStack host-based and network access controls, in particular, security group and perimeter firewall policies.