作为信息产业的核心技术, 软件系统被广泛地应用于航空航天、核电、军工、高铁、医疗、金融、自动驾驶等安全攸关的国家战略基础设施和人们的日常生活中.高可信软件系统成为保障国家安全、保持经济可持续发展、维护社会稳定和保护人民生命财产安全的必要条件.

近几年来, 形式化验证方法被认为是一种构建高可信软件系统的有效手段, 相关的验证理论和支撑工具都有了较大的发展.在验证理论方面, 程序精化验证理论^[1-5]能够支持复杂并发系统的验证; 在支撑工具方面, 形式化证明工具Coq^[6]、Isabelle^[7]、程序验证器VCC^[8]、Dafny^[9]和约束求解器Z3^[10]也逐步成熟.这些理论技术的发展给安全攸关系统软件的形式化验证提供了理论基础和工具保障, 同时也出现了大量的系统软件验证项目, 譬如, 在操作系统验证方面, 有seL4^[11], VeriSoft^[12], CertiKOS^[13], CertiuCOS^[14]; 在编译器验证方面有CompCert^[15].

上述系统软件验证项目采用的验证方法主要分为两类, 其中一种方式是利用形式化证明工具手动编写证明脚本来完成系统软件的验证, 这种验证方式的优势在于形式化证明工具能够为系统软件的验证过程产生证据, 同时, 所依赖的信任基 (TCB) 较小, 手动干预使得完成复杂系统软件的验证成为可能; 缺点在于自动化程度低、验证代价比较高.如seL4操作系统, 被证明的源代码 (C语言) 有约8 000行, 而验证代码 (Isabelle) 有约200 000行, 是源码的25倍多^[11].另外一种方式是使用程序验证器接受经过规范标注的源代码生成验证条件, 并将验证条件交给约束求解器自动求解, 这种方式的优点在于强大的约束求解器极大地提高了验证过程的自动化程度, 缺点在于它很难完成复杂系统软件功能正确性的全部验证.因为操作系统内核数据结构之间的关系复杂, 对应的约束条件也会十分复杂, 使得约束求解器无法在有效的时间范围内对其进行判定.因此, 复杂系统软件的功能正确性验证目前几乎不可能全部自动化, 人为干预不可避免.如何减少手动验证工作的代价, 是构建高可信软件亟待解决的问题.

在定理证明工具中, 验证操作系统内核的功能正确性的方法已被广泛采用^[11-14].为了提高验证效率, 都需要开发一些辅助的自动验证工具.其中, CertiuCOS^[14]项目通过在定理证明工具Coq中使用其提供的Ltac策略编程语言开发了大量的自动证明策略来提高验证的效率, 将验证脚本行数与被验证代码行数的比例从几百比一减少到了26:1.这些证明策略主要用来自动生成验证条件, 并自动证明验证条件中分离逻辑断言^[16]间的蕴含关系, 产生的一些描述操作系统内核功能正确性的纯数学命题的绝大部分则交给用户自己手动证明.由于Coq提供的一些自动证明策略 (如omega, ring) 功能很有限, 导致这些与程序上下文无关的纯数学命题的手动证明代价较高, 整个项目证明脚本代码量约21万行, 其中30%的证明脚本是用来手动证明这些纯数学命题的.而这些纯数学命题很多是可以被Z3直接判定的, 因此, 如果能够在Coq中调用Z3来辅助判定这些纯数学的命题, 则可以大大降低验证开销.

本文在Coq中实现了一个证明策略smt4coq, 能够在Coq中自动证明32位机器整数相关的纯数学命题.图 1给出了smt4coq证明策略的使用效果示例, 目标是证明定理∀x∈Int32, ∀x∈Int32, x⊕y=0→x=y.其中, 图 1(a)是用Coq提供的基础证明策略和相关的其他定理 (same_bits_eq, bits_xor, biths_zero) 的证明示例, 而图 1(b)所示为直接使用本文开发的smt4coq策略进行自动证明.

本文做出如下几点贡献:

1) 设计了一个编译框架, 支持将Coq中命题的语法形式翻译成可被Z3判定的命题, 为利用Z3自动证明Coq中的定理奠定基础;

2) 实现了一个Coq的自动证明策略smt4coq, 它能够在Coq中调用Z3证明32位机器整数相关的数学命题, 包括32位整数上的基本运算、加减、移位等.有机地将定理证明工具与约束求解器结合在一起, 取长补短.相关源码可以从地址http://staff.ustc.edu.cn/~fuming/smt4coq.zip下载获得;

3) 实验结果表明, 使用证明策略smt4coq能够大幅度减少证明代码行数.

本文第1节介绍自动证明策略smt4coq的设计思想.第2节介绍策略smt4coq.第3节介绍对32位机器整数相关命题的翻译过程的实验结果.最后比较相关工作并总结全文和将来的工作.

1 smt4coq自动证明策略的设计 1.1 smt4coq的设计思想

smt4coq是在Coq中开发的一个证明策略插件, 它通过调用功能强大的Z3约束求解器来判定一些相对复杂的数学命题, 而这些数学命题在Coq中可能需要大量的手动证明来完成.图 2给出了smt4coq自动证明策略的算法设计思想.

对于给定的一个命题P, 自动证明策略smt4coq将经过如下步骤完成对该命题的证明.

·第1步:首先对命题P取反, 通过调用Z3判定﹁P是不可满足的 (unsat), 从而得到命题P是成立的.这里, 对命题P取反为接下来的命题规范化做准备;

·第2步:命题规范化, 它的目标是将取反后的命题转化为形如∃x₁, …, x_n.P₁∧...∧P_n的命题, 为翻译成为Z3所接受的命题语法形式做准备.例如:一个形如∀x.P(x)→Q(x) 的命题, 经过取反﹁(∀x.P(x)→Q(x)).这里, P和Q是原子命题, 而该命题等价于∃x.﹁(﹁P(x)∨Q(x)).然后, 根据德摩根定律可以得到规范化的命题形式∃x.P(x)∧﹁Q(x):如果该命题不可满足, 则说明原命题成立; 否则, 存在一个反例让P不满足;

·第3步:规范化Coq命题到Z3命题的翻译, 经过规范化后的命题和Z3接受的命题形式有着直接的对应关系, 上述例子中, 规范化的命题∃x.P(x)∧﹁Q(x) 所对应的Z3的命题为

(declare-const x)(assert P(x))(assert﹁Q(x))

(check-sat);

·第4步:将翻译后的命题作为Z3的输入, 调用Z3进行判定:如果返回结果为不可满足 (unsat), 则进入第5步; 否则, 用户可以手动证明 (第6步) 或者根据报告的反例修改输入命题重新证明 (第7步);

·第5步:应用局部公理消去Coq上下文中当前的证明目标, 这里, 虽然命题P经过Z3的判定是正确的, 但是并没有在Coq中产生相应的证明项, 因此, 我们通过引入一个局部公理∀P.P(任何命题都是正确的) 在Coq中消去当前证明目标, 这个公理只允许在调用Z3返回unsat后被使用.

这里, 我们通过对Coq命题取反和规范化预处理后再翻译成Z3的所接受的命题, 而没有选择直接将其翻译成一条Z3所能接受的命题, 主要有以下两个原因:第一, 当Z3接受的命题过于复杂时, 证明时间会很长甚至根本无法证明 (比如在Z3中无法量化函数, 只能通过declare-fun语句引入); 第二, 直接翻译得到的命题会很长且只有一句, 当翻译的目标语句有问题时, Z3的出错信息只会显示在那唯一一行有错误, 不利于开发过程中的定位错误.

1.2 Coq表达式到Z3语句的翻译

规范化后的命题被分为前提条件和目标.在Coq中, 前提中的变量和命题都是同等的表达式, 但在Z3中, 这是两种截然不同的表达式.smt4coq根据表达式的类型来区分, 类型为Set的表达式是变量, 类型是Prop的表达式是命题.这样, 表达式已被划分为变量、命题和目标 (目标是特殊的一个命题).接下来要把这些表达式转化成接近Z3语法的中间表达式.定义中间表达式语法如下:

〈stmt〉   ::=〈define-data〉|〈define-fun〉|〈declare〉|〈assert〉

〈define-data〉   ::=〈data-args〉〈sub-data〉

〈sub-data〉   ::=〈name〉〈constructors〉〈sub-data〉|null

〈define-fun〉   ::=〈name〉〈input-args〉〈output-arg〉〈expr〉

〈declare〉   ::=〈name〉〈declare〉|〈name〉

〈assert〉    ::=〈forall-expr〉|〈expr〉

〈expr〉   ::=〈app-expr〉|〈atom〉

stmt表示Z3的一条语句, 根据其作用, 分为数据定义语句 (define-data)、函数定义语句 (define-fun)、变量声明语句 (declare) 和命题语句 (assert).

目前, smt4coq支持翻译归纳类型表达式 (非递归类型)、箭头类型表达式、全称命题表达式、函数调用表达式、常数符号表达式和构造子表达式.其中, 遇到新的归纳类型、构造子或常数符号时, 首先查找符号映射表:如果不在表中, 则根据其类型声明新的类型定义或函数定义; 如果出现了目前未定义的表达式, 则报错.

中间代码本身已经很接近Z3的代码了, 但翻译中需注意一些细节.比如, Z3只支持特定的泛型函数 (比如“等于”), 遇到其他的泛型函数要报错.另外, Z3不支持递归函数的定义, 需要把递归函数转化为等价的命题形式.

通过使用配置文件增加可扩展性, smt4coq将部分数据结构与函数采用直接映射的方式翻译, 这个映射储存在配置文件里, 可由用户自定义.考虑到在执行策略时配置映射表会大大拖慢证明速度, 所以把映射表的配置放到编译时, 每次用户更新配置文件后都要重新编译一遍插件.选用直接映射而不是翻译, 主要是出于以下几点考虑.

1) Coq与Z3类型系统差异巨大, 很多表达式无法精确翻译.Coq支持归纳证明、高阶函数、全递归函数, 然而这些在Z3中都无法直接定义;

2) 很多数据类型在Coq中是递归定义的, 但在Z3中有对应的基本类型.比如Z(整数), 在Coq中是用二进制的方式递归定义的, 但在Z3中有对应的Int类型, 如果在Z3中也递归定义整数, 那么证明的效率会大为降低;

3) Z3对函数的限制非常多, 比如高阶函数与递归函数都无法直接定义.为了方便、快速, 有些Z3中存在的函数, 直接映射相较于重新构造是一个更实际的选择.

1.3 调用Z3判定命题是否正确

调用Z3判定翻译后的命题, 并接收输出结果.如果结果是sat或unknown, 说明证明错误或出现异常, 插件会报错, 转为用户手动处理; 如果结果是unsat, 说明证明成功.由于该策略调用外部程序Z3, 虽然Z3判定命题为真, 但是Coq内部并没有生成对应的证明项并储存证明.为了解决这个问题, 创建一个Coq源文件如下:

Local Axiom by_smt: forall P:Prop, P.

Ltac smt4coq:=intros; smt; apply by_smt.

之后, 编译该文件成独立模块.这样对用户就封装了一个黑盒, 用户只需使用smt4coq策略就可自动证明相关定理.局部公理by_smt对其他文件不可见, 可以防止用户滥用这个公理而产生错误的证明.

2 smt4coq自动证明策略的实现

smt4coq证明策略目前实现了对整数、布尔值以及机器整数的有关命题的翻译和自动化证明.下面介绍插件源码结构以及具体的实现.

2.1 源码结构

smt4coq证明策略通过扩展Coq定理证明工具的源代码, 使用OCaml编写新的证明策略插件模块来实现.表 1给出了smt4coq证明策略插件的源码详细描述.其中, 配置文件config.ml允许增加Coq和Z3之间新的符号映射关系, 从而可以支持更多的Coq命题到Z3命题之间的翻译变换, 目前只建立了Coq的32位机器整数所涉及到的符号到相应的Z3符号之间的映射关系 (因为CertiuCOS项目只用到了32位整数, 但是可以扩展到任意长度的整数).

2.2 配置文件的描述

配置文件实际上也是一个OCaml源码文件.由于Coq没有提供让插件直接修改证明环境外内存的接口, 所以如果在运行时读取配置文件, 那么读取的配置信息退出证明就被销毁, 无法储存在内存中.这样, 每次运行插件都要重新读取配置文件, 极大地影响了运行速度.因此, 本插件使用修改配置文件再重新编译的方法来配置插件.配置文件主要的部分是一个Hash表, 键是Coq的表达式名称, 值是对应的Z3函数, 每次翻译表达式时先查表, 如果有对应的值就直接输出.该配置文件只提供一个简单映射功能, 实现对Coq内置的整数运算 (add, sub, mul等) 和布尔值运算 (andb, orb等) 的映射, 以及对用户定义的机器整数的映射.其他复杂的函数翻译、命题翻译是由插件自动完成, 无需配置.采用配置文件的原因是Z3中内置了整数、布尔值和机器整数类型及其运算, 如果按照翻译普通类型定义和函数定义的方法翻译过去, 会运行得非常缓慢, 不如直接采用映射的方式.但对于其他的表达式, Z3并没有内置, 就只能采用第1.2节所述的过程来翻译.

2.3 确保用户配置文件的正确性

从概率上说, 用户错误地配置映射关系造成错误证明几乎不可能发生.原因如下.

1) smt4coq基于Z3实现自动证明, 所以需要映射的表达式只有Z3内置的类型与函数, 即只映射整数、布尔值以及机器整数这3种类型和相关操作.而这3种数据类型及其操作都非常基础, 而且特征性强, 用户很难配置错误;

2) 在Z3中, 相应函数都有特定的类型限制, 用户如果映射了错误的函数, 极有可能会报错.比如, 如果用户将Z3中的加法add映射到Coq中的not函数, 那么就会出现参数数量错误以及类型不匹配的问题而报错;

3) 基本运算都是成套出现的, 用户需要同时映射加减乘除这些函数, 如果有一个映射错误, 那会产生结果的不一致, 很容易发现错误.比如, 如果把加法映射成乘法, 那么证明加法是减法逆运算时就会报错, 而这显然是不正确的.

2.4 机器整数类型及运算的翻译

机器整数在Coq中被定义为一个结构体, 成员包括一个Z类型整数和一个整数大小范围的限制.而Z3中内置了位矢量类型和对应的位矢量操作, 所以可以直接把Coq中的x位机器整数映射为x位矢量 (_BitVec x) 类型, 原来定义的整数运算, 比如and, or, add, mul等, 可以一并替换为Z3内置的位矢量运算bvand, bvor, bvadd, bvmul等 (这些操作对任意长度的机器整数都适用).表 2列出了部分位矢量函数.

表 3中, 以命题∀x∈Int32, ∀x∈Int32, x⊕y=0→x=y为例, 给出了Coq中32位机器整数的语句与Z3语句之间的对应关系.

3 实验结果

CertiuCOS操作系统内核验证项目^[14]和CompCert验证编译器^[15]底层都是使用相同的32位机器整数的Coq实现 (Integer.v文件), 在未使用自动化证明策略之前, 每个定理都要手工一点点构造证明, 证明动辄上百行, 而且还要证明很多引理, 原来共计4 477行代码.使用smt4coq自动化证明策略之后, 绝大多数的定理都只需一条策略即可证明, 代码量下降到1 832行.表 4给出了Integer.v中的部分定理在使用smt4coq前后证明策略数的对比情况, 结果表明:smt4coq可以自动证明这类32位机器整数相关的数学命题, 大大提高了证明效率.

我们还使用smt4coq测试了Software Foundations (一个交互式学习Coq的电子书) 中的Basic.v, Logic.v, Ind.v等文件中的部分命题, 将很多冗长的证明都缩减为1行, 使总共2 681行的证明缩减为962行 (还有很多命题关于复杂的递归数据类型及高阶函数, 无法证明).

4 相关工作比较和结论

目前有两个类似的工具:SmtCoq^[17]和Coqsmtcheck^[18].SmtCoq是在Coq中实现了一个约束求解器, 它本身的功能没有Z3强大, 导致不能自动证明本文中与32位机器整数相关的命题.coqsmtcheck只能证明关于实数相关的简单数学命题, 不支持32位机器整数相关命题的证明, 且难以扩展.本文在定理证明工具Coq中开发了一个自动证明策略插件smt4coq, 它通过将经过翻译变换的Coq命题输入给约束求解器Z3, 然后使用Z3进行自动判定来提高证明效率.目前, smt4coq只支持对整数、布尔值以及机器整数相关命题的翻译和证明, 将来会对它进行扩展, 以支持更多数据类型的翻译和相关命题的证明.smt4coq发挥了Z3的自动证明的优势, 但其也继承了Z3的不足, 无法像Coq那样产生命题对应的证明项.为了弥补这一不足, 将来可以考虑在Coq中实现Z3的某些判定算法, 同时产生证明项.