Java卡小程序的正确性保证

理论计算机科学电子笔记113（2005）217-233www.elsevier.com/locate/entcsJava Card Applet的正确性保证Lars-EscherichiakeFredlundBox 1263，164 29 Kista，瑞典计算机科学研究所，瑞典电子邮件：fred@sics.se摘要本文描述了一个实验中，一个框架的模型检查Java字节码，结合应用程序的运行时监测技术，通过代码重写，被用来保证正确性的Java卡小程序。保留字：Java字节码，运行时监控，代码重写，Java卡。1介绍Java Card平台[8]是一个用于构建多应用智能卡的平台。它基于Java的一个子集，它省略了线程并发、垃圾收集和许多API函数等特性。然而，为了支持在同一卡上共存的多个应用（例如，钱包小应用程序和忠诚度小应用程序两者），存在小应用程序的概念。Java Card applet是通过扩展Java Card API类来实现的javacard.framework.Applet. 简 单 地 说 ， 需 要 一 种 实 现 来 提 供 方 法install，该方法在安装applet时被调用，方法select和remove用于选择/取消选择卡上的特定applet，以及“main”方法进程，该这 是 为 这 个 applet 设 计 的 。 小 程 序 也 可 以 实 现 一 个 方 法getShareableInterfaceObject，以允许同一个卡上的其他小程序调用它。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.01.033218L-埃。Fredlund/Electronic Notes in Theoretical Computer Science 113（2005）217不幸的是，Java Card编程平台对分离小程序的支持很弱。 例如，标准中没有任何内容阻止恶意的或写得不好的小应用程序分配卡上的所有持久存储器（存在的很少），并且由于该标准不需要垃圾收集，这是非常不期望的状态的小应用程序。小程序间调用也存在类似的问题，尽管它们是由相当弱的防火墙机制控制的。因此，允许新的小应用程序进入功能正常的智能卡存在重大危险，因此Java Card的主要创新之一，即，在同一张卡上共存的多个应用程序实际上根本不被使用。为了改善这种情况，SICS的正式设计技术组一直在使用全自动和低成本（在执行速度和内存使用方面）的验证方法，这些方法可能被卡上（或非卡上）运行时系统用于在加载时确定是否允许新的小程序加载到具有预先存在的小程序的在[3]中报道的第一个实验中，我们使用Java字节码的模型检查分析了多applet Java Card智能卡的方法间调用。在本文中，我们扩展的治疗内存分配的关注。 如果一个小程序的安全性不能证明使用模型检查，我们作为一个补充技术仪器编译的小程序与运行时监视器，以保证它坚持一个安全的内存分配策略。为了给Java Card applet的分析提供一个语义基础，我们使用了程序图的抽象概念，用过程/方法来捕获程序的控制流，并且可以有效地计算。这种程序图的行为是通过下推系统的概念来定义的，下推系统为具有方法（可能是递归）的程序提供了一个自然的执行模型，并且存在用于LTL的完全自动的模型检查器，例如，摩托车[7]。在3.1节中详细阐述了转换的细节，在3.2、3.3和3.4节中更详细地描述了Moped模型检查工具的逻辑和我们的使用文中所考虑的例子是Schlum-berger提交的一个真实的applet小应用程序是单片的，不与其他小应用程序通信。在第4节中，我们形式化并尝试使用模型检查来验证applet（在个性化过程之后）由于该属性的满意度严重依赖于数据的属性，这需要使用比调用图提取工具中实现的抽象更少的粗糙抽象进行推理，因此我们考虑在第5节中补充使用运行时监控技术来保证属性。L-埃。Fredlund/Electronic Notes in Theoretical Computer Science 113（2005）2172192构造方法调用图我们使用一个外部静态分析工具Soot [12]，适用于Java Card1，来生成调用图，它抽象了所有内容（例如数据变量和方法调用的参数），但方法体内部的方法调用的存在和顺序。分析工具执行安全的过度近似（关于LTL安全属性的保留），在这个意义上，即使在运行时不能调用对应的调用，调用边也可能存在于结果调用图中，但反之则不成立。例如，当静态分析不能确定在方法调用中调用哪个类方法时，通常是由于子类型，则在每个可能的类中生成对目标方法的调用边缘，从而增加了生成的调用图中的不确定性。静态分析工具生成包含异常行为信息的图形。在这项工作中，特殊的边缘和节点，被翻译成非确定性的结构，从而有效地增加了程序行为的非确定性在一个保守的方式。调用图的生成相对于Java Card防火墙机制也是保守的，在静态分析中没有考虑。也就是说，在运行时将无法通过Java Card运行时环境的安全检查的方法调用将始终包含在方法调用图中。为了细化分析，并允许分析Java Card API的使用，SUN 的Java Card Development Kit （版本2.1.2）的API类生成过程的结果是一组方法调用图，表示在运行时环境调用一个（公共）可调用applet方法install（在小程序安装、小程序选择的方法选择和调试tion/diselection，允许小程序间调用的getShareableInterfaceObject，以及每次（用户）与Java Card小程序交互时调用一次的主处理方法进程由于我们在本案例研究中希望观察applet对内存的分配，因此标准方法调用图生成过程已得到增强，以额外包含有关new和newarray调用的信息。Java虚拟机（字节码）指令。新指令的一个实例-在一个方法调用图中，一个新的（合成的）方法Events.newInst将被表示为一个调用，一个newarray指令将被表示为一个调用Events.newarrayInst方法。1 来处理，例如，缺少java.lang.Class类220L-埃。Fredlund/Electronic Notes in Theoretical Computer Science 113（2005）217→∆2.0.1方法调用图方法M被划分为类C，类C本身又被划分为包P。我们假设通常的Java命名约定具有完全限定的名称，即，一个类有一个名字Package。标识符和方法有一个名称Class。识别器。定义2.1[方法图，改编自[9]]方法图是一个元组m=0（Vm），→m，λm，µm）使得：(i) Vm是m的程序点，(ii) →m <$Vm×Vm是m的转移边(iii) λm：Vm→T为m的每个程序点指定程序点类型从集合T={entry，seq，call，return}。(iv) µm：Vm（M）为m的类型调用的每个程序点指定一个非空的方法集。我们假设程序点集Vm是两两不相交的。程序程序的点是setV=0m∈MVm。程序点类型指示节点是否是入口方法的点，（seq）没有方法调用或返回发生的节点，（call）发生方法调用的节点，或（return）方法执行结束的节点，控制流程返回到调用方法。使用改进的Soot工具从Java Card applet中提取的方法调用图具有以下不变性质：（i）每个方法恰好有一个入口程序点;（ii）每个方法恰好有一个返回程序点;（iii）调用节点中的不确定性是由于在解析方法调用的目标时缺乏精确性（由于子类型），而不是由于两个不同的调用（顺序方法调用总是由传输边分隔）。L-埃。Fredlund/Electronic Notes in Theoretical Computer Science 113（2005）217221M为了方便起见，我们引入谓词v：t=<$λ（v）=t，其中t∈Tv：locm=v∈Vv：entrym=entrv：entrymv：classc=m. v：locmm∈cv：packagep=c. v：classc<$c∈p为了这个案例研究，我们进一步定义了一个谓词v：api，如果程序 点 v 出 现 在 Java Card API 包 （ java.lang ， javacard.framework ，visa.openplatform，javacard.security或javacardx.crypto之一）中的方法中，则该谓词成立。3模型检查方法调用图3.1下推系统下推系统为递归程序提供了一个自然的执行模型.它们形成了一类研究得很好的无限状态系统，其中许多重要的问题，如等价性检查和模型检查是可判定的[2]。定义3.1[PDS，来自[6]]下推系统（PDS）是一个元组其中：P= （P，Γ，π）(i) P是控制位置的有限集合;(ii) 是一组有限的堆栈符号;(iii) ∆⊆(P×Γ)×(P×Γ٨)isafinitesetofrewriterules⟨p,γ⟩→−q，σP×Γπ是P的集合。Ifp，γ→−q，σ重写P的规则，则对于每个ω∈Γπ，配置<$q，σ·ωπ是配置<$p，γ·ωπ的直接后继。P 的游程是一个序列ρ=p0，σ0p1，σ1p2，σ2···，使得对于所有i，pi+1，σi +1是pi，σi的直接后继者。现在我们定义一组方法M如何导出PDS。M222L-埃。Fredlund/Electronic Notes in Theoretical Computer Science 113（2005）217⎪∆定义3.2[诱导的PDS，形式化[7]]一组方法M诱导一个PDS如下所示P= （P，Γ，π）(i) P由单个控制位置p组成;(ii) r是程序点的集合V(iii) n是集合m∈Mv∈VmProd（v），其中Prod（v）是一组重写规则：{⎪⎨{⟨p,v⟩→−如果v：return，则返回p，vJ|v →mvJ}if v：entryN∈m（v），p，v→− p，vJ·vjj |vJ：条目mJ，v→mvJ，或v：seq如果v：调用下推系统的重写规则可以被解释为简单地操纵程序的调用堆栈，PDS是从该程序中获得的。给定一个构形c∈p，v·σ∈point（c）=v。3.2规范语言我们的规范语言是线性时态逻辑（LTL），程序点谓词p作为原子命题，但省略了类型谓词v：t。 选择线性时态逻辑作为规范语言，而不是例如模态μ-演算，因为我们编码到下推系统的模型检查问题也是有效可判定的，这完全是由于LTL的有效模型检查器Moped [7]的存在。逻辑的运算符是标准的。 如果φ和是公式，那么<$φ、Xφ和φU也是。公式的意义是关于无限长的游程rc0c1c2 We................................................................ 定义的。设ri表示从构形ci开始的r的子集。 然后满足R| = φ的公式φ通过游程r被定义为：L-埃。Fredlund/Electronic Notes in Theoretical Computer Science 113（2005）217223⟨⟩|∆►∆R| = p我的点（c0）：pR| =<$φ我的非r| = φR|= φ = φ我的R| = φ和r|=R|= φ = φ我的R| = φ或r|=R| = X φ我的R1|= φR| = φU我的有一个i ≥ 0使得ri|n = rj|= φ对于所有0 ≤ j p com_schlumbergersema_slb_Main_process_entry m_loop> pcom_schlumbergersema_slb_Main_process_77 m_loop>p com_schlumbergersema_slb_Main_process_78 m_loop>p javacard_framework_APDU_getBuffer_entrycom_schlumbergersema_slb_Main_process_81 m_loop>p com_schlumbergersema_slb_Main_process_81 m_loop>...p com_schlumbergersema_slb_Main_process_ret m_loop>p com_schlumbergersema_slb_Main_process_ret m_loop>p com_schlumbergersema_slb_Main_process_ret m_loop>p Events_newArrayInst_entrycom_schlumbergersema_slb_Main_processedRecord_295com_schlumbergersema_slb_Main_process_ret m_loop>...Fig. 1. 反例摘录工具可以快速4检查这样的公式;对于SLB applet，结果是公式不成立，并且自动生成反例（从也不满足该属性的原始系统生成的简化系统）。作为一个例子，我们包括了图1，它显示了配置的演变（一对控制位置p和一个堆栈，符号）的过程中调用process方法。 方法的名称有虽然已经被篡改了，但该图仍然说明了问题：对process方法的调用可以通过对processedRecord方法的调用，使用newarray字节码指令分配内存（注意Events.newarrayInst的入口点出现在最终配置中的“堆栈”顶部使用新指令的分配的对应属性确实保持，即，在调用process方法后，不为非数组对象分配内存检查applet的字节代码表明似乎使用了开放平台5个性化方案，即，该代码包含对visa.openplatform.OPSystem.setCardContentState方法的调用。到 检查分配是否仅在个性化第一个属性被重新定义到属性之前发生：在com.schlumbergersema.slb.主工艺内始终锁定 visa.openplatform.OPSystem.setCardContentState从未locEvents.newArrayInst也就是说，在任何调用进程期间，4在不到一秒的时间内，在用于生成调用图的相同硬件上，5http://www.glo bal pl at for m. COM228L-埃。Fredlund/Electronic Notes in Theoretical Computer Science 113（2005）217⎛⎝⎞⎠已调用个性化方法。Moped工具确认此属性适用于SLB小程序。不幸的是，它下面的属性表达了一个更强的属性，要进行处理，任何数组分配都必须始终调用setCardContentState方法：在com.schlumbergersema.slb.主工艺内alwayslocEvents.newArrayInst最终locvisa.openplatform.OPSystem.setCardContentState尝试验证这个属性与轻便摩托车不幸失败，并生成一个反例总结一下内存的状态：在任何调用进程的过程中，都有可能发生个性化，如果发生了，就不会分配更多的内存。然而，也存在这样的可能性，即在进程方法的调用期间分配了数组，但是之后没有个性化发生。这并不一定表明存在错误;可能是小程序在运行时环境调用进程方法之间保持一个状态，该状态记录是否发生了个性化，即，分配属性是数据相关的，并且这些数据相关性在调用图生成期间已经被抽象掉，从而生成误报。显然，调用图生成过程可以使用静态分析技术进行细化然而，确定哪些抽象需要最终证明或反驳该属性通常不是我们可以期望能够自动解决的任务。在下一节中，我们将探索另一种技术来保证内存分配属性。5监视内存分配显然，内存分配属性是一个安全属性，因此我们可以通过实现运行时监视器来控制applet的执行来监视器有义务保持（监视的）安全属性，并在检测到小程序即将违反其安全属性时停止（监视的）小程序的执行。为了检查内存分配控制属性，L-埃。Fredlund/Electronic Notes in Theoretical Computer Science 113（2005）217229它跟踪是否发生了个性化，如果没有，则允许内存分配，如果发生了，则不允许。与这种运行时监视器组合的小应用程序可能不满足关于行为的所有要求（例如，进度属性），但不会违反其安全属性。5.1实现细节监视器可以以不同的方式实现：如果它是可访问的，则在运行时系统中，或者作为单独的线程/进程，或者运行时监视器的代码可以直接与被监视的应用程序内联。对于Java Card平台，实现方法的选择是显而易见的，因为它缺少线程，并且无法访问API库。applet代码必须使用代码插装技术与运行时监视器代码进行物理组合。applet代码中任何可能违反监视器的操作都必须在监视器代码之前检查所讨论的操作是否安全。因此，对于案例研究，我们监控对API 方 法 visa.openplatform.OPSystem.setCardContentState ， 我 们 使 用applet代码中的字节码指令new和newray来监视内存分配（在本研究中，我们不考虑间接内存分配Java Card API方法）。由于Java字节码是结构良好的，并且字节码验证器保证了调用约定等得到遵守，因此Java非常适合通过代码插装来实现运行时监控;参见Erlingsson和Schneider [5]的讨论。我们已经实现了一个使用Soot [12]工具进行Java Card程序的自动指令化实验的工具;事实上，该工具与用于调用图提取的工具相同。使用Soot工具的一个显著优点是它提供了Java（Card）字节码方法的定义良好的高级抽象视图一个方法保证有单一的入口和返回程序点，运行时堆栈被抽象出来，有利于分配给局部变量，部分由于堆栈指令的缺失，运行时堆栈由少数几条指令组成（而不是任意的Java字节码指令），并且对于实现程序转换，有足够的支持在方法体中间插入新的字节码指令。为 了 继 续 SLB 案 例 研 究 ， 我 们 在 Soot 中 实 现 了 一 个 通 用 的Transformer，当它识别出一个新指令（或newarray）或对个性化方法的调用时，它会插入一个对运行时监视器的适当调用。Transformer的代码（用于新指令）为：...230L-埃。Fredlund/Electronic Notes in Theoretical Computer Science 113（2005）217System. out. println（）;...protected void internalTransform(Body body、String phaseName、Map选项）{String s = body. getString（）;...Iterator stmt= units.snapshotIterator（）;while（stmt.hasNext（））{String s=（String s）; stmtIt.next...publicvoid onDestination（）{//我们发现了一个新的表达式，用仪器记录它！units.insertBefore（Jimple.v（）.newStaticInvokeExpr（allocating），s）;}}}...boolean containsNewExpr（Stmts）{if（sinstanceofAssignStmt&&（（AssignStmt）s）.getRightOp（）instanceofNewExpr）return true; return false;}监视器例程有一个状态变量personalized，它确定是否允许分配：public class Monitoring {private static boolean personalized= false;public static void personalize（）{ personalized= true;}public static void allocating（）{if（personalized）ISOException.throwIt（ISO7816.SW_UNKNOWN）;}}L-埃。Fredlund/Electronic Notes in Theoretical Computer Science 113（2005）217231接下来，Soot从中间表示中生成Java字节代码，最终生成一个与监视器代码相结合的新applet。在从中间表示生成字节码的过程中，必须解决Java Card平台特有的一些问题。在我们的实验中，Soot被用作Java编译器，并且为了能够运行所得到的（插装的）Java Card applet（例如，在Sun的Java Card模拟工具中不幸的是，转换器工具的目标是转换由SunJava编译器生成的代码。为了生成转换器工具可以接受的字节码输出，我们必须改变Soot编译器，以（i）生成Sun的转换器将识别为遵守关于使用短整数的限制的代码，以及（ii）生成遵循Java Card文档中提出的相当苛刻的一旦解决了这些问题以及编译到Java Card的一些小问题，我们就能够在Sun的Java Card模拟器中模拟插装的通过检查applet的源代码，我们能够设计一系列APDU消息（从卡环境接收到的事件导致对进程的方法），如果安全保护监视器未被内联，已经导致applet违反其内存分配策略。 也就是说，即使在个性化之后，它也会尝试分配新的内存。applet本质上是惰性地分配一个记录数组，并且在第一个记录已经被分配时就已经发出个人化的信号，即使后来的分配可能发生，因此它违反了自己规定的策略。回顾过去，我们相信仅仅使用模型检查和自动数据抽象的组合来发现这样的问题是非常困难在（插装的）小程序代码大小、小程序的内存大小和执行速度减慢方面的影响可以忽略不计。除了包含小型监视器类本身之外，唯一的代码添加是对监视器类的调用，这些调用表示个性化和内存分配。然而预计发生这种呼叫的地点的数量很少。5.2第二个内存分配属性作为运行时监控的第一个实验的后续，我们决定也监控有界内存分配的较弱属性，即，小程序分配的内存量有一个界限。 为了允许监视此属性，存储器控制Transformer很容易6例如，检查是否只使用了短整数运算232L-埃。Fredlund/Electronic Notes in Theoretical Computer Science 113（2005）217扩展到通过分析Soot中的类层次结构来计算分配的内存量（对于新的或newray也就是说，计算要分配的对象的字段（包括超类的字段），并估计在运行时系统中表示每个字段的大小（大小不是由Java标准预先确定的）。因此，代码中的一条新指令被预先固定了一个对monitor方法的调用，参数是分配请求的大小（对象的大小或数组的大小），如果执行新指令将超过预定的分配界限，则负责停止applet的执行。显然，像有界分配属性这样的属性是一个很好的例子。一个applet属性类的例子，可以由卡制造商在卡运行时系统中实现，或者，正如我们在这个例子中所展示的，它可以通过将任何要加载到卡上的applet代码与保证属性的定义良好的运行时监视器相结合来同样很好地确保。Java Card感兴趣的此类可监视属性的其他示例是，例如，比Java Card标准提供的防火墙机制更严格的特定6结论和今后的工作本文研究了如何使用轻量级形式化方法来保证典型Java Card应用程序的重要安全属性，例如，使用模型检查并通过实现运行时监视器来强制确保安全属性。模型检查工作使用的Java卡小程序的方法调用的时间约束的自动模型检查的框架。该框架是通过将基于类的静态分析工具与下推系统和线性时序逻辑的自动模型检查器相结合来实现的。运行时监控实验是有前途的，但需要适当的形式化。我们希望（i）开发一个通用的代码重写函数，该函数在时间逻辑中给定安全属性，将探测器插入到代码中以保持监视器状态更新，以及（ii）使用Java Card的可用操作语义，例如。[1]证明代码重写函数尊重Java Card的操作语义和时态逻辑的语义。我们亦会研究可否以重写小程式程式的程式码作为系统性的技术，为发卡机构推行特定于卡片的政策。关于本文中提出的工作的进一步信息，包括原型实现，可以在网页http://www.sics.se/fdt/projects/vericode/jcave.html。L-埃。Fredlund/Electronic Notes in Theoretical Computer Science 113（2005）217233确认该研究是在Veri Card项目内进行的，并得到了欧盟IST计划的财政支持。我要感谢Gennady Chugunov和Dilian Gurov对这项工作的贡献，关于模型检查部分的工具支持和理论开发，并感谢Pablo Giambiagi对运行时监控技术潜力的有趣讨论。引用[1] Barthe，G.，G.杜费湖Jakubiec，S. M. de Sousa和B. Serpette，JavaCard平台的形式化可执行语义，在：D。Sands，editor，Proceedings of ESOP302-319URLftp://ftp-sop.inria.fr/lemme/Gilles.Barthe/esop01.ps.gz[2] Burkart，O.， D. 高加索， F. Moller 和B. Ste Escheren，验证 对 无限 结构， 在：J. Bergstra，A. Ponse和S. Smolka，editors，Handbook of Process Algebra，North Holland，2000 pp. 545-623.[3] Chugunov，G.，L. Fredlund和D. Gurov，多小程序JavaCard应用程序的模型检查，第五届智能卡研究和高级应用会议（CARDIS87比96[4] 科贝特，J.，M. Dwyer ，J. Hatterdham，S.劳巴赫角Pasareanu和H. Zheng，Bandera：Extracting Finite-State Models from Java Source Code ， in ： International Conference onSoftware Engineering，2000，pp. 439-448[5] Erlingsson，U.和F.B. Schneider，SASI Enforcement of Security Policies：A Retrospective，in：新安全模式研讨会会议记录，1999年。[6] Esparza ， J. ， D. Hansel ， P.Rossmanith 和 S.Schwoon ， Eachcient algorithms for modelchecking pushdown systems，in：Proc.CAV232-247.[7] Esparza，J.和S.Schwoon，A BDD-based model checker for recursive programs，LectureNotes in Computer Science2102（2001），pp.324-336.[8] JavaCard 2.1.1文档，技术报告，Sun Microsystems（2000），http://java.sun.com/products/javacard/\discretionary{-}{}{}specs.html#211.[9] 詹森，T.，D. L. Metayer和T. Thorn，基于控制流的安全特性验证，IEEE安全与隐私研讨会，1999年。[10] SchlumbergerSema，Java Card applet安全属性，内部可交付成果，验证卡项目，任务6.3。[11] 施耐德，F. B、可强制执行的安全策略，技术报告TR 99 -1759，康奈