字节码中间表示程序的分模块形式化验证方法

摘要

一种字节码格式中间表示程序的分模块形式化验证方法涉及程序安全技术领域，所述方法运行于双栈结构的虚拟机，包括以函数为单位形式化重写待验证字节码程序并给出其形式化规格说明；将函数划分为指令序列并给出其规格说明；形式化证明每一个指令序列符合对应的规格说明；函数中所有指令序列的证明连接后形成函数的证明，所有函数的证明连接起来得到整个程序的证明；满足规格说明中所描述的存储特性和部分正确性特性，达到增强字节码程序可信程度的目的。本发明可与常规的测试、静态和动态检查等方法结合，应用于航空、核工业控制等领域安全关键程序的检查，具有可信度高、可自动化检查等特点。

说明书

技术领域

本发明涉及程序可信领域，特别涉及一种针对字节码中间表示程序的分模块形式化验证方法。

背景技术

字节码中间表示既能运行于虚拟机，也能作为编译过程中定义良好的程序表示形式，是当今网络软件和计算设备中广泛使用的重要技术。字节码中间表示程序验证能够提高相关软件的可信程度，同时为构造证明保持编译器提供中间表示支持，具有重要的实用价值和理论价值。

传统的字节码中间表示程序验证的主要研究工作集中于JVM内部检查器，目标是类型正确性，从而保证存储安全性。随着研究工作的深入，人们逐步认识到仅有类型安全性检查远远不够，还需要进一步研究其它更多程序性质。近年人们提出一些用于字节码程序验证的逻辑系统，代表性研究工作包括：Quigley设计了一个用于字节码程序的类霍尔(Hoare)逻辑系统，证明了含有循环的程序片段。Benton提出一种组合逻辑系统，用于一种.NET公共中间语言(CIL)的命令式语言子集，并给出纯手工证明。Bannwart和Muller提出一种支持对象、引用、方法和继承等面向对象特征的逻辑系统，用来证明类JAVA字节码。MRG项目主要着眼于程序资源，提出一种针对字节码的具有资源感知特征的操作语义，以及相应的逻辑系统。字节码建模语言BML(BytecodeModeling Language)作为一种可理解的字节码程序规范，应用开发人员可用它在字节码层面书写程序标注，以规范字节码程序的行为功能，与之对应的JML语言提供JAVA源语言层面的规范描述。该研究同时包含一个并不完整的JML到BML编译器，其局限性在于证明检查仍然需要借助一个复杂的验证器。

本发明针对的目标运行环境为双栈式虚拟机，一为计算栈，所有数据存取和算术运算均在此栈完成；二为函数调用栈，专门处理函数调用和返回的栈操作。

由于字节码中间表示程序抽象控制栈复杂、而控制流结构信息不足，以前方法无法有效解决这类程序的分块验证，而现实中有大量的需求，因此设计有效、可自动检查的形式化验证方案，具有重要的实际意义和应用价值。

发明内容

本发明利用程序证明技术，设计出一种提高程序可行程度的字节码分块形式化验证方法，该程序的分块验证方法方法通过将一个程序以函数为单位划分得到指令序列，为函数和相应的指令序列添加规格说明，并经过基于逻辑系统的形式化证明，再将证明结果按照指令序列、函数和程序的顺序逐步组合形成整个程序的证明，从而建立程序的全局良型性，确保程序满足其规格说明中规定的存储安全性和部分正确性。该方法具有易实施、易检查、难伪造等特点。

本发明针对双栈结构的虚拟机，采用独立的函数调用栈处理函数调用/返回过程中的控制结构，利用指令序列划分的方式提取字节码中间表示程序的控制流结构信息，给出了一种字节码中间表示程序的分模块验证方法。所述方法是在具有计算栈和函数调用栈的双栈式虚拟机中实现的。所述计算栈处理所有数据的存取和算术运算。所述函数调用栈处理函数的调用和返回。所述方法以一下步骤进行：

步骤(1)，所述双栈式虚拟机的初始化，

设立一个以上的函数模块，其中包括用于计算数值的阶乘的字节码中间表示程序的函数模块，

还设立：函数形式化规格说明模块、指令序列划分模块和形式化验证模块，其中：

函数模块，由字节码指令组成，所述的指令包括：pushc w、pushv f₁、popf₂、binop bop、unop uop、brtrue f₃、call f₄、ret以及goto f₅，其中：

pushc w：将整数w放入当前计算栈顶，该栈的指针减1，执行本条指令的当前指令地址pc_w加1；

pushv f₁：将内存地址f₁处的值放入当前计算栈顶，该计算栈指针减1，执行本条指令的当前指令地址pc_f1加1；

pop f₂：将当前计算栈顶的值存入内存地址f₂处，该计算栈指针加1，执行本条指令的当前指令地址pc_f2加1；

binop bop：执行包括加、减、乘、除双目运算bop，执行本条指令的当前指令地址pc_bop加1；

unop uop：执行取负单目运算uop，执行本条指令的当前指令地址pc_uop加1；

brtrue f₃：如果所述计算栈的栈顶单元为1表示真，跳转到指令地址f₃处执行，令执行本条指令的当前指令地址pc_f3的值改为f₃；否则执行下一条指令，执行本条指令的当前指令地址pc_f3加1；

call f₄：函数调用，将下一条指令地址pc_f4+1放入当前函数调用栈顶，该函数调用栈的栈指针减1，跳转到f₄处继续执行，令执行本条指令的当前指令地址pc_f4的值改为f₄；

ret：函数返回，从当前函数调用栈的栈顶取出返回地址ra，该函数调用栈的栈指针加1，跳转到返回地址处继续执行，令执行本条指令的当前指令地址pc_ret的值改为ra；

goto f₅：跳转到作为目的地址的f₅处继续执行，令执行本条指令的当前指令地址pc_f5的值改为f₅；

步骤(2)，所述函数形式化规格说明模块，把待验证的字节码中间程序以函数为单位划分并存入各函数模块，同时为每一个函数写出具有存储安全和部分正确性特征的形式化规格说明，格式为<p，g>，其中：

p表示在执行一段代码之前所述双栈式虚拟机的状态S必须满足的条件，包含所述内存、计算栈和函数调用栈中变量的取值范围，所述一段代码是指函数、指令序列或单独指令；

g表示这段代码执行前后的所述双栈式虚拟机两个状态之间必须满足的条件，包括所述两个状态之间变量必须满足的数学和逻辑关系，从而给定了整个函数的功能说明；

步骤(3)：所属指令序列划分模块将步骤(2)得到的所有函数逐个地划分为指令序列，并按所述<p，g>格式给出规格说明，一个指令序列以函数入口处、或无条件跳转指令goto f₅的目标地址f₅处、或无条件跳转指令goto f₅相邻后续地址处的指令开始；一个指令序列以无条件跳转指令goto f₅或者函数返回指令ret结束；

步骤(4)：所述形式化验证模块区别不同情况地证明步骤(3)所述的所有指令序列内的指令符合对应的规格说明：

设：某指令序列内的任意一条指令i，该指令i的地址为pc，当前规格说明为<p，g>，分情况证明如下：

情况1：如果该指令不是跳转指令、函数调用和返回指令，则给出其后续指令pc+1处的规格说明<p′，g′>，判断后续指令序列满足规格说明<p′，g′>：

如果当前状态S满足p，当前指令i能安全执行；如果当前状态S满足p，执行指令i后到达状态S′，则状态S′满足p′；如果当前状态S和函数返回前状态Sr满足g，则执行指令i后到达状态S′，状态S′和函数返回前状态Sr满足g′；

情况2：如果是函数调用指令call f₄，则表示程序控制流从当前函数foo进入被调用函数bar的入口点f₄，返回点为pc+1，需要给出该入口点f₄以及指令地址pc+1处的规格说明<p′，g′><p″，g″>，判断如下条件得以满足：

如果当前状态S满足p，则call指令执行后的状态S′满足p′；如果当前状态S满足p，则bar函数返回状态S″满足p″；如果当前状态S和foo函数返回前的状态Sr满足条件g，执行函数bar后到达状态S″，则状态S″和函数返回前的状态Sr满足条件g″；

情况3：如果为函数返回指令ret，则要求在pc点能够完成状态转移，这样既能够满足函数返回的状态转移也能满足调用函数的g，而无关于返回地址的信息；这里需判断函数调用栈满足递归定义的良型性：

如果函数调用栈中为空，则处于最外层的函数没有返回代码指针，也不存在函数返回点状态；

如果函数调用栈不为空，则判断以下条件满足：在ret指令执行之前，如果程序状态满足p，则函数调用栈顶存在一个返回地址指针，而且从次栈顶以下的栈仍然保持良型性；同时判断在所有带有程序规范<p，g>的程序点处，所有非函数调用/返回指令执行过程中都必须保持函数调用栈的良型性；

情况4：如果为条件跳转指令brtrue f₃，则跳转成功与否依赖于其判定条件是否得到满足，因此证明过程中需要使用考虑不同的执行情况，每一种情况都类似于情况1中的一条指令；

情况5：如果为无条件跳转指令goto f₅，则安全执行的充分必要条件是当前断言能够蕴含目标代码处的断言，是条件跳转指令的特例；

步骤(5)：函数中所有指令序列都符合其对应的规格说明，每个指令序列的规范不仅包含当前序列内部代码块的规范，还包含所有可能被该调用的其它指令序列的规范，就表明函数本身符合其对应的规格说明；所有函数都符合其对应的规格说明，就表明整个程序符合其对应的规格说明。

根据本发明的字节码程序验证方法能够对安全关键的字节码中间表示程序进行最为严格的形式化证明，以得到程序满足规格说明中所描述的存储特性和部分正确性特性，达到增强字节码程序可信程度的目的。

该字节码程序验证方法可与常规的测试、静态和动态检查等方法结合，可应用于航空、核工业控制等领域安全关键程序的检查，为这类安全关键软件的开发、认证和维护提供可信的手段。该验证方法具有易实施、易检查、难伪造等优点。

附图说明

图1示出了根据本发明进行字节码程序形式化验证的流程图；

图2示出了包含规格说明字节码程序及其对应的C程序实例；

图3示出了根据本发明验证方法进行指令序列划分并给出的规格说明。

具体实施方式

为使本发明的目的、技术方案和优点更加清楚，下面将结合附图对本发明的实施方式作进一步地详细描述。

图1示出了根据本发明进行字节码代码形式化验证的流程图。如图1所示，首先在步骤101中，将一个采用循环方式计算数n的阶乘的字节码中间表示程序函数facor重写如图2下半部分，其对应的C语言程序如图2上半部分，<p0，g0>为函数的规格说明，其中p0表示函数调用之前状态S必须满足的条件，该条件包括：计算栈顶有2个以上可用单元；函数调用栈顶有一个可用的返回地址；内存中为变量r保留一个存储单元；内存中为变量n保留一个存储单元，且该单元中存放的数大于等于0。而g0给出了整个函数的功能说明，表示如果函数调用之前满足p0，则factor函数执行之后到达状态S′，S′状态变量r的值是S状态变量n的阶乘。

接着在步骤102中，给出划分指令序列之后的结果及其规格说明。这段程序包含3个指令序列，标号0-2的指令构成指令序列0，指令序列1是标号为3-15的指令，指令11-15是指令序列2。本验证方法需要给出以下位置的代码规格说明：每一个指令序列的开头，调用指令、跳转指令(包括goto和brture)的目标位置，以及紧跟调用指令之后的调用返回行。函数的规格说明为(p0，g0)。(p3，g3)是循环体的规格说明，p3表明有足够的运算栈空间、变量r和n的值仍在有效范围内，g3表明内存中的变量值必须满足循环不变量。循环循环条件判断开始处规格说明(p11，g11)与(p3，g3)相同。

在步骤103中分别证明指令序列0、1和2满足其规格说明，以指令序列0为例，分别证明每一条指令：

对于指令序列0指令“0 pushc 1”，地址为0，规格说明为<p0，g0>，证明过程如下，为其后续指令寻找规格说明<p1，g1>，使得：剩余指令序列满足条件p1；如果当前状态S0满足p0，当前指令安全执行，将立即数1放入栈顶，此时栈顶单元内保存的值为1；如果当前状态S0满足p0，执行指令后到达状态S1，状态S1满足p1；当前状态S0和函数返回前状态S15满足g0，执行指令后到达状态S1，状态S1和状态S15满足g1。

对于指令序列0指令“1 pop r”，地址为1，规格说明为<p1，g1>，证明过程如下，为其后续指令寻找规格说明<p2，g2>，使得：剩余指令序列满足条件p2；如果当前状态S1满足p1，当前指令安全执行，从栈顶取出数据并赋值给变量r，此时变量r的值为1；如果当前状态S1满足p1，执行指令后到达状态S2，状态S2满足p2；当前状态S1和函数返回前状态S15满足g1，执行指令后到达状态S2，状态S2和状态S15满足g2。

对于指令序列0指令“2 goto 11”，地址为2，规格说明为<p2，g2>，证明过程如下，当前指令序列的规格说明中应当包含跳转目标地址11处指令的规格说明<p11，g11>，使得：如果当前状态S2满足p2，当前指令安全跳转，执行指令后到达状态S11，状态S11满足p11；当前状态S2和函数返回前状态S15满足g2，执行指令后到达状态S11，状态S11和状态S15满足g11。

至此，指令序列0满足其规格说明的良型性得到证明。

类似地，对指令序列1和2中的所有指令进行证明，得到所有指令序列的证明。之后，所有互不重叠的良型指令序列表明函数factor符合其规格说明，是具有良型性的程序。

本发明具有如下优点：

1.易实施：字节码形式的中间表示使用非常广泛，其代码量较大，而且相关软件通常采用模块化的开发方法，本方法支持从指令序列到函数级别的分块验证，和软件开发方法非常吻合，易于实施；

2.易检查：程序验证过程中，在相关工具的支持下交互实现，其证明结果采用人工或者机械化的方法检查；

3.难伪造：因为其验证原理采用了基于逻辑系统的方法，证明计算过程看起来比较复杂，但其基础却简单而牢固，程序规范和代码实现密切相关，一般非专业人员无法制出。