网址：http://www.elsevier.nl/locate/entcs/volume54.html12页烟囱检测Massimo Bartoletti，Pierpaolo Degano，GianLuigiFerrariDiartimentodiInformatica-Universita`diPisa，Italy电子邮件：{bartolet，degano，giangi}@ di.unipi.it摘要我们提出了两个控制流分析的Java字节码。它们安全地近似于在运行时授予/拒绝代码的权限集这种静态信息有助于优化堆栈检查算法的实现1介绍Java平台的一个主要创新涉及其安全方法：该语言配备了用于表达和实施安全策略的结构和机制。由于实际执行的代码是以中间面向对象语言的形式出现的在过去的几年里，在开发Java字节码验证器的正式模型方面有相当大的进展。一些作者表明，字节码验证的问题可以在静态时使用类型系统形式化地理解和描述[3，4，14]。所有的建议被证明是enjoy类型的健全性属性（在字节码片段，他们认为）。此外，类型推断算法可以转换为正确的字节码验证器，参见例如。[2，5，10]。Java安全体系结构的另一个关键方面是动态检查授予运行代码的权限。粗略地说，我们必须确保无论何时主体调用某个方法，它都有权限到.在运行时，通过堆栈检查强制执行权限：如果权限属于调用堆栈上的所有主体，则授予该权限。一个例外是所谓的特权操作，允许它们执行授予其主体的任何代码，而不管调用序列如何。由于栈帧的分析可能是昂贵的，由于栈检查的运行时间开销可能会增长得非常高：因此，改进和优化栈检查的有效技术是有序的。在本文中，我们开发了一个静态分析，提高了运行时检查的权限。我们减少了要检查的帧的数量，同时保持了普通堆栈检查算法的相同精度。还有，2001年由ElsevierScienceB出版。 诉 在CCBY-NC-ND许可下开放访问。2∈∈∈∈{\displaystyle{\mathbb}我们的分析可以用于通过将检查移动到实际需要它们的地方以及通过去除冗余的检查来优化字节码。我们的方法基于控制流分析（CFA）[9]，这是一种静态技术，用于预测程序对象在执行期间可能假设的值集的安全和可计算近似值。这些近似值然后用于以安全的方式分析程序的属性：如果一个属性在静态时有效，那么它将在运行时始终有效。反之可能不正确：分析可能“偏于安全”。 CFA和其他静态程序分析技术通常比程序验证更有效，因此更近似，因为重点是大型程序的全自动处理我们的主要技术贡献是制定了一对夫妇的控制流程分析Java程序的抽象表示。这种抽象表示专门化了通常的调用图，专注于权限检查和方法调用（和保护域），类似于[8]。 调用图被赋予操作语义。本质上，程序可以通过的状态由堆栈σ表示，由调用图的节点组成，每个都被解释为实际堆栈帧的抽象。控制点是栈σ：n的顶部n，并且计算步骤由下式表示：堆栈之间的过渡，写为σ<$σJ。对于每个节点n，我们的第一个分析计算一个近似值，即在每次运行中被拒绝的权限的子集δ（n），导致n.类似地，我们的第二个分析计算了在每次运行到n时授予n的权限的子集γ（n）。 这两种分析在操作语义上都是正确的。 假设n是权限的安全检查P，而Pδ（n）（resp. Pγ（n））。 每当有一个人，tation [] v. σ：n，安全检查总是失败（相应地，成功）。然后，我们的分析计算的近似值用于减少堆栈检查算法停止的深度。当检查权限P时，它可能到达一个框架m，使得Pδ（m）或P γ（m）。 在第一种情况下，会引发一个ControlException，而在第二种情况下，检查成功。2程序模型我们表示字节码程序为导向图，只有安全检查和控制流程明确。在此基础上，我们进行了分析。调用图是三元组G=（N，E，S），其中：• N是节点的集合，包括一个可区分的元素N。 每个节点n NN与标签l（n）相关联，标签l（n）描述由节点表示的控制流原语。标签产生了三种节点：调用节点，代表方法调用;返回节点，代表从方法返回;检查节点，执行访问控制3⊥⊥ ∈⊥►我们的团队{\displaystyle{\mathbb}政策粗略地说，我们可以认为标记为check（P）的节点具有与Java语言中的CockController.checkPermission（P）指令相同的含义特殊节点N扮演着一个单一的、孤立的入口点的技术角色。• E=E callE transE entry<$N×（N\ {<$N}）是边的集合。 边缘被分割成调用边n−→nJ∈ E call，建模过程间流，以及转移边n−−·nJ∈ E transs，其对应于过程内流。此外，我们有入口边的集合·−→n ∈ E入口，包含所有对（N，n），对于n S。N元素只出现在入口边缘。• S NN 是入口节点的非空集合。我们假设一个程序可能有许多入口点，因为它实际上发生在被设计为既作为小程序又作为独立应用程序启动为了给出与JDK 1.2引入的访问控制策略一致的访问控制策略的规范，我们为每个节点n NN赋予以下附加信息：• （n），与n关联的权限集。 Java安全体系结构将权限限制在整个保护域，我们的模型没有显式处理我们只要求，每当n−−·nJ，n和NJ都携带相同的许可集。• Priv（n），一个布尔谓词，指示n是否表示特权代码。在下文中，我们假设上述所有信息都是从字节码中提取的，例如通过[7，8，9]中提出的构造。在本文中，我们将使用[8]中的一个示例，该示例描述了一个小型电子商务应用程序。从Java程序中提取的调用图如图1所示（有关更多细节，我们请读者参考[8]）。带圆圈的节点表示特权代码块。保护域和节点之间的映射如图1所示。二、调用图的操作语义由转换系统定义，转换系统的配置是节点序列，对调用堆栈进行建模。图3中定义了转换关系（稍后讨论JDK谓词的定义）。我们还需要一个可达性关系 说明程序G可以导致给定的状态：G[]G<$σσ<$σ ′G<$σ′我们说一个状态σ是G可达的当且仅当G<$σ。在这里，我们使用[6]中提出的完全访问控制算法的稍微简化版本，因为我们让特权帧利用它们自己的所有权限。简化的算法执行调用堆栈的自顶向下扫描。堆栈中的每个帧引用包含类的保护域，4spender（）n3：呼叫主要（）克莱德n6：呼叫n4：呼叫n7：呼叫n5：呼叫debit（）n11：支票（P借方）n12：呼叫canpay（）n8：check（Pcanpay）n13：呼叫n9：呼叫n 14：呼叫n10：返回n15：返回read（）n16：检查（P读取）write（）n18：检查（P写入）n17：返回n19：返回n2：呼叫n1：呼叫图1.一、调用图。被调用的方法属于哪个。一旦发现其保护域没有所需权限的帧，就会引发一个ControlException。该算法成功时，发现一个特权帧carry- ries所需的权限，或当所有帧已被访问。该算法的一个正式规范在图中给出4、这就是JDK的定义。我们在此强调一个重要的观点。 在JDK 1.2安全架构中，可以将权限P授予位于保护域D内的代码片段，即使P不属于显式关联的权限保护域方法权限客户端未知提供程序系统斯潘德克莱德canpay（），debit（）main（），read（），write（）{P借记，P可支付}∅{P借记，P支付，P读取，P写入}许可图二、保护域。5D►[]PHPJDK（P）P ∈ N（n）中文（简体）σ：nJDK（P）P∈N（n）Priv（n）σ：nJDK（P）[JDK][JDK]≺[JDKPriv]n∈S[][n][编辑]∅l（n）=调用n−→n′σ：nσ：n：n′[电话]l（n）=check（P）σ：nJDK（P）σ：nσ：n′n−−·n′[检查]l（m）= returnn−−·n′σ：n：mσ：n′[返回]图三.操作语义学。图四、访问控制策略的具体说明以.1我们的模型可以防止这种行为，因为JDK规则确保：<$n∈N，σ∈N<$。 P∈/P误差（n）=<$σ：nbJDK（P）还要注意，我们的JDK推理规则是固定的，- 是的因此我们不能对AllPermission和FilePermission（“*"，“write”）等权限进行建模，因为它们可能会通过更改Java系统二进制文件来破坏安全性。在下文中，我们将说许可P被拒绝（相应地，授予）到状态σ，如果σbJDK（P）（分别为σ JDK（P））。此外，给定调用图中引用的所有权限的有限集合将由Permission表示。回到我们的例子，考虑节点n16：调用者n9和n13都是私有的，读，读。 因此，在n16的安全检查将1这可以通过implies（）方法实现6DPin（n）={DPout（m，n）}（m，n）∈EDP输出（m，n）排泄量（n）如果=DPcall（m）电话（n）−·→nDP（m）反式如果m−→n如果DP呼叫（n）=排泄量（n）在（n）中的最大DP如果Priv（n）否则∅DP（n）反式=CUP（m，n）∈E{DPout（m，n）}∈DP（ m，n）出来DPin（n）如果l（n）=check（P）andkill（n，P）如果l（n）=check（P）和<$kill（n，P）和<$Priv（n）kill（n，P）=def（m，n）∈E. P∈/DPout（m，n）图五.否认的分析。总是通过。这同样适用于n18，因为它的唯一调用者是特权n14。现在考虑n11：它的一个调用者（n4）有权限Pdebit，而另一个（n6）没有。的确，在11号出口的安全检查是必要的。另外，请注意，涉及clyde的任何执行都不会通过n11中的检查：那么权限Pcanpay总是被授予n8的两个调用者（n3和n12），并且在n8处的检查也是多余的。我们的静态分析旨在发现冗余检查，即总是成功的检查，以及总是失败的检查3静态分析我们的第一个分析被称为拒绝的分析（DP简称）。它为每个程序节点n计算一个安全近似值，即拒绝任何状态σ：n的许可集合的子集。该分析由图5中的控制流方程组DP（G）定义（实际上它定义了DP的补DPw.r.t.许可）。注意DP是一个前向分析，我们感兴趣的是满足等式的最大集合控制流程信息通过有限的属性空间表示7→PLPP± FL=Lin× Lout× Lcall× Ltranss，其中Lin、Lcall、Ltranss是从N到（Permission）的全函数，而out是从E到（Permission）的全函数空间。（许可）。假设（Permission）是由偏序的，标准构造为每个空间都配备了逐点序。作为一个例子，集合Lin由下式给出的关系±in部分排序：l in±inliJn= def < $n∈N。n（n）n（n）类似地，我们在这些空间上定义一个连接算子。 回到我们的例子：l inHinliJn= defλn：N. n（n）n（n）有了上面的描述，我们的函数空间变成了有限完备格。因此，L也是有限完备格。图5中的方程组定义了该晶格的元素之间的传递函数FDP，即FDP：L→ L。控制流方程的任何解δ∈ L必须满足δ= FDP（δ）：在这种情况下，我们记为δ|=DP（G）。实际上，FDP是单调（和连续）函数，因此链L（L）2（L）最终稳定到最大解方程系统的一部分。现在我们可以说明DP分析的正确性。对于每个可达状态σ：n，拒绝给n的权限是任何解的δcall（n）分量的超集定理3.1（DP分析的设G是一个调用图，G <$σ：n，δ |= DP（G）。然后又道：P∈δcall（n）=<$σ：nbJDK（P）直觉告诉我们解决方案是如何构建的。节点入口处未被拒绝的权限是其所有调用者出口处的（未被拒绝的）权限的并集。调用节点仅在它们具有特权时才生成非拒绝权限;否则它们传播其入口点的非拒绝权限检查节点传播可能通过检查的调用方的权限返回节点没有传出边，所以它们在这里是请注意，当跨越保护域的边界时，可以丢弃权限例如，边n6n11的δout分量于图1是：δout（n6，n11）=δcall（n6）（n11）δcall（n6）=δin（n6）=δout（n2，n6）<$δout（n7，n6）=（δ call（n2）<$δ call（n7））<$（n6）=<$。（一）我们的第二个分析被称为授权分析（简称GP）。类似于DP，它为每个节点n给出了8GPin（n）=（m，n）∈E{GPout（m，n）}如果GPout（m，n）=GPcall（m）排泄量（n）−·→n总平均收入（m）反式如果m−→n如果GP呼叫（n）=排泄量（n）在（n）中的RGP如果Priv（n）否则∅如果l（n）=check（P）andkill（n，P）GP（n）=反式{GP（出来m，n）} n{P}CUP∈DP（m，n）（m，n）∈E出来GP（n）在如果l（n）=check（P）和<$kill（n，P）和<$Priv（n）见图6。的分析。授予任何具有topn的状态的权限。该分析由图6中的方程组GP（G）定义。GP也是一个向前分析，我们寻找满足等式的最大集合在节点入口处授予的权限是在其所有调用方出口处授予的权限。调用节点仅在它们具有特权时才生成授予的权限;否则它们将在其入口点传播这些权限。检查节点生成它强制执行的权限和授予可能通过检查的所有调用方的权限。作为GP分析的一个例子，我们计算授予节点n16的权限集：γcall（n16）=γin（n16）=γout（n9，n16）<$γout（n13，n16）=（γcall（n9）<$γcall（n13））<$（n16）=（n9）（n13）={P借方，P可支付，P读取，P写入}（二）我们现在可以声明我们的GP分析的正确性。对于每个可达状态σ：n，授予n的权限是任何解的γcall（n9∈||定理3.2（GP分析的设G是一个调用图，G <$σ：n，γ |= GP（G）。然后又道：P∈ γ call（n）=JDK（P）.回到我们的例子，GP的正确性定理确保了任何顶部节点为n16的状态都将通过安全检查，因为P读取γcall（n16）（参见等式2）。2）的情况。因此，GP分析静态地捕获该检查的冗余，然而，如第2节中直观地讨论的，该检查被动态地测试。这是我们的分析如何通过从代码中删除冗余检查来优化堆栈检查的一个例子。图7显示了电子商务示例的DP和GP分析的最大解决方案。可以计算DP和GP分析的最大解通过对标准工作列表算法的轻微调整（参见[9]）。我们的宝宝-SIC运算是二进制集合的并集和交集。他们的计算需要一系列的步骤线性权限，即每任务集的大小.然后，工作列表算法的简单实现所执行的基本操作的数量的（粗略）上限为O（|E|2·|许可|2）的情况。nδcall（ n）γ调用（n）n1−n2n3−n5n6−n7 n8n9n10n11n12n13−n 14n15n16−n 19∅{P读，P写}{P借记，P支付，P读取，P写入}{P读，P写}∅{P读，P写}{P读，P写}{P读，P写}∅{P读，P写}∅许可{P借记，P可支付}∅{P借记，P可支付}{P借记，P支付，P读取，P写入}{P借记，P可支付}∅{P借记，P可支付}{P借记，P支付，P读取，P写入}{P借记，P可支付}{P借记，P支付，P读取，P写入}图7.第一次会议。DP和GP的最大解决方案。4优化堆栈检查上一节的正确性结果揭示了堆栈检查算法的可能优化。当必须对权限P做出访问控制决策时，调用堆栈（用节点代替保护域）自顶向下检查如下。假设n是10∈[]PHP（P）P∈/δcall（n）σJDK（P）σ：nJDK（P）P∈γcall（n）σ：nJDK（P）[JDK]∅[JDK]δ[JDK]γ当前扫描的节点。如果P∈δcall（n），则抛出一个ControlException。否则，如果P γcall（n），则算法成功。如果两者都没有发生，搜索将继续。这种优化的堆栈检查算法在图8中详细说明，并被证明可以产生与标准JDK相同的结果。图8.第八条。优化访问控制策略的具体说明定理4.1（JDK的正确性）设G是一个调用图，G <$σ. 然后，对于任何许可P：σ►JDK(P) ⇐⇒ σ►JDK٨(P)5总结发言本文提出了两种Java字节码的控制流分析方法.第一个分析产生一个安全的近似值，近似值是在运行时授予字节码的权限集，第二个分析近似值是被拒绝的权限集。这些分析为减少堆栈检查的运行时间开销提供了依据.在这里，我们专注于Java字节码，但是相同的静态技术可以应用于处理其安全架构通过堆栈检查提供动态权限检查的编程语言或系统（例如C[19]）。许多作者提倡使用静态技术来优化安全属性的检查。Walker[16]提出了类型化编译模式的概念：类型对关于程序安全性的断言进行编码，以确保不会发生对安全属性的运行时违反。另一种方法是由Jensen，LeM`etayerandThorn[8]提出的。 它通过线性时间时态逻辑对安全属性（包括堆栈检查）的类进行形式化。然后，使用模型检查来证明局部安全检查执行给定的全局安全策略。Wallach和Felten在[17，18]中通过利用置信逻辑[1]和称为安全传递风格的技术来解决优化堆栈检查的问题。Pottier，Skalka和Smith[11]引入了一个类型系统来建模11Java堆栈检查的简化版本。这两种方法隐含地描述了冗余的检查，而我们的控制流程分析则直接描述了冗余的检查。我们的建议扩展到完整的访问控制策略，需要调用图构造算法挑出新线程可以生成的程序点。这一步似乎是这项工作的难点。事实上，我们认为我们的分析只需要轻微的修改。我们的程序模型不处理Java的动态链接特性。实际上，整个程序在构建其调用图之前就可以使用了。扩展我们的方法来处理动态链接需要大量的工作。第一步是动态链接相关的调用图。然后，必须组合各种程序片段的可用解决方案。在[13，15]中可以找到一些关于照顾动态链接的数据流分析的初步工作。6致谢最后两位作者部分得到了MURST项目TOSCA的支持，和第二作者也由MURST 项 目 Interpretazione Astratta ， Sistemi di Tipo e AnalisiControl Flow.引用[1] M. Abadi，M. Burrows，B. Lampson和G.普洛特金分布式系统中访问控制的演算。ACM ToPLAS，706[2] A.科格里奥，A.戈德堡，和Z.乾实现JVM字节码验证器的可证明正确T.R. Kestrel研究所，1998年。[3] S. N. Freund和J.C. 米切尔Java字节码语言中用于对象初始化的类型系统310-327[4] S. N. Freund和J.C. 米切尔Java字节码语言和验证器的正式框架在ACMOOPSLA147比166[5] A. 金伯格Java加载和字节码验证的规范在第五届ACM计算机和通信安全会议上，pp。49[6] L. 龚Java 2平台安全性：架构、API设计和实现。Addison-Wesley，1999年。[7] D. 格罗夫湾DeFouw，J.Dean和C.钱伯斯面向对象语言中的调用图构造在ACM OOPSLA108-124[8] T. 詹森，D. LeM'etayer和T. 桑恩验证基于控制流的安全策略。T.R. IRISA，1998年。12[9] F. Nielson，H. R. Nielson和C. L.汉金程序分析原理。Springer，1999年。[10] T. 尼普科已验证的字节码验证器。在FOSSACS 2001，LNCS 2030中。[11] F. 波捷角Skalka和S.史密斯静态访问控制的系统方法在ESOP30-45岁[12] Z.乾JavaTM虚拟机指令的一个大子集的对象、方法和子程序的形式规范。在Java的形式语言和语义学中，LNCS 1523，pp。271-311，1998年。[13] A.龙捷夫湾G. Ryder和W.兰迪程序片段的数据流分析。在ESEC/ SIGSOFTFSE，1999年。[14] R. Stata和M.阿巴迪Java字节码子程序的类型系统在ACM POPL149比160[15] V. Sreedhar，M.伯克和J. D. Choi一个在动态类加载的情况下进行过程间优化的框架。2000年SIGPLAN编程语言设计与实现会议。[16] D. 沃克一种用于表达安全策略的类型系统在ACM POPL 2000中。[17] D. S. Wallach，A.W. Appel和E.W. 费尔滕SAFKASI：一种基于语言系统的安全在ACM TOSEM 2000中。[18] D. S. Wallach和E.W. 费尔滕了解Java堆栈检查。在1998年IEEE安全与隐私研讨会上。[19] C. 《介绍C》，SAMS出版社，2000年。
我的内容管理
展开
