BANANA: 移动环境下的安全分析工具

理论计算机科学电子笔记99（2004）319-337www.elsevier.com/locate/entcsBANANA背后：移动环境C. Braghina，1，A.Cortesia，2，R.Focardia，3，F.L. Lucciob，4，和C。Piazzaa，5aDipartimmodInformatica，Uiversita`CabDipartimentodiScienzeMatemiche，Universita`diTrieste摘要我们提出了一个调查的工作控制流分析进行的威尼斯队在Me菲斯托项目。我们研究的安全问题，特别是信息泄漏检测，在移动环境演算的上下文中。我们描述BANANA，一个基于Java的环境嵌套分析工具，通过专注于分析精度和算法优化。关键词：静态分析，环境演算，安全。1介绍近年来，网络已经成为我们日常计算环境的一个重要方面在这样的框架中，可以以不同的方式支持移动性。*部分得到MIUR项目“Modelli formali per la sicurezza ” 、 EU Con-t rac t I S T-2001 - 32617“M y T h S“ 和 F I R B p r o j t（ R B A U 018 R C Z ） “I n t e r p r e t az i o n e astratta e model checking perla verifica di sistemi embedded”的支持。1电子邮件：braghin@dsi.unive.it2 电子邮件地址：cortesi@dsi.unive.it3电子邮件：focardi@dsi.unive.it4电子邮件：luccio@dsm.univ.trieste.it5电子邮件：piazza@dsi.unive.it1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.014320C. Braghin等人/ Electronic Notes in Theoretical Computer Science 99（2004）319-形式：物理，例如，膝上型计算机、四处移动的个人记事本、进入网络计算机插槽的智能卡，以及逻辑的，例如，代码或代理移动性。在这种情况下，主要的科学和技术挑战是为在不受信任和可能未知的环境中运行的应用程序提供安全性实际上，分布式应用程序依赖于网络通信，因此，除了成为计算机病毒的潜在受害者之外，它们还可以以许多方式被篡改和窃听，并且由于这个原因，它们是脆弱和不安全的。一般来说，移动代码和通信可能需要跨越管理域和防火墙，以及不受信任的站点。诸如密码学之类的技术可以解决与数据通信有关的一些问题，但是，当交换可执行代码时，这样的技术可能不再足够。许多研究都致力于保护服务器免受不可信和潜在恶意的移动代码的攻击。相反，必须保护移动代码免受可能试图公开或修改其敏感私有数据的潜在恶意服务器的攻击。这些安全问题构成了一个非常有趣的工作台来评估静态分析技术的理论和实际影响。给出一种静态验证安全属性的方法，原则上，具有使属性检查更有效的优点;此外，它允许我们编写通过构造而安全的程序，例如，当所执行的分析被证明暗示某些行为安全属性时。大量的研究是可用的，依赖于不同的静态技术和建模语言，验证不同的安全属性[3，14，16，25]。在本文中，我们提出了一个调查的工作控制流分析进行的威尼斯队在Me菲斯托项目。我们的目标是双重的：一方面，解决移动代码的信息流安全与控制流分析技术，另一方面，优化我们和现有的方法的时间和我们的方法基于Cardelli和Gordon [11]提出的移动环境（MA）的演算，其中环境的概念捕获了广域网、移动计算和移动计算的结构和属性。环境是代理和位置概念的抽象。与智能体一样，环境可以通过利用其能力来移动。此外，环境可以任意嵌套，形成一个树形结构，对管理域的分层组织进行为了在一个抽象的方式来研究这个问题，我们考虑的这样，我们可以研究一个非常一般的信息流概念，我们认为，它也应该适用于更“具体”的信息C. Braghin等人/ Electronic Notes in Theoretical Computer Science 99（2004）319-321微积分[9，17]。我们的重点是多级安全，一个特定的强制访问控制安全策略：每个实体都绑定到一个安全级别（为简单起见，我们只考虑两个级别：高和低），信息只能从低级别向高级别流动。通常，施加两个访问规则（i）No Read Up，低级实体不能访问高级实体的信息;（ii）No Write Down，高级实体不能向低级实体泄漏信息。为了检测信息泄漏，典型的方法（参见，例如，[1，2]）直接定义了信息如何从一个层次流到另一个层次。然后，验证在任何系统执行中，是否不可能从高电平向低电平传输信息是足够的。我们采取了上述做法。我们研究的出发点是Niel-son等人在[ 15 ]中提出的控制流分析。在[7]中，我们改进了这种分析，以检测信息泄漏。这两种分析都已在B anana（边界环境嵌套分析）工具[4]中实现，该工具是一个Java小程序，可在http://www.dsi.unive.it/mefisto/BANANA/上获得。本调查将描述该工具中实现的分析的技术细节，以及B anana背后的实现问题。本文的其余部分组织如下。在第2节中，我们介绍了移动环境演算的基本术语，并简要报告了[15，20]和[6，7]的控制流程分析。然后，在第3节中，我们介绍了在Banana工具中实现的算法，这将在第4节中详细描述。第五节是论文的2移动环境在本节中，我们首先介绍了移动环境演算的基本术语，然后我们简要报告了[15，20]的控制流分析及其在[6，7]中提出的改进。2.1移动环境移动环境演算已经在[10，11]中引入，其主要目的是显式建模移动性。事实上，环境是任意嵌套的边界，可以通过适当的功能四处移动。进程的语法如下所示，其中n∈Amb表示环境名称。直观地说，限制（νn）P引入了新名称n，并将其作用域限制为P;进程0不做任何事情; P|Q是P和Q并行运行;复制提供了递归和迭代，如！P表示任意数量的322C. Braghin等人/ Electronic Notes in Theoretical Computer Science 99（2004）319-P，Q ：：=（νn）P限制|0不活动|P|Q组合物|！P复制|一nl[P]环境|不在洛杉矶，P进入的能力|不出岛P退出的能力|不开放岛 P打开的能力Fig. 1.移动环境平行的P。通过nla[P]我们将环境命名为n，进程P在其中运行ltn和ltn外的能力移动它们的分别将环境包围在环境n中和打开ltn用于溶解兄弟环境n的边界。业务进程P的语义通过进程之间的适当的归约关系→给出。直觉上，P→Q表示P通过某种计算还原为Q的可能性。(See[10]更多详情。我们将使用标准符号P→Q来表示过程P到过程Q的约简，该约简在0个或多个步骤中执行。引入了环境上的标签la∈Laba和能力（transi- tions）上的标签lt∈Labt，因为在静态分析中习惯于指示我们用Lab表示所有标签LabaLabt的集合。我们使用特殊标签env∈Laba来表示外部环境，即，包含观察过程的环境。给定一个进程P，我们还引入符号Laba（P）来表示P中的环境标签集加上特殊标签env，Labt（P）表示P中的能力标签集，Lab（P）表示Laba（P）Labt（P）。此外，Na=|实验室a（P）|，Nt=|实验室t（P）|，且N实验室=|实验室（P）|= Na+ Nt。我们用N表示出现在P中的算子的全局个数。 请注意，NLab（la，lJ）∈I<$）JJ=<$（la，lJ）∈I<$图三. 控制流分析这个过程是一个pair（I，H）的封闭条件，它依赖于在进程P上可执行的所有可能的移动。除了open、in和out这三个功能之外，它主要依赖于子进程上的递归调用。例如，开放能力的规则规定，如果标记为la的某个环境在环境n上具有开放能力lt，则由于存在的兄弟环境标记为laJ，其名称为n，则执行这种能力也应记录在清单中，即，嵌套在LA中的所有环境/能力必须也嵌套在LA中。例2.5再次考虑例2.4的过程P3. 请注意，它可能进化到一第1页[ 0 ]|一[ 0]. 很容易证明P3的最小解是其中I={（en v，la），（env，la），（l a，l a），（la，lt）}，H={（la，n），（la，m）}.1212212注意，分析通过对（env，la）正确地捕获了m从n退出的可能性。Q分析的正确性证明了每一个减少的语义是正确的模仿分析，±表示组件明智的集合包含。326C. Braghin等人/ Electronic Notes in Theoretical Computer Science 99（2004）319-envenv122Theorem2.6[1 5]LetPeaprocess. If（I，H）|=CFP和βCF（P）±（I，H）和P→βCF（PJ）±（I，H）.2.3边界环境嵌套分析上一节中的分析不是面向安全的，因此它没有利用关于边界内“安全”嵌套的信息。在[6，7]中，我们提出了一个更精确的抽象域，它分别考虑安全边界内外的嵌套，从而产生一个更复杂的控制流分析，用于检测不需要的边界交叉，即，信息泄露其主要思想是区分嵌套，受边界保护或不受边界保护。更具体地说，组件将一个域的一部分分割为两个（不需要一个完整的连接）集， 和I代表受保护和不受保护的嵌套，R代表受保护，B代表边界，E代表外部环境。因此，重新定义分析的结果是由三元组t（IB，IE，H）的平均值s表示的。同样在这种情况下，分析是由一个表示函数和一个参数定义的。所述表示函数集合在I_B（I_E）中包括最初（未）包含在至少一个边界环境中的所有环境的集合例2.7再次考虑例2.4的过程P3，即， 的形式：P=lalaltaaaa3n1[m2[outn] ]，其中l1∈LabB（P）且l2∈LabL（P），因此P的表示函数如下：β B（P）=（{（la，la），（la，lt）}，环境1 2 2{（env，la）}，{（la，n），（la，m）}）。表示函数正确地捕获了1 1 2边界环境N保护他的所有子环境和能力，即，，b（la，la）和d（la，lt）记录在图IB中。Q我们没有报告整个分析质量标准（更多详细信息见[6，7]相反，我们通过考虑，例如，输出能力（见图4）。在分析的规范中，谓词路径B（la，l）用于简化符号。直观地，它表示从标记为la的环境到标记为l的环境的嵌套的受保护路径，其中没有环境是边界。输出能力的规则规定，如果标记为la的某个环境在环境n上具有输出能力lt，则由于存在标记为laJ，其名称为n，则执行该功能的结果也应该根据新生成的嵌套的优先级，在I/B或I/E中该规则分为三种不同的情况：（i）环境退出边界，从而移动到未受保护的环境，（ii）所有环境都受到保护，最后（iii）所有环境都不受保护。在在第一种情况下，从移动的环境层到新的保护层的所有嵌套都必须在嵌套中复制，因为在移动的过程中，C. Braghin等人/ Electronic Notes in Theoretical Computer Science 99（2004）319-327env1env2212不（out） （IB，IE，H）|=Bouttn. Pi（IB，IE，H）|=BPl，l，l∈Lab（P）：case（（la，lt）∈I<$B <$（la，la）∈I<$E<$I<$B<$（la，la）∈I<$E'<$（la，n）∈H< $）=<$一 一个'a"一'""如果（l∈Lab（P）），则（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'""''''""'''不受保护 in和open-capabilities的行为类似.图四、细化控制流分析的规范--排除规则例2.8设P为例2.7的过程。P的最小解是三元组t（IB，IE，H），其中IB={（la，la），（la，lt）}，IE={（env，la），（env，la），（la，lt）}，并且ndHn={（la，n），（la，m）}。Q2 1 2现在我们得到定理2.6的一个推广：Theorem2.9LetPeeaprocess.If（IB，IE，H）|=BP和βB（P）±（I<$B，I<$E，H<$）和P→ P <$PJ，则nβB（PJ）±（I<$B，I<$E，H<$）.正如预期的那样，分析结果应该以信息流的形式阅读。如果在分析中h（高级别数据）不出现在以下中的任何一个中，则在边界环境之外的秘密数据/环境不可能两人都渴望着去见上帝。推论2.10设P是一个进程，h∈Laba（P）是一个高级标号。让B日本语HJJJ吉吉βenv（P）±（IB，IE，H）和（IB，IE，H）|=P不会泄漏秘密H。P和<$（l，l）∈IE，lH. 然后，例2.11例如，考虑例2.2的过程P2的进一步改进。在这种情况下，高级数据愿意进入某个翻译器进程，该进程可能是来自外部的低级代码环境威尼斯b1[信封b2 [出口c1威尼斯。在C2比萨。0|hdatah[ inc3translator . 0]|pisab3 [打开c4信封。0个字符]|翻译员m[装于c5信封内。0个字符]|打开C6翻译器。 0在这种情况下，翻译器关于信息泄漏正确地工作，即，它只会进入边界。特别是，这意味着它永远不会携带328C. Braghin等人/ Electronic Notes in Theoretical Computer Science 99（2004）319-安全边界之外的高级别数据。然而，如果我们计算[15]的CFA，我们得到以下最小解：I={（env，b1），（env，b2），（env，h），（env，b3），（env，m），（env，c5），（env，c6），（b1， b2），（b2，h），（b2，m），（b2， c1），（b2， c2），（h，c3），（b3，b2），（b3，h），（b3， b3），（b3，m），（b3，c 1），（b3，c 2），（b3，c 4），（m，h），（m，c5）}H={（b1，venice），（b2，envelope），（b3，pisa），（h，hdata），（m，translatorr）}请注意，（env，h）对出现在I中，即使没有导致这种情况的执行。另一方面，细化分析正确地捕捉到了这样一个事实，即转换器只在边界pisa内部被机密数据hdata输入一次，并且它永远不会离开它，即，h只出现在受保护的嵌套的I/B中。I∈B={（b1，b2），（b2，h），（b2，m），（b2，c1），（b2，c2），（h，c3），（b3，b2），（b3，h），（b3，b3），（b3，m），（b3，c 1），（b3，c 2），（b3，c 4），（m，h），（m，c5）}I={（env，b1），（env，b2），（env，b3），（env，m），（env，c5），（env，c6），（m，c5）}H={（b1，venice），（b2，envelope），（b3，pisa），（h，hdata），（m，translatorr）}因此，边界分析比[15]中的边界分析严格更精确Q3嵌套分析在本节中，我们描述了到目前为止所描述的分析的不同实现，这些分析是Banana工具的核心3.1控制流分析像[7，15，20]这样的环境嵌套分析的计算需要相当高的复杂度，因此设计高效的技术非常重要。这是尼尔森和塞德尔在[23]中提出的工作背后的第一个动机。假设N是进程的大小，作者提出了两种不同的算法，分别在O（N4）和O（N3该算法首先将控制流分析约束转换为Horn子句。然后，通过满足性标准算法[12]处理这些子句，以计算最小解。由于此类算法总是考虑与分析约束相对应的所有基础子句，因此即使在最好的情况下，也需要生成所有子句。在文献[5]中，我们介绍了两个新的算法，它们改进了Nielson和Seidl提出的技术的时间和空间复杂度。空间C. Braghin等人/ Electronic Notes in Theoretical Computer Science 99（2004）319-329env这两种算法的复杂度分别为O（N4logN）和O（N3logN）bits，而我们的算法的复杂度为O（N2logN）bits.关于时间，最坏情况的复杂度是相同的顺序，即，时间复杂度分别为O（N4）和O（N3在Nielson和Seidl技术中，这些复杂性是紧密的，因为需要生成所有的基础Horn子句，如上所述。相反，我们的方案对于某些特定的小解决方案（例如，这两个问题的复杂度分别为O（N3）和O（N2这些改进首先通过增强数据结构表示来实现。然后，我们用直接的操作方法来解决问题，即，而不需要通过霍恩公式。最后，我们将计算减少到控制流分析约束，这些约束是获得最小解所必需的。事实上，算法以一种非线性的方式动态地选择仅对于分析的计算有效地必要的约束。这意味着不会发生无用的重复，也不需要像Nielson和Seidel方法那样在内存中表示所有可能的约束现在让我们简单地描述一下我们的O（N4）算法，称为算法1，并在图5中示出。该算法开始于一个空的分析I和一组缓冲器，其中包含与初始过程表示对应的所有对。回想一下，为了分析的正确性，在最后的I中应该包含对。在每一轮中，从缓冲器中提取一对，并将其添加到溶液中。然后仅考虑被提取的对潜在地“激活”的约束，即，只有在前提中有这样一个元素的约束。然后将这些约束所需的所有对插入到缓冲器中，以便最终将它们添加到解决方案中。这是重复的，直到达到一个固定点，即，直到约束所需的所有元素都在解中。在这种按需生成中最重要的成分是使用缓冲器和矩阵，该矩阵允许使用缓冲器中的每对标签仅一次以生成新的标签对。现在让我们更详细地分析算法1。我们假设进程的解析已经完成，生成了一个长度为Nt的数组帽，包含了输入进程的所有功能比如说，cap[i]可以包含以n为目标。 7在解析过程中，计算表示βCF（P），给出两个初始集合I0和H0，它们被分解为一个nNa×NL ab比特矩阵。这里n表示整数1≤n≤N a，对应于第n个环境名称.名称和整数之间的对应关系保存在解析时生成的符号表中。330C. Braghin等人/ Electronic Notes in Theoretical Computer Science 99（2004）319-我我很高兴！=NILdo（l，lcasecap [i] of：in≠tn：if（l对于k：= 1到N，if（MI[k，l]anddMI[k，j]anddMH[j，n]）thenpushcI（j，l）else if（lif（MI[l，j]anddMH[j，n]）thennpushhcI（j，l如果（ltHif（MIn[j，l]andMIn[l，j]）npushhcIn（如果n：i∈对于k：= 1到N，if（MI[j，l]anddMI[k，j]anddMH[j，n]），则n推hcI（k，l）否则，如果（lI HifMIn[j，l]thenpushhcIn（j，l如果（ltHif（MIn[j，l]andMIn[opentn：if（l对于k：= 1至N，实验室做if（MI[l，j]anddMI[j，k]anddMH[j，n]），否则，如果（lI HifMIn[如果（ltHif（MI[j，l]andMI[j，l]），则n为pushhcI（j，l图五. 算法1B_I_n，并定义为一个N_a×N位矩阵M_H_n，是正确的。 通过两次调用P，我们可以以这样的方式构建BI索引，即从1到Na的列由环境标签索引，而其他列由您的能力索引。 在I/O中的所有对都被存储在一个缓冲区中，其中应用了使用操作pushI/O（1，1 '）和pop I/O（）。利用矩阵B检验，有效地检验了一个元素是否被插入到bufI中，从而保证了一个元素被插入到bufI中的次数不超过一次。具体地，如果B1 [1，1 ']=假，则新命令pushcI（1，1'）适用，并且它既执行push c I（1，1 '）又将B1 [1，1']设置为真。最后，我们初始化另一个大小为Na×NL ab的可扩展I，它将包含分析的最终结果。 此外，在MI中，从1到Na的列由环境标签索引，从Na+ 1到NLab的列由能力索引标签这个初始化阶段只需要O（N）步，因为对P的两次解析是足够的。例3.1设P为[10，11]的防火墙访问过程，其中代理通过先前安排的密码k，kJ和kJJ穿过防火墙C. Braghin等人/ Electronic Notes in Theoretical Computer Science 99（2004）319-331(see[22]详细分析与此示例相关的安全问题）：P =（νw）wa1[ka2[ outt1w. 在t2kJ. 在t3w. 0个字符]|打开t4kJ。打开T5KJJ。0个字符]|kJa3[open t6k. [ 0][0]如使用图3中所示的控制流分析的规范计算的P的最小解是对（I，H），其中：I={（env，a1），（env，a2），（env，a3），（a1，a 1），（a1，a2），（a1，a 3），（a1，a 4），（a1，t 1），（a1，t 2），（a1，t 3），（a1，t 4），（a1，t 5），（a1，t 6），（a2，t 1），（a2，t 2），（a2，t 3），（a3， a1），（a3， a2），（a3， a3），（a3， a4），（a3， t1），（a3， t2），（a3， t3），（a3， t6）}，H_n={（a1，w），（a2，k），（a3，kJ），（a4，kJJ）}.让我们看看算法1如何应用于过程P。在这种情况下，Na= 5且Nt=6，husBI和MI是5×11位的矩阵，MH是5×5位的it矩阵x，并且可以是长度为6的数组，初始化为cutoutt1w，int2kJ，int3w，opent4kJ，opent5kJJ，打开t6k 在初始解析之后，M中被设定为JJJHtrue是{（a1，w），（a2，k），（a3，k），（a4，k）}，而bufI和BI包含对（env，a1），（env，a3），（a1，a 2），（a3，a 4），（a1，t 4），（a1，t 5），（a2，t 1），（a2，t 2），（a2，t3），（a3，t6）n.设对（env，a1）是bufI的顶元素。while-l o oop的前6轮将从bufIpair到MIpair（没有执行pu s h）。第七轮• bufI=（a2，t1），（a2，t2），（a2，t3），（a3，t6）• MI=（env，a1），（env，a3），（a1，a2），（a3，a4），（a1，t4），（a1，t5）• BI=A（env，a1），（env，a3），（a1，a2），（a3，a4），（a1，t4），（a1，t5），（a2，t1），（a2，t2），（a2，t3），（a3，t6）n.我们提取bufI的顶部元素（a2，t 1），因此l：=a 2，l我们展示了第一次迭代，i= 1，其中cap[1]是因此，我们有ln=w。由于l 唯一使if条件为真的情况是j =a 1且k =env。以来（a1，w）∈MH∞，b（a1，a2）和（env，a1）在MH∞中，对（env，a2）是pushed inbufI（注意它还没有在BI中）。该算法在第24轮之后结束，此时buf_I_n为空。Q更多的细节可以在[5]中找到，其中我们还提出了一种改进的算法，称为算法2，基于图3中描述的分析的优化。由于篇幅原因，我们省略了它的描述。332C. Braghin等人/ Electronic Notes in Theoretical Computer Science 99（2004）319-BL3.2边界环境嵌套分析在2.3节中，我们用表示和具体化函数描述了分析。可以证明这种分析的最小解总是存在的，它可以按如下方式计算：首先将表示函数应用于过程P，然后应用分析来验证所提出的解的正确性，如果需要的话，向三元组添加新的信息，直到达到固定点。迭代过程计算与迭代顺序无关的最小解。3.3移动环境可以进一步增强“边界环境”的概念更具体地说，在[8]中，我们考虑了一个过程P，其中只有高级别的数据是已知的（即，实验室H是固定的），分析的目的是检测“不受信任的”环境中的哪些环境这个问题可以通过重新执行第2.3节的边界环境嵌套分析来妥善解决。一个成功的分析推断边界环境，直到达到一个固定点，返回一组应该“保护”的环境该算法如图6所示。它从初始标号L0开始分析过程P.它可能会成功（在这种情况下，达到一个标签Lk，它完全满足我们感兴趣的安全属性），也可能会失败。后一种情况仅仅意味着我们的分析不能保证进程P该分析目前使用简单的定点算法实现，但我们正在努力将第3.1节中提出的优化扩展到嵌套分析。例3.2考虑例2.2的过程P2：威尼斯x[信封y[出口c]威尼斯。 在c比萨] |hdatah[在c信封中]]|| 开C信封• 给定P中的高级标签LabH的集合，初始标签划分0 0L0计算。L0=（LabH={h}，Lab={x}，Lab={y，z}）C. Braghin等人/ Electronic Notes in Theoretical Computer Science 99（2004）319-333BBLBLBE边界推断算法输入：一个进程P和一个分区L0.(i) 使用输入P和标签Li计算嵌套分析。(ii) 在定点算法的执行期间，每当高水平环境nl abelledhgetsintoanunp rotedenvronme nt，即，l：（l，h）∈I1. 如果（env，h）∈I_E，则在具有f_i_e的情况下，分析结果不能推断出保证不存在信息泄漏的令人满意的标记;2. 如果（env，h）/∈I∈E，则我们可以得到：– 应考虑一个新的标号Li+1，对每个l进行标号，使得（l，h）∈I∈Eabound ary。 LetL={l|（l，h）∈I<$E}则Li+1=（实验室H、实验室i L}，Labi\{L}）。L– （1）i=i+1。见图6。 边界推理算法• 将表示函数βL0应用于P，则返回三重t（Io，Io，H）：B En={（x，y），（x，h），（y，c），（h，c）}C={（env，x），（env，z），（z，c）}H={（h，hdata），（x，venice），（y，envelope），（z，pisa）}执行Fix-P算法时，pair（y，h）是在进程P执行过程中，环境包络离开环境包络，从而在进程P执行过程中，在进程P执行过程中，环境包络离开环境包络，从而在进程P执行过程中，环境包络离开环境包络。• 此时，应考虑新的标签分区1 1L1=（Lab（P）H={h}，Lab={x，y}，Lab={z}）又是一次。在它的执行过程中，对（z，h）∈I∈E，在执行过程P期间，包含机密数据的边界包络在低环境PISA内打开的事实。• 此时，考虑以下新标签划分2 2L2=（Lab（P）H={h}，Lab={x，y，z}，Lab= λ）再次计算定点算法，最终达到定点因此，应该被标记为边界的环境的集合是{venice，envelope，pisa}。Q4工具概述前面部分中描述的控制流分析算法已经在Banana（边界环境嵌套分析）工具中实现，我我334C. Braghin等人/ Electronic Notes in Theoretical Computer Science 99（2004）319-编辑解析分析输出编辑器文本编辑器安全性标记解析器开始Proc词法分析器分析Nielson定点计算统计ProcparProc数据结构语法检查器AmbProcAmbProc分析结果图形编辑器移动环境过程Ident[过程]识别[过程]安全性标记安全标签检查威尼斯NullProcWarsawNullProcBraghin等人定点计算后处理安全结果00语法树a Java applet，可在http://www.dsi.unive.it/mefisto/BANANA/获得。Banana的主要成分可以概括如下：• Mobile Ambients的文本和图形编辑器，通过以非常用户友好的方式设置环境嵌套功能和安全属性来指定和修改流程。• 一个语法分析器，用于检查语法错误并从Mobile Ambient进程中构建语法树。• 一种分析器，用于计算运行时所有可能嵌套的过近似值。该工具支持三种不同的控制流分析，即Nielson等人在[15]中的分析、Braghin等人在[6]中的分析（在工具中称为Focardi Cortesi Braghin）以及Braghin等人在[8]中的分析（FCB边界推断）。[15]中描述的分析的五种不同实现在该工具中可用它们对应于：- 图3中约束的最小解的定点计算（在工具中称为Nielson）8;- Nielson和Siedl的优化算法（Nielson Optimized）的约束的最小解的定点计算;- 图5的算法1（缓冲边界分析，B.B.A. v1）;- [ 5 ]的算法2（B.B.A. v2）;- [ 5 ]中的算法2和一些代码优化（B.B.A. v2优化）。• 后处理模块，根据[6]中提出的基于边界的信息流模型解释分析结果，其中信息流对应于高级别（即，秘密的）环境（即，边界）环境，朝向低水平（即，不信任）环境。• 一个详细的输出窗口，报告后处理模块获得的分析和安全结果，以及有关所执行分析的计算成本的见图7。 Banana工具的概述这个算法的时间复杂度是O（N），所以这个算法的时间复杂度是O（N）。C. Braghin等人/ Electronic Notes in Theoretical Computer Scien