Статья посвящена статическому анализу поиска ошибок конфигурирования межсетевых экранов (брандмауэров). В отличие от известных работ для моделирования поведения брандмауэров предлагается использовать не списки управления доступом ACL (ACL - Access Control Lists), а процессные модели, выразительные возможности которых гораздо шире, а теория более развита, что позволяет описывать гораздо более сложные модели программ конфигурирования. Статический анализ поиска ошибок предлагается осуществлять методами логического программирования как доказательство или вывод свойств процессов конфигурирования, что является гораздо более изящным, полным и не имеющим ограничений подходом проверки корректности конфигурирования брандмауэров. Требования (свойства) корректности предлагается формализовать на языке модальной логики. Переход от этого формального описания свойств предлагается алгоритмически формировать как цель в языке ПРОЛОГ. В статье приводятся примеры логических программ проверки корректности конфигурирования брандмауэров на языке ПРОЛОГ и результаты их испытаний.