Рассматривается проблема обеспечения информационной безопасности в кредитно-финансовых организациях с использованием межсетевого экрана. Отмечено, что существующие способы и средства защиты не могут в достаточной мере оказывать противодействия постоянно развивающимся киберугрозам, в связи с чем многие исследования в области защиты информации направлены на поиск новых методов, которые могут повысить эффективность применяемых мер. В статье проведен анализ наиболее часто встречающихся угроз информационной безопасности, приводится статистика инцидентов, связанных с применением вредоносного программного обеспечения, которое остается основным инструментом злоумышленников. Также приводится анализ основных проблем обеспечения информационной безопасности на примере типовой модели дистанционного банковского обслуживания (ДБО). Отмечено, что эффективная работа межсетевого экрана, который используется для защиты информации в системе ДБО, возможна только при условии, что задан полный, корректный и непротиворечивый набор правил. Целью данной статьи является разработка метода формальной проверки правил функционирования межсетевого экрана для обеспечения информационной безопасности в кредитно-финансовых организациях. Приведен пример перехода от вербального описания набора правил к формальной логике и программной реализации кода на языке Python с использованием библиотеки Z3. Приведены рекомендации по применению разработанного метода в кредитно-финансовых организациях. Сделан вывод о том, что на объектах кредитно-финансовой сферы со сложными сетевыми информационными системами и множеством правил защиты, на этапе разработки этих правил необходимо предусматривать их формальное описание для возможности автоматизированного тестирования на непротиворечивость средствами SMT-решателей и разработанный метод позволяет решить эту задачу.