0 概述

软件的可信性是确保金融、国防、政务等相关系统正确性和安全性的关键, 目前大多数软件产品通过软件测试方法来验证其正确性^[1]。随着软件规模的增加和内在逻辑的复杂化, 常规测试用例的覆盖率较难达到100%, 无法彻底消除软件中隐含的错误和Bug。为保证软件系统的可信性, 最有效的解决方案是利用严格的形式化方法来对软件进行验证^[2]。2016年9月, 美国国防部推出“不可破解”代码技术, 即利用形式化验证技术进行代码编写, 使程序无法被攻破。形式化验证方法是采用数学逻辑和各种推理技术, 并基于已建立的形式化规约对软件特性进行分析和验证, 以此评判系统是否满足期望特性^[3-4]。

近年来, 形式验证技术和工具不断发展, 许多研究已成功使用形式化验证方法提高软件可信性。为提高商业软件的可靠性, 一些公司例如微软、Facebook、Amazon、华为等已开展形式化技术研究和工具的研发。然而, 形式化验证过程复杂且证明代价较高, 其已成为工业应用的门槛^[5]。

已有的形式化验证项目多数是针对高级语言的形式化验证, 为保证程序在实际运行时的正确性, 则需要证明编译系统的无差错性, 才能使得验证的程序经过编译器生成的汇编级代码满足预定的规范。面向汇编级程序验证则可解决以上问题, 但是手动撰写汇编代码规约和交互式完成证明, 代价高且效率低。此外, 从软件程序结构角度来看, 顺序结构在程序中所占比例最大, 而对顺序语句的证明非常耗时且不可绕过对其证明。为此, 本文归纳总结各种证明方法的规律, 提出一种面向汇编级顺序语句块的形式语义自动规约且能自动生成证明脚本的方法, 并从慕尼黑大学构建并维护的形式化验证效率的基准数据集中, 随机抽取10个顺序语句块为测试集, 对本文方法进行测试验证。

1 相关工作

形式化证明工具为形式化验证技术的应用提供了支撑^[6], 本文以所使用的形式化验证工具类型为视角, 可将形式化证明技术大致分为手动撰写证明脚本和自动化验证两类。

手动撰写形式化证明脚本即验证者通过交互式定理证明器, 如Isabelle^[7]、Coq^[8]和HOL4^[9]等, 依据待验证程序运行环境建立形式化模型, 根据其满足的属性建立形式化规约, 并在交互式定理证明器中完成推理验证。2004年—2006年, 澳大利亚国家ICT实验室(NICTA)发起实施的L4.verified项目^[10]采用交互式的定理证明器Isabelle, 对seL4微内核的ARMv6进行了功能正确性及访问控制安全性的证明, 提供了一种程序功能正确性的形式化证明方法, 但其是在假定编译器正确的条件下验证高级语言的抽象层。seL4所证明的代码为高级语言(C语言), 源代码约8 000多行, 但其在Isabelle中的验证代码约20万, 是源代码的20多倍, 证明耗费了600万美元的经费。Verisoft XT^[11]对整个计算机系统自底向上从硬件层到应用软件层进行普适形式化证明, 完成了一个完整的软硬件的验证链^[12], 但该项目由20人参与, 耗时3年完成, 代价较高。

文献[13]研发的反黑客攻击操作系统CertiKOS采用模块分层验证法, 拥有并发性, 可同时在多个CPU内核上多线程运行, 并且整合了精化验证确保操作系统内核的高可信。文献[14]使用定理证明器Coq完成了一个商用抢占式实时操作系统内核, C/OS-II的关键功能模块正确性验证, 包括任务调度程序、时钟中断程序、时钟管理及4种同步通信机制(消息队列、互斥锁、消息邮箱和信号量), 总计约3 450行C代码, 覆盖了68%左右的常用API。这2个项目都是采用交互式证明器Coq编写脚本进行形式化验证, 证明开销工作量约平均每年2人~5.5人。文献[15]选择组合应用定理证明器Isabelle/HOL和程序验证工具VCC, 验证了汽车电子嵌入式操作系统eAutoOS的内核和系统服务模块的正确性, 其中内核代码约2 900行, 验证工作量约每年3人, 系统服务C代码约5 000行, 系统验证总工作量约每年2人。

为提高验证效率, 简化验证难度, 自动化验证工具相继被提出, 如PVS^[16]、Z3^[17]、danfy^[18]和vale^[19]等。运用自动化验证工具对代码量一定的应用程序形式化验证, 无需验证者手动撰写大量的证明脚本, 仅需按照自动化验证工具的规范写明待证明代码的使用条件(例如前置条件、后整条件)和验证属性, 即可快速得到程序是否正确性的验证结果。文献[20]提出一种基于SMT求解器的路径敏感程序验证方法, 在一定程度上减少了SMT的路径搜索空间。文献[21]使用Promela建模语言对智能购物合约进行建模和模型检测, 验证了形式化方法对智能合约的作用。文献[22]实现一个基于xv6的单CPU系统内核Hyperkernel, 通过Z3求解器自动形式化验证了45个系统调用和中断处理程序。但是其为了避免证明路径爆炸, 对内核接口做了一定限制, 并且简化了虚拟内存的实现, 避免无限的循环和递归的验证, 其验证结果具有一定的局限性。

在交互式定理证明器中, 手动撰写证明脚本能够在证明过程中留下证明依据, 便于定位软件发现所出现的错误, 并且通过手动干预可以完成较复杂的系统级验证。但是其缺点在于自动化证明程度低, 证明开销较大。自动化证明方法能解决手动撰写证明脚本效率低和代价高的问题, 但是当出现证明路径爆炸时, 使用该方法会导致证明终止。例如, 当所设置的后置条件过强或者循环不变量错误时自动化验证将停止, 此时也无法定位证明过程的错误问题。基于此, 本文提出一种交互式定理证明器实现顺序语句的自动化规约和验证, 以达到降低形式化验证开销的目标。

2 自动证明系统架构与模型

软件实际运行是在硬件环境的存储器和处理器支持下完成的, 本文以交互式定理证明器Isabelle作为验证工具, 所构建的自动证明系统架构与模型如图 1所示。首先在Isabelle环境下建立与硬件环境同构的系统模型, 并定义为一个软件的工作对象集合——状态空间, 其由代码C、内存数据D、处理器和设备控制器的寄存器的集合等各种存储单元组成。此外, 在Isabelle环境下还需建立与硬件架构相对应的指令接口模型。

Isabelle环境是对待验证软件所建立形式化规约和证明的模块, 在该模块中, 首先运用本文所实现的自动翻译程序, 将待验证的汇编程序自动翻译到Isabelle环境中形成指令函数序列。然后根据程序实现所使用的数据对象建立状态空间。在此基础上, 分析待验证程序的数据对象和每一条语句对数据对象状态的改变, 将程序执行后的系统状态作为后置条件, 根据功能正确性和谓词逻辑进行自动形式化规约, 并运用霍尔逻辑和各种推理规则对其生成自动验证脚本。

Hoare逻辑使用严格的数理逻辑推理为计算机程序的正确性证明提供一组逻辑规则, 其核心是使用Hoare三元组描述一段代码的执行如何改变系统状态。Hoare三元组表示为 < P, C, Q>, 其中, P是前置条件即代码在执行前系统状态, Q是后置条件即代码执行后系统状态, C是一条或者多条指令代码^[23-24]。

假定程序段的指令序列为: < I₁, I₂, …, I_n>表示程序F各条语句执行的先后顺序, < S₁, S₂, …, S_n>表示执行程序F各语句后系统各状态, 系统的初始状态为S₀。顺序语句推理规则如下:

$ \frac{P\left(S_{0}\right)\left\{I_{1}\right\} Q_{1}\left(S_{1}\right), Q_{1}\left(S_{1}\right)\left\{I_{2}\right\} Q_{2}\left(S_{2}\right)}{P\left(S_{0}\right)\left\{I_{1}, I_{2}\right\} Q_{2}\left(S_{2}\right)} $

该规则为在前置条件P(S₀)下执行指令I₁后置条件Q₁(S₁)成立, 且在系统状态Q₁(S₁)下执行指令I₂, 后置条件Q₂(S₂)成立, 则可推出前置条件P下执行指令序列 < I₁, I₂>, 系统状态Q₂(S₂)成立。因此, 在证明一个顺序组合语句时, 可以先证明2个子语句I₁、I₂的性质, 然后将其合并得到整个组合语句的性质。

3 自动形式化规约及验证 3.1 自动形式化规约步骤

根据Hoare逻辑中顺序语句推理规则, 在第2节所建立的系统模型中如验证顺序语句块代码的功能正确性, 需要手动撰写执行每条指令的前置条件和后置条件, 并撰写大量的手动证明代码完成验证。本节所提出的算法可以自动形式化规约与验证, 其概述如算法1所示。

算法1  顺序语句自动形式化规约与验证算法

输入  汇编级顺序语句块, 前置条件P

输出  后置条件Q和证明脚本

1.读入汇编级语句块将其转换为Isabelle模型中的指令序列I={I₁, I₂, …, I_n}

2. $\forall ~\mathrm{i.i} \in[1, \mathrm{n}] \wedge \mathrm{P} \wedge \mathrm{S}\left(\mathrm{I}_{\mathrm{i}}\right) \Rightarrow \mathrm{Q}_{\mathrm{i}} $

3.依据前置条件P, 指令序列I和每条语句的后置条件Q_i生成证明脚本

4.输出后置条件Q和证明脚本

算法1描述的是对于给定的一个待验证的软件系统中的一段程序代码, 在完成以下步骤后可以完成对其顺序语句自动形式化规约和验证。

步骤1  自动翻译。将给定的软件系统中的程序编译成一个汇编代码, 然后执行本文所实现的自动翻译程序, 将其转换为Isabelle所定义的指令函数序列。

步骤2  自动规约。读入步骤1生成Isabelle所定义的指令函数序列, 执行本文设计实现的自动规约程序, 输出顺序程序段每条汇编指令的后置条件(公理语义)和每条汇编语句的公理语义的证明脚本。

步骤3  自动验证。在定理辅助证明器Isabelle中执行步骤2生成的每条汇编语句的证明脚本, 自动验证程序的正确性。

3.2 证明策略

为保证覆盖所有可能的情况, 本文将程序的前置条件设置为最宽松的状态, 称最弱前置条件。一个程序的最弱前置条件为程序能够被运行的最低前置条件, 即代码段中已经保存了正确的指令, 且程序计数器EIP指向第1条指令。因此, 程序的前置条件定义为:

definition P ::"state bool" where

"P S ≡ (

((C S) 0x0 = pushl 1 regi 0x0 ebp) ∧(*代码段*)

((C S) 0x1 = movl 2 rr 0x0 0x0 esp unuse_r 0x0 0x0 ebp unuse_r) ∧

…∧

(EIP (R S) = 0x0) (*EIP指向第1条指令*)

)"

针对汇编级顺序语句块功能语义正确性验证, 定义的正确性引理需要保证在任何正确的系统状态下, 执行顺序语句块都能满足所定义的正确性引理。对任意一条顺序语句I_i功能语义的正确性引理定义如下:

lemma L_i :

assumes

1.“Q_i-1 S₀ S_i-1”and

2.“S_i=Step S_i-1″

3.“(C S_i-1)(EIP(R S_i-1))=instr”

shows“Q_i S₀S_i”

在系统状态S₀状态下执行i-1条语句后, S_i-1为可信系统状态, 且在系统状态S_i-1下执行第i条语句后系统状态S_i成立, 则表示在系统状态S₀状态下执行i条语句后系统状态为S_i。

对于指令I_i, 证明 < I₁, I₂, …, I_i>执行后的后置条件“Q_iS₀S_i”成立。它成立的前提为I_i执行前状态是明确的:“Q_i-1S₀S_i-1”; 指令I_i的语义是明确的:“R_iS_i-1S_i”。因此, 只要给出由“Q_i-1 S₀S_i-1”和“R_iS_i-1、S_i”, 推出“Q_iS₀S_i”论证方法即可。

综上所述, 引理证明思路如下:

1) 在初始状态S₀下, 由指令I₁的语义可以推出其执行后的状态S₁和它满足的条件Q₁:“Q₁S₀S₁”。

2) 在状态S₁下, 由指令I₂的语义可以推出其执行后的状态S₂和指令执行前S₁之间满足的条件R₂:“R₂S₁S₂”, 同时由“Q₁S₀S₁”和“R₂S₁S₂”可以推出S₀和S₂之间满足的关系Q₂:“Q₁S₀S₁”。

3) 推理执行i-1条顺序指令序列 < I₁, I₂, …, I_i-1>, 系统的状态S_i-1以及S₀与S_i-1之间的关系Q_i-1:“Q_i-1S₀S_i-1”, 它表示了顺序指令序列 < I₁, I₂, …, I_i-1>的语义。

4) 在“Q_i-1S₀S_i-1”和S_i-1的基础上, 根据指令I_i的语义, 推出其执行后的状态S_i与指令执行前S_i-1之间满足的条件R_i:“R_iS_i-1S_i”, 同时由“Q_i-1S₀S_i-1”和“R_i S_i-1S_i”可以推出S₀和S_i之间满足的关系Q_i:“Q_iS₀S_i”。

由此得到结论:在指令执行任意一个时刻i-1, 只要已经得到了此刻系统状态的属性(即顺序指令序列 < I₁, I₂, …, I_i-1>执行后的语义“Q_i-1S₀S_i-1”), 在此基础上只要分析一条指令的语义“R_i S_i-1S_i”, 就可以得到顺序指令序列 < I₁, I₂, …, I_i>执行后的语义“Q_iS₀S_i”。

在交互定理证明器Isabelle2017中, 任意一条顺序语句I_i功能语义正确性引理及其证明脚本如下:

lemma L_i:

assumes

1.“Q_i-1 S₀ S_i-1” and

2.“S_i = step S_i-1”

3.“(C S_i-1)(EIP (R S_i-1))=instr”

shows “Q_i S₀ S_i”

proof -from 2 and 3 have 4:“R_i S_i-1 S_i”

by (auto simp:R_i_def)

from 4 and 1 have“Q_i S₀ S_i”

by (auto simp:R_i_def Q_i_def Q_i-1_def)

thus?thesis by auto

qed

上述证明策略已经在Isabelle2017得到证明, 且发现任意一条语句功能正确性引理和自动证明脚本都遵循一定的规律, 因此, 可以依据本节证明策略, 设计一种算法以实现顺序语句块自动形式化规约与验证, 提高形式化验证的自动化程度和效率。

3.3 自动规约算法与自动验证 3.3.1 问题的形式化描述

由于并发、异常、中断等因素给一个程序片段带来不确定性, 而一个系统实施正确的同步机制后, 可以保证一条机器指令具有原子性。本文假定每一条机器指令具有原子性。

每一条汇编指令都有一个操作码和若干个操作数。从一个方面考虑, 这些操作数可能有寄存器、存储单元、立即数等, 也可能不是被该指令修改的寄存器或存储单元, 而是用来计算最终被指令修改的存储单元的地址的一些寄存器, 以及作为寻址中基址的变量的地址、立即数等, 或是用来计算源操作数存储单元地址的一些操作数, 称其为名义操作数。从另一个方面考虑, 指令中涉及到一些操作数, 唯一地确定了一个要被指令写入数值的存储单元地址和用来计算写入数值的若干个操作数存储的地址或寄存器, 本文称其为原义操作数。自动规约过程中需要根据名义操作数计算出原义操作数。例如指令“movl values(%ebx, %edi, 4), %eax”中名义操作数包括values、%ebx、%edi、4、%eax。原义目标操作数为%eax, 原义源操作数地址为values+%ebx+%edi×4的存储单元长度为4的数据对象。本文从汇编指令中直接获取的是名义操作数, 用原义操作数来表达指令的语义。

任意给定一条汇编指令, 指令执行产生的效果就是重写0个或者多个数据对象。例如mov指令重写一个原义操作数和一个指令指针寄存器。add指令重写目标操作数、重写标志寄存器和一个指令指针寄存器。指令“movl %eax, values(%ebx, %edi, 4)”的原义操作数S_i-1.values+S_i-1.%ebx+S_i-1.%edi×4被重写为S_i-1.%eax; 指令指针EIP重写为下一条指令的地址。自动规约算法在Isabelle中将该指令的后置条件规约成:

S_i=S_i-1

R:=(R S_i-l)EAX:=(D S_i-1)(addr),

EIP:=EIP(R S_i-1)+1

其中, address(values)表示变量values的地址, addr=address(values)+EBX(R S_i-1)+EDI(R S_i-1)×4。

3.3.2 汇编级顺序语句块的自动规约

选择一个处理器后, 它的指令集以及与其对应的汇编格式集合即确定, 指令的名义操作数和原义操作数也即确定, 于是便于建立汇编指令的形式化规约。对一条汇编指令规约其语义的工作包括:

1) 归纳出从名义操作数计算原义目标操作数和原义源操作数。

2) 将每一个原义目标操作数表示为原义源操作数的一个表达式。

3) 在此基础上构建指令的后置条件。

在自动规约算法的实现过程中, 需要保存当前程序工作对象集合的当前状态, 定义信息存储对象的类型:

Struct wobj {

char type; // 0:寄存器; 1:存储单元。

unsigned int addr; //如果是存储单元, 则表示数据对象的//地址

char reg_name[NameLen]; //如果是寄存器, 则表示寄存//器名

unsigned int len; //数据对象的长度

string value; //存放数据对象的值, 用字符串构成的表达//式表示

struct Wobj*next; //指向下一个工作对象存储节点

char flag; // 0:仅仅读取过; 1:修改过。

}

符号约定:算法中用S_i表示strcat(“S”, itoa(i)), 即用S₀, S₁, …等表示在Isabelle中可以识别的标识符“S₀” “S₁” “S₂”等。

1) 初始化:为保证覆盖所有可能的情况, 本文将程序的前置条件设置为最宽松的状态, 称最弱前置条件。一个程序的最弱前置条件为程序能够被运行的最低要求, 即代码段中已经保存了正确的指令, 且程序计数器EIP指向第1条指令。

(1) 工作集链表:创建一个工作集状态信息对象链表(wl)的首指针struct wobj* wobj。

(2) 临时对象:创建一个存放汇编指令的字符串string instr; 一个存放操作数的数组struct {unsigned int addr; unsigned int len; unsigned int value; char type/*寄存器或内存单元*/; struct wobj* local; } operand^[10];当前指令操作数个数unsigned int wnum。

(3) 源操作数和目标操作数:struct sd{unsigned int addr; unsigned int value} src, dest; 当前指令编号unsigned int i=1;假定程序的汇编指令数为n。

2) 读取编号为i的汇编指令, 把指令字符串存放在instr中; 把所有的操作数存放在operand数组中。

3) 对operand中每一个操作数:在wl中查找是否存在。如果存在, 则设置operand中该元素的loc指针指向找到的数据对象; 否则创建一个wobj对象链接在wl的尾部, 并填充addr、len、next、value等值, 其中, value的值设置为:(D S₀)(addr)或RegisterName(R S₀)。设置operand中该元素的loc指针指向找到的数据对象。

4) 根据instr中确定源操作数组和目标操作数组。对每一个目标操作数src确定其wl中的节点、操作数的地址或寄存器名、操作符op、源操作数dest。对每一个目标操作数计算它的新值:op (dest.value, src.value)。

5) 后置条件:假定x₁, x₂, …, x_u是存储器操作数, y₁, y₂, …, y_v是寄存器操作数。输出:

definition Q_i:"statestatebool"

Q_i xy=(S_i=S_i-1 D:=(D S_i-1)(x_l.addr:=x_l.value, x2.addr:=x2.value, …, xu.addr:=xu.value)

R:=(R S_i-1)(y₁.name:=y₁.value, y₂.name:=y₂.value, …, yv.name:=yv.value

EIP:=EIP(R S_i)+0x1)

6) 当前指令语义:根据instr中的指令来定义S_i-1与S_i之间的关系“R_i S_i-1 S_i”。该关系的定义要根据指令的类型分情况确定源操作数、目标操作数, 目标操作数的值用源操作数表达的表达式。举例说明:假定该指令只有一个存储单元目标操作数dest和一个存储器目标数reg_name, 则“R_i S_i-1 S_i”定义如下:

definition R_i:"statestatebool"

R_{i xy}=(y=x D:=(D x)

(x.addr:=exprosion_of_source_operand)

R:=(Rx)(reg_name:=exprosion_of_source_operand)

7) 当前状态引理

lemma L_i:

assumes

1.“Q_i-1 S₀ S_i-1”and

2.“S_i = step S_i-1”

3.“(C S_i-1)(EIP (R S_i-1))=instr”

shows “Q_i S₀ S_i”

8) 当前状态的证明脚本

proof -from 2 and 3 have 4:“R_i S_i-1 S_i”

by (auto simp:R_i_def)

from 4 and 1 have “Q_i S₀ S_i”

by (auto simp:R_i_def Q_i_def Q_i-1_def)

thus?thesis by auto

qed

9) i←i+1。如果i≤n, 转2);否则结束。

3.3.3 自动验证

执行3.3.2节所设计的算法后, 将生成定理证明器Isabelle可以读入的thy文件, 导入到本文所建立的Isabelle系统模型中, 可实现自动化验证。

4 实验结果与分析

第3节提出的自动规约和形式化验证方法, 使用C语言和python语言实现自动生成后置条件和证明脚本, 并在交互定理证明器Isabelle2017中运行所生成的证明脚本, 验证本文所提出的方法有效性。

文献[10]对C语言程序进行验证, 使用时间(单位:人/年)来衡量验证代价, 文献[13-15]的验证也使用时间为单位评估验证每个模块所耗费的开销。为此, 本文借鉴上述方法同样使用时间来评估所提出方法的时间开销。

笔者团队在完成操作系统设计与形式化验证VTOS项目^[24]的过程中, 已掌握形式化验证的策略, 具备了丰富的验证经验。但在验证C代码时需要将汇编指令手动写入所构建的Isabelle模型中, 同时还需要为每一条指令建立语义规约, 然后才能使用相应的验证策略证明程序的功能正确性。这些操作对于经验丰富的专业形式化验证人员也需要耗费较多的时间, 例如在验证VTOS消息模块的mini_send函数的顺序语句时, 13条汇编指令的证明脚本为557行, 在验证最顺利时大约花费4 h。若验证者验证策略使用不当或者定理证明器使用不熟练, 则完成验证顺序语句将耗费更长时间。而运用本文所提出的自动规约和验证方法, 针对min_send顺序语句所耗费的时间为130 s。

SV-Comp^[25]是由慕尼黑大学构建并维护的形式化验证效率的基准数据集, 为评估形式化验证技术提供了公平的测量数据, 如文献[26-28]均选用该库验证任务作为测试集。为验证本文所提方法可行性, 在SV-Comp的验证任务C程序库中随机选用了9个测试集进行测试, 在Win10操作系统、Intel Core i7-5700HQ处理器(2.70 GHz@4cores)和16 GB DDR3内存实验平台下运行本文算法, 实验结果如表 1所示。

在表 1中, 第1列表示选择的测试集名, 第2列表示测试集的程序行数, 第3列表示所生成的证明脚本能否在Isabelle2017中验证通过(T表示通过), 第4列表示证明脚本的行数, 第5列表示验证每个测试集所用的时间。实验结果表明, 本文所提出方法具有较高的可行性。

5 结束语

本文依据软件实际运行环境在Isabelle中建立系统模型, 并提出一种面向汇编级顺序语句块的自动形式化规约及验证算法, 通过10个顺序语句程序测试集验证该算法的正确性。实验结果表明, 与完全人工操作相比, 该算法验证效率较高, 降低了形式化验证工作的复杂度。