This article focuses on static analysis for firewall configuration errors. In contrast to the well-known works in this paper we propose to describe the behavior of the firewalls as process models and not as access control lists ACL (ACL - Access Control Lists).The expressive possibilities of process models are much wider and more developed that allow describing a much more complex model of the configuration software. Static analysis is proposed to realize by the methods of logic programming as a proof properties of the configuration process that is much more elegant, full and unfettered approach to validate the configuration of firewalls. Requirements (properties) of correctness is proposed to formalize in the language of modal logic. The formal description of the properties is transformed in the goal of Prolog. The article gives examples of logic programs to validate the configuration of firewalls in Prolog and the results of their tests.