Inconsistency Analysis of Time-Based Security Policy and Firewall Policy
Inconsistency Analysis of Time-Based Security Policy and Firewall Policy
复制标题
DOI：
10.1007/978-3-319-68690-5_27
复制
发表时间：
2017-11
期刊：
影响因子：
--
通讯作者：
Yi Yin;Y. Tateiwa;Yun Wang;Y. Katayama;N. Takahashi
中科院分区：
文献类型：
--
作者：
Yi Yin;Y. Tateiwa;Yun Wang;Y. Katayama;N. Takahashi
防火墙中的数据包过滤根据一组称为防火墙策略的预定义规则接受或拒绝数据包。近年来，基于时间的防火墙策略在许多防火墙中广泛使用，例如思科ACL。防火墙策略始终是在安全策略的指导下设计的，安全策略是概述网络访问权限需求的通用文档。正常的防火墙策略和安全策略的一致性很难保持，更不用说基于时间的防火墙策略和安全策略了。尽管有很多安全策略和防火墙策略的分析方法，但它们都不能处理时间限制。为了解决这一问题，我们首先将基于时间的安全策略和防火墙策略表示为逻辑公式，然后使用可满足性模理论(SMT)solverZ3对它们进行验证和不一致性分析。我们已经实现了一个原型系统来验证我们提出的方法，实验结果表明了该方法的有效性。
Packet filtering in firewall either accepts or denies packets based upon a set of predefined rules called firewall policy. In recent years, time-based firewall policies are widely used in many firewalls such as CISCO ACLs. Firewall policy is always designed under the instruction of security policy, which is a generic document that outlines the needs for network access permissions. It is difficult to maintain the consistency of normal firewall policy and security policy, not to mention time-based firewall policy and security policy. Even though there are many analysis methods for security policy and firewall policy, they cannot deal with time constraint. To resolve this problem, we firstly represent time-based security policy and firewall policy as logical formulas, and then use satisfiability modulo theories (SMT) solverZ3to verify them and analyze inconsistency. We have implemented a prototype system to verify our proposed method, experimental results showed the effectiveness.