Model Checking Firewall Policy Configurations
Model Checking Firewall Policy Configurations
复制标题
模型检查防火墙策略配置
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
T. Samak
中科院分区：
文献类型：
--
作者：
A. Jeffrey;T. Samak
使用防火墙来强制执行访问控制策略可能会导致非常复杂的网络。每个防火墙可能都有数百或数千个规则，并且在网络中合并时，它们可能会导致意外的组合行为。为了减轻此问题，最近人们对使用模型检查技术来分析防火墙策略配置的行为和报告异常感兴趣。防火墙策略分析的现有技术基于决策图，大多数通常减少了有序的二进制决策图（BDDS）。 BDD是一种丰富的数据结构，不仅仅是解决布尔公式，支持更多的逻辑操作。通常，搜索布尔值的搜索算法（所谓的卫星赛车）优于BDD。在本文中，我们表明，BDD提供的额外结构对于防火墙政策分析不是必需的，而SAT求解器就足够了。理论分析和实验数据都支持该论点。
The use of firewalls to enforce access control policies can result in extremely complex networks. Each individual firewall may have hundreds or thousands of rules, and when combined in a network, they may result in unexpected combined behavior. To mitigate this problem, there has been recent interest in the use of model checking techniques for analyzing the behavior of firewall policy configurations, and reporting anomalies. Existing techniques for firewall policy analysis are based on decision diagrams, most normally reduced ordered Binary Decision Diagrams (BDDs). BDDs are a rich data structure, supporting more logical operations than just solving boolean formulae. Typically, search algorithms for boolean satisfiability (so-called SAT-solvers) outperform BDDs. In this paper, we show that the extra structure provided by BDDs is not necessary for firewall policy analysis, and that SAT solvers are sufficient. This argument is supported both by theoretical analysis and by experimental data.