协议场景中的隐蔽通道检测新方法

--理论计算机科学电子札记119（2005）93-116www.elsevier.com/locate/entcs场景和隐蔽渠道：另一个游戏...LocHelouet1IRISA/INRIA，Campus de Beaulieu，35042 Rennes Cedex，FranceMarc Zeitoun2LIAFA，Case 7014，2 place Jussieu 75251 Paris Cedex 05，FranceAldric Degorre3ENS Cachan，Bretagne，Campus de Ker Lann，av.R. Schuman，35 170 Bruz，France摘要隐蔽通道是系统中的信息泄漏，它使用资源秘密地传输消息。它们不仅对安全性、性能构成威胁，而且对系统的盈利能力构成威胁。 提出了一种从协议场景模型中检测隐蔽通道的新方法。首先将场景中的隐蔽通道发现问题建模为一个博弈，在这个博弈中，一对恶意用户S，R试图传输信息，而协议的其余部分试图阻止它。 一种转换器，其输入词汇是对系统的观察然后，我们描述了隐通道的存在作为{S，R}和解码器的获胜策略的存在关键词：场景，游戏，隐蔽渠道。1介绍隐蔽通道是违反系统安全策略的信息流隐通道一词最早由[19]引入秘密渠道是1电子邮件：loic. irisa.fr2电子邮件地址：mz@liafa.jussieu.fr3电邮地址： aldric. eleves.bretagne.ens-cachan.fr1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.07.01094L. Hélouët等人/理论计算机科学电子笔记119（2005）93被认为是对信息系统的威胁，有几个原因。第一个明显的原因当然是安全问题，因为隐蔽通道可以用来秘密传递信息。秘密渠道也可能是一种经济威胁。它们可用于利用现有系统传输信息（通常以低速率），而无需为所提供的服务付费。此外，它们通常基于对资源或功能的模糊使用，这严重影响了系统的性能。隐通道通常分为存储通道是使用系统的资源来写入可由第三方读取的信息的通道。定时通道是一种以第三方可以观察到的方式修改系统响应时间的通道。信息泄漏的特征还在于其带宽，即每秒通过隐蔽通道传输的比特数。在[23]中，认为任何系统都不应允许大于每秒100比特的速率，对于安全性要求高的应用一些建议[9，23]已经定义了处理隐蔽通道的策略。建议[23]系统地尝试使用正式技术来检测隐蔽通道。当一个隐蔽通道被发现时，它需要记录它的使用场景，并计算其带宽。 人们普遍承认，关闭所有秘密渠道是不可能的[22]。关闭通常意味着禁止访问所有用于信息传递的资源。然后，它将继续避免所有共享资源，协议中的消息重复，甚至计算机中的内部时钟更明智的解决方案是在已知的隐蔽信道上添加噪声（例如通过随机访问所使用的资源另一种解决方案是监控隐蔽信道的使用，从而在检测到非法信息流时做出适当的决定隐通道的特征首先被提出作为信息系统中的一个置信度问题。信息系统中的确认概念为每个用户定义了他可以访问的服务以及他可以与之通信的用户。隐蔽的渠道可以用来将信息传递到这个保密区之外。[4，3]中定义了这种系统愿景的安全模型，并且已经提出了几种检测间接信息流的方法：共享资源矩阵[18]，公理方法[1]......最近，隐蔽信道的存在已经通过非干扰特性定义[12，10]如下：一组用户U和一组用户UJ之间的干扰，当且仅当 非干扰也受到质疑[30]，因为传输单个比特的信息会导致L. Hélouët等人/理论计算机科学电子笔记119（2005）9395不干涉违规。已经提出了几种不干扰的方法，通过类型化[34]（如果不能正确类型化，则系统包含干扰）或使用进程代数[20]。通常，非干扰方法根据高和低两个安全级别对系统的数据和过程进行分类。高级进程可以访问系统中的任何数据，并与所有其他高级进程通信，而低级进程不允许直接或间接地从高级进程读取信息。还要注意的是，确认和不干扰都假设当通信双方不被允许相互发送信息时会发生非法信息流。然而，在合法的信息传输上，可能存在非法的信息泄漏。这种隐蔽信道通常被称为一个经典的例子是水印：它可以通过改变一些比特来添加隐藏信息到合法的信息流中然而，隐藏通道的搜索通常不涉及合法数据的内容，这更像是一个隐写问题。另一种可能性是将数据隐藏在协议帧的一些无用部分中，以在合法的数据流中传递隐蔽信息[28]。这种隐蔽通道是频繁的，但可以很容易地检测和关闭。协议中的另一种可能性是使用信息从参与者传递到另一个参与者的方式来编码信息。这不是一个保密或不干涉的问题，因为参与者之间允许信息这也不是隐写术的问题，因为传输的消息没有改变。这种情况可以被认为是一个“基于协议”的隐蔽通道。 事实上，协议本身被用作在更经典的隐蔽通道中存储数据的资源。检测这种隐蔽通道要困难得多，因为它们涉及协议中的几个消息。当然，基于协议的隐蔽通道检测以比非干扰更不通用的方式解决非法信息流然而，数据传递并不被定义为对改变的行为的检测，因为基于协议的隐蔽通道的参与者都表现正常。有关隐蔽信道的更完整的参考书目，请参考[31]。本文提出了一个场景框架来检测潜在的使用场景有几个优点：首先，场景通常是人们可以获得的关于系统行为的第一个信息它们也用于描述系统需求。在系统开发的早期阶段检测隐蔽通道可以帮助修改系统，此时仍然可以以合理的成本进行修改。使用场景的第二个原因是，有几个建议要求用这种模型记录隐蔽通道的使用研究秘密通道96L. Hélouët等人/理论计算机科学电子笔记119（2005）93直接从场景中提供了立即记录非法信息流的示例除了这些考虑之外，场景可以用作系统行为的部分知识。事实上，通常很难获得一个系统的模型。场景是捕获系统最常见行为的良好候选对象。然后，从这个模型，隐通道分析可以执行。可能有人会说，场景只对系统的一部分进行建模，因此可能会错过一些非法的数据流。我们在本文中提出的研究并不声称是详尽无遗的，它通常被承认，一个差距总是存在于一个模型和它的实现。这一差距可能是由于实施细节或模型的简化。因此，基于模型的研究可能会错过一些隐藏的通道，或者相反，展示不切实际的场景。我们的基于场景的方法也有同样的缺点，只揭示了然而，应该记住，场景旨在以抽象的方式表示将出现在实现中的执行（如果它们被认为是一组需求）或存在于实现中的执行（如果它们表示所实现系统的输出跟踪）。出于这个原因，我们认为在场景中识别的隐蔽通道有很多机会在实现中使用。建议的方法是从一个系统的场景描述开始。根据该描述，隐蔽通道被建模为一个游戏，其中一对被破坏的用户{S，R}尝试发送信息，而协议的其余部分尝试阻止该信息继续发送。如果{S，R}在博弈中有获胜策略，并且如果R可以解码用一个根据策略构建的传感器来传输。本文的主要贡献是一种算法，该算法将游戏的竞技场划分如果Y不为空，则证明了从Y的任何顶点都存在编码任意大小信息的获胜策略。这种方法接近于对场景的非干扰定义，但具有几个优点。首先，隐蔽通道的特征不在于发送单个比特的可能性，如在非干扰框架中经常发生的那样，而是编码和解码任意大小的消息的可能性。除此之外，使用记忆策略可以在攻击者的行为中引入一些智能。我们的方法的另一个利益是，它不需要考虑安全级别或高和低安全级别之间的区别，这允许考虑合法渠道。本文件的结构如下。 第2节定义了情景符号L. Hélouët等人/理论计算机科学电子笔记119（2005）9397→我们在报纸上用的。 第3节给出了如何使用协议的功能对信息进行编码的示例第4节回顾了博弈论的一些基本定义，这些定义将用于表征隐蔽通道。第五节描述了场景中潜在的隐通道存在，并给出了检测算法。第6节展示了如何为给定的隐通道构建解码器，第7节总结了这项工作。2场景基础在过去的十年里，场景语言引起了人们极大的兴趣。最近已经提出了几种语言：消息序列图[17]，实时序列图[14]，UML序列图[24].所有这些语言都有一个共同的行为表示观，即通过几个操作符组成的基本时序图场景描述了可能的执行作为系统中事件发生之间的因果依赖关系当然，每种语言都有自己的语义微妙之处，但基本上，场景可以定义为偏序的组合。组成偏序来描述系统行为的想法并不新鲜[25]。然而，认识到场景作为有用的语言是一个最近的现象。在1992年之前，场景只考虑分布式系统的输出跟踪。在MSC'96语言[17，27，26，29]和UML序列图[ 24 ]的定义之后然而，像许多图形语言一样，场景不能用于详尽地设计系统。他们更致力于表现抽象和不完整的行为。通常的趋势是对系统的典型执行进行建模，或者通过场景来对例外情况进行建模，从而覆盖可能行为的大子集因此，即使不完整，场景仍然与检测系统的属性相关。在本文的其余部分，我们考虑了消息序列图。然而，本文提出的方法当然适应其他sce- nario形式主义。消息序列图由两种图组成.基本计时图（称为基本消息序列图-或简称bMSC）是由高级消息序列图组成的，粗略地说是bMSC标记的自动机。定义2.1bMSC是一个元组M=（E，≤，A，I，α，φ），其中E是一组事件，≤是事件之间的偏序，A是一组动作名称，I是一组称为实例的过程，α：E→A是一个将事件关联起来的函数每个事件的动作名称，以及φ：EI是一个将位置与每个事件相关联的函数。对于bMSCM，我们将定义为Min（M），用于因果顺序关系的最小事件集，即没有因果关系98L. Hélouët等人/理论计算机科学电子笔记119（2005）93∈ ≤ ×{}≤1 ×2=−→ ×B ×≤1≤2{（e1，e2）∈E1×E2|φ（e1）= φ（e2）}.前任。偏序本身并不足以对有趣的行为进行建模，已经提出了一些算子，如选择，循环和序列。顺序组合主要包括沿着它们的共同实例轴合并两个bMSC这在下面的定义中得到了更正式的定义。定义2.2两个bMSC M1和M2的顺序组成是bMSC。M1<$M2=（E1E2，≤1<$2，A1<$A2，I1<$I2，α<$1<$$>α2，φ1<$φ2），其中本文提出的方法主要研究隐通道中发送方执行的事件和接收方执行的事件之间的关系，以及它们之间的因果关系。因此，我们需要在一个实例上投影的概念，它包括在bMSC中隐藏其他实例的所有事件。定义2.3 bMSCM=（E，≤，A，I，α，φ）在物体i上的投影I是bMSCπ i（M）=（EJ= φ−1（i），EJEJ，A，i，φ|EJ）。 当我们假设在实例轴上的全序时，我们经常用w πi（M）= e1···en来表示M在实例i ∈ I上的投影，使得{e1，.，e n}= φ−1（i）和φp< q，e pΛR（D，t））<$ΛR（D，tJ）/=π或（πΛR（D，tJ））πΛR（D，t）/=π更非正式地说，E（D，m）认为，R不可能从m开始区分S的两个选择。 此外，当E（D，m）成立时，则有可能在顶点m上永远循环而不传递信息。注意，E（D，m）可能是由于某种非确定性，但也可能是由于接收器的可观察动作的空性。当E（D，m）对D的所有节点成立时，则强连通分量D不能用于传输数据。如果一个协议可以强制一对发送者/接收者停留在一个强连通分量D中，其中没有事件是可观察的，或者观察到的事件序列总是相同的，而与发送者的选择无关，那么在D中没有数据传输是可能的。注意，当n是sink节点时，E（n，n106L. Hélouët等人/理论计算机科学电子笔记119（2005）93--联系我们{|∈−→}|}−B（b）a）n1BC氮碳ϵn3ABn5Fn0的eDn4（a）cn0abBC一dn1n2ϵ见图4。 属性E考虑图4-a中的图形，描绘了HMSC的强连接组件D={n0，n1，n2}。节点是HMSC节点，并且从一个节点到另一个节点的转换由λR（t）标记 E（D，n0）成立，因为R在transition（n0，a，n1）之后所得到的语言是{abc;ad}n，而在transition（n0，ab，n2）之后所得到的语言是{abc}.{abc;ad} E（D，n2）是一个holds，其中 n2包含一个不可观测的跃迁（用λ表示）. 然而，如果n1由发送实例控制，E（D，n1）不成立，对于离开n1的两个转移，从不相交语言产生的可观察结果。因此，D可以用于编码信息。 如果我们考虑图4 -b中的强连通分支DJ={n0，n1，n2，n3，n4，n5}，则E（DJ，x）对于xn1，n2，n3，n4，n5平凡地成立，因为这些节点只有一个输出变换。如果n0由发送实例控制，则E（DJ，n0）不成立，并且从标记为a或d的转换开始足以生成可观察到的信息，即使输出可以通过两个不同的选择生成。现在可以识别数据传输的区域，让我们计算HMSC的获胜区域。对于发送实例，获胜区域是在不失去信道控制的情况下可以进行数据传输的区域，对于协议，获胜区域是不可能进行无限数据传输的区域显然，汇聚节点是协议的获胜区域。以类似的方式，由协议控制的所有连接组件也为这个玩家赢得了胜利。最后，不完全由协议控制但不允许数据传输的区域也是协议的获胜区域。这3种情况的0吸引子也是协议的获胜子集（其中0是代表协议的参与者隐通道博弈是一个迭代可达性博弈。事实上，有缺陷的用户希望协议在可以进行信息编码的节点中无限地传递。设H=（N，-→，B，l）为HMSC。 的与H相关联的区域被定义为AH=（N0，N1，E），其中N0={n∈Nn选择节点S和R都不控制n，N1= N0，λ R = λ R（），E=（n，λR（b），nJ））（n，b，nJ）。如前所述，我们希望将隐蔽通道定义为允许无限编码的Muller游戏，也就是说，其输入L. Hélouët等人/理论计算机科学电子笔记119（2005）93107∅联系我们--有限游戏可以遍历无限次编码节点。我们首先将竞技场划分为两个集合，Y是无限编码总是可能的，X是没有编码或只有有界编码是可能的。算法：Partition（AH）X=0（方案的获胜集Y=（获胜组为对/接收器）CC=T arjan（H）/* 计算H*/的强连通分量。Stack=具有按深度排序的连接组件的堆栈（顶部最深）而Stack则会D=POP（堆栈）如果DY第1000章：第一次见面（1）D：=D-Y如果D=，则PUSH（T arjan（D））结束，如果否则如果m∈D，<$E（D，m），则如果D_Att_RS（{m}_Y），则情况（2）Y=属性RS（{m}Y）其他案例（3）PUSH（T arjan（DAttRS（{m}Y）PUSH（T arjan（D−AttRS（{m}Y）end if其他案例（4）/* 这里，DY=且E（D，m）对于所有m∈D*/X=XDend if结束if结束while该算法计算一组节点X，协议有一个策略来防止S和R传递任意长度的信息，以及X的补数Y。如果Y不为空，则协议中可能存在从S到R的隐蔽通道该算法研究与场景描述相关联的领域中连续连接的组件对于每个连接的组件，可能发生图5所示的几种情况该算法的重要不变量是在所有阶段Y是到目前为止找到的编码状态的S，R还请注意，任何离开108L. Hélouët等人/理论计算机科学电子笔记119（2005）93∩∈ <$∈ <${}Case1Case2属性S，R（{m}Y）n4 YDn1DM一BYn3n2堆栈i+1栈i堆栈i+1栈iCase3属性S，R（{m}Y）案例4DDYYamB栈i堆栈i+1栈i堆栈i+1DBamn3Dn2n1DD连接的组件导致位于更深组件中的顶点因此，将连通分量的节点分类为深度n处的X或Y节点可以依赖于深度n+ 1处的所有分量的节点的分类。每次研究一个分量D时，它要么相对于到目前为止计算的集合Y是稳定的，并且可以添加到X或Y，要么是不稳定的，并且被分成子分量。在第1种情况下，DY不为空。对于D还不能推导出任何东西，必须对D-Y的所有连通分量进行细化研究。在情况2中，mD，E（D，m）和DAtt RS（mY）。因此，从D的任何节点，S和R可以强制协议返回到m，或者移动向Y的一个节点。所以，D可以加到Y上，因为我们希望Y被吸引力封闭，Y=AttRS（{m}<$Y）。在情况3中，mD，E（D，m），但D<$Att RS（mY）.因此，D中有一些节点仍然是可能的，以避开Y的m个或所有节点。因此，我们必须在DAttRS（{m}Y）和D−AttRS（{m}Y）的连通分量中改进搜索。在情况4中，D是连通分量，并且不包含允许信息传递此外，由于D Y是空的，因此不可能离开D到达可以进行数据传输的区域的一部分。因此，D可以加到X上。图五. 算法的不同配置让我们在图6的示例中应用该算法。这个区域的强连通分量CCi由接收器/接收器对控制的节点用正方形表示，由协议的其余部分控制的节点用圆形表示汇聚节点L. Hélouët等人/理论计算机科学电子笔记119（2005）93109--¬--∃ ∈¬-{∈|∈}∈CC8一一CC11CC2c3eB1314C一C一DC2CCC3B5B1516一B一4B的cc4一CBCC567CC7912一811FCeCC610应该由发送者/接收者控制。它们显然是协议的获胜节点，因为轮到攻击者我们首先从堆栈中的CC7.CC5.CC6.CC4.CC3.CC8.CC2.CC1开始，X=0，Y=0。 由于E（CC i，n）对所有节点n∈CC i和i∈ 3成立，所以该算法的第五步是平凡的。7. （注意：这些CCi的选择节点由S、R控制。然后，情况4适用，它只是将这些连通分量的顶点添加到X。在步骤5之后，我们因此有X={ 5， 6，7， 8， 9， 10， 11， 12}。第六步弹出CC8，具有不同的性质，因为它包含节点13和<$E（CC8，13）。这里，案例3应用，我们必须将CC8分成两个连通的分量，CC8，1=CC8-AttRS（{13}）={ 13， 15}和CC8 ， 1=CC8-AttRS（{13}）={ 14，16}。然后，步骤7和8将CC8，1添加到Y，因为它符合情况2，并将CC8，2添加到X（情况4）。同样，CC2将添加到Y，CC1将添加到X。该算法以X={ 1， 5， 6， 7， 8， 9， 10， 11， 12， 14， 16}和Y={ 2， 3，4， 13， 15}终止。见图6。计算X和Y既然我们已经计算出了一个集合，从这个集合中，可以通过有限的步骤到达一个能够进行信息编码的节点停留在Y不足以确保信息的传递：Y不够准确。我们也不能要求所有节点y使得某个连通分量D的E（D，y）无限频繁地出现，因为博弈可能卡在一个特殊的连通分量上，而对S，R来说仍然是一个获胜的博弈。因此，我们可以将隐通道博弈的获胜条件定义为Muller条件Win（Y）= 2YP2YnP，E（P，n）. 一个节点yY，使得W Win（Y）和E（W，y）将被称为编码节点。W在（Y）中的获胜子集定义了协议中可以由110L. Hélouët等人/理论计算机科学电子笔记119（2005）93联系我们¬ ∈∈-我...| ∀⊆}发送实例以创建隐蔽通道。对于攻击者来说，停留在协议行为的受限部分（通常是HMSC图的小的强连接组件）可能足以传输信息。这是方便的，因为发送方需要更少的存储器来实现隐蔽信道4，但是使得信道更容易受到监视应用的攻击，将用户的行为与诚实用户的行为进行因此，一个EGY对于发送方来说是使用协议的更大可能部分来发送信息，同时模仿诚实用户的行为。命题5.4设GH=（AH，Win（Y））是与H相关联的穆勒对策，其中Y =。 从GH，可以计算由S和R控制的节点的最大策略f Y，使得：i) Y中任何符合fY的无限游程都无限地经常通过一组编码节点。ii) 对 于 所 有 编 码 节 点 y 和 所 有 v0 ， . vl 使 得 v0···vl.y 是 一 条 路 径 ， fY（v0···vl.y）至少包含两个变迁t1，t2使得Λ R（Y，t1）<$Λ R（Y，t2）=<$.我的律师。 如果Yi=π，则从一个出租m的构造中，πy∈Y，πD，πYJ∈D，使得E（D，YJ）和y满足RS（YJ）. 因此，对于所有y，有一个从y到编码节点的（位置）策略。因此，存在从任意节点到编码节点，以及从编码节点到另一个编码节点的策略f由于编码节点的数量是有限的，因此任何符合该策略的策略都将无限地通过一组编码节点。然而，请注意，这个策略f不一定是最大的。让我们建立与穆勒博弈相关的奇偶自动机PH。我们称K为PH的大小。我们的奇偶自动机的状态将是形式v1. v k.y，其中k< K。我们可以观察到，这个奇偶自动机的策略实际上是PH的子图。我们还可以注意到，如果PH中的策略不允许无限频繁地通过一组节点，则该策略将是获胜策略i∈Iv1i. v ki.y i不包含编码节点。 因此，我们认为，一个策略f将是一个获胜策略i，i是与f相关联的PH的子图不包含i∈I v1i. v ki.y i它不包含编码节点。从一个获胜的策略f，可以加上一条从一个节点开始的链4.实现了Bu？ciConWin（Y）=Yy WY，E（W，y） 是足够的展示策略，符合播放遍历一些编码节点无限频繁。然而，Muller条件允许策略使用更大部分的规范（这不能由Buüc约束来定义）。在这种情况下，诚实的渠道使用更有可能与诚实的行为相似