AUTOMATION OF VERIFICATION OF INCORRECTNESS FOR FIREWALL CONFIGURATIONS
This article is devoted to the automation of the search of firewall configuration errors on the basis of logical analysis. As a rule, process models have been used for a description the behavior of firewalls, and the language of modal logic has been applied in order to formulate requirements (properties) of incorrectness. We focus on the presentation of a detailed methodology of the transition from process models of a description the behaviors of firewalls and conditions of their incorrectness (which were formulated in the language of modal logic) to the specific logical programs that allows to implement verification of incorrectness of firewall configurations