没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记162(2006)267-271www.elsevier.com/locate/entcs基于安全的SOS元理论研究穆罕默德·礼萨·穆萨维埃因霍温理工大学计算机科学系Box 513,NL-5600 MB埃因霍温,荷兰摘要SOS元理论在定义元定理方面非常成功,使用这些元定理可以证明语言结构的有用性质。由于这些元定理的通用性和独立于语言的表述,它们可以节省大量的标准证明。语言结构的安全属性看起来像是有希望变成SOS元定理的候选者,并且已经在进程演算安全的上下文中尝试了这个方向。在本文中,我们给出了一个基于语言的安全性的背景下,这个问题的探索性说明。 为此,我们简要介绍了信息流安全,特别是不干扰,这是这个领域的核心概念。然后,我们指出了一些有趣的联系之间的非干扰和我们最近的工作与数据互模拟的概念。最后,这些概念的SOS元定理的一些想法。关键词:形式语义,结构化操作语义,基于数据的安全,非干扰1引言SOS元理论[1]在定义通用标准方面非常成功,可以保证语言结构的有用属性。由于这些Meta定理的通用性和语言独立性,它们可以节省大量的标准证明.语言结构的安全属性看起来像是有希望变成SOS元定理的候选者,并且已经在进程演算安全的上下文中尝试了这个方向[10]。在本文中,我们在基于语言的安全性的背景下对这个问题进行了探索性的描述[9]。这里提出的一些想法可以直接应用于进程演算安全。在本文的其余部分,我们简要概述了信息流安全[9],特别是作为该领域中心概念的不干扰[4]1 电子邮件:M.R. tue.nl1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2005.12.092268M.R. Mousavi/Electronic Notes in Theoretical Computer Science 162(2006)267然后,我们探索了非干扰与我们最近关于数据互模拟概念的工作之间的一些有趣联系[5]。关于这些概念的SOS Meta定理的一些想法将在第3节中给出.第四部分总结全文,并指出今后的工作.2互模拟与非干扰安全性的一个重要方面是保密性。保密意味着敏感的或更高级别的信息在与较低级别的用户交互的过程中永远不会透露。换句话说,保密保证了高级别的信息永远不会泄漏到低级别。信息泄漏的一个简单场景是通过将高级别数据项显式分配给低级别可观察变量,但它远远超出了这一点。低级用户可以通过非常隐式的观察来推断关于高级数据项的信息,利用所谓的隐蔽通道,例如,通过测量执行时间或功耗。互不干扰[4,9]是确保端到端保密性的重要手段。这只是意味着,人们不能通过观察系统的低级别部分来推断出任何关于高级别数据/行为的信息。除了保密性之外,最近还利用非干扰来支持其他安全方面,例如可用性[11]。假设我们有一个编程/规范语言,它对数据类型有两个级别的配置。我们将程序的操作状态表示为其中p是程序文本,h是高级数据,l是低级数据,所有这些都基于给定的域P、H和L。假设一个程序的操作语义是用上述状态之间的标记转换来定义的,这些状态具有标记χ∈X。在我们的设置中,一个程序被称为非干扰的,如果不考虑更高级别的数据状态,它总是可以在执行过程中生成相同的行为以及较低级别的数据部分。为了使这种非正式的解释正式化,必须作出一些选择。首先,必须固定行为的概念,为了简单起见,我们选择(强)互模拟语义。当然,在较弱的语义中探索相同的思想仍然是我们工作的一个有趣的延续。另一个重要的选择涉及更高级别数据状态的更改。人们可以选择开放系统语义,其中高级数据状态可以在执行期间任意更改,或者选择封闭系统语义,其中高级数据只能由系统中指定的实体更改。我们调查这两种可能性在本文的其余部分,并提出了两个概念的非干扰,称为SL非干扰和ISL非干扰,分别为开放和封闭系统然后,以下定义(受[8]的低双相似性和[5]的数据双模拟的启发)是两种可能的非干扰形式化定义2.1(SLNI互模拟和SL非干扰)对称关系RP2称为无状态非干扰(SLNI)互模拟,计算时的换算关系,jujJJχJ J JjJ(p,q)∈Rhp,l,l,χ,p,hp p,h p,l ⇒∀hqq,hqM.R. Mousavi/Electronic Notes in Theoretical Computer Science 162(2006)267269xjJ J J J J<$q,hq,l<$q → <$q,hq,l<$q(p,q)∈R. 程序p和q是SLNI-双相似的,记为当存在包含(p,q)的SLNI互模拟关系时,由p参与q。当p参与p时,程序p是SL非干扰的 。请注意,与通常的双相似性概念不同,SLNI双相似性不一定是自反的,因此不是等价的。直观地,上述非干扰定义要求非干扰程序再现相同的低级别数据状态,而不管高级别状态如何。这个定义的有趣之处在于,在每次转换时,程序都使用所有可能的高级和所有相等的低级数据状态进行比较这类似于我们在[5]中的无状态互模拟概念。正如我们在那里所激励的那样,无状态互模拟是非常健壮和组合的,但它通常非常强大,难以建立。关于SLNI互模拟和SL非干扰可以进行类似的观察。SL非干扰的替代方案是下面定义的ISL非干扰的概念。定义2.2(SBNI互模拟和ISL非干扰)对称关系R(P×H)2称为基于状态的非干扰(SBNI)互模拟,计算时的换算关系,jujJJχJ J J JJJ((p,hp),(q,hq))∈Rl,l,χ,p,hp p,hp,lχJ JJJ J J J<$q,hq,l<$q → <$q,hq,l<$q((p,hp),(q,hq))∈R. 程序p和q是初始状态-少非干扰(ISLNI)-双相似,记为pParticipislniq,当存在包含((p,hp),(q,hq))的SBNI-互模拟关系时,对所有hp,hq∈H.当p参与p时,程序p是ISL非干扰的。上面的定义是由这样一个事实激发的,即低级状态可以被低级用户观察和改变,而高级状态的改变则掌握在系统手中,如果系统是封闭的,我们就不需要迎合高级状态的中间变化。注意,ISL非干扰比SL非干扰弱。我们用下面的简单例子来说明上述两个定义及其区别例2.3考虑一种具有终止常数skip、赋值、条件(ifthen else)和顺序复合(;)运算符的编程语言,这些运算符具有预期的操作语义。赋值(:=)和条件(==)可以分别将变量与值或其他变量进行比较和赋值。假设h是一个高级变量,l是一个低级变量。以下程序l:= h和if(h == 5)thenl:= 6 elsel:= 7既不是SL也不是ISL非干扰,因为它们导致不同的行为或低水平值,这取决于高水平变量h的初始值。此外,如果(h == 5),则h:= 6,否则skip既不是SL也不是ISL非干扰,因为取决于h的初始值,它立即终止或采取一个更多的分配步骤。这种行为是一个很好的时间隐蔽信道的来源。然而,程序h:= 5 ; l :=h和h:=l; 如果(h == 1),则h:= 6,否则跳过都是ISL而不是SL非干扰。如果高级变量没有并发变化,低级观察者不能通过查看上述程序的不同执行来推断高级变量270M.R. Mousavi/Electronic Notes in Theoretical Computer Science 162(2006)267但是,通过将这些程序与更高级别的组件并行,我们可以观察到不同的行为和最终结果,这取决于更高级别变量的中间值例如,对于程序h:= 5; l:= h,在执行第一次赋值后,程序演化为l:= h。 很明显,l:= h是不干涉的,因为l的值由h的值决定,现在不一定是固定的。3论不干涉结构操作语义学[6]是一种普遍接受的方法来定义语言的标记转换语义。SOS风格中的语义规范包括许多演绎规则,这些规则基于其组成部分的转换来定义一段语法的可能转换规则格式[1]将演绎规则的某些语法形式定义为对于某些目的是一个杰出的类别的规则格式是关注的一致性的概念的行为等价。翻译成我们的术语,行为等价的一致性通常意味着相应的不干涉概念的组合性。这就是为什么在[10]中,一个特定的同余格式被用作证明不干涉的规则格式的基础。按照这种方法,[5]的s fsl和sfisl格式提供了一个方便的起点。然而,我们打算研究以下可能性,以改进我们环境中[10]的格式(i) 我们希望研究如何将不干涉问题与其组合问题分开。在我们看来,这将简化结果(这次是两个独立的)规则格式。使用一种规则格式,可以检查非干扰属性是否适用于特定构造,并且使用另一种格式,可以检查在不同上下文下证明的非干扰的鲁棒性根据我们的主观判断,[10]中报告的规则格式(ii) 其次,我们建议分别研究受限制的语言语境和构式的组合性和非干扰性。这与使用SOS元理论来证明整个语言的属性的常见做法相反。我们很难想象任何一种通用语言都会为其所有语法上有效的程序提供组合非干扰例如,任何具有通用赋值运算符的语言都不应该适合这样的格式,而某些赋值模式可以很容易地证明是无干扰的。M.R. Mousavi/Electronic Notes in Theoretical Computer Science 162(2006)2672714结论在本文中,我们提出了一些想法的概念,基于语言的非干扰的概念的基础上互模拟与数据。随后,我们提出了一些设计标准SOS格式的出发点,以保证受限上下文的不干扰。本文提出的初步设想还有待于进一步研究,以便提出一种具体的基于语言的不干涉格式。我们希望我们的工作可以受到启发,并扩展非干扰类型系统的实验工作(例如,[2,7])。引用[1] L. Aceto,W. J. Fokkink和C.维尔霍夫结构操作语义学。在Handbook of Process Algebra,第3章,第197-292页中。Elsevier Science,2001年。[2] A. Almeida Matos,G.布多和我。卡斯特拉尼反应式程序的键入不干扰,在Proc.计算机安全基础研讨会(FCS[3] R. Focardi和R. Gorrieri。 证券财产的分类(第一部分:信息流程)。 LNCS第2171卷,第331-396页。Springer,2001年。[4] J. A. Goguen和J. Meseguer。安全策略和安全模型。IEEESymposium on Security and Privacy,第11-20页。IEEE计算机学会,1982年。[5] M.穆萨维,M。Reniers和J.F.格鲁特SOS与数据一致。在LICS'04会议记录IEEE计算机学会,2004年。[6] G. D.普洛特金操作语义学的结构化方法。Journal of Logic and Algebraic Programming,60:17[7] F. Pottier和S.康雄信息流推理是免费的。在ICFP'00的Proc.中[8] A.萨伯菲尔德通过互模拟对多线程程序进行确认。LNCS第2890卷,第260-274页。Springer,2003,2003.[9] A. Sabelfeld和A. C.迈尔斯基于数据库的信息-数据流安全。IEEE Journal on Selected Areas inCommunications,21(1):5[10] S.蒂尼组成非干扰特性的规则格式。Journal of Logic and Algebras Programming,60:353[11] L. Zheng和A. C.迈尔斯端到端可用性策略和互不干扰。在CSFW'05会议记录中
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 5
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
最新资源
- WebLogic集群配置与管理实战指南
- AIX5.3上安装Weblogic 9.2详细步骤
- 面向对象编程模拟试题详解与解析
- Flex+FMS2.0中文教程:开发流媒体应用的实践指南
- PID调节深入解析:从入门到精通
- 数字水印技术:保护版权的新防线
- 8位数码管显示24小时制数字电子钟程序设计
- Mhdd免费版详细使用教程:硬盘检测与坏道屏蔽
- 操作系统期末复习指南:进程、线程与系统调用详解
- Cognos8性能优化指南:软件参数与报表设计调优
- Cognos8开发入门:从Transformer到ReportStudio
- Cisco 6509交换机配置全面指南
- C#入门:XML基础教程与实例解析
- Matlab振动分析详解:从单自由度到6自由度模型
- Eclipse JDT中的ASTParser详解与核心类介绍
- Java程序员必备资源网站大全
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功