Mignis: A semantic based tool for firewall configuration

ABSTRACT. The management and specification of access control 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 Netfilter, a firewall system integrated in the Linux kernel. We define an abstraction of the concepts of chains, rules, and packets existent in Netfilter 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 which are unaffected by the relative ordering of rules and that does not depend on the underlying Netfilter chains. We give a semantics for this language and show that it can be translated into our Netfilter abstraction. We present Mignis, a publicly available tool that translates abstract firewall specifications into real Netfilter configurations. Mignis is currently used to configure the whole firewall of the DAIS Department of Ca’ Foscari University.