没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记128(2005)17-25www.elsevier.com/locate/entcs流动环境中的流量敏感泄漏分析*Chiara Braghin1, Agostino Cortesi2,Dipartimento diInformaticaUniversit`aCa摘要在本文中,我们提出了一个改进的控制流分析,旨在研究移动环境演算中的信息流安全。改进是通过使分析对时间敏感来实现的:分析能够在计算Mobile Ambient进程的运行时拓扑的安全近似时跟踪能力应用程序的时间依赖性。关键词:静态分析,环境演算,安全,信息流。1介绍在分布式系统的环境中,资源和数据在几乎位于任何地方的用户之间共享,用户很可能从网络上的不可信来源获得一些(可能)恶意程序,并在其自己的系统内执行它们,从而产生不可预测的结果。此外,在执行电子商务或家庭*部分由MIUR项目“AIDA抽象解释:设计和应用”,欧盟合同IST-2001-32617“MyThS”和FIRB项目(RBAU 018 RCZ)“Interpretazione astratta e model checking per la veri fica disistemi em-bedded”支持。1电子邮件:braghin@dsi.unive.it2电子邮件:cortesi@dsi.unive.it1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2004.11.03918C. Braghin,A.Cortesi/Electronic Notes in Theoretical Computer Science 128(2005)17由于远程连接的这些安全问题构成了一个非常有趣的工作台来评估静态分析技术的理论和实际影响。给出一种静态验证安全属性的方法,原则上,具有使属性检查更有效的优点;此外,它允许我们编写通过构造而安全的程序,例如,当所执行的分析被证明暗示某些行为安全属性时。由于程序运行时行为的大多数非平凡属性要么是不可判定的,要么是NP的,因此不可能准确地检测它们,并且需要某种形式的近似。所以,一般来说,我们期望产生一个可能比程序执行过程中发生的更大的可能性集合。控制流分析(CFA)[11]的目的是静态地预测程序动态行为的安全和可计算的近似。它可以使用不同的公式来表示,例如流行于函数和面向对象语言分析的基于约束的形式主义,或流逻辑风格[3,10,14]。在类型系统中,流逻辑明确区分了分析建议的解决方案何时可为程序所接受的规范,以及分析信息的实际计算通过预测一个系统的行为,当被评估的系统不满足兴趣属性时,它也会产生积极的信息,而类型系统方法是根据规定性规则给出的(一个系统要么被接受,要么被丢弃)。在最近的几个发展中,已经证明了Flow Logic是一种强大的方法,能够处理各种计算演算:Adjuda-calculus,Concurrent ML,命令式对象演算,pi演算[1],Mobile Ambients演算[9,12,13]和spi-calculus [2]。在[5]中,我们应用[9]中提出的基于流逻辑的控制流分析来验证在移动环境中建模的过程中信息流的缺失[7]。为了尽可能抽象地研究这个问题,考虑了这允许研究信息流的一个非常一般的概念,它也应该适用于微积分的不同版本,例如,[15]第六章:“生”与“死”的区别特别是,引入了一个新的安全边界概念[5]来模拟这种情况下的多级安全策略。信息泄漏可以用敌对环境访问在安全边界内不受保护的机密数据通过这项工作,我们进一步完善了[5]的分析,以便使C. Braghin,A.Cortesi/Electronic Notes in Theoretical Computer Science 128(2005)1719它对气流敏感。更具体地说,(i)解决方案是流程表示的幂集,而不仅仅是一个单一的矩阵表示;(ii)通过将新对标记为活动并记录启用的功能,分析跟踪功能应用的时间依赖性。执行细化的控制流分析可以很容易地集成到工具中[4]。BANANA论文的其余部分组织如下。在第2节中,我们介绍了移动环境演算的基本术语,并简要报告了一个控制流分析,旨在计算一个安全的近似的可能的环境嵌套发生的运行时执行的进程。然后,我们描述了如何形式化的多级安全设置的移动Ambients。在第3节中,我们提出了一个改进的分析,以使其低敏感。2背景2.1环境演算在[7]中引入了移动环境演算,其主要目的是明确地对移动性进行建模。事实上,环境是任意嵌套的边界,可以通过适当的功能四处移动。进程的语法如下所示,其中n∈Amb表示环境名称。P,Q ::=(νn)P限制 |nAa的t[P]环境|0不活动|进入n 的能力|P|Q成分|退出能力|!P复制|打开Atn.P打开n的能力直观地,限制(νn)P引入了新名称n并将其范围限制为P; P |Q是P和Q并行运行;复制提供递归和迭代。通过nla[P],我们表示命名为n的环境,在ltn和ltn之外的功能移动它们的封闭ambients in和out ambientn;使用能力openltn消除兄弟环境音 环境和过渡上的标签是引入它是因为在静态分析中习惯表示进程P的操作语义是通过进程间的一个适当的约简关系→和一个结构同余关系→给出的直觉上,P→Q表示P通过某种计算还原为Q的可能性(另见[7])。例如,设P1是一个对从威尼斯发送到伦敦:威尼斯[信封][出威尼斯。在伦敦0个字符] |Q]|伦敦[[打开信封。0]]20C. Braghin,A.Cortesi/Electronic Notes in Theoretical Computer Science 128(2005)17最初,信封在威尼斯现场。然后,它退出威尼斯,进入伦敦工地,分别在威尼斯和伦敦应用其能力一旦sitelondon收到信封,它就会通过使用打开信封的功能来读取信封内容最后,进程P1到达状态:Venice [Q]|伦敦[0]。为了表达多级安全策略,信息被分为不同的机密级别。这是通过利用环境标签来实现的。特别地,环境标签的集合被划分成三个不相交的集合:高、低和边界标签。标有边界标签的环境(边界环境)负责确定机密信息。如果在进程执行期间,高级别环境未被限制在边界内,则会发生信息泄漏,从而可能暴露于恶意环境攻击。例如,设P2是过程P1的扩展,其中信封包含需要从威尼斯安全发送到伦敦的机密数据hdata(标记为高)。veniceb1[e nvelopb2[[outc1venice。我在c2lond on。0|hd atah[[ 0]|伦敦b3 [打开c3信封。0]]在这种情况下,威尼斯,信封和伦敦必须标记边界保护hdata在整个执行过程中。(See[5]详细内容)。2.2移动环境[9]中提出了第一个控制流分析,旨在对运行时可能发生的进程嵌套进行建模。在移动环境的情况下,通过分析计算的控制结构由环境的分层结构表示,由树结构的节点之间的父子关系给出。该分析不是面向安全的,因此它没有利用关于边界内的“安全”嵌套的信息。在[5]中,我们提出了一个更准确的抽象域,它分别考虑安全边界内外的嵌套,从而产生了一个更复杂的控制流分析,用于检测不需要的边界交叉,即,信息泄露其主要思想是区分巢是受保护还是不受边界保护。更具体地说,分析是expressedinttisoftuple(IB,IE,H),其中:• 这两个参数(IB和IE)是(L aba×Lab)的一个重要元素。如果进程P在其执行期间包含标记为la的环境,其内部具有标记为l的能力或环境,则(la,l)为预期属于I.B.或我爱你 根据保护的水平,嵌套(B代表边界,E代表外部环境)。C. Braghin,A.Cortesi/Electronic Notes in Theoretical Computer Science 128(2005)1721L(out)(I,I,H)|=outn.P i(I,I,H)|=Pˆˆ ˆBÆ不BEˆˆ ˆBBEl,l,l∈Lab:一 一个'a"一case((la,lt)∈I<$B <$(la,la)∈I<$E<$I<$B <$(la,la)∈I<$E<$'(la,n)∈H)=H'""如果(l∈Lab),则(l,l)∈Ia aa a''BnˆEOele(la,la)∈I<$E <$ (l,lJ)∈I<$B|pat hB(la,l)⊆IˆE''case((la,lt)∈I<$B <$(la,la)∈I<$B <$(la,la)∈I<$B (la,n)∈H<$)=<$(la,la)∈I<$Bcase((la,lt)∈I∈E <$(la,la)∈I<$E <$(la,la)∈I<$E (la,n)∈H<$)=<$(la,la)∈I<$E'""''''""'''• H_∞∈H_∞(Laba×Amb)的第三个边值问题,名称和标签之间的区别。如果进程P包含环境标记la与hnamen,n(l a,n)是期望的,以Hee lon e l o ng e lo n e l onen 。分析由表示和指定函数定义[11]。表示函数旨在将具体值映射到其最佳抽象表示。在INUB(INUE)中,所有功能集合都有代表性环境的嵌套最初(不)包含在至少一个边界环境中。它是以函数βB(P)的形式给出的,β B(P)把过程P映射成一个与P的初始状态相对应的三元组t(IB,IE,H) ,其中t为零封闭标记为L的环境。这种具体化是一个三元组(I_B,I_E,H_B )的封闭条件,它涉及到进程P上可执行的所有可能的移动。 除了open、in和out这三个功能之外,它主要依赖于子进程上的递归调用。由于空间有限,在图1中我们只报告了超出能力的规则在规范中,谓词路径B(la,l)用于简化表示法:它表示从环境标记la到环境标记l的嵌套的受保护路径,其中没有环境是边界。输出能力的规则规定,如果某个标记为la的环境具有输出能力,在环境n上的能力l t,其可以由于名称为n的标记为l a j的直接祖先环境的存在而应用,则执行该能力的结果必须根据新生成的嵌套的保护级别来确定。该规则分为三种不同的情况:(i)环境离开边界,从而移动到未受保护环境,(ii)所有周围环境都受到保护,最终(iii)所有周围环境都不受保护。在第一种情况下,从移动的环境语言到新的保护语言的所有嵌套都必须在I/O中复制,因为它们都是移动的他们变得不受保护。 in和open-capabilities的行为类似.Fig. 1. 控制流分析的规范。22C. Braghin,A.Cortesi/Electronic Notes in Theoretical Computer Science 128(2005)171 1 2 23正如预期的那样,分析结果应该以信息流的形式阅读如果在分析中h(高级别数据)不出现在以下中的任何一个中,则在边界环境之外的秘密数据/环境不可能两人都渴望着去见上帝。例2.1假设P3是一个过程,它模拟了这样一个事实,即机密数据hdata在可能被发送到不安全的外部环境之前被插入到安全的信封注意,在纯Ambient演算中没有通信原语。在没有这样的原语的情况下,在接收器(在我们的示例中,地点venice)和接收器之间的包络的交换可以被建模为由环境包络执行的输出和输入接收器动作的序列。通过这种方式,envelope将从接收器移动到接收器,在那里它将被打开以读取其内容(在我们的情况下,是环境hdataB H C C B C威尼斯 [hdata[ in信封. 出来威尼斯0个字符]|包络 [第0话]|开放 [hdata]在这种情况下,环境hdata相对于信息泄漏表现正确,因为它从不离开边界venice。但是,如果我们计算CFA,我们得到pair(env,h)apersinIE,env表示外部环境,从而导致错误警报。Q3一种流敏感控制流分析方法第2.2节的CFA既对上下文不敏感,又对上下文不敏感:它不考虑执行能力的时间顺序,也不能区分能力路径中的阻塞和非阻塞能力。再次考虑例2.1的过程P3:在这种情况下,只有当c1包络中的能力已经被消耗时,才执行c2包络中的能力仅当环境HDATA在包络内部时,并且因此不启用输出能力。相反,分析还考虑了以下情况:其中当环境HDATA在Venice内部时(即,系统的旧快照),并且当它在封套内时(即,系统为了完善分析,以便识别何时存在能力,启用或不启用(即,它已准备好被消耗),且如果在I/OB或I/OE中有一对表示系统的旧快照或当前情况,我们通过以下方式丰富抽象域:• 添加第四分量L,其是能力标签的列表的集合。更具体地说,每个列表表示沿路径的功能标签的有序序列C. Braghin,A.Cortesi/Electronic Notes in Theoretical Computer Science 128(2005)1723不(或)S|=Bouttn. PiS|=BP<$(I<$B,I<$E,H<$,L)∈ S:if(lt∈head(L))则l,l,l∈Lab:一 一个'a"一case((la,lt)A∈I<$B <$(la,la)A∈I<$E<$I<$B <$(la,la)A∈I<$E<$'""'(la,n) ∈H<$)=<$Φ((l,l))<$Φ((l,l))<$top(l,L)<$一不a a'不一一一如果(l),则(l(l)a aa a''Bn一∈IˆEOelse(la,la)A∈I<$E <$ (l,lJ)A∈I<$B|pat hB(la,l)⊆IˆEcase((la,lt)A∈I<$B <$(la,la)A∈I<$B <$(la,la)A∈I<$B (la,n)A∈H<$)=<$(la,la)A∈I<$B <$Φ((la,lt)A)<$Φ((la,la)A)<$tp(lt,L)case((la,lt)A∈I∈E <$(la,la)A∈I<$E <$(la,la)A∈I<$E (la,n)A∈H<$)=<$(la,la)A∈I<$E <$Φ((la,lt)A)<$Φ((la,la)A)<$tp(lt,L)'''""'''''""''''保持阻止列表尾部的能力。例如,在进程P3中,在初始状态,L={[c1,c2],[c3]},其中inc1envelope和openc3hdata都准备好被消耗。• 用A或NA标记I/B或I/E中的对,指示对是否有效(即,它发生了,但是它不能用于生成进一步的嵌套,因为它属于系统的旧快照)。为此目的,我们定义一个函数Φ,给定一对,它补充标签(例如,Φ((l,lJ)A)=(l,lJ)NA)。 例如,在进程P3中,在开始时(b1,h)A,但是一旦hdata移动到包络内部,它必须改变为(b1,h)NA。分析的结果是过程表示的幂集:S={(IB,IE,H,L)}。在这种情况下,分析在表示和指定函数的项中是给定的。 代表职能收集环境和能力之间的所有初始嵌套,用Aonly环境嵌套和对(l,lt)标记,其中lt是启用的能力的标签。同样,我们不报告整个分析质量标准。相反,我们通过考虑,例如,输出能力(见图2)。out-capability的规则规定,只有在启用时才考虑该功能。如果是这样,那么执行的结果这一能力必须根据以下两种情况来确定:新生成的巢的保护水平。此外,参与移动的对的标签应相应地更新,并且l不从L中的列表的头部删除。图二. 细化控制流分析的规范。正如预期的那样,分析结果应该以信息流的形式阅读如果在分析中h(高级别数据)不出现在以下中的任何一个中,则在边界环境之外的秘密数据/环境不可能这对夫妇渴望在美国的一个国际组织。24C. Braghin,A.Cortesi/Electronic Notes in Theoretical Computer Science 128(2005)17Hˆ定理3.1设P是一个过程,h∈Laba是一个高级标号,S=JJJ{(I,I,H,L)}. LetβB(P)→S,S|=BP,andnd()JJ = h。然后,B E env我,我∈IE,lP不会泄漏秘密H。例3.2再次考虑例2.1的过程P3.表示函数给出了进程P3在其初始状态的快照S0={{(b1,h)A,(h,c1)A,(h,c2)NA,(b1,b2)A,(b1,c3)A},{(env,b1)A},{[c1,c2],[c3]},{(b1,venice),(h,hdata),(b 2,envelope)}此时,inc1envelope和openc3hdata都被使能。如果应用开放规则,我们得到:S1=S 0<${{(b 1,h)NA,(h,c1)NA,(h,c2)NA,(b1,b 2)A,(b1,c3)NA,(b1,c1)A,(b1,c2)NA},{(env,b1)A},{[c 1,c 2]},{(b1,venice),(h,hdata),(b2,envelope)}现在,只有在c1信封启用:S2=S 1<${{(b 1,h)NA,(h,c 1)NA,(h,c 2)A,(b 1,b 2)A,(b 1,c 3)A,(b2,h)A},{(env,b 1)A},{[c1],[c 3]},{(b 1,venice),(h,hdata),(b2,envelope)}最后,启用的功能都不能被消耗,因此定点算法停止。添加到解决方案中的两个快照表示进程P3运行时执行的两个可能的跟踪。同样在这种情况下,结果应该按照信息流来阅读:因为h没有出现在我认为,分析正确地证明了这里没有信息泄漏。Q引用[1] C. Bodei,P. Degano,F. Nielson和H. R.尼尔森π-演算的静态分析及其在安全中的应用。信息与计算,168:68[2] C. Bodei,P. Degano,F. Nielson和H. R.尼尔森密码过程中Dolev-Yao密码的流程逻辑。FutureGeneration Computer Systems,18(6):747[3] C. Bodei,P. Degano,H. R. Nielson和F.尼尔森使用流逻辑进行安全分析。EATCS公报第70卷;扩充版将由世界科学出版社出版,2000年。[4] C. Braghin,A. Cortesi,S.菲利普河Focardi,F. L. Luccio和C.露天广场 边界环境嵌套分析工具。In H. Garavel和J. Hatterykirk,编辑,Proc. of 9th Int. Conf. 关于系统构造和分析的工具和算法(TACAS'03),计算机科学讲义第2619卷,第437-441页。Springer-Verlag,柏林,2003年。[5] C. Braghin,A. Cortesi和R.福卡迪移动环境中的安全边界。Computer Languages,28(1):101[6] M. Bugliesi湾 Castagna和S. 克拉法 盒装的氛围。 第四届计算机科学理论方面国际会议论文集(TACSSpringer–Verlag, Berlin,[7] L. Cardelli和A. D.戈登移动环境。理论计算机科学,240(1):177C. Braghin,A.Cortesi/Electronic Notes in Theoretical Computer Science 128(2005)1725[8] F. Levi和D.桑吉奥吉移动安全环境。ACM Transactions on Programming Languages andSystems,25(1):1[9] F. 尼尔森河R. Hansen和H. R.尼尔森 移动环境的抽象解释。计算机程序设计科学,静态分析特刊,47(2[10] F. Nielson和H. R.尼尔森流逻辑和操作语义。电子笔记理论计算机科学,10,1998。[11] F. Nielson,H. R. Nielson和C.汉金程序分析原理。Springer–Verlag, Berlin,[12] F. Nielson,H. R. Nielson和M. 萨吉夫 移动环境的Kleene分析。 第九届欧洲编程研讨会论文集(ESOPSpringer–Verlag, Berlin,[13] H. R. Nielson和F.尼尔森移动环境的形状分析。Nordic Journal of Computing,8(2):233[14] H. R. Nielson和F.尼尔森流逻辑:静态分析的多范式方法。第223-244页[15] A. Regev,E. M. Panina,W.西尔弗曼湖Cardelli和E.夏皮罗BioAmbients:An Abstractionfor Biological Combustion. Theoretical Computer Science,325(1):141-167,2004.
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 5
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
最新资源
- 掌握数学建模:层次分析法详细案例解析
- JSP项目实战:广告分类系统v2.0完整教程
- 如何在没有蓝牙的PC上启用并使用手机蓝牙
- SpringBoot与微信小程序打造游戏助手完整教程
- 高效管理短期借款的Excel明细表模板
- 兄弟1608/1618/1619系列复印机维修手册
- 深度学习模型Sora开源,革新随机噪声处理
- 控制率算法实现案例集:LQR、H无穷与神经网络.zip
- Java开发的HTML浏览器源码发布
- Android闹钟程序源码分析与实践指南
- H3C S12500R升级指南:兼容性、空间及版本过渡注意事项
- Android仿微信导航页开门效果实现教程
- 深度研究文本相似度:BERT、SentenceBERT、SimCSE模型分析
- Java开发的zip压缩包查看程序源码解析
- H3C S12500S系列升级指南及注意事项
- 全球海陆掩膜数据解析与应用
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功