A firewall is one of the major security tools available for protecting computer domains. Today, almost all companies have at least one firewall to filter incoming and outgoing traffic according to some requirements called security policy. The configuration of firewalls is however complex and error prone. During the last years, many techniques and tools have been proposed to analyze firewalls. However, most of existing worksare informaland the formalfoundationof firewall is still a missing part. The goal of this paper is to present an overview of the most important problems related to the firewall configuration and analysis. Also, it proposes a formal language for the specification and the verification of firewalls.