基于Z3的Coq自动证明策略的设计和实现-张恒若 , 付明.pdf

上善若水

261

8页

0次

2022-05-20

免费下载

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn

Journal of Software,2017,28(4):819−826 [doi: 10.13328/j.cnki.jos.005196] http://www.jos.org.cn

基于 Z3 的 Coq 自动证明策略的设计和实现

∗

张恒若

付

明

2,3

(中国科学技术大学信息科学技术学院,安徽合肥 230026)

(中国科学技术大学计算机科学与技术学院,安徽合肥 230026)

(中国科学技术大学苏州研究院软件安全实验室,江苏苏州 215123)

通讯作者: 付明, E-mail: fuming@ustc.edu.cn

摘要: 形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来

验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高;而

使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动

化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.结合上述两种方式的优点,在定理证明工具 Coq

中实现了一个自动证明策略 smt4coq,它通过在 Coq 中调用约束求解器 Z3 自动证明 32 位机器整数相关的数学命题,

提高了自动化验证的程度,减少了用户手动验证程序的开销.

关键词: 形式化验证;定理证明工具;约束求解器;Coq;Z3

中图法分类号: TP311

中文引用格式: 张恒若,付明.基于 Z3 的 Coq 自动证明策略的设计和实现.软件学报,2017,28(4):819−826. http://www.jos.org.

cn/1000-9825/5196.htm

英文引用格式: Zhang HR, Fu M. Design and implementation of Coq tactics based on Z3. Ruan Jian Xue Bao/Journal of Software,

2017,28(4):819−826 (in Chinese). http://www.jos.org.cn/1000-9825/5196.htm

Design and Implementation of Coq Tactics Based on Z3

ZHANG Heng-Ruo

, FU Ming

2,3

(School of Information Science and Technology, University of Science and Technology of China, Hefei 230026, China)

(School of Computer Science, University of Science and Technology of China, Hefei 230026, China)

(Software Security Laboratory, Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou 215123,

China)

Abstract: Formal verification is an effective approach to construct high confidence software. Verifying the functional correctness of

complex system software by manually writing proof scripts in proof assistant tools is feasible with the low degree of automation, and the

verification cost is relatively high. The automatic program verifiers verify programs by taking the annotated source code as their input to

generate verification conditions automatically solved by SMT solvers. This approach has a high degree of automation, but it is impossible

to verify the functional correctness of the entire system software. By combining the advantage of the above two methods, this paper

implements a novel Coq tactic plug-in named “smt4coq”, which allows calling the Z3 SMT solver in Coq to automatically prove

mathematical propositions involved with 32-bit machine integers. The new tactic improves the degree of automation and reduces the cost

of manual verification.

Key words: formal verification; proof assistant tool; SMT solver; Coq; Z3

∗ 基金项目: 国家自然科学基金(61103023, 61229201, 61379039, 91318301, 61632005)

Foundation item: National Natural Science Foundation of China (61103023, 61229201, 61379039, 91318301, 61632005)

收稿时间: 2016-06-20; 修改时间: 2016-09-08; 采用时间: 2016-11-26; jos 在线出版时间: 2017-01-24

CNKI 网络优先出版: 2017-02-20 13:43:28, http://www.cnki.net/kcms/detail/11.2560.TP.20170220.1343.003.html

820

Journal of Software 软件学报 Vol.28, No.4, April 2017

作为信息产业的核心技术,软件系统被广泛地应用于航空航天、核电、军工、高铁、医疗、金融、自动驾

驶等安全攸关的国家战略基础设施和人们的日常生活中.高可信软件系统成为保障国家安全、保持经济可持续

发展、维护社会稳定和保护人民生命财产安全的必要条件.

近几年来,形式化验证方法被认为是一种构建高可信软件系统的有效手段,相关的验证理论和支撑工具都

有了较大的发展.在验证理论方面,程序精化验证理论

[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)所示为直接

使用本文开发的 sm

t4coq 策略进行自动证明.

Theorem xor_zero_equal:

forall x,y,

xor x,y=zero→x=y.

Proof.

intros.apply same_bits_eq.

intros.assert(xorb(testbit x,i)(testbit y,i)=false).

rewrite←bits_xor; auto.

rewrite H.apply biths_zero.destruct(testbit x,i).destruct(testbit y,i).

reflexivity||discriminate.

Qed.

Theorem xor_zero_equal: forall x,y,

xor x,y=zero→x=y.

Proof.

smt4coq.

Qed.

(a) 原始证明代码 (b) 使用 smt4coq 的证明代码

Fig.1 An example using smt4coq

图 1 smt4coq 策略使用效果示例

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn

Journal of Software,2017,28(4):819−826 [doi: 10.13328/j.cnki.jos.005196] http://www.jos.org.cn

基于 Z3 的 Coq 自动证明策略的设计和实现

∗

张恒若

付

明

2,3

(中国科学技术大学信息科学技术学院,安徽合肥 230026)

(中国科学技术大学计算机科学与技术学院,安徽合肥 230026)

(中国科学技术大学苏州研究院软件安全实验室,江苏苏州 215123)

通讯作者: 付明, E-mail: fuming@ustc.edu.cn

摘要: 形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来

验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高;而

使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动

化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.结合上述两种方式的优点,在定理证明工具 Coq

中实现了一个自动证明策略 smt4coq,它通过在 Coq 中调用约束求解器 Z3 自动证明 32 位机器整数相关的数学命题,

提高了自动化验证的程度,减少了用户手动验证程序的开销.

关键词: 形式化验证;定理证明工具;约束求解器;Coq;Z3

中图法分类号: TP311

中文引用格式: 张恒若,付明.基于 Z3 的 Coq 自动证明策略的设计和实现.软件学报,2017,28(4):819−826. http://www.jos.org.

cn/1000-9825/5196.htm

英文引用格式: Zhang HR, Fu M. Design and implementation of Coq tactics based on Z3. Ruan Jian Xue Bao/Journal of Software,

2017,28(4):819−826 (in Chinese). http://www.jos.org.cn/1000-9825/5196.htm

Design and Implementation of Coq Tactics Based on Z3

ZHANG Heng-Ruo

, FU Ming

2,3

(School of Information Science and Technology, University of Science and Technology of China, Hefei 230026, China)

(School of Computer Science, University of Science and Technology of China, Hefei 230026, China)

(Software Security Laboratory, Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou 215123,

China)

Abstract: Formal verification is an effective approach to construct high confidence software. Verifying the functional correctness of

complex system software by manually writing proof scripts in proof assistant tools is feasible with the low degree of automation, and the

verification cost is relatively high. The automatic program verifiers verify programs by taking the annotated source code as their input to

generate verification conditions automatically solved by SMT solvers. This approach has a high degree of automation, but it is impossible

to verify the functional correctness of the entire system software. By combining the advantage of the above two methods, this paper

implements a novel Coq tactic plug-in named “smt4coq”, which allows calling the Z3 SMT solver in Coq to automatically prove

mathematical propositions involved with 32-bit machine integers. The new tactic improves the degree of automation and reduces the cost

of manual verification.

Key words: formal verification; proof assistant tool; SMT solver; Coq; Z3

∗ 基金项目: 国家自然科学基金(61103023, 61229201, 61379039, 91318301, 61632005)

Foundation item: National Natural Science Foundation of China (61103023, 61229201, 61379039, 91318301, 61632005)

收稿时间: 2016-06-20; 修改时间: 2016-09-08; 采用时间: 2016-11-26; jos 在线出版时间: 2017-01-24

CNKI 网络优先出版: 2017-02-20 13:43:28, http://www.cnki.net/kcms/detail/11.2560.TP.20170220.1343.003.html

820

Journal of Software 软件学报 Vol.28, No.4, April 2017

作为信息产业的核心技术,软件系统被广泛地应用于航空航天、核电、军工、高铁、医疗、金融、自动驾

驶等安全攸关的国家战略基础设施和人们的日常生活中.高可信软件系统成为保障国家安全、保持经济可持续

发展、维护社会稳定和保护人民生命财产安全的必要条件.

近几年来,形式化验证方法被认为是一种构建高可信软件系统的有效手段,相关的验证理论和支撑工具都

有了较大的发展.在验证理论方面,程序精化验证理论

[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)所示为直接

使用本文开发的 sm

t4coq 策略进行自动证明.

Theorem xor_zero_equal:

forall x,y,

xor x,y=zero→x=y.

Proof.

intros.apply same_bits_eq.

intros.assert(xorb(testbit x,i)(testbit y,i)=false).

rewrite←bits_xor; auto.

rewrite H.apply biths_zero.destruct(testbit x,i).destruct(testbit y,i).

reflexivity||discriminate.

Qed.

Theorem xor_zero_equal: forall x,y,

xor x,y=zero→x=y.

Proof.

smt4coq.

Qed.

(a) 原始证明代码 (b) 使用 smt4coq 的证明代码

Fig.1 An example using smt4coq

图 1 smt4coq 策略使用效果示例

of 8

免费下载

软件学报计算机技术

关注

评论