Кафедра ИУ3
27 мая 2014, 16:00

Логический анализ поведения межсетевых экранов

Докладчик: Тун М.Т.

Организация: МГТУ им. Н. Э. Баумана

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