移动环境监测：基于安全属性的扩展方法及其在广域网应用程序中的应用

52网址：http://www.elsevier.nl/locate/entcs/volume66.html24页环境监测G. 法拉利1文凭 意大利比萨大学InformaticaE. 莫吉2文凭 Informatica e Scienze dell'Informazione，意大利R. Pugliese3文凭 意大利佛罗伦萨大学信息系统摘要在Cardelli和Gordon的Mobile Ambients中，环境是移动性的单位，它可以包含进程（数据）和子环境。自从Cardelli和Gordon的开创性工作以来，已经提出了几种基于环境的结石（Seal，Box-安全环境、安全环境、盒装环境），主要用于支持安全性。在操作层面上，这些（盒子和）基于环境的演算只在过程的能力上不同我们提出了一种扩展基于环境的演算的方法更具体地说，我们在每个环境中附加监护人，其监控子组件（即，过程和子环境）以及与外部环境的相互作用。在我们的建议中，监护人和进程扮演着双重角色：监护人是监控和抑制行动的集中实体，而进程是执行行动的分散实体。 我们反对使用监护人来强制执行安全属性。1引言验证广域网（WAN）应用程序的安全要求WAN应用可以集成具有不同安全要求的异构计算环境。此外，安全策略不能使用1 由MIUR项目NAPOLI和欧盟项目PROFUNDIS IST-2001-33100支助2 由MIUR项目NAPOLI和欧盟项目DART IST-2001-33477支助3 由MIUR项目NAPOLI和欧盟项目AGILE IST-2001-32747支助c2002年由Elsevier Science B出版。V. CC BY-NC-ND许可下的开放访问。53WAN应用程序的整个当前状态。任何实际的方法都将确定WAN应用程序状态的哪一部分可能相关，并且可能受到安全策略决策的影响。最后，安全策略通常不是静态的：必须支持撤销先前授予的访问权限。因此，形式化的安全模型必须提供合适的机制来指定和验证各种安全策略的属性，包括策略更改和动态策略。在过去的几年中，一些研究活动已经探索了通过编程语言技术来加强WAN 应用程序安全性的方法： 基 于 语 言 的 安 全 性 。根据 Schneider ，Morrisett和Harper [41]，我们基本上可以区分两种不同的基于语言的安全方法：程序分析和程序转换。基于程序分析的方法需要对应用程序的代码有充分的了解。根据安全策略分析代码（静态或动态）。该方法确保只有不违反安全策略的代码才有机会被执行。访问控制的安全类型（参见[11，18，29]）提供了这种方法的很好的例子。另一个有趣的例子是在建模Java安全权限时使用的（静态和动态）技术（参见例如[48，38，3，25]）。在基于程序转换的方法中，执行安全策略的操作被合并到应用程序的代码中。其基本思想是一个引用监视器，它可以观察应用程序的执行，并在应用程序违反某些安全要求时停止应用程序。在这里，我们可以区分内联引用监视（reference monitoring，EM）和执行监视（Execution monitoring，EM）。 在这种方法中，应用程序代码被一些在运行时执行安全检查的附加代码所丰富。这意味着可能影响安全策略的事件是事先已知的[21]。当应用程序代码事先不可用时，执行监视适用。因此，应用程序代码必须被视为一个黑盒，它必须被包装在一个引用监视器[23]。本文提出了一种支持多种动态安全策略规范的形式化模型。该模型的基本思想是将计算机制（通信和移动原语）与执行安全策略的管理者（我们称之为监护人）分开。每个守护者基本上定义了一个本地安全上下文，该上下文仅控制当前状态的一部分。然而，监护人之间需要一定程度的协调，以支持网络间的安全策略。我们的建议与执行监控的想法密切相关，监护人就像指定允许的交互的安全自动机[21]。我们的方法的新颖性是由监护人协调。监护人的协调能够支持一套丰富的安全策略。换句话说，安全策略是可编程的分布式实体。我们的方法的主要特点总结如下54计算机制（进程行为）和安全支持（监护人允许和拒绝）之间的区别允许描述各种本地安全策略。从软件工程的角度来看，保持操作规范和权限规范的分离也很重要。监护人提供了一个描述本地安全策略的单元：可以授予代理进入、退出和在被监视的计算环境中通信的许可。安全决定是了解地点的监护人之间协调活动的结果。协调的安全决策通过确保权限符合本地安全策略来控制访问权限的传播。在本文中，为了证明该方法的适用性，我们引入了监护人演算。我们选择Boxed Ambient（BA）作为我们调查的起点[5，6]。这种移动环境演算的变体[13] 放弃开放能力，并为环境交互引入ne-grain机制（受Seal演算的启发[15]）。这些更改为安全策略的规范提供了更好的支持。监护人演算保留了Boxed Ambients的独特功能，但它不依赖于类型系统来强制执行安全的环境交互。在我们的方法中，环境配备了监护人，监护人监控环境内组件的活动及其与外部操作环境的相互作用。因此，每个监护人指定并执行本地安全策略，并且监护人协调限制周围移动的权限为了说明我们的方法，我们提出了一个简单的例子，资源访问控制中指定的BA。我们考虑一个系统s，它由一个资源r和一个移动进程n组成，s[ Qj n[ P] j r[ R]]让我们假设资源r由值v组成，因此R是进程！hv i： 0，并且使用资源等于读取值v。例如，进程P在r：（x）“：P 0中，即n进入r并从父进程mbie ntr读取值。我们是守护者 到ea cha mbienta，因此在我们的微积分中，上述系统变为s（Gs）[Qjn（Gn）[P] jr（Gr）[R]表达式n（G）[P]表示环境n在监护人G的控制下运行进程P。我们通过考虑当进程P试图执行inr操作时会发生什么来验证监护人之间的协调：(i) Gn 授权在mbie nts内将（mbie ntn）i n迁移到r;(ii) Gr 在mbie nts内授权mbie ntn进入内部（a mbie ntr）;(iii) Gs 授权在一个盒子里移动一个盒子。换句话说，对于环境移动授予的许可是结果55Rs（G0）[Qjr（G0）[n（G0）[（x）“：P0] jR]]s（G0）[Qjr（G00）[n（G0 0）[P0[x：=v]] jR]]四个实体的协调步骤：请求服务的过程和三个监护人Gn，GrGs 实现动作中涉及的环境的局部安全性。执行环境移动所需的四个实体之间的协议可能看起来具有沉重的运行时开销。然而，如果考虑环境移动的低级描述 见[22，39]），它涉及到三个环境和执行运动动作的过程。请注意，协调步骤遵循辅助性原则，即，只有直接涉及该动作的环境才能禁止该动作，并且位置不允许，例如，监护人Gn 仅在封闭环境S内授权移动。移动操作的结果是S R N读取r中的值需要协调四个实体，即r和n中的过程和监护人。特别是，监护人G0必须授权从子环境n读取。读取操作的结果是S R N在本文中，我们将证明监护人是强大的，足以动态地执行各种安全策略。以资源访问控制为例，介绍了监护人Gr 可以根据其名称阻止某些环境进入，允许非常有限的交互模式，例如，形式为只读一次然后退出的协议（否则，代理N可以执行多次读取），执行入侵检测检查，例如，代理n可能被想要进入r的其他环境用作特洛伊木马，通过授予具有相同名称的环境不同的特权来区别对待它们。本文的其余部分组织如下。在第2节中，我们回顾了盒装环境。第三节介绍了盒装环境语的监护人演算及其基本语义理论。第4节讨论了几个例子，说明监护人的表达能力，以实施广泛的安全协议。 最后，与相关工作的比较见第5节。2 Boxed Ambients：一种基于环境的语言在本节中，我们将介绍Boxed Ambients [5]（BA，在本文的其余部分），这是一种受Mobile Ambients [13] 启发的基于环境的语言。 BA使用与Mobile Ambients相同的移动原语，但依赖于受Seal演算启发的不同通信模型[15]。这个模型的结果是丢弃了开放原语，允许在父级和子级之间进行跨环境边界的通信，以及本地通信。56vXX我们对BA的语法和操作语义的介绍从原来的一个方面进行了几个方面的改进，即：我们不区分价值和（顺序）过程的句法范畴;我们考虑额外的过程动作对应的名称，过程和环境创建。当我们引入监护人时，这种关系会产生不同，监护人可能会禁止进程动作发生，即使在没有监护人的演算中，动作是异步和非阻塞的。为了更好的可编程性，我们还介绍了顺序组合（其中包括串联的能力），条件选择和递归定义（而不是复制）。我 们定义了网的转移关系，即模结构同余过程。直觉上，顺序过程（即值）是语法实体，而网是描述系统在给定计算时刻的状态的语义实体。演算的语法由以下BNF给出：n2姓名：：=：x2Var：：=：X 2PId：：=：：：b2B ool： ： =？jb1_b2j>jb1^b2j：bjv1=v2名称等于ya2Act ： ： =newjspawnjboxjinjoutjwrjwrup jwrdnjrdjrdupjrddn v; P2Proc：：=njxja（v;？x）：PjP1;P2j1 jifbthenP1elseP2jX（v）从语法上讲，进程P也可以是名称n或变量x，当然从语义上讲，它们是值而不是进程（因此它们不会产生以处理过渡）。Action pre xa（v;？x）：P 代表了一个过程，可以执行动作a：是值的序列（实际参数），并且是一个变量序列（形式参数），它可以在P. 形式参数被实际参数v所取代 通过同步（与其他进程），因此a（v;？x）：P绑定变量体育教学 P1，P2为顺序组合，1表示成功终止. 最后，我们有条件选择和流程调用X（v），其中我们假设对于每个流程标识符X（元数n），存在唯一的定义方程X（x）=P（其中长度为n）。关于BA的原始表示，我们使用三个额外的动作：new（？x）：P是对名称生成器的新名称的请求，因此它对应于BA的（x）P;spa wn（P1）：P2与P2并行地激活P1，因此它对应于BA的P1jP2;box（n;P1）：P2在名为n的新名称中将P1映射，因此它对应于BA的n[P1]jP2。XX57vXv其余的行动直接对应于BA的行动。动作in（n）：P和out（n）：P是用于环境移动。作用wr（v）：P和rd（？x）：P用于本地通信：wr（v）：P输出val-1的序列。ues，rd（？x）：P输入一个值序列并将它们绑定到序列的变量。 动作wrup（v）：P和rdup（？x）：P是针对与父通信和工作类似，而wrdn（n; v）：P和rddn（n;？x）：P代表与一个名为n的子节点的通信。在[5]中，BA的操作语义是用过程上的结构同余和归约关系来定义的。这里，操作语义由网的转移关系=）给出，其中网N基本上是过程模结构同余。 净过渡F;N=）F0; N0 根据过程转换P来定义a（v）0. 这> P区分是方便的，因为监护者与过程转换同步（而不是与净转换同步）。进程终止（用P #表示）是一个谓词，它表示P是否可以成功终止。该谓词用于定义进程顺序组合的转换。1rec1号P[x：=v]#X（v）#如果X（x）=P;P1#P2#P1; P2 #iftbtrueP1 #ifbthenP1elseP2#bfalseP2 #我ifb thenP1 elseP2#a㈤过程转换P0，其中是闭合值的序列（即，v> P没有自由变量），是一个谓词，说明P可以执行动作a（v）并成为P0。X之前的操作规则的形式是一a（v;？x）：Pa（v;v0）>P[x： =0]受到限制和0 这取决于a。新new（？x）：Pnew（n）>P[x： =n]产卵spawn（ P1）：P2产卵（P1）>P2框box（ n;P1）：P2框（n1;P1）> P2在in（ n）：Pin（ n）> P出来out（ n）：out（n）> Pvv58vvvvWRwr（v）：Pwr（ v）> P路rd（？x）：Prd（ v）>P[x： =]鲁普wrup（v）：Pwrup（v）> Prduprdup（？x）：Prdup（v）>P[x： =]世界新闻网wrdn（n;v）：Pwrdn（n;v）> PRDDNrddn（n;？x）：Prddn（n;v）>P[x： =]其余的规则都相当标准。a（v）0rec P[x： =]>Pa（v）0如果X（x）= PX（v）> Pa㈤均p0a（v）01> P1;fP1#P2;c> P2a（ v）0a（ v） 0P1;P2> P1;P2a㈤P1;P20> P2a（v）0iftb真P1> P1b假P2我> P2如果b则P否则Pa（v）0如果b则P否则Pa（v）01 2> P11 2> P2条件选择的规则依赖于布尔表达式B.派生btrue和bfalse的规则是显而易见的，只有名称相等的规则值得一提=tn= n真=fn1=n2false如果n16=n2注意，布尔表达式v1=v2只有在v1和v2是名字时才有值，因为在其他情况下，比较没有意义。注2.1我们并没有定义关于过程的观测同余，但是任何这样的同余至少会证实方程（1;;）形成幺半群。2我们现在可以定义BA的净转换。 形式上，净N2Net=（Proc+（Name Net））是进程P和命名子网n [N]的多集合。我们在命名的网n [N]上定义变迁，因为我们希望总是有一个顶层的环境n（有一个相关的监护人），它可以忽略网的演化（相反，在类似环境的演算中，变迁是在通用过程上定义的）。网转移定义在形式为F; n [N]的构形上，其中F_fin_Name包含n [ N ]中的所有自由名。 F跟踪整个网络中的自由名称（即迄今为止生成的名称），并需要确保名称的全局新鲜度 。 当 转 换 不 生 成 新 名 称 时 ， 我 们 写 n[N]=） n[N0] 而 不 是F;n[N]=）F;n[N0]。净转移F;n[N]=）F0;n[N0]定义为：5900000F;n[N]=）F0; n[N0]0F;n[N; n[N]]=）F0; n[N; n[N0]]新w（n0）产卵（P1）框（n1;P1）结构规则2 2 221 1 2 21 1 22以及由过程转换引起的基本净转换。对于每一个净过渡，我们命名为过渡中（主动或被动）涉及的环境（当环境中的一个过程参与导致过渡的动作/交互时，环境是主动的）。基本的网络变迁分为三类。异步和非阻塞转换：新P> Pn62F n处于活动状态F;n[N;P]=）F[fng;n[N;P]P产卵> P2n活跃n[N;P]=）n[N;P1;P2]框P> P2n活跃n[N;P]=）n[N;n1[P1];P2]异步和可能阻塞的转换：in（ n2）0P> P在n[N;n1[P;N1];n2[N2]]=）n[N;n2[n1[P;N1];N2]]out（n2） 0出来P> Pn[N;n2[n1[P;N1];N2]]=）n[N;n1[P;N1];n2[N2]]在上面的规则中，我们假设n 1是主动的，n，n 2是被动的。同步转换：wr（ v）0rd（ v）0P1Comm> P1P2> P20 0n活跃n[N;P1;P2]=）n[N;P1;P2]wr（ v）0Prdup（v） 0rdup1> P1P2> P20 0n1和n2活动n1[N1;P1;n2[P2;N2]]=）n1[N1;P1;n2[P2;N2]]rd（v） 0wrup（v） 0鲁普P1> P1P2> P20 0n1和n2活动n1[N1;P1;n2[P2;N2]]=）n1[N1;P1;n2[P2;N2]]rddn（n2;v）0wr（v） 0RDDNP1> P1P2> P20 0n1和n2活动n1[N1;P1;n2[P2;N2]]=）n1[N1;P1;n2[P2;N2]]60vXn[N; P; n[P; N]]=）n[N; P0; n[P0; N]]我wrdn（ n2;v）均p0rd（v） 0世界新闻网1> P1P2> P2n1和n2活动1 1 1 2 221 11 2223守卫盒装环境：一个扩展与监护人在本节中，我们描述了受保护的盒装环境（简称GBA），即BA与监护人的扩展基本的想法是，监护人Gg（v）0（其中是封闭值的序列）形式上v> G类似于过程转换。但是，监护人转换相当于对流程操作（或交互）的许可。GBA的语法由下面的语法给出。在这里，我们只显示新的和扩展的句法类别，所有其他类别都没有改变。W 2GID：：=：g2Perm：：=new jspawn jbox jin1 jin2 jin3 jout1 jout2 jout3jjrdup1 jrdup2 jwrup1 jwrup2 jrddn1 jrddn2 jwrdn1 jwrdn2G2Gard：：=g（x）whenbthenGjG1_G2jW（v）jGn g（x）当bj？j > j G1^G2v; P 2过程：：=： JG注释3.1动词由句法范畴Perm给出。对于每个基本网络转换和转换中涉及的每个环境n，存在一个许可g。直观地说，g（v）意味着（环境n的）监护人G允许基本的净转换，只要转换的参数（以及所涉及的其他环境的名称）是指定的那些参数。in. 因此，监护人的作用仅仅是约束过程的作用（和相互作用）2我们取b那么G作为监护人g（x）的基本构造，其中g是一个权限，是一个由结构绑定的变量序列，b是一个布尔表达式，G是监护人。监护人的其他结构受到同步进程演算的启发，如SCCS [33]。当然，还有许多其他的进程代数形式可供选择，但同步演算似乎特别适合强调监护人的整体性质，即。每个环境一个监护人监护人G完全由给出方程组hW（x）=G中使用的每个W，并且Gi.Giji2Ii de ning the meaning of注3.2对于指定监护人，BNF的第一排。然而，第二行中给出的静态组合子是非常方便的派生形式。261v> G0过程和价值的句法范畴Proc被扩展为一个新的产生式G，因为价值现在也包括监护人。操作语义由一个转换关系给出==） OVERNETSa㈤0d和> Pg（v）> G流程转换是由第2节中的规则定义的，但是现在的名称创建规则是新new（？x;G）：Pnew（n;G[x：=n]）> P[ x：= n]在GBA的前x新（？x; G）：P是对新名称的请求，监护人G类似于新名称的类型，并且关联名称监护人遵守静态范围的规则。监护人转换由以下规则定义允许b [x：=]真的g（v）关闭g（ x）当b时，则G> G[ x：= v]g（v）的g00g（v）0我或 G_ G> Gg（v）i2f1;2gW0G[ x：= v]> GW（v0）g（v）0W（ x）=G1 2> G> Gg（v）拒绝1g（v）Gn g（ x）当b> G0ng（ x）当bg（v）的g0否认2Gn g（ x）当b> Gg0gg0（v）> G0ng（x）当bg（v）的g0g（v）01和> G1G2> G2>关闭G^Gg（v）0 ^0g（v）>1 2> G1G2>>注3.3我们没有定义关于监护人的观测全等性，但任何这样的全等性将至少验证以下等式性质：（怎么样？;_）和（>;^）形成交换幂等幺半群;的分布性（？;_）超过^，即 ？ G =？（G1_G2）^G =（G1^G）_（G2^G）;的交换性ng（x）当b有？时，_和^，即？n g（x）当b =？时，（G1_G2）n g（x）when b =（G1n g（x）when b）_（G2n g（x）whenb），对于^也是如此。2我们现在可以为GBA定义新的过渡。 形式上，一张有监护人的M2GNet=（过程+（名称GardGNet））是多进程集合Pvv62翅片11F;n（G）[M]=）F0; n（G0）[M0]F;n（G）[M; n（G）[M]]=）F0; n（G）[M; n（G0）[M0]F;n（G）[M;P]==）F;n（G0）[M;n（G）[P]; P]n（G）[M;n（G）[P;M]; n（G）[M]=）n（G0）[M;n（G0）[n（G0）[P0; M]; M]n（G）[M;n（G）[n（G）[P;M]; M]]=）n（G0）[M;n（G0）[P0; M]; n（G0）[M]并将子网n（G）[M]命名为监护人。 净转换定义为形式F; n（G）[M]的配置，其中F：名称！加德联合公司到目前为止生成的名称的监护人。F就像一个全局环境，当一个新的名字被生成时，它被扩展，当一个新的环境被创建时，它被查找（即一个盒子动作被执行）。当一个转换不产生新的名字时，我们写n（G）[M]=）n（G0）[M0]代替F;n（G）[M]=）F0;n（G0）[M0].根 据 一 个 结 构 规 则 （ 类 似 于 BA ） 定 义 了 净 转 移 F;n （ G ）[M]==）F0;n（G0）[M0].子网2 2 222 21 1 1 2 221 1 1 22 2和基本的净转换，分为三组（如前所述），由过程转换激活，但具有与转换中涉及的环境的监护人所授予的许可相异步和非阻塞转换：new（ n1;G1）均p0new（n1;G1） 0新> P G> Gn162dom（女）F;n（G）[M;P]=）F[n7！G];n（G0）[M;P0]产卵（P1）P产卵（P1）0产卵> P2G> Gn（G）[M;P]==）n（G0）[M;P1;P2]框（n1;P1）Pbox（n1;P1） 0框> P2G> GG1=F（n1）1 1 1 2在（new）中，请求新名称的进程P必须为其提供监护人，因此在名称生成时建立名称监护人关联（并记录在部分函数F中）。在（框）中，新环境的监护人从F恢复，而在新环境中运行的进程是在环境世代的时间被摧毁。异步和可能阻塞的转换：in（ n2）0P在1（n;n2）0中在2（n;n1）0中在3（n1;n2）0中> P G1在> G1G2> G2G> G1 1 1 2 2222111 2out（ n2）均p0输出1（n;n2）0输出2（n;n1）0输出3（n1;n2）0出来> P G1> G1G2> G2G> G2 2 1 1 12111 222同步转换：wr（ v）均p0rd（v） 0（v）01Comm> P1P2> P2G> Gn（G）[M;P; P]=）n（G0）[M;P0; P0]1 21 263n（G）[N; P; n（G）[P; N]]=）n（G0）[N; P0; n（G0）[P0; N]]n（G）[N; P; n（G）[P; N]]=）n（G0）[N; P0; n（G0）[P0; N]]n（G）[N; P; n（G）[P; N]]=）n（G0）[N; P0; n（G0）[P0; N]]n（G）[N; P; n（G）[P; N]]=）n（G0）[N; P0; n（G0）[P0; N]]wr（ v）均p0rdup（v） 0rdup2（n2;v） 0rdup1（n1;v） 01rdup> P1P2> P2G1> G1G2> G21 1 1 1 2 2 22111122 22rd（ v）0Pwrup（v） 0wrup2（n2;v） 0wrup1（n1;v） 01鲁普> P1P2> P2G1> G1G2> G21 1 1 1 2 2 22111122 22rddn（ n2;v）均p0wr（v） 0rddn1（n2;v） 0rddn2（n1;v） 01RDDN> P1P2> P2G1> G1G2> G21 1 1 1 2 2 22111122 22wrdn（ n2;v）均p0rd（v） 0wrdn1（n2;v） 0wrdn2（n1;v） 01世界新闻网> P1P2> P2G1> G1G2> G21 1 1 1 2 2 22111122 22注3.4在一个有监护人的网络中，当一个新的环境名为n时（即当一个盒子动作被执行时），我们必须为这个新的环境提供一个监护人。在GBA中，我们决定新环境的守护者由创建名称n的进程（通过执行新操作）提供。我们回顾了替代方案，并讨论了它们的优缺点。有四个实体可以为新环境提供监护人(i) 产生n的新动作的过程Pn;(ii) 进程Pn的守护者Gn;(iii) 处理过程Pb，其产生框动作spawningn[P];(iv) 进程Pb的守护者Gb。选项i和iii使进程了解监护人。 选项i和ii需要一个全局环境来记录在创建名为n的环境时要使用的监护人。选项ii太通用了，因为Gn不知道Pn计划如何使用n，所以它将为所有新名称提供相同的监护人。选项iii似乎是最灵活的，因为新环境的监护人是在环境生成时决定的。我们选择了备选方案一，它更严格，但也更安全，它体现了一个名字一个政策的原则。2定义3.5【消去】给定M2GNet，消去M中出现的所有监护人，得到净jMj2NetjM j可以通过对M的结构进行归纳而得到形式上的定义。下面的性质表明，监护人的引入对净转移只有命题3.6如果M=）M0，则jMj=） jM0j我们通过给出几个守护者的简单示例来结束本节，守护者是静态类型的动态代理：？、什么都不允许。 在n（？）[M]子网仍然能够进化，64但却是孤立的“一切都是允许的。Immobil e=>nout1（x）nin1（x）力不动：网n（Immobile）[M]不能移动。Shh= >n（x）禁止本地通信，Comm（）=>n nn n（x）when：x：将本地通信限制为类型的值（我们需要一个谓词：，它执行动态类型检查）。没有办法定义一个对应于安全环境的单线程类型的守护者[31]，但是可以通过禁止spawn操作来防止新线程的创建。注释3.7有人可能想知道监护人执行的执行监视会引入多少运行时开销。在环境运动（进）和（出）的情况下，四个实体之间的一致性是移动环境[22]和安全环境[39]的分布式抽象机器中发生的事情的忠实代表。[22]的异步分裂可能会导致许多阻塞情况，这些情况在原始语义中不存在，但可以允许，因为我们主要对安全属性感兴趣。类似地，盒装环境通信的实现将需要多个部分的合作。在所有其他情况下，与守护者的同步代表了真正的开销。这种开销可以通过采用异步通信来减少，这相当于每个环境具有一个数据存储库（因此与监护人的同步对应于与数据存储库的交互）。规则（新的）和（框）引入了与扩展和对环境F的访问相关的开销，将名称映射到监护人。这种环境可以扩展，但关联永远不会被覆盖，因此一些简单的缓存技术可以大大减少开销。最后，我们讨论一下spawn规则。BA/GBA进程可以被认为是一个线程，每次执行一个动作因此，动作spawn（P）对应于请求开始执行P的新线程的系统调用（因此与监护人的同步对应于与操作系统的交互）。目前，监护人不能区分复杂的值（仅在名称之间）。然而，通过在值上扩展新的谓词（除了名称相等之外），可以设想产生新线程的权限是基于对P的运行时分析的。2654示例在本节中，我们提供了几个示例，展示了监护人动态执行安全策略的表现力。为此，我们将在我们的演算中描述一些已经在文献中讨论过的环境交互协议，以指出和讨论环境类演算的优点和缺点 在例子中，我们可以使用导出形式g（p）thenG和G n g（p），其中p：：=xj nj是模式。派生形式的意义是显而易见的，例如。g（x）则G对应于g（x）当>则Gg（n）thenG对应于g（x）当x=nthenG，x 62 FV（G）g（）则G对应于g（x），当>则G时，x62 FV（G）。例子中的守护者似乎可以分为两类：除非明确禁止，否则一切都是允许的（利用\deny”组合子），只允许非常有限的交互模式（利用动态组合子：\allow”，\choice”和\recursion”）。示例中未使用\and”组合器。它可以用于将实现基本策略的监护人组合成更结构化的策略，就像包装器的被动组合一样[23]。4.1防火墙rewall协议（见[12，31，6]）已经被引入来检查哪些是通过rewall控制访问所需的活动。在这个协议中，ambientf描述了一个rewall，我们假设rewall的名称必须始终保持未知。外部代理a可以通过引导环境k进入rewallf，但是外部代理没有权限从rewallf退出（因此携带机密信息，如名称f，外部）。 下面的网（没有监护人）描述了最初的孔古-比率：a[in（k）：out（k）：Pa]; f[k[Xk（f）];Pf]其中Xk（f）=out（f）：in（f）：Xk（f）。rewall协议的预期行为对应于以下转换序列：a[in（k）：out（k）：Pa]; f[k[Xk（f）];Pf]k从f退出a[in（k）：out（k）：Pa];k[in（f）：Xk（f）]; f[Pf] a从n到kk[a[out（k）：Pa];in（f）：Xk（f）]; f[Pf]kentersbackintoff[k[a[out（k）：Pa];Xk（f）];Pf]a从k退出f[k[Xk（f）];a[Pa];Pf]k在初始状态下是back，a可以与Pf然而，从初始配置开始还有其他的转换序列违反了协议特别是a可以从f中出来66(even如果Pa不知道名字f），则从k乘电梯返回。我们现在描述f和k的两个简单监护人（Wf和Wk），它们动态地执行预期的安全策略。没有对监护人进行假设，因为恶意代理也可能有恶意监护人。Wk=out1（;xf）thenin2（;）thenin1（;xf）thenout2（xf;）thenWk监护人Wk描述了强制执行以下操作顺序的安全策略：(i) k从封闭环境f中退出（并且xf绑定到f）(ii) k允许一个环境进入(iii) k回到环境f(iv) k允许一个环境离开（同时保持在f内）当这些动作终止时，导频环境k回到其原始状态。当x 6 = k时，Wf=Immobil eni n2（;x）监护人Wf确保rewall的不动性，并且仅允许具有名称k的环境穿过rewall。请注意，Wk没有明确使用rewall的名称f，而Wf使用名称k表示pilotambients。由于名称-监护人的关联是在名称-生成-时间进行的，这意味着名称k必须在名称f之前生成。然而，这不是一个强约束，因为我们希望保持f私有，因此最好尽可能晚地生成它，（即，就在生成具有名称f的环境之前）。有人可能会说，监护人Wf的限制太多了。 特别是，可以采用一个更简单的监护人为所有的rewf，不使用k，e。G. Wf=一动不动可以通过其他机制来确保具有穿过rewall的许可的唯一环境具有名称k然而，这似乎需要仔细设计的Pf（有更多的全球性假设），因此，它似乎不是我们作为一个可行的选择。4.2列车运行列车协议（见[8]）可以描述如下：有一列列车t在两个车站a和b之间移动，乘客p在车站内时可以进出列车，但在车站之间移动时不能。如果乘客p想在某个车站上车，他需要在火车到达该车站时得到通知。在[8]中，通过利用一个新的环境重命名原语对该示例进行建模。 直觉上，列车环境采用合适的名称来隐含地通知乘客它何时到达某个车站，而当它移动时，它采用乘客不知道的名称（这样乘客就不能进入或离开列车）。列车协议提供了一个很好的形象化的例子，在存在的流动性的访问控制。我们将通过一个协调活动672=3out（;）然后W0有一个合适的环境称为公告。当列车到达某个车站（分别为a或b）时，通过列车产生的环境通知（@a或@b注4.1在Mobile Ambients [13]中，环境重命名可以用微积分原语来表示，尽管翻译不保持原子性，并且可能会引起不必要的干扰。相反，在GBA中，环境重命名在演算中不是内部可表示的，但是我们避免将其作为原语引入，因为它与原则不一致“一个名字一个安全策略”。2下面的网（没有监护人）描述了初始配置：a[];b[];t[Xt];p[X1]，其中Xt=in（a）：box（@a;out（t）：0）：out（a）：in（b）：box（@b;out（t）：0）：out（b）：Xt，i. e. THE列车T在A站和B站之间移动。X1 对一般乘客建模，例如 X1=in（a）：in（t）：in（@b）：out（@b）：X2意思是：进入a站，上t车，听广播@b，在b站上车o。在此之后，乘客可以离开车站b，或登上另一列火车，到达第三个车站c。这第二个behavior是由X建模in（t0）：in（@c）：out（@c）：X.我们现在描述三个监护人： 对于站点a和b，W@s 用于广播ts@a和@b，以及用于列车t的W t。对于乘客p，不作任何假设Ws =Immobi leW@s=in2（;）则W@s_1@sW0 0@s=out2（;）则W@s监护人W@s强制执行以下操作顺序：第一个乘客进入@ s，然后@ s离开火车，最后乘客离开@ s。Wt =in1（;xs）thenbox（x@s;）thenWt（xs;x@s）Wt（xs;x@s）=in2（;）则Wt（xs;x@s）_在3（;x@s）中，则Wt（xs;x@s）_out2（;x@s）thenout1（;xs）thenWt守护者Wt 描述了列车的安全性。首先到达车站并发布公告，然后乘客上车（即。 输入T）或得到O（即，输入@ S），最终@ S退出T并且T离开站S。68X一4.3可加密数据包在这个协议中，从[13，30]，一个包被用来驱动一些信息到不同的目的地。在我们的公式中，代理a使用一个可路由的数据包p被携带到其目的地。环境p支持以下交互：它允许代理a进入p并通知p到达其最终目的地的路线M。然后p执行M指定的运动序列，完成后a从p退出，p返回其原始状态。本协议的安全要求如下：可路由分组p不能执行M中指定的不是移动动作的动作;代理A应该只在到达最终目的地时才离开分组;在协议完成之前，不应允许其他代理进入数据包p内部。下面给出了代理和可重命名数据包的行为=in（p）：wrup（M）：out（p）：P，其中，动作wrup在a的父环境中（即，在可路由分组p中）产生进程Mp=rd（？x）：ne w（？z;？）：x;box（z;1）：Xp，其中x之后的框动作被利用来通知监护人Gp 当目的地到达时。请注意，由于z是一个新名称，因此x不知道它。我们现在描述用于可路由分组p的守护者。这个守护者强制执行协议指定的操作顺序，无论a有多恶意：Gp=in2（;xa）thenwrup2（xa）thennew（z;）thenGp（z;xa）G_p（z;x_a） =1（;）则G_p（z;x_a）_out1（;）则Gp（z;xa）_box1（z）thenout2（;xa）thenGpGp瓜尔豆球，例如， 两个不同的路由不能进入该分组，并且与要遵循的路径相冲突。 GP不能保证P最终到达由M指定的目的地，除非由M使用的所有环境都是固定的。事实上，我们不能依赖代理a来确保这个属性。然而，我们可以将Gp修改为Gp的m个边界中的所有仅移动的运动，已知为不可移动（这意味着必须在名称P之前创建这些环境的名称）。X695相关工作政策执行机制。已经利用了几种替代方法来在联网计算系统中实施安全这些方法可能在所需的信任级别、强制执行的安全策略的灵活性以及组件生产商和用户的成本方面有所不同。一个全面的安全框架可以通过各种互补问题的结合而产生。正如[42]中所指出的，像代码签名和沙箱（例如考虑这些概念的Java实现[26，24]）这样的方法成本低，但不能强制执行灵活的安全策略（签名的组件可能以任意方式运行，用户必须信任组件生产者，沙箱组件是孤立的，不能相互交互三种明智而灵活的基于语言的技术|类型系统、内联引用监视器和验证编译器。|在[41]中指出并评价了。类型系统（例如，在[45，28]中使用的那些方法）针对所需的安全策略静态地分析应用程序代码;它们需要代码的全部知识，必须按照类型系统编写，并且通常不需要任何运行时开销。内联引用监视器通过在目标应用程序中插入额外的代码来强制执行所需的安全策略，从而该技术已用于软件故障隔离（参见，例如，[46])，并且在[21]中给出了使用安全自动机作为指定安全策略的机制的两个在[43，44]中，类型专门化被用来删除（在某些情况下）所有运行时安全检查从程序转换为内联监视执行，同时保证转换代码的安全性认证编译器产生目标代码以及证书，即机器可检查的证据，表明目标代码遵守某些安全策略。这种技术已经被使用，例如，用于生成证明携带代码[34，35]和执行标准安全策略（