Mignis: A semantic based tool for firewall configuration

The management and specification of access control rules that enforce a given policy is a non-trivial, complex, and time consuming task. In this paper we aim at simplifying this task both at specification and verification levels. For that, we propose a formal model of Net filter, a firewall system integrated in the Linux kernel. We define an abstraction of the concepts of chains, rules, and packets existent in Net filter configurations, and give a semantics that mimics packet filtering and address translation. We then introduce a simple but powerful language that permits to specify firewall configurations that are unaffected by the relative ordering of rules, and that does not depend on the underlying Net filter chains. We give a semantics for this language and show that it can be translated into our Net filter abstraction. We then present Mignis, a publicly available tool that translates abstract firewall specifications into real Net filter configurations. Mignis is currently used to configure the whole firewall of the DAIS Department of Ca' Foscari University.