基于重写逻辑的Java源代码抽象认证技术web工具

理论计算机科学电子笔记248（2009）19-29www.elsevier.com/locate/entcsMaude1中的Java源代码自动认证工具M.阿尔巴-卡斯特罗2 M.阿尔蓬特3 S. P. Ojeda5D. Romero6Dpto. 西班牙政治大学信息系统摘要在以前的工作中，提出了一种基于重写逻辑的Java源代码抽象认证技术，重写逻辑是一种语义框架，已在基于规则的编程语言Maude中有效地实现。 从Maude编写的（通用）Java抽象语义的规范开始，我们开发了一种抽象验证技术，该技术基本上由使用Java抽象语义的可达性分析组成。 我们提供了将抽象域与所考虑的Java程序的变量相关联的设施所以，所得到的状态空间是有限的。作为抽象验证的副产品，安全证书被交付，其中包含一组（抽象）重写证明，可以由代码消费者使用标准重写逻辑引擎进行检查。 主要优点是必须显式信任的代码量非常小。本文提出了一种Web工具，通过为不同的安全属性提供适当的抽象域，同时对用户隐藏方法的技术细节，实现了抽象认证技术。该工具已被设计为易于扩展到其他属性和域。它目前支持两种标准Java编译器无法处理的安全属性的认证：安全整数运算规则和关键词：自动认证，重写逻辑，Maude，Web工具1介绍Proof–Carrying Code (PCC) is a technique that can be used for safe execution ofuntrusted 在PCC的典型实例中（参见图1），代码接收者（代码消费者）指定了一组安全需求（安全策略），1这项工作得到了欧盟（FEDER）和西班牙MEC/MICINN（赠款TIN 2007 -68093-C 02 -02）、西班牙-阿莱曼纳综合行动A2006-0007、巴伦西亚省政府（赠款GVPRE/2008/113）和UPV-VIDI赠款3249 PAID 0607的部分支持。Mauricio Alba-Castro得到LERNet的支持AML/19.0902/97/0666/II-0472-FA，Pedro Ojeda由巴伦西亚省政府根据FPI赠款BFPI/2007/076提供支助，Daniel Romero由MEC/MICINN根据FPI赠款BES-2008-004860提供支助2电子邮件：malba@dsic.upv.es3电子邮件地址：alpuente@dsic.upv.es4电子邮件地址：sescobar@dsic.upv.es5电子邮件：pojeda@dsic.upv.es6电子邮件：dromero@dsic.upv.es1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.07.05620M. 阿尔巴-卡斯特罗等人/理论计算机科学电子笔记248（2009）19安全JML注释，、、、、、、、没有cccDo NotRunco，deCc，，z_源Java证书确认，好的，J，c，、、、Java方法，代码， 认证检查器，，？、、、是的，、S代码制作人代码消费者、、、运行代码，zzFig. 1. Java PCC基础架构程序的安全行为，代码生产者创建一个正式的安全证明（证书），证明不受信任的代码符合安全策略。然后，接收者能够使用简单而快速的证明验证器（证书检查器）来确定证明是有效的，因此，不受信任的代码可以安全执行。在[1]中，我们提出了一种基于重写逻辑的Java源代码认证的抽象PCC方法[12]。从用Maude编写的Java语义规范开始，我们提供了将抽象域与不可信Java程序中的变量相这使我们能够实现一个抽象的验证方法，该方法基本上由使用抽象Java语义的可达性分析组成。作为抽象验证的副产品，交付了一个可靠的安全证书，它由一组（抽象）重写证明组成。这种简单的技术允许我们证明任何标准Java编译器都无法处理的不同安全属性，例如安全整数运算[1]和本文描述了一个实现[2，1]中的抽象认证技术的Web工具该工具为不同的属性提供了适当的抽象域，同时对用户隐藏了方法的技术细节。 它允许对安全性能进行认证，即，一个系统的属性，定义为某些事件没有发生，我们将其描述为重写逻辑中的不可达问题。给定一个由项重写系统描述的并发系统和一个指定系统状态永远不会发生的安全属性，所有这些状态从所考虑的初始状态不可达允许我们推断出所需的安全属性。遵循图1中描述的PCC基础设施，我们的工具可以在代码生产者端用于认证Java源代码。我们总结了它的设计原则以及安全策略和证明的表示问题，并表明，在这样的系统中的可信计算基础（TCB）确实可以很小。本文是[ 2 ]的技术的一个新的、完全重新设计的实现，以便：（i）处理非干扰策略，（ii）在前一版本的基础上改进功能和性能，以及（iii）使系统更易于使用和扩展。M. 阿尔巴-卡斯特罗等人/理论计算机科学电子笔记248（2009）19212抽象认证方法为了降低验证的计算成本并避免专家的具体化负担，我们通过使用抽象解释来强制程序的有限我们的方法，这是在[1]中提出的，可以总结如下。从[7]中形式化的重写逻辑中的Java语义的具体化开始，我们开发了一个抽象的，有限状态的操作语义（在重写逻辑中），它是参数w.r.t.抽象域，适合于程序验证。使用这种抽象的有限状态操作语义，我们定义了一种源代码认证技术。认证工具的关键思想是使用标准的Maude（广度优先）搜索命令来测试Java状态的不可达性，这些Java状态表示安全属性的对应物，在测试成功的情况下，提供相应的重写证明，证明这些状态的不可达性正如预期的结果证明。证书被编码为（抽象的）重写序列，该重写序列与扩展的抽象语义和抽象的Maude编码一起，可以由标准归约引擎通过以下方式进行检查：重写过程非常简单。我们使用[7]中给出的Java重写逻辑语义，并由JavaFAN验证工具[6，8]使用。这种语义处理Maude中指定的完整Java 1.4语言的一个非常大的子集，包括多线程、继承、多态、对象引用和动态对象分配。但是，Java本机方法和许多可用的Java这种语义的新颖性和趣味性基于以下优点：（i）形式规范为可以在数学上进行规范化的语言提供了严格的语义定义;（ii）即使对于像Java [6]和JVM [8]这样的大型语言，也可以使用相对较少的资源来开发这种形式规范;（iii）Maude编程语言[3]实现重写逻辑，提供了形式分析基础设施，因此其形式分析工具（例如状态空间宽度优先搜索和LTL模型检查）可以免费用于Maude中指定的每种编程语言;（iv）尽管它们具有普遍性，但这些形式分析可以以具有竞争力的安全策略通过对Java源程序变量的一组抽象要求来表达。这些是使用Java建模语言JML语法编写的。JML是一种行为接口规范语言，它接受Java代码使用者通过使用与Java代码方法混合的JML断言、要求和确保子句来声明安全策略， 得到认证。JML批注的文本可以位于标记之后的一行中//@，或者在标记/*@和@*/之间的多行中。/*@需要方法前置条件>;@确保方法后置条件>;@assert谓词>;@*/7参见[7]中提供的不同编程语言22M. 阿尔巴-卡斯特罗等人/理论计算机科学电子笔记248（2009）19\--该工具自动生成抽象的Maude编码，以及包含初始状态的搜索命令，该初始状态包括包装的补充Java程序，以及最终状态，这取决于预期的方法结果。该工具可以生成三种不同的证书：完整证书、简化规则证书和简化标签证书。完整证明包括重写证明中使用的所有Maude方程和规则（以及相应的匹配替换）。根据Maude对规则和方程的不同处理，只需记录规则给出的重写步骤，而省略方程的重写，就可以得到一个极其简化的规则证明。这是因为，在Maude中，用方程归约是确定性的，而且Maude在这方面非常有效率。最后，归约的标签只记录应用规则的标签该工具可以验证符合用户定义的整数算术安全属性的代码 该工具还可以验证遵守用户定义的输入输出数据不干扰策略的代码非正式地，我们认为，变量[5，9，10]的级别标签（高标签到秘密变量，低标签到公共例2.1考虑下面的Java方法，从[10]中借用，它包含一个条件语句。它的输入变量high和low分别被标记为High和Low机密标签，这意味着变量high是秘密的，变量low是公开的。尽管在if语句的保护范围内，从变量high到low存在非法和间接的信息流，但该Java函数确实遵守这是一个暂时的违反，因为从常量0（实际上是一个公共值）到变量low的合法和直接的转换在if语句之后。public int findDuplicate（int findDuplicate）{/*@requires AbsValue （ low ） == #Low&&AbsValue （ high ）==#High;@ensureAbsValue（\result）==#Low;@*/if（high== 1）low=1;low=0;return low;}该示例的非干扰认证的抽象域是一组确认标签LV值= #高，#低[ 2 ]。JML子句&&“requires AbsValue（high）== #High AbsValue（low）== #Low;“声明变量high被标记为High，因此它是秘密的，并且变量low被标记为Low，因此它是公开的。子句“确保AbsValue（result ）== #Low;“声明方法的结果应该是公共的。M. 阿尔巴-卡斯特罗等人/理论计算机科学电子笔记248（2009）1923\\联系我们≤我们的优势|}{|}联系我们|}现在让我们描述一下我们的工具中包含的抽象域，这些域用于验证大量使用整数运算的Java程序 其中包括抽象域EvenOdd（偶数和奇数整数的抽象域）和Mod 4（Java整数模4的抽象域）。也就是说，EvenOdd=bot，#even，#odd，top ， 其 中 bot= ， #even= int （ n ） n mod2 = 0 ， #odd= int （ n ） nmod2=1，8top= int（Int）。 另一方面，Mod 4 =bot，#0，#1，#2，#3，top，其中#k=int（n）n mod4 =k对于k0 1 2 3JML子句“requiresAbsValue（n）==#even;“声明变量n与抽象域EvenOdd相关联，其值应该是偶数。子句“确保AbsValue（result）== #even;”声明方法的结果值（由关键字 result 表 示 ） 应 该 是 偶 数 。 子 句 “assert AbsDomain （ k ） ==EvenOdd;“声明局部变量k与抽象域EvenOdd相关联。我们还提供了几个组合的抽象域参数w.r.t.两个Java变量x、y和捕获Java整数上的布尔关系。作为概念的证明，我们考虑两个布尔关系：x y和x> y。例如，JML子句<“assert AbsDomain（i）==（EvenOdd，（=，n））;“声明变量i是使用域EvenOdd抽象的，并且其值小于或等于n的值。例2.2考虑下面这个带有while语句的Java程序，它要求输入一个条件，以确保满足所考虑的安全属性。在假设输入参数n属于抽象域Mod4的情况下，要求输出的奇偶性为偶数EvenOdd是与变量sum相关联的抽象域。为了处理while的条件，我们必须对变量i使用组合域：JML子句“assert AbsDomain（i）==（Mod 4，（=，n））;“，声明变量i是使用域Mod 4抽象的，

下载后可阅读完整内容，剩余1页未读，立即下载