基于自动机的防火墙安全策略研究

Journal of King Saud University沙特国王大学沙特国王大学学报www.ksu.edu.sawww.sciencedirect.com防火墙安全策略Ahmed Khoumsia，*，Mohammed Erradib，Wadie Krombiba加拿大舍布鲁克大学电子计算机工程系b摩洛哥拉巴特穆罕默德五世大学ENSIAS接收日期：2016年5月29日;修订日期：2016年11月16日;接受日期：2016年11月16日2016年11月30日在线发布摘要防火墙是网络安全策略的核心。提出了一种基于自动机的防火墙安全策略研究方法。我们首先提出了一个程序，synn- thesizes一个自动机，描述了一个安全策略作为一个表的规则。然后，综合程序被用来开发程序，以检测：不完整性，异常和差异的安全政策。一种方法被开发来表示自动机的政策合格的混合，并具有实际的效用，如容易确定的白名单和黑名单的政策。所开发的程序已在时间和空间的复杂性方面进行了深入的评估。然后，进行了一个真实的案例研究。所得到的结果证实，开发的过程具有合理的复杂性，其实际执行时间是秒的顺序。最后给出了所有结果的证明。©2016作者。制作和主办由爱思唯尔B.V.代表沙特国王大学。这是CC BY-NC-ND许可下的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。1. 介绍当今世界通过互联网完全连接，而其安全性仍然是研究和工业界的一大挑战网络攻击获得了巨大的关注，并构成了网络管理人员的日常威胁和当务之急。防火墙作为网络安全的重要组成部分，已经被广泛应用于抵御这些攻击的前沿阵地.*通讯作者。电子邮件地址：Ahmed. USherbrooke.ca（A.Khoumsi）。沙特国王大学负责同行审查今天，防火墙被认为是任何定义良好的网络安全策略的核心元素。防火墙安全策略由用于过滤来自安全网络的传入和传出通信（数据包）的过滤规则组成。设计不佳的防火墙安全策略可能导致接受恶意数据包或拒绝可接受的数据包。因此，防火墙安全策略的正确设计和分析是许多研究人员已经解决的重要问题，例 如 Acharya 和 Gouda （ 2010 ， 2011 ） ， Al-Shaer 和Hamed （ 2004 ） ， Al-Shaer 等 人 （ 2009 ） ， Bryant（1986），Cuppens等人（2012），Garcia-Alfaro等人（ 2012 ） ， Al-Shaer 等 人 （ 2013 ） ， Al-Shaer 等 人（2014），Al-Shaer等人（2013），Bryant（1986），Cuppens等人（2012），Garcia-Alfaro等人（2013）。（2008年，2013）、Hoffman和Yoo（2005）、Kalam等人（2003）、Kamara等人（2003）、Karoui等人（2013）、Liu等人（2007、2008、2010）、Lee和Yannakakis（1996）、Lu等人（2007）、Mallouli等人（2007）、Madhuri和Rajesh（ 2013 ） 、 Mansmann 等 人 （ 2012 ） 、 Pozo 等 人（ 2012 ） 、 Wool （ 2004 ） 、和 Yuan et al. （ 2006年）。阻碍，术语政策和规则http://dx.doi.org/10.1016/j.jksuci.2016.11.0081319-1578© 2016作者制作和主办由爱思唯尔B.V.代表沙特国王大学。这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。制作和主办：Elsevier关键词防火墙安全策略;自动机策略;完整性验证;异常检测;离散检测;混合策略;空间和时间复杂性52A. Khoumsi等人分别表示“防火墙安全策略“和”过滤规则”。在现有的作品中，每一个建议的形式主义解决一个特定的防火墙设计或分析方面，以解决一个特定的问题。这激发了目前的工作，其中一个自动机为基础的方法开发，以解决不同的问题，使用单一的形式主义。这种方法是基于一个自动机，描述了一个政策最初指定的规则表的建设。该自动机用于检测策略中的不完整性、异常和差异。还提出了一种方法来表示自动机的规则表称为混合策略，具有实际效用。所提出的程序已经在时间和空间复杂性方面进行了深入的评估;请注意，我们的复杂性评估比文献中更精确。所得到的结果作为正式证明的命题。此外，我们讨论了陈等人的一个现实生活中的政策用例的结果。（2012年）。本文其余部分的结构如下。第二节介绍了相关工作.第3节中给出了有关政策的说明。在第4节中，我们提出了一个程序，描述最初由规则表指定的策略的自动机。第5-在第5节中，我们提出了一个方法，确定一个策略是否完整。第6节定义了两类异常，分为冲突和非冲突。在第7节中，我们提出了检测三种类型的冲突异常的方法：阴影，一般化和相关异常。第8节提出了检测两种类型的非冲突异常的方法：LP冗余和MP冗余。在第9节中，我们展示了描述策略的自动机如何用一种叫做混合策略的实用形式。第10节介绍了一种检测和解决同一策略的几个设计之间的差异的方法。在第11节中，我们根据空间和时间复杂性评估了第4节至第10第12节讨论了我们的方法在一个真实案例研究中的应用。在第13节中，我们回顾了我们的贡献，并提出了未来研究的想法。最后，在附录A中给出了我们结果的形式证明。2. 相关工作和贡献Hoffman and Yoo（2005），Wool（2004），Kamara etal.（2003）等在防火墙方面的研究提供了一些实用的分析算法，例如测试、分析配置和检测策略中的漏洞 。 Acharya 和 Gouda （ 2010 ， 2011 ） ， Liu 和 Gouda（2008，2010），Al-Shaer等人（2009）是更基本的，并提供了时间复杂度估计的分析算法。Elmallah和Gouda（2014）表明，防火墙的几个问题的分析是NP难的。Madhuri和Rajesh（2013）通过存在至少一个与策略的多个规则匹配的数据包来定义策略中的异常。 Al-Shaer和Hamed（2004）、Karoui等人（2013）提出了检测策略中的异常的技术，其中策略由Al-Shaer和Hamed（2004）中 的 策 略 树 和Karoui 等 人 中 的 决策 树指 定 。（ 2013年）。Garcia-Alfaro等人（2013），Cuppens等人（2012）提出了研究状态异常的方法。Liu和Gouda（2008）展示了如何检测同一策略的几种设计之间的差异，其中策略由Liu和Gouda（2007）定义的防火墙决策图（FDD）建模。Yuan等人（2006）介绍了一个工具包Fireman，它可以检测几种类型的错误，例如违反或不一致的政策。Fireman 是 用 二 进 制 决 策 图 （ Binary Decision Dia-grams，BDD）（Bryant，1986）实现的.Mallouli等人（2007）提出了一个框架来生成测试序列，以检查策略与规范的一致性。 系统行为由扩展的自动机描述（Lee和Yannakakis（1996）），并且我们希望应用于该系统的策略由基于组织的访问控制（OrBAC）描述（Kalam等人， 2003年）。Lu等人（2007）提出了一种方法来验证两个策略是否等效。Mansmann等人（2012）提出了一种可视化和分析防火墙配置的工具，其中策略以分层方式建模。Pozo等人（2012）提出了CONFIDDENT，一个模型驱动的防火墙设计，开发和维护框架。Garcia-Alfaro等人（2008）提出了一种机制来检测安全策略的配置规则中的异常。在上述每一项工作中，使用给定的形式化解决了一个特定的问题：分别使用策略树（Al-Shaer和Hamed，2004）、FDD（Liu和Gouda，2007）和BDD（Bryant，1986）研究异常、差异和违规/不一致。这一观察激发了Krombi et al.（2014），Khoumsi et al.（2014）的工作，其中使用相同的自动机模型来解决各种政策问题。本文对后两篇文献作了改进，并有以下新的贡献：1. 我们展示了我们的方法如何比FDD更有趣，特别是在删除，添加，修改和切换策略中规则的效率方面（见第4.5节）。2. 我们提出了一种方法来解决策略的几个实现之间的差异（见第10节）。3. 我们展示了如何构建可混合的策略并阐明它们的效用 ， 特别 是 确定 策 略 的白 名 单 和黑 名 单 （见 第9节）。4. 我们评估了执行策略自动机的空间和时间复杂度，并表明这种自动机执行比执行策略规则表更有效（见Prop. 18）。5. 我们正式证明了第4节至第11节中给出的所有结果（包括Krombi et al.（2014），Khoumsi et al.（2014）中已经给出的结果）（见附录A）。6. 我们举例说明我们的方法在现实生活中的政策中的应用（见第12节）。7. 我们更清楚地解释了为什么我们的复杂性评估比文献中更精确（第11.2、11.3和11.4节）。为了有一个自包含的论文，我们还介绍了Krombi et al.（2014），Khoumsi et al.（2014）的主要贡献。事实上，由于本文是第一个正式证明这两个参考文献的结果，他们的贡献。安全实施是另一个相关的问题，可以简单地定义为自动防止不可信的系统防火墙安全策略的设计与分析53¼-[半]半个小时 ]ω我我违反安全政策Sui和Mejri（2013）提出了一种在不受信任的程序上实施安全策略的方法。Shen等人（2013）研究了云存储环境中的安全实施。安全执行是我们近期的工作之一（更多细节将在未来工作列表中给出，第13节）。3. 预赛防火墙的策略是一组规则，指定应用于到达防火墙的数据包的操作（例如接受、拒绝）因此，规则R可以由一对（Condition，Action）定义，这意味着：如果到达防火墙的数据包P满足Condition，则必须对P应用Action（授权或拒绝访问）。以下是关于规则R的条件和动作的更多精确度：条件由多个（比如m个）过滤字段指定F0;.. . ; Fm-1，其中每个F j是一组值。到达防火墙的每个数据包P都有几个报头H0;. ; H m-1，其中每个H j是一个值。 条件满足P（也称为：P匹配R），如果对于每个j0;. .m1：Hj属于Fj.动作可以是接受或拒绝，包括授权或阻止P穿越防火墙。表1表示策略描述的结构：每个规则Ri由若干字段F0;. ;Fm-1表示-通过属于Port的端口由属于Protocol的协议传输。例 如 ， 具 有 报 头 （ 190.170.15.10 ） 、（82.15.15.11）、（25）、（UDP）的数据包是来自190.170.15.10的数据包，目的地是82.15.15.11，并且通过UDP协议通过端口25传输。这个数据包被防火墙接受，因为接受是R4的动作，这个数据包匹配的唯一规则。4. 自动机构造在本节中，我们介绍自动机的构造过程。 给定一个表的几个（说n）规则R 1;. R n指定一个策略F，该过程构造一个描述F的自动机。自动机A可以表示为由标记的转换连接的状态图（表示为节点）。我们考虑具有一个初始状态和一个或多个最终状态的自动机。一个自动机接受所有的transi- tions序列开始在其初始状态，并达到最终状态;这些序列的集合被称为语言的自动机。整数的区间由通常的符号指定a;b，a;b，a;b和a;b。表3定义了一些符号在图中使用。1和2.4.1. 第一步：通过自动机每个规则Ri都由一个具有m1个状态的自动机Ai来在Ri的条件下，通过作用ai。 规则是q0;q1;... 其中q0和qm是初始状态和最终状态，我我按优先级递减排序，即当分组P到达时，分别 每个q j（j-m）通过一个transi连接到q j <$1，我我防火墙，我们首先验证P是否匹配R1：如果是，则1是exe-用Fj的值的区间的名称来标记Tj。A我我我切;否则（即，P不匹配R1），我们验证P是否与R2吻合以此类推，直到我们找到一条与P匹配的规则，或者所有规则都被验证。表2中给出了策略的示例，其中每个规则的条件由字段IPsrc、IPdst、端口和协议定义。Fj列中的符号表示Fj的定义域的任何值。表达式a： b： c： 0= x表示通过将所有可能值赋予32位值a： b： c： 0中的32-到达防火墙的分组P匹配规则Ri，如果它来自并且目的地分别属于IPsrc和IPdst的地址，并且111n n nR2190： 170： 15： 0= 24 80： 15： 15： 0= 2425; 81 TCP拒绝表3图中使用的符号。1和2.2019 - 02-15 00：00：00 00： 0000：00190： 170：15： 0b1¼80： 15：15： 0I1½½0;a1½K11/4/20;25K21/4/25;81K31/4/81;83K41/4/83;216J1¼½0;b1I2¼½a1;a2][J2¼½b1;b2]32J3¼b2;232I3¼a2;2●●表1策略说明的结构。规则F 0.. .Fj...Fm-1行动R1F 0.. .Fj...Fm-1的1.. .. . ... ......... ....RnF0.. .F j...F m-1an表2政策的例子规则IPsrcIPdst端口议定书行动R1ω80： 15：15： 0= 24ωω接受R3190： 170： 15： 0= 24 80： 15： 15： 0= 24 25; 83ω接受R4ω接受54A. Khoumsi等人我我我ðÞ我！H12 12JR1/4小时iR我M●ðÞ1哎！ hi一个！1212i！H 12R12●hi32½ÞJ图1步骤1：从表2的策略中获得的自动机。图2步骤2：通过标准化区间图的自动机。1.一、还包含状态Ei，使得每个状态qj（j-m）通过由与标记为Tj的间隔互补的间隔标记的转换连接到Ei。直观地，状态qm（resp.Ei）在分组匹配时达到（相应地，不匹配）Ri.例如，从表2的策略的四个规则，我们分别得到图1的四个自动机。IP地址占32位，端口号占16位，考虑两种协议：UDP和TCP。Singleton interval由它们的唯一值指定，如25，81，83。4.2. 第二步：标准化自动机设状态的级别q是从初始状态到达到q所执行的转换的数量，并且例如，我们从图2的自动机得到图2的自动机。1 .一、4.3. 第三步：组合自动机步骤3的目的是通过应用结合所获得的自动机的乘积算子来构造自动机在步骤2中。该操作符要求要组合的自动机具有相同的字母表，这证明了步骤2。让我们首先归纳地展示如何将步骤2中获得的两个自动机Aω1和Aω2组合成记为Aω1Aω2的自动机：通过组合A ω和A ω的初始状态q0和q0来 构 造 初 始 状 态 q 0 ; q 0。1 2 1 2这是其起源国的水平各种自动机在步骤1中获得的字符串不使用相同的字母表。考虑例如图1的自动机的0级转换。一 曰：● 对于Aω1Aω2的每个构造状态hr1;r2i和每个标签r：–IfRrA和A使用½0;232，而A和用半a;a]，半0;a一个！s1和r2！S21 4 23121然后分别构造状态hs1;s2i和和一个2;232.步骤2的目的是重写自动机，使他们有相同的字母表（这种重写过渡s;s岛–If 俄.西和r1/4E，然后是con-对步骤3有用）。这是通过将每个域Fj的域划分为一组不相交的区间来实现的，使得标记任何Ai的级别j转变的每个区间是该划分的区间的并集对于每个水平j，我们如下进行我们构造一个有序列表（按递增顺序）L，其中包含标记第j级变迁的区间的端点。例如，对于图1的自动机的第0级，所获得的有序列表是L00;a1;a2; 232。我们定义的区间，其端点是连续元素的排序列表。这些区间形成域Fj的定义域的一个划分。例如，从上面的排序列表L0中，我们定义了区间I1;I2和I3，它们形成了1/ 20;23 2n的划分。 （符号I1、I2和I3见表3。）我们考虑由区间I标记的每个转换，并将其替换为由形成I的分区的区间标记的转换。例如，标记为0; 2的转换分别被标记为I1;I2和I3的3个转换替换。构造 状态hs1;E2i和转换hr; Es;E i.-如果A ω 2有跃迁r 2！s2和r1/4E1，然后构造状态 hE1;s2i 和过渡E1; r2E1;s2.图中给出了两个自动机乘积的一个简单例子。3.第三章。两个以上自动机的乘积是通过迭代两个自动机的乘积来简单地我们用CF表示Aω1;. . ;Aωn. CF状态定义为1;. . . 其中ri可以是q或Ei。CF的每个最终● 匹配状态是使得对于一个或多个i，r i^qi的状态。设R i是具有最小索引i的规则，使得ri- E i ; R i的动作与这样的匹配状态相关联。不 匹配状态是状态E1;E2;. . ;En.没有与之关联的操作。例如，如果我们将步骤3应用于图4的四个自动机。2，我们得到图2的自动机CF。 四、在自动机里●●●212防火墙安全策略的设计与分析551我23412341416例如，让我们示出图4的自动机CF可以如何用于执行表2的策略F。考虑到防火墙被一个数据包P到达，该数据包P的报头H0到H3分 别 是190：170：15：12 bits; 180：15：15：20 bits; 123bits和124 TCP bits。 我们从h，q，q，q，i开始. 我们执行过渡标记为190： 170： 15： 0= 24（含H0），达到1111图3两个简单自动机的乘积：（c）=（a）和（b）的乘积hq1;q2;q3;q4i.然后，我们执行的标记跃迁8 0：1 5：1 5：0=24（包含H1 ），达到 hq2;q2;q2;q2i。然后，我们执行标记为not 25;81; 83（包含H2）的转换，并到达hq3;E2;E3;q3i。最后，我们执行转换标记的TCP（含H3）和到达hq4;E2;E3;q4iassocii-1 4所以P是可以接受的。4.5.自动机的高效构造图4步骤3：自动机CF通过组合图4的自动机获得。二、Liu和Gouda（2007，2008）提出了一个有趣的相关工作模型和分析政策。我们的方法的优点是存储的政策规则信息的状态的自动机。此外，与我们的方法，删除，添加，修改和切换规则的策略不需要从一开始就重建自动机。让我们首先考虑规则删除，即。我们必须从AF得到自动机AFnR。我们将通过图3的例子来说明我们的过程，其中（a）和（b）是两个规则R1和R2的自动机，（c）是由R1和R2组成的策略F的自动机。因此，如果我们从F中移除R2，我们的过程应该从（c）生成（a）在第一步中，我们从F的自动机的状态中擦除R的自动机的状态标签。在我们的示例中，我们擦除(b)（即： q0; q1; q2; E2），并获得图（1）。 五、稍等-222的图1和2中，明确指定了标记每个转换的间隔，以帮助读者理解步骤2。在图4中，使用了一种更紧凑的符号，其中符号为ω和notX<$。在第j层的跃迁中的标号ω对应于域F j的定义域。例如，级别2的两个转变中的标签ω对应于间隔1/20;216π（域的F2），这是在事实的联盟K1[K2[K3[K4[f25 g[f 81 g[f 83g. 如果X是一个值的集合，那么notX<$表示我们从中移除X的集合ω。例如，级别2的转换中的标签not 25; 81;83对应于不带值2 5;8 1;83的½ 0 ; 2，这给出第二步，我们删除其起源和目的地的过渡状态被相同地标记在我们的示例中，我们移除图5的（1）中的状态E1的传出转换，并获得(2)图5中。在第三步中，我们最小化自动机。在我们的例子中，我们将图5的（2）中的两个状态E1组合起来，得到图5的（a）。3.第三章。将R到F上很简单：我们构造R的自动机（如4.1节所示），然后使F和R的自动机乘积（如4.3节所示）。用规则R2替换规则R1是通过组合删除R1和添加R2的过程来实现的。切换两个规则Ri和Rj包括在K1[K2[K3[K4.4.4. 执行策略的下面的命题陈述了自动机CF执行F，在这个意义上，当数据包P到达其策略为F的防火墙时，我们可以通过对P执行CF来确定P是否被F接受或拒绝：提案1. 考虑一个防火墙的政策F是由一个数据包P，其头部是H01。 . . Hm-1。 我们开始于CF的初始状态，并执行分别标记为“0;. . ;' m - 1，使得每个' j包含Hj。 设r^hr1;. . . 表示到达的状态。 对于每个ri，我们有ri^q m当且仅当P匹配ri。 如果r是匹配状态（如果P匹配一个或多个规则，则会发生这种情况），则P匹配的最优先级规则的操作正是C F中与r相关联的操作。R1和R2在每个状态中的R1和R2。 . . i，然后重新分配动作以匹配状态。因此，我们的方法的一个优点是，删除，添加，修改和切换规则不需要从一开始就重建自动机。5. 检测不完整性如果每个到达防火墙的数据包都符合F的一个或多个规则，则称策略F是完整的。否则，政策图5规则删除的图示。56A. Khoumsi等人Mm¼¼4MM¼¼1341241234217.1. 阴影异常考虑两个规则Ri和Rj，它们具有不同的动作（即，aiij）。<如果Ri与所有匹配Rj的数据包匹配，则Rj被Ri遮蔽。因此，Rj从未被应用。从这个定义和命题1，我们推出以下命题：3号提案 考虑一个策略F及其两个规则Ri和R j. Rj被 Ri遮蔽当且仅当：ij;ai

下载后可阅读完整内容，剩余1页未读，立即下载