基于代理的设计的组件接口概念及其在安全性验证中的应用

理论计算机科学电子笔记54（2001）网址：http://www.elsevier.nl/locate/entcs/volume54.html9页基于代理的设计A. Bracciali，A.Brogi，G. Ferrari，E.Tuosto1;2比萨大学信息学系Corso Italia 40，56125比萨，意大利摘要我们提出了一个行为扩展的组件接口的概念。 我们的目标是统一的原因封闭和开放的基于组件的系统的正确性。我们的方法的特点是，我们执行一个本地分析nite片段的相互作用自然建模的流动性和协调方面。我们提出了一个半自动的技术，减少了验证协议的安全性验证的正确性在基于组件的系统。1引言网络化的异构应用正逐渐成为现代软件环境的主要组成部分。这些应用程序（例如，用于蜂窝电话的网络浏览器）需要固定服务器和移动设备在应用程序运行时进行协作，并且网络服务的动态集成是一个关键方面。在这种情况下，编程技术采用组件的抽象来将服务封装在黑盒中。服务通过接口描述语言来描述。最近的发展集中在扩展这些语言，以指定组件的交互协议。然后，通过组合或协调语言来实现服务集成，这些语言描述了组件粘合在一起的方式。此外，网络应用程序强烈强调软件组合中的安全问题。组件可能确实是恶意的，并且可能被设计为窃取和/或破坏它们将运行的主机上的信息在本文中，我们扩展了[6]中提出的形式化框架，以描述和推理由自治的、交互的组件组成的系统。特别是，我们将展示如何这样的框架可以适当地应用于分析安全协议，被视为组件的行为特征。1 这项工作得到了MURST国家项目TOSCA的支持。2 电子邮件：fbraccia，brogi，giangi，etuostog@di.unipi.itc2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。Bracciali等人2我们的出发点是交互模式的概念，它是软件组件交互行为的抽象，用微积分的子集表示[10]。不同的是，从现有的方法的基础上进程代数，我们限制自己考虑尼特行为的组件的描述。事实上，我们认为，试图一次性描述基于组件的编程的所有方面必然会导致实际可用性低的复杂公式。另一方面，组件之间的相互作用往往遵循经常性的夜间模式。这种简化导致一个正式的框架，适合本地和统一推理的静态和动态组合物的属性。因此，在[6]之后，我们引入了一种简单的接口描述语言来指定组件的交互模式。一组交互模式形成了一个上下文，该上下文可能由于上下文内发生的交互或由于新组件动态地加入上下文而演变。本文的主要贡献是表明在同一个形式化框架内统一处理基于组件的程序设计的组合和安全问题是可能的。通过扩展交互模式的概念，提出了一种新的、半自动的安全协议验证方法。我们的做法可归纳如下：我们用密码原语扩展了交互模式，以Abadi和Gordon [1]的spi演算的风格。本文对文献[1]中提出的协议的魔术实例的概念进行了修正，从而给出了协议的安全性质。我们开发了一种证明技术来验证安全协议的正确性。证明技术包括两个主要步骤：(i) 要验证的属性首先表示为协议主体之间交换的某些关键数据的完整性和保密性。这对应于定义协议的一个魔术实例，如果所需的属性成立，则该协议将这些数据预期采用的值进行x。(ii) 然后，通过检查不存在能够利用协议的魔术实例的主体不能接受的通信来欺骗协议主体的入侵者。2交互模式交互模式既描述了组件的行为，即它们可以执行的通信，也描述了组件最初与环境的通信通道。我们已经说过，相互作用模式只能表达夜间行为。 组合环境的抽象称为上下文，即多连通集Bracciali等人3件.如果组件是完全连接的，即它们没有开放名称，则上下文是关闭的，否则它是开放的。交互模式的完整语言是从微积分中派生出来的，主要的区别是没有递归和显式的限制运算符（实际上，所有的局部名称都需要不相交）。通过传送信道名称，上下文的连接拓扑可以动态地改变。在本文中，我们将介绍许多功能的框架，只是非正式的。形式语义、组合操作和其他方面的形式定义可以在[6]中找到。假设我们正在指定一个分布式系统，其中有一个简单的服务器，它提供了对给定资源的引用（名称）。每次服务器与可能的客户端交互时，它都遵循相同的协议：它在通信信道上接收请求（例如，信道名称通常以下划线开头），然后通过同一信道发送应答（名称z），除非它从同一信道接收到某种中断。这种行为可以用以下交互模式来表示（c）[在（c，查询）中]。 （out（c，z）.0 + in（c，break）.0）]其中在（c，查询）中（分别，out（c，z））是同步输入（分别，输出）动作，其中查询和Z是发送的数据，并且（C）表示可以用于将服务器连接到其它组件的信道。定义2.1一个interactionp模式由一个term（X）[E]组成，其中X是E的开放名的集合，是表达式E中出现的名的子集。行为表达式E由以下语法定义：E：：= 0 j：Ejj E jj E jE+E D：：=C j：：：=in（C; D）jout（C; D）jC：：=netj：组件可以通过执行同步通信动作（输入和输出）在信道（C）上发送和接收数据（D）。和微积分一样，通道名可以在通信中交换数据的签名D可以是任意复杂的，例如，允许方法调用的结构以及加密机制（见第3节）。对复数项d的输入动作与通过与d的模式匹配提供兼容项的输出同步。名称集合C包含系统中的每个组件都知道的可分辨名称netnet这个名字的引入是为了模拟所有可能发生在网络上的不可信通信，每个组件都可以参与其中。沉默的行动表示组件可以独立执行的内部计算外部环境，它可以用来明确地描述本地的选择。像往常一样，进程是通过-演算的前x，并行和选择复合运算符构建的。然后，通过将它们的一些通道连接在一起，在系统中组成组件。从语法上讲，这包括识别一些开放的Bracciali等人4属于同一上下文的那些交互模式的名称。一旦连接了某个开放名称，该名称就不再可用于环境，并将从开放名称集中删除。除了系统的静态增量构造之外，相同的连接机制还对意图加入运行环境的组件的动态相互作用进行建模，例如，在代码移动性的情况下。下面的示例显示了上下文中组件的组成。例2.2一个客户端，表达一个与前面描述的服务器行为兼容的行为，可以发送一个请求，然后要么接受一个应答（y是一个名字，在这里用来代替变量，在样式中），要么自主决定发送一个中断，例如：经过一定时间后：（s）[ out（s，query）.（in（s，y）.0+.out （s，break）.0）]这说明了如何使用对内部（局部）选择进行建模。这两种交互模式可以通过替换[x/ c，x/s]组合在一起，获得以下封闭上下文：f （ ） [ out （ x ， query ） .（ in （ x ， y ） .0+.out （ x ，break）.0）]，（）[in（x，query）. （out（x，z）.0 + in（x，break）.0）]g上下文中的交互模式，因为它们的通道已经连接，所以可以一起通信。在第一次通信之后，上下文演变为：f（）[（in（x，y）.0+.out（x，break）.0）]，（）[（out（x，z）.0+in（x，break）.0）]g根据客户端的选择，这两个组件可以通过两种方式进行交互：接下来可以传递引用z或break。 请注意，正如预期的那样，在这两种情况下，两个组件都可以完全执行它们的任务，在某种意义上是兼容的和正确组合的组件。上述框架允许我们描述一个通用组件的基本片段，通过适当地连接它们来组成系统（上下文）中的组件，并观察结果系统的行为。可以分别通过封闭和开放上下文对静态和动态系统进行统一建模。这两个不同的场景需要不同的正确性属性公式。封闭上下文的正确性概念是相当标准的，它可以概括为没有死锁。 对于每个可能的计算，上下文中的所有交互模式都简化为successful pattern（）[0]。相互作用模式的精确性对这一性质的有效验证作出了明智的开放的上下文也可能因为新模式加入运行的系统而演变。在这种情况下，必须重新定义正确性的概念，以应对动态演化上下文的不完整性。我们引入了一个较弱的正确性概念，即可行性，它直观地对应于不存在任何贡献都不能解决的死锁。Bracciali等人5最终将加入上下文的组件。一个开放的上下文是可行的，当且仅当存在一个可以连接上下文的交互模式，并使其既封闭又正确。可行性看起来像是一个可取的，易于验证的，在开放系统的生命中不变的。例如，只有在不破坏其可行性的情况下，才应在现场内接受移动组件。下面的例子说明了一个可行的上下文。例2.3我们在例2.2中给出了一个正确的上下文。 现在考虑一个只包含不能生成中断事件的客户端的上下文;例如：f（s）[out（s，query）.在（s，y）.0]g中，上下文是可行的，因为即使是能够处理中断事件的服务器：（c）[ in（c，query）.（out（c，z）.0+in（c，break）.0）]可以连接上下文（通过替换[x/ s，x/c]），使其闭合和正确。事实上，只有上下文的演变，其中查询和引用被交换，导致成功的上下文。相反，如果我们考虑一个可行上下文与一个能够发送中断的客户端的双重情况：f（s）[ out（s，query）.（in（s，y）.0+.out（s，break）.0）]g它不能被不能处理中断事件的服务器加入：（c）[ in（c，query）.输出（c，z）.0]由于后者将使上下文不正确，因为上下文的一个演变导致（永久）死锁上下文，所以本地且非开放的名称x不能被加入上下文的任何新组件访问f（）[out（x，break）.0]，（）[out（x，answer）.0] g.3安全属性和“魔术”上下文现在，我们扩展了设置的交互模式与机制，以表达安全的通信协议组成的组件。作为一个主要的例子，我们展示了如何指定和验证安全协议的属性上下文必须保护其数据/资源不被不可信组件破坏（完整性）或访问（保密性）。我们考虑可以分布在网络上的组件，并使用公共信道相互通信。因此，为了面对安全问题，通信需要基于密码学的安全协议。协议可以在恶意入侵者可以操作的上下文中实现为交互模式。入侵者是可以动态加入上下文并与协议的预期主体我们提出了一种方法，它减少了验证的安全协议的正确性的上下文中执行的协议。特别地，我们将寻找一个能够“破解”协议而不考虑整个上下文的正确性的入侵者的存在。由于Bracciali等人64这种分析的存在性，一个比可行性假设弱的概念 我们说一个上下文是可能正确的，当且仅当存在至少一个计算，其中所有的交互模式都简化为成功模式（）[0]。给定一个可能正确的上下文C，一个交互模式是C兼容的，当且仅当它可以加入C而不破坏它的可能正确性。提出的方法包括在修改使用的概念，磁- IC实例，最初介绍了在[1]。协议P的一个神奇的例子B写为P，是一个实例，其中P中的一些变量已被固定为基础价值非正式地，如果P是安全的，则在不可信环境中P的所有可能的成功执行都应该将固定值分配给所选参数，而不管入侵者的任何可能的干扰。验证协议的安全属性的问题被简化为比较入侵者与协议及其魔法版本的兼容性在形式上，我们说P对于w.r.t.是不由P定义的性质，如果b只有当存在一个入侵者I，它是P兼容的，但不是BP兼容。 换句话说，如果协议是不安全的，通过伪造与预期值不同的值，我成功地欺骗了P的委托人，同时仍然保持P的可能正确性。另一方面，我不能欺骗（神奇地）知道的委托人的神奇版本B正确的值并且不能接受不同的数据（即，该方法包括两个步骤。P[I死锁）。3.1安全属性安全协议不允许对其“敏感”数据的意外访问或修改。在这个意义上，协议的安全性被简化为某些通信数据的身份确定其完整性意味着所需安全属性的数据和值是至关重要的任务。 为了更好地理解这一步骤，让我们考虑一个简单的协议。该协议规定，主体A首先向主体B发送（或更好地，打算发送）密钥k，然后它向B发送用k加密的随机数n：A=（）[out（net，k）.out（net，fngk）.0]，4B=（）[in（net，x）.in（net，fygx）.0]其中fn g k，如spi演算中的ke，是用keyk对n的加密。通信动作封装了加密和解密机制：通过密钥k（例如，in（net，fx g k））接收加密数据的尝试仅在使用k加密数据时才成功，否则将发生死锁。 另一方面，可以接收加密的数据，即在（net，x）中，而不尝试对其进行解密。为了检查协议fA，Bg是否尊重k的保密性（这显然是错误的，因为A通过网络发送k），我们要求B的第一个输入动作中变量x的值正好是k，与协议执行中的任何可能的干扰这意味着没有人能够为B伪造不同的密钥。对应的魔法实例是：Bracciali等人74A=（）[out（net，k）.out（net，fngk）.0]B4B=（）[in（net，k）.in（net，fygk）.0]3.2验证安全属性一旦一个所需的安全属性已经表示在一个神奇的协议的实例，我们可以验证是否存在入侵者可以违反数据的完整性（恶意）干扰协议。这样的检查是由一个不确定的算法，B协议P和魔法版本BP，要么返回一个P的入侵者-兼容并且不兼容P，或者如果这样的入侵者不存在.直观地说，该算法由以下主循环组成：(i) 尝试构建一个入侵者，它可以从它可以访问的信道上发送的消息(ii) 当没有消息可用时，非确定性地扩展入侵者，并向另一个组件发送与魔术实例中已固定的值不同的值。(iii) 退出循环时，所有主体都被简化为（）[0]，并返回构造的入侵者，或者在点（ii）中不能发送消息，并且不返回任何消息。在前面的例子中，我们粗略地描述了算法的执行过程，我们得到了入侵者的以下增量构造：入侵者通过（net，u）中的动作获取A（k）发送的第一条消息。入侵者通过（net，v）中的动作抓取A（fn g k）发送的第二条消息目前没有更多的信息。入侵者（现在知道k和n）将k'发送到B，其中k'6=k是由第i个入侵者生成的密钥。入侵者然后发送fmgk0 到B，其中h减少到（）[0]（如A在前一步骤中所做的）。所有本金都减少到（ ） [0]。构造的入侵者： I=（）[in（net，u）.in（net，vu）.out（net，k'）.out（net，fmgk0）]已经回来了很容易验证fI; A; B g是一个可能正确的上下文，B实例fI;A; B在I的前两个输入之后发生死锁，因为out（net，k）和（net，k '）中由于不同的基值k和Bk'。I是P兼容的，但它不是P兼容的，这相当于说，该协议不安全。Bracciali等人84总结发言我们已经提出了一个统一的框架来描述基于组件的编程的组合和安全问题。提出了一种半自动证明技术，用于验证以组件组成和交互方式表示的安全协议的正确性最近已经提出了几种形式化技术用于安全协议的分析（参见例如[1，9]和其中的参考文献）。另一方面，大量的基础模型解决了组件组合的问题（参见例如：[2，3，4，7，11]）。我们的方法的显着和新颖的特点据我们所知，只有[12，13]通过考虑可能（部分）不可信的组件的协调来解决组件安全组合的推理问题组件被封装到包装程序中以封装和实施安全策略。我们最近的工作[5]一直致力于扩展本文中提出的框架因此，安全属性一般表示为逻辑公式，而不是魔术instan- tiations。尽管它的简单性，所提出的逻辑允许表达其他类别的安全属性。目前的工作是致力于进一步验证所提出的方法，通过试验其应用到工作台的例子[8]。引用[1] M.阿巴迪和戈登。密码协议演算：spi演算。 信息与计算，148（1）：1{70，1999。[2] F. Arbab，M.Bonsangue和F.德波尔。移动组件的协调语言 在Proc. ACMSymp. 应用计算，ACM出版社，2000年。[3] F. Arbab，M. Bonsangue和F.德波尔。一种用于组件的逻辑接口描述语言。在Ant onio Porto和Gruia-Catalin Roman，编辑，COordination'2000，LNCS1906，第249页，塞浦路斯利马索尔，2000年9月。[4] K. Bergner，A. Rausch，M. Sihling，A. Vilbig和M. 布洛伊 构件的形式化模型。In G. Leavens和M. Sitaraman，编辑，基于代理的系统的基础，第189页{210.剑桥大学出版社，2000年。[5] A. Bracciali，A. Brogi，G. Ferrari和E.托斯托开放式安全协议的形式化入侵者识别工具。提交给软件技术和理论计算机科学的基础，2001年。Bracciali等人9[6] A. Bracciali ， A. Brogi 和 F.图 里尼 协 调互 动 模式 。 ACM Symposium onApplied Computing的相关文章 ACM Press，2001.[7] C.运河湖Fuentes，J.M. Troya和A.瓦莱西洛向IDL添加语义信息。真的实用吗？OOPSLA'99行为语义学集，科罗拉多州丹佛市，1999年。[8] 约翰·克拉克和杰里米·雅各布。认证协议文献综述未出版，1996年8月[9] R. Focardi和R. Gorrieri。安全属性的一种分类。计算机安全，3（1），1995年。[10] R. Milner，J. Parrow，and D.沃克移动过程的演算，I和II。信息 和 计算，100（1）：1{40，41 {77，1992年9月。[11] E. Najm，A.尼穆尔和JB史蒂芬妮分布式对象接口的内部类型。在Proc. 第三IFIP 会议上，开 放式基于对象的分布式 系统的形式化方法-FMOODS'99。Kluwer，1999年。[12] P. Sewell和J. Vitek。不安全组件的安全组合。计算机安全基础研讨会论文集，CSFW-12，1999年。[13] P. Sewell和J. Vitek。不可信代码的安全组合：包装器和因果关系类型。PCSFW：第13届计算机安全基础研讨会论文集。 IEEE Computer SocietyPress，2000.