Verification and synthesis of firewalls using SAT and QBF
Verification and synthesis of firewalls using SAT and QBF
复制标题
使用SAT和QBF验证和综合防火墙
DOI：
10.1109/icnp.2012.6459944
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
S. Narain
中科院分区：
文献类型：
--
作者：
Shuyuan Zhang;Abdulrahman Mahmoud;S. Malik;S. Narain
防火墙被广泛部署以保护网络的安全性，对于企业网络来说，拥有防火墙以防止恶意攻击并确保网络的正常功能至关重要。防火墙可以通过查找访问控制列表（ACL）来允许或丢弃某些数据包来防止危险数据包进入内部网络。但是，ACL通常会遇到冗余问题，这会降低防火墙和网络的性能。本文的贡献是三重的：1）我们提出了一种基于布尔的满意度（SAT）技术，可以比较两个防火墙之间的等价和包容关系，这对于给定的防火墙和优化的一个，2）非常有价值我们提出了一种在防火墙中发现冗余的技术，3）我们将ACL优化问题作为量化的布尔公式问题（QBF），并探索其使用QBF求解器的实际应用。
Firewalls are widely deployed to safeguard the security of networks and it is critical for enterprise networks to have firewalls to prevent malicious attacks and to guarantee the normal functioning of the network. Firewalls prevent dangerous packets from entering the inner network by looking up the Access Control List (ACL) to permit or drop certain packets. However, ACLs often suffer from redundancy problems, which can degrade the performance of firewalls and the network. The contribution of this paper is threefold: 1) we present a Boolean Satisfiability (SAT) based technique that can compare the equivalence and inclusion relationship between two firewalls, which is very valuable for the testing between a given firewall and an optimized one, 2) we present a technique to discover redundancies within a firewall, and 3) we formulate the ACL optimization problem as a Quantified Boolean Formula problem (QBF) and explore its practical application using a QBF solver.