理论计算机科学电子笔记141（2005）19-34www.elsevier.com/locate/entcs证明携带码Martin Wildmoser、Amine Chaieb和Tobias Nipkow慕尼黑大学信息学院摘要在带注释的程序之外，携带代码的证明系统构造并证明保证给定安全策略的验证条件。 注释可以来自各种程序分析器 不能被信任，因为它们需要被验证。 通用验证条件生成器可以被利用，使得注释的组合被递增地验证。新的注释可以通过使用先前验证的注释作为可信事实来验证。我们展示了如何从一个可信的类型分析器的结果可以与不可信的间隔分析相结合，自动验证字节码程序不超过流。所有可信组件都在Isabelle/HOL中进行了形式化和验证。关键词：验证携带代码，字节码，安全策略，类型分析器，Isabelle/HOL1介绍证明携带代码（PCC）使代码生产者能够使代码消费者相信程序是安全执行的。它将程序与机器可检查的安全性证明相关联。代码使用者根据保证程序安全的公式检查这个证明。该公式由验证条件生成器（VCG）为每个程序单独构造在早期的PCC系统[10]中，VCG是一个高度工程化的组件，它试图产生易于证明和检查的证明义务这是以拥有一个难以理解和信任的复杂组件为代价的。VCG中的错误可能导致不安全程序的可证明验证条件。 基本证明携带码[3]通过要求验证条件直接用机器语义表达所需的安全属性来弥补这一点VCG形式1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.02.04020M. Wildmoser等人理论计算机科学电子笔记141（2005）19编译器证明器证明代码分析仪1注释式注释VCG安全逻辑分析仪2受信任组件安全政策Prog.浪证明Fig. 1. PCC系统架构证据策略仍然适用。在这种情况下，它所做的所有公式转换都在逻辑内部，必须被验证。这通常会导致大的证明对象。此外，直接表示安全性的验证条件需要高阶逻辑，这阻碍了自动证明生成。对于一些安全策略，如类型安全、正确的指令解码、程序计数器在范围内等，这仍然是可行的，因为可以从复杂的类型系统中提取证明[9]。纯基础和经典PCC之间的一个有希望的折衷是开放验证器[6]架构。虽然验证[10]中的强大VCG是一项艰巨的任务，但可以使用最小的VCG作为可信核心。它将更复杂的转换委托给不受信任的扩展，这些扩展必须证明它们的工作。在[17]中，我们遵循类似的想法，只是在我们的情况下扩展是被验证的，因此是可信的。我们形式化的参数化框架中的定理证明Isabelle/HOL的通用VCG。该框架定义了通用VCG用作参数的函数的签名和规范要求。通过将这些参数定义为特定的编程语言、安全策略和安全逻辑，可以获得实例化的VCG。如果验证了实例化的参数满足框架在本文中，我们将实例化一个VCG，它检查Jinja字节码程序中的算术运算。Jinja[8]是Java的精简版本，具有对象创建，继承，动态方法调用和异常处理。作为安全逻辑，我们使用一阶表达式语言[16]深深嵌入Isabelle/HOL。程序验证中的一个普遍问题是寻找循环的不变量。我们的VCG假设这些在代码中以注释的形式给出。代码生产者的任务是找到它们。对于许多安全性质，归纳不变量可以使用静态程序自动生成M. Wildmoser等人理论计算机科学电子笔记141（2005）1921∈|V VV分析. 本文的主要贡献是展示如何从Java字节码验证器完成的区间分析和类型推断中获得注释在我们以前的论文中，注释必须由代码生产者手动添加由于必须验证注释作为验证条件的一部分，因此分析器必须不可信。可以使用任何外部工具，其结果可以转换为我们的一阶表达式语言中的注释然而，有时人们知道一些分析师是可以信任的。例如，在Jinja形式化中，我们有一个完全验证的字节码验证器。给定一个字节码程序，它推断所有程序位置的寄存器和堆栈元素的类型。在本文中，我们将展示如何可以实例化的通用VCG，使其结合可信和不可信的信息。我们的目标是验证条件，要求我们验证不可信的部分，并允许我们假设可信的事实。我们称这种验证条件为增量，因为它们只有在假设对特定程序成立时才有一定的价值要检验这一点，有几种可能性。首先，这些假设可能来自可信和有效的分析器。在这种情况下，客户端可以运行这个分析器，并将结果作为可信部分交给VCG。其次，我们可以使用一个分析器，它为每个结果发出一个证书这通常只是PCC的另一个实例，可以通过将分析器的结果作为不可信事实直接提供给VCG来处理。我们可以使用多个VCG，而不是使用一个大的VCG来组合各种不可信来源的结果。在这种情况下，我们可以独立地证明不同分析器的结果2PCC框架我们的通用VCG构造公式的注释控制流图。一个程序的控制流由一个参数函数succsF确定，该函数为每个位置p产生一个与分支条件配对的后继位置列表直觉上，（pJ，B）集合（succsF<$p）意味着在B成立的情况下，pJ可以从p 形式上，我们写假设一个状态（p，m），其中p是程序计数器，m是内存，满足某个公式B。安全策略以函数sF的形式从程序和位置到公式被期望，使得sFp表示当我们在运行时到达p 类似地，我们为位置p处的注释写一个Fp。为具有分支条件B的后继节点pJ的每个节点p，VCG构造该证明义务：（sFpLzaFpLzB）LzwpFppJ（sFpJLzaFpJ）结合注记和分支条件的安全公式sF_p22M. Wildmoser等人理论计算机科学电子笔记141（2005）19VV∧−→V⇒必须隐含从p到pJ的转换的（最弱）先决条件和由pJ处的注释和安全公式组成的后置条件。请注意，标记的连接词Lz和Lz是安全逻辑的一部分，而和是Isabelle/HOL除了这些证据，VCG对初始状态发出安全约束。满足公式initF的状态必须满足安全公式和初始位置ipc的注释。initFlz（sF（ipc）LzaF（ipc））我们的框架要求初始化的初始化，使它覆盖所有的初始状态初始化的一个程序。请注意，initF产生安全逻辑中的公式，并且可以抽象由initS建模的具体初始状态的属性。函数名中的字母F和S表示它们是否属于公式或语义级别。除了initS，我们使用一个状态转换关系e S来模拟程序的语义。我们说一个程序相对于某个安全策略sF是安全的，即isSafe sF，当且仅当所有可达状态都满足安全策略。isSafe sF= invsF其中inv <$I =<$（p，m）∈ReachableS <$。（p，m）|= 我...可达S ={（p，m）|<$（p0，m0）∈initS <$. （（p0，m0），（p，m））∈（e<$S<$）<$}我们在Isabelle/HOL中证明的正确性定理保证了程序的安全性，并且如果可以证明它的通用验证条件，则具有有效的注释。定理正确-vcg：（VCG要求. wf initF succsF wpF sFaFwf∧Π►vcg initF succsF wpF sF aF Π)−→（invsFinvaF）谓词VCGReqs. wf initF succsF wpF aF sF表示参数函数满足我们的框架要求。与... 我们指出，为了更好的可读性，一些参数，如lz，lz，initS和e_（？）利用vcg initF succsF sF aF，我们表示通用VCG的实例到特定参数设置。良构谓词wf用于检查程序上的简单语法约束PCC框架只要求它检查程序中是否有足够的注释。我们的通用VCG在控制流程图中每个周期至少需要一个注释。在这种情况下，它通过使用wpF拉回后续位置的注释来构造未注释位置的公式。详情见[17]。可以向wf添加其他检查，但M. Wildmoser等人理论计算机科学电子笔记141（2005）1923|−−→必须记住，代码消费者应该有效地评估WF。我们不深入VCGReqs对参数提出的要求的细节这些可以在[17]和伊莎贝尔理论[2]中找到。对于特定的实例化，大多数需求都很容易证明。最困难的部分通常是验证succsF和wpF是由eS和initS定义的具体语义的抽象。也就是说，如果语义不正确，如果允许从（p，m）到（pJ，mJ）的转换，则pJ必须在由succsFp和相应的分支条件静态预测的后继者中必须为（p，m）。此外，如果（p，m）满足某个后置条件Q的前置条件，即，（p，m）=wpF<$p pJQ，则Q必须满足（pJ，mJ）。如果所得到的VCG是完整的，也就是说，安全程序产生可证明的验证条件，则需要更强的要求。了wpF运算符必须产生最弱（！）preconditions和successF必须给出精确的控制流程信息。在Jinja的实例化中，我们已经证明了VCG的正确性和完整性。3增量验证一旦证明了特定参数设置的需求，其中一些参数可以由扩展版本替换，而不必重新进行证明。安全策略sF可以由另一安全策略sFJ替换，因为没有要求依赖于它。引理替换sF：VCGReqs. wf initF succsF wpF sF aF−→ VCGReqs. wf initF succsF wpF sFJaF另外，我们可以随时用更强的wfJ版本替换格式良好性检查器wf。引理upgrade−wf：（请参阅。wfJ− →wf）VCG Reqs. wf initF succsF wpF sF aF−→ VCGReqs. wfJinitF succsF wpF sF aF不变量可以用来升级后继函数。为此，我们使用高阶函子upg，它通过将不变量I与其分支条件结合来升级给定的后继函数succsFsu c csFp =[（p1，B1），. . . ，（pk，Bk）]（u pgIsu c csF）p =[（p1，B1IVzIp），. . . ，（pk，BkLVzIp）]引理upgrade−succsF：（（wf − → inv I）VCGReqs. wf initF succsF wpF sF aF）−→VCGReqs. wf initF（upg I succsF）wpF sF aF24M. Wildmoser等人理论计算机科学电子笔记141（2005）19V- -∀−→现在想象一下，我们有两个针对某个编程语言的分析器，我们想使用它们来验证某个安全策略sF。让aF1和aF2作为我们从两个分析器获得的注释一个简单的解决方案是用两个注释集的联合来实例化PCC系统 我们取aF12=λ <$p。aF1α pLz aF2证明了framework 's requirements VCGReqs... wf initF succsF wpF sF aF12. 然后代码生产者必须给我们一个证明，证明vcginitF succsF wpF sF aF12，这将保证invaF12和invsF。这种方法如果两个分析器都不可信，则可以接受否则，我们重复工作，因为两个注释集都必须被证明。或者，我们可以实例化两个VCG，并逐步进行首先，我们为一个简单的安全策略实例化一个VCG，该策略强制执行F1注释.我们展示的要求VCGReqs . wf initFsu c csFwpF（λp. LTruez）aF1（1）和一个sk，生成器以生成无约束的cginitFsuc csFwpF（λp. LTruez）aF1（2）.对于格式良好的程序，这给出了inv_aF_1，并且使我们能够应用引理upgrade_wf和upgrade_succsF来获得另一个实例化，其中VCGReqs_wf_J_initF（upg_aF_1_succsF）_wpF_sF_aF_2（3）成立。对于wfJ，我们使用了一个更强大的良构性检查器。它通过检查（2）的证明来保证wf的正确性并确保inv=aF1。如果wfJ接受程序，则要求生产者发送验证vcginitF（upg aF1succsF）wpF sF aF2（4）的证明，这保证了我们实际感兴趣的安全策略，即invsF，以及invsF2。如果第二个证明可以使用F1的话，这个方法比第一个方法更好，因为F 1现在只出现在蕴涵的左边。如果F1R来自可信的来源，我们还有第三种选择.在这种情况下，我们通过假设或因为我们有分析器的正确性证明，即证明- 是的wfj invaF. 在这两种情况下，代码生产者可以跳过（2），只需要证明（4）。 在本页中-因此，我们将为Jinja字节码验证器应用第二个选项，这在[8]中被证明是正确的它为寄存器和堆栈元素推断的类型可以被信任，并且不能在验证条件内再次验证可信注释的其他示例是系统不变量。这些是由Jinja虚拟机为任何格式良好的程序维护的属性。例如，Jinja虚拟机为系统异常预分配对象例如OutOfMemory，并始终将这些对象保持在堆中的特定位置这可以表示为安全逻辑公式，并产生系统不变量。M. Wildmoser等人理论计算机科学电子笔记141（2005）19254Jinja字节码Jinja字节码是Java字节码的缩小版本，涵盖了基本的面向对象功能：对象创建，继承，动态方法调用和异常。在本文中，我们只使用基本的算术和移动指令。我们的intervall分析还没有强大到足以处理对象引用和方法调用。具有这些功能的程序可以在我们的PCC系统中进行图2示出了将从1到n的所有数相加的方法。这两个安全检查可防止算术运算过快，并使我们的区间分析器能够生成线性感应不变量。每个方法都在自己的框架中执行，框架包含程序计数器、寄存器和操作数堆栈。除此之外，Jinja状态包含一个堆映射引用到对象。程序位置是三元组（C，M，pc），其中pc是C类的方法M中的当前指令的编号。寄存器和堆栈包含布尔值（例如Bool True）、整数（例如Intg 5）、引用，例如地址3，空指针，例如指针或伪元素，例如单元。数据类型val = Bool bool| Intgint|地址|Null|Unit每个值都有一个与之关联的类型：数据类型ty = Boolean|整数|类cname|NT|虚空Jinja程序在位置（Start，main，0）启动，其中一个方法帧包含空操作数堆栈和未初始化的寄存器。Jinja程序的语义由initS（其初始状态的集合）和eS（将每个状态映射到其直接后继的关系）定义。我们跳过正式定义，因为这里使用的指令足够简单：Pushval将一个常量值推到操作数堆栈上。存储n删除最上面的堆栈值并将其存储在寄存器n中。加载n将寄存器n的内容复制到堆栈上。IfIntLeqt向前跳转t条指令（如果t为负，则向后跳转），如果上层堆栈值小于或等于下层堆栈值，则同时擦除两者。IAdd弹出两个上限值，并将它们替换为它们的总和。最后，Gotot向前跳转t条指令，Return终止一个方法，将最顶层的堆栈元素交给调用者。为了编写注释和指定安全策略，我们必须实例化安全逻辑。一个简单的方法是使用定理证明器Isabelle/HOL的逻辑作为安全逻辑，通过将公式语义定义为金贾状态上的谓词我们在其他实例化中使用了这种浅嵌入技术[15]，但决定在这里使用深度嵌入的一阶表达式语言。浅嵌入大大简化了wpF函数的定义和验证，但使精确控制流函数的定义26M. Wildmoser等人理论计算机科学电子笔记141（2005）19{≤{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy110}►⇒ ⇒⇒加载n推式输入PushIntg 65536push boundIfIntLeq20安全检查PushIntg 0 initialize Rg k商店kPushIntg 0 initialize Rg rStorerlp：加载k载荷nIfIntLeq13 if n k goto ex;加载r elsePushIntg 2147385346IfIntLeq10安全检查加载k推送Intg 1IAdd存储k k：= k+1负 载 k负载rIAdd存储r r：= r+kGoto14 goto lp：例如：负载r返回图二. 示例程序harder. 在深度嵌入中，succsF可以从注释的结构分析中提取信息，例如这有助于限制succsF为动态方法调用和异常产生的分支。此外，一阶的限制简化了验证条件的证明，并允许我们使用Isabelle/HOL之外的其他工具来实现这一目的。我们使用的表达式语言被设计为充分建模Jinja状态，并且可以为所有Jinja指令表达最弱的先决条件[16]。在本文中，我们只需要它的一小部分datatypeexpr= Cn val |RG NAT|圣纳特|Ty expr ty |expr op expr|......这是什么？op= L+z|L−z|拉斯|L=z|L≤z|L字|拉斯我们有常量表达式，寄存器和堆栈访问，类型检查以及算术和逻辑运算。当在一个Jinja状态上计算时，所有这些表达式都会产生一个Jinja值。eval：：prog state expr val的正式定义在[16]中在这里，重要的是要知道，如果表达式的计算结果为Bool True，则将其视为有效公式。，s| = F（eval s F = Bool True）为了定义可证明性判断， 通常会给出一个微积分的介绍-减少和消除规则。然而，如果我们想在Isa- belle/HOL中进行证明，我们也可以从语义上定义可证明性。F，s| = F我们决定这个选项，因为它轻视的正确性和完整性M. Wildmoser等人理论计算机科学电子笔记141（2005）1927→安全逻辑的要求如果我们可以在Isabelle/HOL中证明公式对所有可达状态都成立，则公式被认为是可证明的使用这些表达式，我们实例化了一个安全策略，禁止算术过流。我们只需检查每个加法产生的结果是否低于MAXINT，对于Java，MAXINT为2147483647。safeF**p=if（cmd**p=IAdd）thenSt0L+zSt1L≤zMAXINTelseLTruez实例化工作在于定义后继函数successF和最弱的前提运算符wpF，并证明它们满足框架对它们提出的要求。一阶表达式语言被设计为具有足够的表达能力来定义一个完整的wpF，这是一个在公式级别上精确反映语义的函数。了wpF通过公式上的替换来定义操作[16]。我们不显示它的定义，因为它遵循的原则是简单的。每当一条指令改变了某个子表达式的值时，我们用一个补偿这个效应的表达式来代替它例如，在IAdd的情况下，我们替换每个出现的St 0的后置条件与St 0L+zSt 1。wpF的所有要求都可以很容易地从我们已经证明的这个引理中得出：wf<$（p，m）∈ReachableS<$（（p，m），（pJ，mJ））∈（e <$S<$）−→eval<$（p，m）（wpF<$p pJQ）=eval<$（pJ，mJ）Q它说，在后继状态中评估后置条件相当于评估当前状态中最弱的前置条件5程序分析由于我们对支持不同安全策略的验证感兴趣，因此我们使用通用静态分析器。 它是[ 7 ]中提出的通用抽象解释框架的实现。它将程序转换为控制流程图表示，其中边缘标签表示原始命令和条件。这些标签必须由每个抽象域实现准确地解释，并以类型D D的抽象传递函数的形式给出抽象语义，D是抽象域。用相应的抽象传递函数代替控制流图中的标号，得到抽象语义方程系统的表示只要保证收敛，任何适当的迭代求解器都可以求解它，并提供一个后定点作为它的安全近似。28M. Wildmoser等人理论计算机科学电子笔记141（2005）19负载ist0：=rgiPushvst 0：=v如果假nst0 =0;st 0 =ttPopNop图3.第三章。在标签中编码字节码指令5.1调整分析器到字节码分析字节码程序的主要挑战是，指令具有由虚拟机功能给出的隐式参数。此外，堆栈操作模糊了寄存器方面的对象的依赖性与其他方法[13]不同，我们不将字节码程序翻译成中间语言，而是实现对虚拟机的抽象进行这个决定是由于我们在中间语言上的糟糕经历我们必须忍受的唯一缺点是，最终的实现只对字节码类语言有用我们必须提到的第一步是将字节码指令编码为标签语言。图中给出了一些编码。3 .第三章。任何抽象域实现都必须在这种转换的意义上准确地解释标签例如，当解释由st0：=v编码的Pushv时，抽象传递函数应该考虑堆栈的抽象必须模仿虚拟机上堆栈的行为标签x：=e可以对表达式e到变量x的任何赋值进行编码。但是，对一个赋值的解释可能会因域而异。例如，解释字节码语言的st0：=v并不仅仅是将值v存储在变量st0中，而是应该考虑堆栈元素向下移动的事实这样做的主要原因是，我们将标记语言留给所有域实现，并使用它来编码不同的命令式或字节码语言。为了可读性，我们注意到变量和表达式在一个接近符号的JVM，其中sti和rgj指的是第i个堆栈位置和第j个寄存器。条件跳转必须有两个后继，条件的计算结果为tt或tt。这是在Fig.在IfFalsen的情况下，由分配给后继边的两个标签表示。M. Wildmoser等人理论计算机科学电子笔记141（2005）1929→→∗ − ≤e s：：= x ∈ N|v ∈ V|e sbin e s|联合国见图4。 堆栈表达式rgi：= st 0λ（a，e：：es）。（a[i<$→evala e]，map（λe.e[a[i]/rgi]）es）st 0：= vλ（a，es）. （a，ev：：es）st 0：= st 0+ st 1λ（a，e1：：e2：：es）. （a，（e1+e2）：：es）图五、一些传递函数：=5.2字节码的区间分析我们实现了区间分析的结果提升格的间隔，一个特殊的情况下，一些值格V，格VV，其中V表示的一组变量，我们感兴趣的。这种转换是由一个函子，它有最小的假设上的实施格的值，因此，我们提出的技术适用于所有这样的提升。值的格必须通过抽象值（V）来近似编程语言的值这由函数α：valV确保。他们还必须提供一个算术和逻辑，以反映操作+、>、=等对于区间，我们使用标准的算术，[11 ][12][13][14][15][16] 我们通过区间[c，c]抽象数值常数c我们使用区间[0，0]、[1，1]和[0，1]来表示k、tt和未知真值。处理堆栈我们感兴趣的变量集V由寄存器和堆栈元素svars组成，即V=svars。精确的字节码分析的关键是跟踪堆栈上的值代表什么。这在开发分支条件时非常有用，因为这些条件通常用堆栈元素表示为此，我们将表达式与每个堆栈位置相关联，这是对寄存器相关值的安全描述堆栈表达式的语法在图中给出。四、由于堆栈的形状随着程序的变化而变化，我们用列表来表示它因此，我们的不敏感提升的晶格，因此也间隔分析，是LV=（V→V）×（sexpr列表）。传递函数传递函数是严格的，如果一个表达式的计算结果是V，下一个抽象状态是不可达的，因此将是LV。我们分析了30M. Wildmoser等人理论计算机科学电子笔记141（2005）19Hbcond（st0 =0）（a，e：：es）=案例Ergibinrgj让vi=a[i]HVvarncondbina[j]vj=a[j]HVvarncondbina[i]in（a[i<$→vi;j<$→vj]，es）rgibineJ（a[i<$→varncond bin（evala eJ）]，es）<$ejbcond（st0 =tt）（a，eJ：：es）（a，es）图六、一类分支条件的处理只有格式良好的程序，字节码验证器才能保证不同程序位置上堆栈元素的存在和类型正确性图5中列出了“分配”的一些传递函数有趣的情况是标签对应于Storei指令。与寄存器i相关联的抽象值将改变，因此为了一致性，所有引用寄存器i的堆栈表达式都必须更新。用寄存器i的实际值vi替换堆栈上表达式中的每个rgi，可以准确地更新这些值。在图的第二行5.我们将标签语言v中的值与sexpr表达式ev=α（v）相关联使用evalae，我们在抽象状态a中对表达式e执行自底向上的求值，方法是简单地查找a中的变量，用α抽象常数，否则递归地应用V定义的操作。分支条件的传递函数使用堆栈上的表达式来限制下一个抽象状态。我们考虑堆栈顶部的值在接下来的状态中应该为false的情况。如果这个值的近似值是α（tt），那么下一个状态将是不可达的，否则我们根据图中所示的函数bcond来限制下一个状态六、有趣的情况是当布尔条件是xbinb的形式时，其中x∈B。在这种情况下，提升函子更新与x关联的抽象值vx，vxVvarncond binvb，其中vb是表达式b计算的抽象值，varncond是每个值域的特定函数，并给出了一种最好的方法来限制给定二元运算符和右侧值的抽象值，其中二元条件不成立。值的域也必须为类似的场景，但其中的二元条件是应该举行。bin是二元运算符，使得xbiny惠ybinx成立。其他案件也是类似的。⇒M. Wildmoser等人理论计算机科学电子笔记141（2005）1931§V VV∧最后，每个域实现都必须使函数toAnnotation可用，它将域元素转换为用于注释的安全逻辑中的公式它实现了具体化函数γ。6字节码验证Jinja Bytecode Verifier推断寄存器和操作数堆栈值的类型。这些事实被编码到我们的安全逻辑中，成为形式Ty（Rg 0）（Class Start）的表达式。Lz ...Lz Ty（St 0）Lz..............................................................................................................................................................................使用[8]的类型安全证明，我们可以很容易地导出下面的定理，允许我们信任字节码验证器wtP（bcv）−→inv（conv-Ty（bcv））当Jinja类型检查器wtP接受由字节码验证器推断的bcv类型bcv时，我们可以将这些类型转换为在运行时保持的公式。在3的模式之后，我们用这些类型约束升级了succsF，并用wtP（bcv）加强了也就是说，我们验证VCGReqs.（λ. wfwtP（bcv））initF（upg（λ. conv-Ty（bcv））succsF）wpF sF aF，这给了我们一个正确的金贾VCG。7系统概述7.1生成验证条件图7显示了合成验证条件的过程，这对消费者和生产者都是通用的。Java类文件通过J2ML转换为Jinja ML表示，J2ML是我们使用Perl和Jissa实现的工具[1]。Jissa将二进制类文件解码为文本汇编符号，然后Perl将其转换为Jinja字节码的ML表示。在ML中，我们有间隔分析器以及VCG和BCV的可执行版本。后两个是从它们的Isabelle/HOL形式化自动生成的，我们已经验证了这一点。首先，我们运行区间分析以获得循环的不变量。然后将这些与程序代码一起提供给VCG。 我们已经用后继函数实例化了VCG，该后继函数在内部使用字节码验证器来构造具有寄存器和堆栈类型信息的分支条件。这些对证明构造很有帮助，因为我们的许多Jinja特定证明规则都有类型约束。为了构造证明，我们考虑两种不同的技术：第一种可以使用定理证明器。虽然可以使用其他具有证明对象和对算术的充分支持的它可能不是最好的证明器，因为它是为交互式验证而构建的，但它使我们能够从语义上定义可证明性判断第二种技术是使用证明生成程序分析。32M. Wildmoser等人理论计算机科学电子笔记141（2005）19VVLzLzLzLzLzVV区间注释Java类文件金贾字节码金贾字节码验证验证条件类型的伊莎贝尔/HOL分支条件图7.第一次会议。Jinja验证条件的生成7.2Isabelle的证明结构对于图中循环的入口点（lp：）2区间分析给出了这个表达式：Cn（Intg 0）≤Rg r Rg r≤Cn（Intg 2147385346）Cn（Intg 0）≤RG KLZ Rg kL≤zCn（Intg 65535）Lz Rg nL≤zCn（Intg 65535）如果我们使用这个注释，我们就得到了一个可由Isabelle的简化器自动证明的验证条件简化器使用eval的重写规则自动将一阶语言中的表达式转换为HOL命题。例如，这里有一个规则，可以将L+z转换为Isabelleevals（Ty e）=BoolTrue evals（Ty ej）=Bool True−→evals（eL+zeJ）=-Intg（evalse）+-Intg（evalseJ）请注意，此规则具有类型约束作为附带条件。这些可以自动释放，类型信息由BCV放入分支条件中所得的HOL公式经简化后可用于Isabelle的决策程序。对于上面的例子，线性算术曲面。 如果我们从例子程序中去掉内部安全检查，区间分析就不能再找到归纳不变量，因为它不知道Rgk和Rgn之间的关系，即. 2LzRgn=（Rgk）Lz（Rgk1+zCn Intg 1）。 但是，如果我们手动添加此关系作为不变式，该程序可以自动验证，但现在需要一个有界算术的片段来找到乘法表达式的上限7.3打样程序分析在分析器到达后修复点之后，它应该返回一个证明，证明找到的注释是正确的，即形成有效的霍尔三元组。这将避免像前一种情况那样对注释进行反向化，前一种情况需要存在特殊的决策过程，例如，如果编程J2MLVCG间期分析器BCVM. Wildmoser等人理论计算机科学电子笔记141（2005）1933语言允许乘法。我们独立于[12]开发了这种技术，并且几乎完成了对区间分析的实现更多细节见[5]。这种技术是有吸引力的，因为我们得到的证明很短。直观地说，由于分析器推断这些不变量，它们的正确性证明将依赖于一小组定理，这些定理表示分析器正确地操纵域元素证据生成分析提出了合理但不完全的有效证据生成决策程序，这有助于验证分析程序。7.4验证检查Isabelle可以以LF风格记录证明对象[4]。这些都可以传递给消费者。在那里，Isabelle证明检查器是一个相对较小且简单的ML程序，因此可以在没有机器检查证明的情况下进行信任8结论我们的通用VCG可以被实例化，这样它就可以使用可信和不可信的分析结果。它可以被工具化，只有第一个需要被验证。在本文中，我们采用了不可信的间隔分析器和可信类型分析器（BCV），以自动验证，Jinja程序不过流。这是对我们以前工作的重大改进[17] [15] [16]，我们手动注释程序我们的Jinja和PCC的形式化它表明，它是可行的，有一个完全验证的可信代码库的PCC系统。 未来 我们试图从不同的角度来延伸这项工作。计划采用更先进的程序分析技术Jinja我们的通用验证条件的一个缺点是，它们包含大量冗余和不相关的信息。我们计划通过优化后处理功能来改善这一点。在开放验证器[6]中，不受信任的扩展被用来抽象核心验证器的精确结果这是类似的，除了我们更倾向于使用经过验证的优化器。引用[1] 吉萨 网站， http://www.quiss.org/jissa/。两 千34M. Wildmoser等人理论计算机科学电子笔记141（2005）19[2] VeryPCC项目网站，慕尼黑，http://isabelle.in.tum.de/verypcc/，2003年。[3] A. W.阿佩尔基本的证据携带代码。 在第16届IEEE计算机科学逻辑年会（LICS[4] S. Berghouth和T.尼普科 简单类型高阶逻辑的证明项。 在J·哈里森和M. Aagaard，编辑，Theorem Proving in Higher Order Logics，1869卷Lect。对比中的注释Sci. ，第38Springer-Verlag，2000.[5] A. Chaieb. 生产-生产程序分析。技术报告，TU，慕尼黑，12月。2004年[6] B.- Y. E. Chang，A.奇利帕拉湾C. Necula，和R. R.笨蛋 开放式验证框架基础验证者。ACMSIGPLAN语言设计与实现中的类型研讨会（TLDIACM SIGPLAN通告，2005年。[7] P. Cousot和R. 库索 程序分析框架的系统设计。 第六届ACM SIGPLAN-SIGACT编程语言原理研讨会会议记录，第269-282页，圣安东尼奥，德克萨斯州，1979年。ACM Press，New York，NY.[8] G. Klein和T.尼普科 一个类似Java的语言、虚拟机和编译器的机器检查模型。Research report，National ICT Australia，Sydney，2004.[9] G. Morrisett，D.沃克，K. Crary和N. Glew. 从系统F到类型化汇编语言。第25届ACM Symp.程序设计语言原理，第85-97页。ACM Press，1998.[10] G. C. Necula 用Proofs编译。博士论文，卡内基梅隆大学，1998年。[11] F. Nielson，H.R. Nielson和C.汉金程序分析原理。Springer，1999年。[12] S.徐，H. Yang和K.逸从抽象解释结果自动构造霍尔证明。 在第一届亚洲编程语言和系统研讨会上，LNCS卷。 2895，第230-245页，北京，2003年。斯普林格。[13] R. 瓦莱莱湖亨德尔河谷孙达雷桑山口Lam，E. Gagnon和P. 有限 因此，我们需要一个优化框架.在CASCON 1999的Proceedings，第125[14] 慕尼黑验证卡项目网站，http://isabelle.in.tum.de/verificard/，2002年。[15] M. Wildmoser和T.尼普科验证机器代码安全性：浅嵌入与深嵌入。在proc 第十七届国际Conf. 高阶逻辑中的定理证明（TPHOLs 2004）。Springer Verlag，2004年。十六页。[16] M. Wildmoser和T.尼普科断言字节码安全性。第15届欧洲编程研讨会（ESOP 05），2005年。出现。[17] M. Wildmoser ， T. 尼 普 科 湾 Klein 和 S. 南 斯 原 型 证 明 携 带 代 码 。 在 Proc.3rd IFIPInt.Conf.Theoretical Computer Science（TCS 2004），2004。
我的内容管理
展开
