封闭环境中的信息流安全问题研究及类型系统设计

76网址：http://www.elsevier.nl/locate/entcs/volume66.html22页封闭环境Silvia Crafa1米歇尔·布列西1Dipartimento diInformaticaUniver sita`Ca朱塞佩·卡斯塔尼亚2De' partement摘要本文从抗干扰性的角度研究了封闭环境中的信息流安全问题.我们开发了一个健全的类型系统，提供了静态的保证，没有不必要的信息流类型良好的进程。非干扰的规定，并证明，在一个类型的概念，上下文等价的盒装环境类似于相应的等价定义为移动环境。1介绍Boxed Ambients演算[4]是一种新的进程演算，它来源于Mobile Ambients[8]，为分布式和移动代理系统中的资源保护和访问控制提供了更细粒度的抽象。在Mobile Ambients（缩写为MA）中，代理是形式为n[P]的进程，表示环境，名为n，执行进程P。进程可以并行组成，如PjQ，行使能力，如M：P，声明本地名称，如（n）P，或者简单地什么都不做，如0。环境可以被嵌套以形成树结构，该树结构可以通过运用能力in、out和open来动态地重新配置。作为示例，该系统k[inn：P1jm[outn：P2]] jn[openk：Q]包含两个环境，k和n，并行运行。该系统可能演变如下。首先，环境k可以通过行使“在n中“的能力而迁移到n1 电子邮件：fsilvia，micheledsi.unive.it2 电子邮件：Giuseppe. ens.frc 2002年由Elsevier Science B出版。诉在CC BY-NC-ND许可下开放访问。77n[o penk：Qj k[P1j m[outn：P2]。 N o wn可以“dissolve v e”k释放其内容：n [ Q j P 1 jm [ out n：P 2 ] ]。最后，y，m可以是：n[QjP1]jm[P2]。 此外，环境和过程可以通信。在MA中，交流是匿名的，发生在环境中。 系统（x）P j hM i表示两个进程的并行组合，输出进程hM i“丢弃”消息M，输入进程（x）P读取消息M并继续为P f x：= M g。Boxed Ambients的演算（以下简称BA）是MA的一个变体，它从MA继承了具有完全相同语义的移动性的原语in和out（但不是open至于通信，除了本地交换之外，BA还依赖于一组额外的原语，这些原语提供了父级和子级之间跨环境边界的值交换。在语法上，这是通过指定交换应该发生的位置的标记来实现的：例如，（x）nP表示来自子环境名称n的输入，而hMi“是到父环境的输出（在后一种情况下，我们说的是向上交换）。父-子交换的语义由以下约简定义3：（x）nPjn[hMi“Q]›Pfx：=Mg jn[Q]hMinPjn[（x）“Q]›Pjn[Qfx：=Mg]作为副产品，这种通信语义产生了环境的本地和向上匿名信道作为该环境的“资源空间”的直接解释 通过依赖于这种解释，可以形式化资源访问的精确概念，即：（x）nP是对n的读访问，而hMinP是写访问。在[5]中，我们证明了BA为资源访问安全提供了一个有效的框架：具体地说，我们使用BA的类型化版本来建模多级Manda- tory访问控制（MAC）策略，包括军事（无读，无写）和商业（无读，无写）安全4。盒装环境与信息流安全我们在[5]中定义的类型系统是针对资源访问控制的，并且专门设计用于保护资源，即通道，免受未经授权的客户端的不希望的使用。在这里，我们改变视角，专注于针对信息流的不同为了激发视角的变化，考虑以下示例，其中`是`[（x）hPjh[hMi“QjR]]⑴3 这些都不是我们在[5，4]中介绍的缩减。本文第二节讨论了新语义的选择4 虽然我们在[5]中研究的资源访问控制策略是基于不同的归约语义，但这些技术可以平滑地适应新的语义（参见第2节讨论）。78在[5]的系统中，试图通过封闭在低水平环境中的过程，`从h读取被归类为读取，因此被军事和商业安全部门视为“不安全”而拒绝，而不管M的信息内容如何另一方面，如果表达式M是公开的，即，在低级别，没有理由不允许读访问：一段数据从高流向低，但是该流是“安全的”，本文件的目的是提供静态保障措施，防止“不安全”的信息流动。信息流的第一个相当直观的概念可以直接与数据流相关：如果没有高级数据从高级主体流向低级主体，则系统是“安全的通过对用于数据通信的传输层（即信道）的静态控制，这种形式的安全信息流很容易被解释和实施如果我们根据数据和通道的安全级别对其进行分类，则可以通过以下要求来保证不存在这种形式的（怎么样？高级数据只能沿着高级通道传送，并且高级通道只能位于高级主题内。信息流安全的一个更微妙、更有趣的概念与隐式信息流的存在有关，这是通过系统范围的副作用间接传输信息的方式（即隐蔽通道）造成的为了说明，考虑上述系统（1）的以下专门化，其中P是`[（x）hhNi“jh[hMi“]] j（x）`P（2）假设M和N是低水平值，则在该系统中不存在直接流然而，在P和环境h之间建立了一个隐蔽通道，因为P是通过取决于高环境h的存在的交换释放的，并且高水平环境的存在（或不存在）可以被同化为一位高水平信息，在所讨论的系统中，这些信息向下流动信息流安全与不干扰定义（隐含的）信息流的确切含义可能很难（也许是不可能的），许多作者都依赖于不干涉，这是一个更容易形式化的概念，意味着没有流动。不干涉的概念最早是由戈根和梅塞格提出的[14]对于确定性状态机。其思想是确定在给定的系统中，高级主体（或“用户”）的“输入”是否可能影响，即，干扰低水平受试者的“输出”。如果后者对前者是不变的，则判定系统是无干扰的。非干扰性后来[13]在类似CCS的过程演算中被重新表述为所谓的非演绎成分（NDC）属性，这意味着低级别的观察者对系统中高级别组件（源）的存在不敏感。在这里，我们采用相同的方法，并重新表述NDC属性，以捕获基于环境的特定计算方面，即局部性和移动性。79概述我们的技术提供保证BA中的非干扰是基于静态类型。我们依靠类型来形式化高和低数据和过程的概念，并定义非干扰定义下的过程等价关系。类型系统是基于环境和能力类型，类似于在MA的同伴类型系统中此外，我们的类型系统的类型携带安全注释，这些注释定义了值和进程的安全许可过程具有其封闭环境的间隙，而值（即，能力和名称）被分配如下的安全级别：名称具有与它们的类型相关联的安全级别，而能力被判定为在将数据和过程划分为“高”和“低”之后同样，这个概念是在类型系统的帮助下形式化的（参见第3节）。作为我们形式化的下一步，我们引入了一个行为等价关系来比较过程。这个关系是在[9]中为MA引入的等价关系的类型化版本：一个上下文等价，当且仅当两个过程被插入任何任意但类型良好的封闭上下文时，它们都允许相同的基本观察。我们的可观察性谓词类似于[9]中研究的谓词，但经过改进以捕获盒装环境之间交互的核心形式，即环境沿着其向上通道交换价值的能力。因此，我们说，一个过程P显示一个名称n，如果P（在任何数量的步骤中，减少到一个过程）包含一个可以接受与外部环境的相互作用的环境n，也就是说，如果P（或任何过程，它减少到）在结构上等价于（m1）： （mk）（n[hMi“P0j Q0]j Q0 0）其中n2=fm1; ：;mkg. 虽然，这种观察的概念特别集中在通信上，环境移动性仍然通过其对向上通信的影响而被间接地观察到，如下面的例子所示（高级别环境H的存在触发低级别环境的向上通信）：（x）`Pj`[inh：outh：hMi“] jh[ ]最后，我们介绍了上下文等价的概念诱导的低级别的观察：两个（良好类型的）进程P和Q是equi-valent，P=LQ，如果当-ever他们被插入到一个任意的（良好类型的）上下文，他们表现出相同的低级别的名称。基于此，我们可以将BA的[13]的NDC属性表述为：（？？）过程P是无干扰的当且仅当8H2HPj H=LP.如[13]中所述，P的非干扰仅针对与P平行出现的高电平源进行检查。在这种情况下，这是很自然的，因为CCS流程的拓扑结构是完全平坦的。相反，在BA环境中，80因此，与P交互的高级进程也可以（i）包围P或（ii）被包围在P内。这样看来，我们对不干涉的定义应该加以推广，以涵盖这些额外的情况。然而，事实上，所给出的定义确实解决了这些情况，因为并行运行的环境可能由于移动性而任意嵌套。主要成果和论文计划本文的主要贡献是（i）为新版本的BA定义了一个健全的类型系统，更重要的是，（ii）证明了良好类型的过程确实是无干扰的，在我们刚刚概述的意义上。非干扰证明建立在Cardelli和Gordon在[9]中为MA开发的技术工具上，使其适用于BA，并严格依赖于选择上下文等价作为底层等价关系。事实上，正如我们在第6节中所讨论的，我们目前的结果并没有扩展到更精细的等价关系，例如倒钩同余[19]。该 文 件 继 续 如 下 。 在 第 2 节 中 ， 我 们 提 出 了 一 个 新 版 本 的 BoxedAmbientsCalculus，它与[4]的不同之处在于其通信模型的语义。由此产生的演算具有更简单的表示，并且其对环境交互的更细粒度的控制更自然地使得能够发展代数几何理论和安全评估。在第三节中，我们描述了BA的一个健全型系统，其良型过程在第四节中被证明是无干扰的。第5节和第6节专门讨论相关工作和结论。2盒装环境在本节中，我们回顾了[4]中Boxed Ambients的语法，并提出了一个新的归约语义，从[11]中借用（它首次引入Seal Calculus），并根据跨环境边界通信的新规则进行定义。新的演算仍然坚持了原始演算的资源局部性原则，同时为环境提供了对他们与孩子之间的交流的完全控制。2.1语法类型化演算的语法由以下产生式定义表达式位置M：：= mQ名字：：= M名称、变量阿克斯z变量“母环境白藜芦醇MMr.JolieM：M输入MM出口路径？当地81过程P：：=0停止M：P行动 （n：W）P限制Pj P组合物M[P]环境！P复制 （x1：W1;：：;xk：Wk）P输入hM1; ：;MkiP输出表达式类型W：：=amb[E]ambient可编程能力交流E; F：：=shhno exchange1Wneexchange进程类型不 * = [英;法]综合交易所在MA中，进程可以被命名，如在n[P]中，可以被并行组合和复制，可以在内部或外部行使能力，可以声明本地名称，可以不做任何事情或交换值。 输入进程可以在本地读取一个值，如（x：W）？P，从一个名为n的subambient，如（x：W）nP，或从封闭上下文：（x：W）“P。提供相应的原语用于输出。 像往常一样，语法允许形成无意义的过程形式，如in（outm）或（outn）[P]：这些项可能是归约的结果，但仅限于病态项。我们使用一些符号约定。我们使用m; n;：q来在名称上进行范围，x; y; z在变量上进行范围。A; B;C; A;B;C。我们写（x~：W~）P为（x1：W1; ： ：;xk：Wk）P，hM~i为hM1; ：;Mki，和（p~）P，对于（p1）：（pk）P。 像往常一样，我们省略了拖尾死进程，将M：0写为M，将hM~i写为hM~i0，将a[ ]写为a[0]。我们也省略了类型限制中的注释和不重要时的输入前缀。最后是上标？表示本地通信，被省略。2.2动态语义过程P的自由名集合fn（P）和自由变量集合fv（P）的定义是直接的，只要我们知道前者受限制约束，后者受输入前缀约束。我们确定的流程，-绑定名称和变量。此外，假设x~和M~表示x1; ：;xk，82M1; ：;Mk，我们写作Pfx~：=M~g来表示在P中Mi对xi的避免捕获的同时替代。83求值上下文E：：=（n：W）EPjEEjPn[E]（回车）a[inb：PjQ] jb [R]›b[a[PjQ] jR]（退出）a[b[outa：PjQ] jR]›b[PjQ] ja [R]（）（输入a）（输出a）（x~）PjhM~iQ<$Pfx~：=M~gjQ（x~）aPja[hM~i“QjR]<$Pfx~：=M~gja[QjR]hM~iaPja[（x~）（STRUCT P均P0› Q 0Q 0QP›Q（CONTEXTP›QEfPg›E fQg结构同余被定义为0和j的交换幺半群，并且在以下规则(Res死亡） （（m）0 0(Path天冬氨酸）（M：M 0）：PM：（M 0：P）（重复）！P！PjP（ResRes） （m）（n）P（n）（m）Pn6=m(ResPar）（m）（PjQ）Pj（m）Q m62fn（P）（ResAmb）（m）a[P]a[（m）P]m6=a结构全等对于图1的归约关系的定义是功能性的。图1.一、减少：P›Q环境移动性由移动环境的规则（进入）和（退出）管理。通信可以是本地的，如在Mobile Ambients中，也可以跨越环境边界，在父对象和子对象之间进行。通信的规则与[4]的规则不同。归约语义的原始公式使用不同的交互模式，因为父子同步总是涉及本地前缀，如以下示例所示：n[（x）pPjp[hMiPj（x）Qjq[hNi“]（3）环境n作出向下请求，以读取p的局部值M，而环境q作出向上写入请求，以将其值N传送到其parent。利用原始语义，（x）Q的输入前缀可以与任一输出非确定性地同步相反，使用新的语义，84上述系统（3）中的交换是P和Q之间的本地交换，因为同步需要向下和向上的交换请求来新的约简仍然符合BA的设计原则，即资源局部性。环境可以被视为拥有两个通道：一个专用通道，仅可用于本地交换，以及一个“向上通道”，环境提供给其封闭上下文进行读写访问。至少有两个原因支持新语义。首先，它通过减少通信的原始语义的内在非确定性，增强了微积分的代数理论。其次，它增强了移动性的类型化，因为移动性可以独立于通信进行类型化（见下一节）。当然，也有取舍。事实上，新的约简需要一个环境来知道它的孩子的名字，以便与他们交流。这使得对某些协议进行编码变得困难，例如向所有子节点广播消息，而这些协议很容易用原始语义来表达。我们将讨论两个版本之间的相对表达能力，以备将来工作之用，并将重点放在信息流安全上。2.3静态语义BA的类型结构类似于MA的伴随类型系统[10，6]。环境类型。 与Mobile Ambients一样，Boxed Ambients也是“交流场所”。然而，Boxed Ambients允许不止一个对话的“主题”：特别地，环境的类型显示其向上对话的主题，但是它在本地和与其子环境交换的值可能具有不同的类型。更确切地说，amb[E]是其用于外部通信的信道携带类型E的值的所有环境的类型。过程类型。进程的类型被定义为两个位置的构造函数[E; F]，它跟踪具有这种类型的进程可能具有的本地（E）和向上（F）交换的类型能力类型。所有的能力都被分配了一个类型常量，标记为cap。这是可能的，而且是合理的，因为新的通信语义将环境的本地交换与任何嵌套的子环境所尝试的向上访问分开。因此，新演算中的环境移动性不受环境内交换的值的类型的约束，并且因此与通信正交。因此，我们在[4]中研究的模态类型在这里不需要，因为环境迁移率没有约束。要实现这一点，请考虑以下过程：n[（x：W）RjhMij（x：W1）pP j（y：W2）qQ jp[hN1i“] jq[hN2i“] ]上面的进程可以安全地与任何进程类型一起类型化，前提是（i）M;N1;N2 h av e类型，关于iv el y，W1，W2，（ii）p和qh av e类型amb[W1]和amb[W2]，（iii）P;Q和R具有类型[W;E]，其中E是交换类型，使得n：amb[E]。特别地，在上述过程中，在三个交换的值M;N1;N2之间 不存在 类型 混淆的 风险，因为来自孩子的读请求85它们是不同的，并且它们不干扰本地通信。图2总结了类型规则该系统满足以下基本性质：命题2.1（主语缩减）如果P：T且P <$Q，则Q：T。证据作为命题3.2的推论。23一类安全信息流在这一节中，我们丰富了BA的类型系统，以便提供静态的安全措施，防止不安全的信息流在演化的良好类型的进程。我们预先假设一个完整的安全级别格（;），并让;;范围超过安全级别。然后，我们将这个格的元素划分为两类，定义3.1 [低级别和高级别]令（;）是安全级别的完整格。 证券分类是将的划分为两个非空集合L和H，其中L是下闭的。 在此分类的基础上，我们定义了如下序：，（2L_2H）3.1类型和判断交换类型E和过程类型的定义见第2节。表达式的类型重新定义如下：表达式类型W：：=amb[; E]环境UCAP[]scap[]不安全能力安全性能每个环境类型都使用一个安全级别进行注释，该级别定义了该类型的环境名称的清除 能力类型也有一个相关的安全级别，并分为安全和不安全。特别地，ucap是危险能力的类型，这些能力是信息流的潜在来源：类型规则将确保这些能力只能在高级别环境中使用。能力类型也被标注了安全级别：环境类型的标注用于为环境分配安全级别，而能力类型的标 注 用 于 记 录 流 程 执 行 的 操 作 的 安 全 性 。 直 觉 是 ， 在 cap[]（withcap2fucap;scapg）中，是路径上能力（安全级别）的最大下限这通过以下“帽型”组成形式化. scap[]scap[]=scap[u]. ucap [] ucap []= scap [] ucap []= ucap [] sca p []= ucap [u]其中u是相对于定义3.1中引入的顺序86（ENV（ENV NAME）`a2=Dom（）？ 的（SUB PROC）E2fshh;E0g;;a：W`（P拒绝）a：W;0`;a：W;0`a：WF 2 fshh;F0 g[英;法]6[英0;法0]（SUBSUPTION）P：T T6T0‘P：T0（PATH）（IN）`M：琥珀色`inM：cap（OUT）`M：琥珀色`M1：cap`M2：cap`outM：cap（PREFIX）`M：cap`P：[E; F]`M1：M2：帽子（PAR）`P：[E; F]`Q：[E; F]`男：女：[英;法]（西北）;n：amb[G]`P：[E; F]`P j Q：[英;法]（AMB）`男：琥珀色的。``（n：amb[G]）P：[E;F]（DEAD）的M[P]：[嘘;嘘]（REPL）`P：[英;法]`0：[嘘;嘘]（INPUT）;x~：W~`P：[W~;E]`（x~：W~）P：[W~;E]（INPUT“）;x~：W~`P：[E;W~]“（x~：W~）“P：[E;W~]（INPUTM）“啊！P：[英;法]（OUTPUT）`M~：W~`P：[W~;E]`hM~iP：[W~;E]（OUTPUT“）M~：W~`P：[E;W~]`hM~i“P：[E;W~];x~：W~`P：[G;H]`（x~：W~）MP：[G;H]（OUTPUTN）`N：amb[W~]`M~：W~`P：[G;H]`hM~iNP：[G;H]图二.类型系统下一步是确定在流程通信中交换的值的安全许可。 这是由以下级别函数形 式 化 的 ：交换类型！ 安全级别，其中cap 2 fucap; scapg和？87是安全等级（amb[; E]）=（W1Wn） =tf（ W1）; ：;（ Wn）g（嘘）= （cap[ ]）=？正如我们在引言中所预期的，我们因此规定能力应该总是被认为是“低级”值，因为传递一个能力并不公开该能力中出现的名称。此外，请注意，能力的类型确实会跟踪目标环境的级别：需要此信息来检测由于使用（而不是交换）所讨论的能力而产生的信息流。类型系统是根据以下类别的判断来定义的格式良好的类型环境`E格式良好的交换类型`[E; F]级的格式良好的进程类型`M： W良好类型的表达式`（;）P：[E; F]良好类型的过程对格式良好的（交换和进程）类型的判断是功能性的，以强制数据沿着环境边界内部和跨环境边界的（匿名）通信通道安全流动在判断好类型的进程时，我们在旋转门上使用了两个注释，其含义如下：是包围P的环境的间隙（如果有的话），而是迄今为止遇到的动作的间隙的下限，它有助于定义P应该进行类型检查的间隙。为了理解类型规则的基本原理，考虑以下示例（通常，`表示低级，而h和k是高级）。. 过程“[（x）h h M i“]是不安全的，因为可观察到的M作为与高水平亚环境“交换值”的结果而被启用H. 因此，观察‘上的向上通信可以揭示‘内的高水平环境h的存在。同样的推理表明，相反，l[（x）h0 j hM i“]是一个安全过程。信息流可能产生于高层次和低层次行为的微妙组合。特别地，这样的动作不需要如上面的示例所建议的那样顺序地发生。一个隐式的信息流，也可能是运行两个并行线程的结果：. 进程“[（x）hhNiPj（y）hMi“]是不安全的，因为本地交换88前面的两个例子都表明，“安全”进程应该满足一个非常基本的不变量，即在高级同步（如（x）h）之后的“动作”必须不能用于进一步的低级同步交互。这说明了在进程类型判断中的作用。当给一个过程P加上一个换句然而，这个条件本身是不够的。. 考虑过程P=h[`[（x）kouth：0]]，其中，低电平环境`首先H. 在这种情况下，在最高级别上，环境的存在代表了依赖于私有（高级）信息的公共（低级）信息。 这是一个问题，因为在顶层测试`的存在的能力可能会隐含地向任何底层观察者揭示h的存在。 为了理解这个问题，并从非干扰的角度来表达它，我们可以将观察者编码为上下文：C（）=`1[in`：out`：hNi“]j（）。 现在，取H=k[inh：in`：hMi“0]，例行检查验证上下文将P与P j H区分开。最后一个例子表明，离开高级别位置的低级别环境可能会泄露有关该高级别位置的秘密信息这表明（i）当目标环境是高水平时，OUT能力应该被认为是不安全的，以及（ii）只有高水平环境才应该被允许行使这种能力。3.2类型规则环境与类型形成正如我们所预期的，格式良好类型的规则提供了对显式流的保护，因为它们保证了高级值只在具有更高许可的通道（或环境）上循环。这是通过要求环境a的清除率是其向上交换清除率的上限（规则类型Amb）和其包含的过程执行的交换的上限（规则类型Proc）。（ENVEMPTY）？ 的（ENV NAME）`Ta2=Dom（）;a：W`（T型 SHH）的嘘（TYPECAP）的盖[]（TYPE AMB）`E（E）`amb[ ; E]（TYPE PROC）`Ei（Ei）i = 1; 2`[E1;E2]子类型和包容子类型的关系与Section2. 包容规则要求目标类型是格式良好的，8900类型推广。（SUB PROC）0 0E2 fshh;E g; F 2 fshh;F g0 0[英;法]6[英;法]（SUBSUPTION）0 0 0 0（;）P：[E; F][E; F]6[E ;F]`[E ;F]0 0表达式`（;）P：[E ;F]正如x3.1的最后一个示例所建议的，如果n是高级别的，则应将n之外的能力视为不安全的。 另一方面，任何环境都可以安全地行使输入能力（低级别环境“进入高级别环境h”可能会创建信息流，但前提是“被允许最终退出h”）。（P拒绝）a：W;的a：W;a：W（PATH）`M1：cap[1]`M2：cap[2]（cap2fscap; ucap g）`M1：M2：cap [1]第二章[2]（IN）`M：amb[; E]`in M：scap[]过程（SAFE-OUT）`M：amb[; E]62H`out M：scap[]（UNSAFE-OUT）`M：amb[;E] 2H`out M：ucap[]根据下面的规则，我们定义了安全（;;H），（2H）_（H）：直观地说，一个过程P是安全的，如果（i）它被包含在一个高水平的环境中，或者（ii）由P执行的“动作”的间隙不随P的进展而减小。（安全-前缀）`M：scap[]`（;）P：[E;F]Safe（;;）`（;）男：女：[英;法]（不安全-前缀）`M：ucap[]`（;）P：[E;F]（2H）`（;）男：女：[英;法]安全前缀的下界为，遵循前面的直觉。例如，进程（x）hout`仅在级别2H上是良好类型的，因为它表示一个依赖于（如下所述）一个高级操作的低级操作。相反，不安全的前缀只能在高级别环境中使用：这可以防止低级别的90从高层次的环境中逃离请注意，移动性不会影响下限：这是安全的，并留下一定的移动自由（例如，h中的路径：l中的路径也可以在级别2L处执行）。以下四条规则是标准的，应该是不言自明的。（PAR）`（;）P：[E; F]`（;）Q：[E; F]`（;）PjQ：[E; F]（DEAD）`[英;法]`（;）0：[E; F]（西北）; n：amb[;G]`（;）P：[E;F]`（;）（n：amb[;G]）P：[E;F]（REPL）`（;）P：[E; F]“（;）！P：[英;法]（Amb）规则实现了将环境视为“动作”的想法 这就是为什么规则需要假设Safe（;;），就像在rule（safe-prefix）中一样。此外，M中所包含的过程在级别（M的间隙）上类型化，最初设置为最低安全级别。（AMB）`M：amb[;E]`（;？P：[F;E]`[G;H]安全（;;H）`（;）M[P]：[G; H]最后，我们来看看通信规则，它以类似于前缀规则的方式测试谓词Safe。此外，交换一个值会影响延续过程P类型化的下限。因此，当在级别2 L键入时，进程可以安全地与高级别的subambient通信，前提是所有后续操作都是高级别的。因此，例如，进程`[（x）hhxih1]和l[h`1ih Mih]是良好类型化的，而`[hMih hh`1i]不是。（INPUT）;x~：W~（OUTPUT）`（;（W~））P：[W~;E] Safe（;;（Wi））`（;）（x~：W~）P：[W~;E]M~ ：W~`（;（W~））P：[W~;E]安全的（;;（Wi））`（;）hM~iP：[W~;E]（INPUTM）`M：amb[X;W~];x~：W~ `（;）P：[E;F]Safe（;;）`（;）（x~：W~）MP：[E;F]91（OUTPUTN）`N：amb[;W~]`M~：W~`（;）P：[E;F]Safe（;;）`（;）hM~iNP：[E;F]（INPUT“）;x~：W~ `（;（W~））P：[E;W~] Safe（;;（Wi））`（;）（x~：W~）“P：[E;W~]（OUTPUT“）M~ ：W~`（;（W~））P：[E;W~]安全的（;;（Wi））`（;）hM~i“P：[E;W~]通常，类型系统的正确性由主语归约属性保证。提案3.2（受试者减少）如果P：[E;F]和P›Q，则Q：[E;F]。这是相当直接地表明，类型系统检测，并防止，所有不安全形式的显式流，在意义上的属性（？）在导言中（cf.第3页）。更有趣的是，我们可以证明不安全的隐式流也可以被检测到：这是下一节的主题。4互不干涉我们开始介绍“高级源”的概念定义4.1 [高级源]一个进程P是一个高级源当且仅当（i）`（;）P：T，对于所有的安全级别和2个H，和（i i）如果P是M：P0的形式，那么`M：cap[cap]有<$2个H。因此，高级源是良好类型的进程，其可以仅与它们被插入的任何上下文进行“高”顶层交互。这是真实的过程在前缀形式凭借条件（ii）。此外，类型规则的解释验证了任何高级源P的以下属性。首先，与P的所有顶级值交换必须是高级别的，P中的所有顶级环境事件也必须是高级别的。其次，良好类型条件确保没有低级别环境可以逃脱其封闭的高级别上下文。记法：我们以后写P：T来表示P是中的高级源。 此外，我们写`P：[E; F]和`P：ok，当 ;和/或[E; F]不相关。92nnn4.1类型等同接下来，我们引入进程等价的类型化概念等价性是类型化的，因为我们只比较具有相同类型的进程，并插入到尊重其类型的上下文中。我们将这些概念形式化如下[22]。上下文C（）是只有一个hole（）的过程项。我们用C（P）表示用P替换C（）中的空穴所产生的过程。注意，在P中自由的变量和名称可能在C（P）中被绑定。因此，我们不识别上下文，直到重命名绑定的变量和名称。定义4.2Let和be是类型环境，T是过程类型。C（）是一个（=;T）-上下文，如果`（;）C（）：okwith2L在第3节的类型系统中是可导出的，该类型系统丰富了为所有扩展导出`（）：T的规则。Integer，a（= ;T）-context是一个context，其类型为T的hole位于中记录的绑定器的范围内，其自由名和变量包含在中。.此外，上下文C（）必须在低级别类型化，即外部观察者的清除。定义4.3[倒钩]定义P#，P（m）（n[hMi“P0jQ0] jQ00）n2=fmg。进程Pe表示名称n，写作P+i，如果存在Q，使得P=）Q和Q#，其中=）是的反射闭包和传递闭包。现在，我们可以定义我们的“低”类型等价的概念在此基础上，我们有了不干涉的定义。定义4.4[类型化观察等效性和无干扰性]假设P：T和“问：T。 这两个过程是等效的，，书面. P=L Q当且仅当对于所有的（=; T）-xxtC（），其中C（P）和C（Q）闭的，对所有n，（（n））2L，C（P）+，C（Q）+n定义4.5[非干扰]设是一个安全格，P是一个进程。给定一个安全分类，使得`P：T，P对于该分类是安全的i f f。 P=LPj H对所有H使得H：T。如果P对的所有安全分类都是安全的，则它是无干扰的。我们得出结论的主要结果，一个定理，指出类型系统guarantees非干扰良好类型的进程。定理4.6（无干扰）给定任何安全分类，如果P：T和H：T，则。 P=LP j H。请注意，该定理的陈述和证明仅参考良好类型的上下文。因此，它所解决的非干扰分析对应于验证系统的n93PH高HLL低H防干扰设计借鉴了Cardelli和Gordon为Mobile Ambients [9]开发的技术工具，使其适应我们的Boxed Ambients。无干扰的结果来自一个引理，表明高电平源是低电平等效于非活动过程。 更确切地说，我们证明了对于每个上下文C（）和高级源H，如果C（H）是良类型的，那么它在低级时与C（0）是不可区分的。要证明这一结果，需要对过程和周围环境之间所有可能的交互进行表征4.2讨论我们定义的用于派生非干扰证明的类型系统确实有些限制性。虽然这是不幸的，但我们对高级和低级进程之间的交互作用施加的纪律具有与在更简单的进程演算[16]和多线程语言[26，24，1]中的安全信息流的现有类型系统中发现的效果相当的效果第5节详细比较）。此外，即使良好类型化的流程在它们可能执行的操作中受到约束，类型系统仍然允许高级别和低级别之间的非平凡形式的交互，无论是在移动性方面还是在价值交换方面。图3显示了当H是一个高级源时，两个进程P和H的良好类型组合的合法信息流图3.第三章。PjH的信息流特别地，类型系统所实现的流是（i）从H到P的高级子过程的流（反之亦然），以及（ii）从P的高级组件到P的低级组件的流，这些组件由于被高级环境屏蔽而不可观察因此，低级观察者可以仅观察P的低级成分与周围上下文的低级成分之间的信息流还要注意，高级信息可以在P的高级和低级进程之间自由交换，只要后者嵌套在高级进程中。94氛围这是因为类型系统确保了这些低级子过程被限制在高级环境中。在MobileAmbients的演算中，类似的属性将更难实施。这是因为开放能力代表了上下文可能强加给流程的客观动作 要看到这一结果，请注意，为了证明我们在MA中的非干扰定理，应该针对所有与P并行出现的高级进程检查进程P，特别是针对所有高级名称h的高级进程open h：0。 这意味着h[P]形式的进程，其中P是低级别的，应该被类型系统拒绝为不安全的。为了更进一步，考虑过程P= h[`[P0]]，对于任何P0，分别具有h和`高级别和低级别名称。 该过程不是无干扰的，因为`1[in`：out`：hMi“]j（）可以区分P和P j open h：0。类似的推理适用于过程h[in `：P j Q]和h[out l：P j Q]，并且通常适用于任何过程h[P 0]，其中P 0是低级过程。所有这些过程都是良好类型的，并且在我们的演算中没有干扰，在附加的假设下，P0的低级组件不试图逃离h。作为进一步的评论，我们注意到，不干涉的证明不会在存在更精细的等价关系的情况下进行，例如倒刺聚集、互模拟或必须测试。要查看带刺全等的问题，请考虑定义L作为由我们的B-V-V能力谓词P#n。然后，对过程P= [hMijinh：0]和“高层次过程H= h[]。现在取上下文C（）=（），并观察到C（Pj H）<$R= h[`[hMi“]]，而不存在进程R0，使得C（P）›R0和RLR0。5相关工作Volpano和Smith [26，24，25]以及最近的Boudol和Castellani [1]研究了基于类型的技术，以在多线程命令式语言中实施非干扰在他们的方法中，显式流是通过对变量作为-循环施加约束来防止的，而对条件命令和while循环的额外限制则排除了隐式流。在[1]中，作者指出引入并行性可能会引起新的问题，因为信息流可能“伪装成控制流”，程序在执行过程中可能会观察到其他并发组件的行为（并受其影响）。这个问题在[25，1]中通过依赖于一种形式的递归来解决，即咨询高级变量的值后不能再分配给低级变量。 在BA中，即使在不同的设置中，我们也有类似的问题，并且我们的解决方案遵循相同的基本原理，通过对过程执行的“动作”序列施加非递减的间隙与我们更直接相关的是Honda等人[17]的-演算的类型系统和Hennessy和Riely [16]的安全演算的在[17]中，95作者建议使用因果依赖的非正式原则来理解各种编程语言中的信息流的安全性，并基于类型的行为概念来开发类型系统以捕获动作的因果关系。我们的方法是类似的，因为它也借鉴了因果依赖的原则，但我们的框架似乎更复杂，因为在BA过程中可能会通过通信和移动性进行交互。在[16]中，安全级别被附加到进程和读/写通道的能力，并且通过键入强制执行“不读/不写”安全策略。为了证明不干涉，必须施加进一步的限制，即高级过程不能在低级过程中演化，演算必须是异步的。在这些假设下，作者表明，良好类型的异步过程是无干扰的，其中非干扰的定义方式类似于我们的，基于可能的测试等价。我们的类型系统对高进程和低进程之间的价值交换实施了类似的限制，并对移动性实施了相应的限制。与[16]不同，我们的结果对同步情况也成立。在[15]中，Hennessy为安全演算开发了一个增强型系统，对于该系统，也可以证明关于必须测试等价性的非干扰性。在[23]中，Sewell和Vitek介绍了Box-，一种进程演算，提供了组成（部分可信）软件组件和强制执行信息流安全策略的机制。他们的方法是基于彩色语义，它用过去影响它们（进程）的主体集合来注释输出进程;然后用彩色lts来声明安全属性。最后，他们引入了一个静态捕获因果流的类型系统。因此，信息流安全的表征是基于因果模型，而不是在我们的方法中的非干扰。更重要的区别是box-的异步语义（与BA的同步语义相反）以及我们对移动性和嵌套拓扑的处理。值得对这两种方法进行更深入的比较。没有基于类型的非干扰研究似乎已经进行了基于环境的结石。相反，一些文件涉及安全的其他方面。Cardelli等人提出了一个基于组名概念的Mobile Ambients类型系统[7]，它静态地防止了不必要的名称传播Levi和Sangiorgi [18]为Safe Ambients设计的打字系统提供了对环境交互的更精细控制，并防止了“严重干扰”。Dezani和Salvo在[12]中为Mobile Ambients开发了一个类型系统，其中环境类型以类似于我们的方式与安全级别相关联，并且安全检查是开放和移动的。基于类型系统[3]和控制流分析的其他方法也被应用[21，20]来分析（各种方言）移动环境的不同安全属性。特别是Braghin等人。[2]通过定义控制流分析来检测机密数据在任何移动环境之外移动时产生的安全漏洞，从而研究