李希萌(1987-), 男, 博士, CCF专业会员, 主要研究领域为形式化方法, 软件验证
王国辉(1984-), 男, 博士, 高级实验师, CCF专业会员, 主要研究领域为形式化验证, 高可靠嵌入式系统
张倩颖(1986-), 女, 博士, 副教授, CCF专业会员, 主要研究领域为形式化验证, 系统安全, 操作系统
施智平(1974-), 男, 博士, 教授, 博士生导师, CCF高级会员, 主要研究领域为形式化方法, 人工智能
关永(1966-), 男, 博士, 教授, 博士生导师, CCF专业会员, 主要研究领域为形式化验证, 高可靠嵌入式系统, 机器人
各类安全攸关系统的可靠运行离不开软件程序的正确执行. 程序的演绎验证技术为程序执行的正确性提供高度保障. 程序语言种类繁多, 且用途覆盖高可靠性场景的新式语言不断涌现, 难以为每种语言设计支撑其程序验证任务的整套逻辑规则, 并证明其相对于形式语义的可靠性和完备性. 语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果. 对每种程序语言, 提供其形式语义后可直接获得面向该语言的程序验证过程. 提出一种面向大步操作语义的语言无关演绎验证技术, 其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法. 特别地, 借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力, 从而允许借助辅助信息对子结构进行推理. 证明所提出验证技术的可靠性和相对完备性, 通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性, 并在Coq辅助证明工具中形式化了所有理论结果和验证实例, 为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.
The reliable functioning of safety-critical IT systems depends heavily on the correct execution of programs. Deductive program verification can be performed to guarantee the correct execution to a large extent. There are already a plethora of programming languages in use, and new languages oriented toward high-reliability scenarios are still being invented. As a result, it is difficult to devise a full-fledged logical system for each language to support the verification of programs and prove the soundness and completeness of the logical system with respect to the formal semantics of the language. Language-independent verification techniques offer sound verification procedures parameterized over the formal semantics of programming languages. The specialization of the verification procedure with the formal semantics of a concrete programming language directly gives rise to a verification procedure for the language. This study proposes a language-independent verification technique based on big-step operational semantics. The technique features a unified procedure for sound reasoning about program structures that potentially cause unbounded behavior, such as iteration and recursion. In particular, the study employs a functional formalization of big-step operational semantics to support the explicit representation of the computation performed by the sub-structures of a program. This representation enables the exploitation of the auxiliary information provided for these sub-structures in the unified reasoning process. In addition, the study has proved the soundness and relative completeness of the proposed technique, evaluated the technique by verification examples in imperative and functional programming languages, and formalized all theoretical results and verification examples in the Coq proof assistant, and thus provides a basis for developing a language-independent program verifier with big-step operational semantics based on a proof assistant.
软件程序的正确性是影响各类安全攸关系统可靠性的重要因素之一. 为提供最高级别的正确性保障, 往往使用形式化方法[
对程序进行演绎验证的基本方法是直接以某种操作语义[
一类有效简化程序演绎验证的语义定义方式是公理语义[
语言无关(language-independent)的程序验证技术[
当前支持以辅助证明工具为平台进行语言无关程序验证的技术[
本文提出一种能够基于大步操作语义进行程序验证的语言无关验证技术. 语言无关的程序验证过程并不依赖于程序语言的语法结构, 而是在语义层面利用程序中关键子结构执行相关的辅助信息, 完整证明任务. 小步语义描述程序的单步执行
本文所提出技术包含以函数式大步操作语义为参数的验证过程及其可靠性定理. 验证过程将目标语言中程序的验证转化为依托辅助信息的符号执行. 所需辅助信息仅为关于程序中部分关键结构(如循环、递归函数)的局部信息, 其作用类似于各种程序逻辑所需要的循环不变式和函数契约. 本文给出该技术的可靠性证明, 即若程序得到验证, 那么程序满足部分正确性性质(partial correctness)[
本文主要贡献可归结为如下4个内容.
● 一个以程序语言的函数式大步语义为参数的可靠的程序验证过程.
● 验证过程可靠性和相对完备性的证明.
● 使用验证技术对不同范式程序语言的简单程序实例进行验证的过程和结果.
● 所有理论结果和程序验证实例在Coq辅助证明工具中的形式化.
本文第1节具体讨论主要相关工作. 第2节介绍预备知识和符号约定. 第3节给出基于函数式大步操作语义的语言无关验证技术并证明其可靠性. 第4节依托简单命令式语言While, 介绍证明技术的具体使用方法. 第5、6节给出含数组的卫式命令语言GCarr以及含列表的函数式语言Funlst中的进一步实例.第7节给出验证技术的相对完备性结果及其证明. 第8节讨论本文所提出技术的其他方面, 包括其局限性. 第9节总结全文.
Moore提出一种对程序进行演绎验证的技术[
Moore等人提出一种在形式规约中辅助信息帮助下通过符号执行对程序进行可靠验证的技术[
先于文献[
由于本文所提出技术基于程序的大步而非小步执行模型, 故较难用来处理程序语言中的并发特性. 而另一方面, 大步执行模型的定义及其在证明中的使用往往相对简单, 如在大步操作语义中, 一般无需通过引入额外程序语句对控制流状态进行记录; 在其使用中, 亦无需同时关注推导树和规约序列. 大步语义同样具有广泛用途.
通过将被验证程序由某种形式语言进行表示, 进而使用该形式语言的验证技术和工具对对象程序进行验证, 亦可得到适用于多种不同语言的验证工具. 此处形式语言可以为某种演算, 如
程序逻辑相关研究工作是程序演绎验证方面的重要工作, 既有研究成果众多, 在本文范围内无法进行详细讨论. 基本的霍尔逻辑[
程序语言的大步操作语义(或大步语义)描述各类语法结构如何执行操作, 将初始状态转化为终止状态. 典型的初始状态包括程序的控制结构(控制状态)和各个变量的初始值(变量状态). 控制状态和变量状态的组合通常称为语义格局(configuration). 表示初始状态的语义格局称为初始格局(initial configuration). 典型的终止状态给出各个变量的终值. 考虑命名的一致性, 下文将终止状态称为终止格局(terminal configuration).
大步操作语义可借助一系列语义规则进行纸笔定义. 下面以While语言[
While语言是一种高度简化的命令式语言. 其语法结构包括算术表达式
While语言的大步语义规则如
The rules for the big-step operational semantics of the While language (pen-and-paper formulation)
While语言大步操作语义的语义规则(纸笔定义形式)
使用语义规则推导从某个初始格局(
大步操作语义所描述的初始格局与终止格局间的二元关系实为使用语义规则所能推出的最小的初始格局、终止格局对的集合, 理论上可通过最小不动点进行刻画. 然而进行大步操作语义相关的理论证明或者使用大步操作语义进行程序证明时, 往往使用推导树形状上的归纳法[
形式语义的定义工作以及基于形式语义的程序证明工作往往较为繁琐, 容易出错. 辅助证明工具(proof assistant)[
本文使用记号
设
设
(1) 当
(2) 当
以下给出用
本程序计算变量
具体化初始格局集合
Φ
Φ
形式规约Φ
上述形式规约中, 在条件
若使用大步操作语义直接证明规约Φ
某种程序语言大步操作语义的纸笔定义通常由一系列如下形式的语义规则构成.
直观上, 该规则表示在借助逻辑谓词
现考虑通过函数定义对大步语义进行形式化. 具体引入一个函数
若函数
以下给出使用函数
The function h formalizing the big-step semantics of the While Language
形式化While语言大步语义的函数
下面基于用函数
定义
本定义中, 实际要求∀
虽然本节仅给出使用函数
定义函数
直观上, 当形式规约Φ未能给出关于从初始格局
以下基于函数
定义
在本定义中, 实际要求∀
为保证验证的可靠性, 以下证明⊢Φ到⊨Φ的逻辑蕴含. 该证明无需假设
定义
直观上不难看出, 若函数
以下证明一关键引理.
引理
证明: 在
若
若
(
=
=
=
≥
≥
=
上述引理指出若形式规约Φ能够得到验证, 那么对任何
定理
基于由单调函数
本节使用定理1证明第3.1节中给出的While语言阶乘程序的形式规约得到满足, 并讨论本文技术对循环结构的处理方式与霍尔式程序逻辑的差异.
关于第3.2节中While语言大步语义的形式化, 容易证明下列引理.
引理
本引理的证明转化为对任意满足
以下讨论第3.1节中形式规约Φ
(1) 若
(2) 若
(
=
=
= {
= {
= {
= {
= (((
= Φ
= {
= {
⊆ Φ
(3) 若
(
=
(i) 若
(ii) 若
RHS = {
= {
= {
= {
∃
= {
= {
= {
= (((
= Φ
= {
⊆ Φ
以上计算过程中, 倒数第4行之前的步骤对循环
定理
由本定理的证明过程可见, 虽然条件⊢Φ
以下结合本例和
Comparison of usual loop invariants and loop specifications in the proposed technique
程序逻辑中循环不变式与本文循环规约的比较
在已有相关工作中, 文献[
本节考虑带有声明和一维数组扩展的非确定性卫式命令语言GCarr[
带有声明、一维数组扩展的卫式命令语言GCarr语法如下, 其中
上述语法中
程序状态
具体化初始格局集合
The function h formalizing the big-step semantics of the language GCarr
形式化卫式命令语言GCarr大步语义的函数
图中表达式
引理
本引理的证明使用与While语言中对应引理(引理2)的证明相同的策略, 证明过程简单机械. 在本引理基础上, 即可使用定理1对GCarr语言程序进行可靠证明.
考虑下列卫式命令语言程序
var
do
if
od
以下通过形式规约描述该程序的功能正确性条件, 并提供关于循环的辅助信息. 其中,
Φmax (
Φmax (
若 0 ≤
Φmax
其中, Φmax (
以下给出Φmax的正确性结果及其证明思路. 详细证明过程包含在本工作的Coq形式化中.
定理
本定理的证明中, 使用定理1将对⊨Φmax的证明任务转化为对⊢Φmax的证明任务, 而后者通过检查(
定理1在本定理的证明中保障了基于化简的证明策略的可靠性. 定理1无需对GCarr语言单独证明, 而是在确认GCarr语言语义函数
本节考虑一个可对列表进行操作的函数式语言Funlst, 通过定义函数
语言Funlst为文献[
这里
具体化初始格局集合
The function h formalizing the big-step semantics of the language Funlst
形式化函数式语言Funlst大步语义的函数
对
引理
本引理的证明使用与While语言中对应引理(引理2)的证明相同的策略, 证明过程简单机械. 在本引理基础上, 即可使用定理1对Funlst语言程序进行可靠证明.
考虑
The program that merges sorted lists in the language Funlst
以Funlst语言编写的有序表合并程序
对一个Funlst语言表达式
对程序
Φmg
若有 (|
Φmg
若有 (|
上述形式规约中前两行要求只要
直观上, 表达式
以下直接给出Φmg的正确性结果. 详细证明过程包含在本工作的Coq形式化中.
定理
本定理的证明中, 使用定理1将对⊨Φmg的证明任务转化为对⊢Φmg的证明任务, 而后者通过(
本文第3节中, 给出了一种适用于循环和递归程序结构推理的通用证明技术, 并且证明了该技术的可靠性. 此后在第4–6节中, 通过程序验证实例初步体现了该技术在处理不同范式程序语言、不同程序结构方面的适用性. 然而, 若要系统性考察证明技术的适用范围, 则须考虑其完备性——是否对任意的形式规约Φ, 若该规约得到满足(⊨Φ), 则该规约能够用该技术证明(⊢Φ). 不难发现, 这一命题并不成立. 对第4节中的阶乘计算程序
仍然考虑
定义
与已有工作(如文献[
定义形式规约Φ↑:=
引理
证明: 以下证明对任意自然数
若
以下假设
(
=
=
≤
=
=
=
=
≤
= Φ↑ 证毕.
定理
证明: 以下证明, 可以使用Φ↑作为满足定理所要求条件的Φ
首先证明Φ≼Φ↑. 由⊨Φ可得, ∀
本定理及其证明并未说明对于一个得到满足的形式规约Φ, 若Φ无法得到证明, 需对Φ所提供信息进行精确化(使之能够得到证明)的最低限度. 直观上, 所需提供的辅助信息应能帮助对可能产生无界行为(unbounded behavior)的程序结构进行推理, 如循环结构、递归函数等, 但通常无需提供进一步的信息, 这是因为若不考虑效率问题, 其他程序结构的推理可借助符号执行加以完成.
最后, 不难证明用来形式化While语言、GCarr语言、Funlst语言大步操作语义的函数
定理
不难证明, 只要
定理6表明, 基于第4–6节中所定义的While语言、GCarr语言、Funlst语言的语义, 获得了定理5意义上相对完备的验证过程. 值得注意的是, 定理1的成立, 以及第4–6节中具体实例验证结果并不依赖于
本文所提出技术与抽象解释方法[
抽象解释是极具表达力和灵活性的形式化程序分析方法. 一般而言, 形式化方法不同领域的技术可存在深层次的关联(如文献[
相较于小步语义, 大步语义常可省去语义格局中的复杂控制信息, 如函数调用栈等. 语言无关的程序证明技术建立在语义格局这一抽象概念上, 无法将程序规约信息标注在具体程序的语法结构中. 故若语义格局中存在调用栈等控制结构, 则使用语言无关的程序证明技术往往需要在形式规约中引入这些控制结构. 因此, 基于大步语义的语言无关程序验证技术有利于简化在程序证明过程中关于语义格局所需考虑的信息.
对某种程序语言, 一个经验性结论是若该语言具有大步语义, 则亦应能定义其小步语义, 并证明其与大步语义等价. 故若某种程序语言已有大步语义, 则可尝试定义其小步语义, 完成等价性证明, 并使用基于小步语义的语言无关程序证明方法验证该语言程序. 然而, 对于实用程序语言, 小步语义的定义和形式化(如文献[
在指称语义中, 显式刻画单调函数迭代的不动点, 本文所提出的验证技术亦涉及单调函数的迭代, 但该技术与基于指称语义的程序验证技术亦有如下重要区别.
本文中迭代的函数
在指称语义中, 需要显式刻画其最小不动点的函数不同于本文中的函数
本文所提出技术适用于许多主流辅助证明工具(proof assistant), 如Coq、Isabelle/HOL、HOL4等. 然而其程序规约和验证条件中所涉及的无穷集合、逻辑量词等特性使其难以直接借助一般编程语言实现为自动化程序验证工具. 文献[
本文所提出技术适用于部分正确性条件[
由于本文的验证技术基于程序的大步语义, 该技术较难用于并发程序验证, 除非在语义设计中将终止格局设置为程序所有可能执行路径前缀的集合, 借以反映程序执行的中间状态.
程序的演绎验证技术能够可靠验证程序的复杂性质, 然而该技术的使用具有较大难度. 难点之一在于, 对不同程序语言, 其演绎验证系统的可靠性需要单独进行证明. 语言无关的程序验证技术[
注意到任何程序语言的大步操作语义均可形式化为一个函数, 刻画其语义推导树或其子树的顶层构造. 以此为切入点, 本文解决了依托大步语义为程序子结构的执行提供辅助信息的问题, 提出了基于大步语义的语言无关程序验证技术. 该技术的核心是一个以程序语言的函数式大步操作语义为参数的验证过程以及该验证过程的可靠性定理. 对于某种具体的程序语言, 以函数形式提供其大步操作语义后, 即可直接得到对该语言具体化的程序验证过程及其可靠性定理, 将程序的演绎验证任务转化为在形式规约中辅助信息帮助下对程序的符号执行和对结果的检查. 形式规约中所需辅助信息仅为循环、递归函数等的不变式和契约——类似于使用语言特定的程序逻辑进行验证所需的辅助信息. 不同范式下确定性、非确定性程序语言中的程序验证实例初步体现了本文所提出技术的有效性. 在Coq辅助证明工具中, 所有理论结果和程序验证实例均得到了机械化验证, 而本文所提出技术亦可在Isabelle/HOL、HOL4等基于高阶逻辑的辅助证明工具中进行形式化.
本工作为基于辅助证明工具的语言无关程序验证工具的实现提供基础. 若要完整实现此类工具, 使之能够有效处理针对实用程序语言的验证任务, 仍需在核心定理的基础上集成额外组件, 以简化关于内存布局、对象等常见语言特性的推理, 并支持依托领域知识(如数学理论)的推理. 对此, 程序逻辑以及辅助证明工具定理库方面的研究成果将具有宝贵借鉴价值. 未来工作的一个重要方向即是探究如何集成对非跨语言共享特性的推理能力和基于领域知识的推理能力, 并通过进一步的实例程序验证来检验其推理能力的增强.
http://www.jos.org.cn/1000-9825/5652.htm]]>
http://www.jos.org.cn/1000-9825/5652.htm]]>
Harrison J, Urban J, Wiedijk F. History of interactive theorem proving. Handbook of the History of Logic, 2014, 9: 135–214. [doi: 10.1016/B978-0-444-51624-4.50004-6]
Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B. Frama-C: A software analysis perspective. Formal Aspects of Computing, 2015, 27(3): 573–609. [doi: 10.1007/s00165-014-0326-7]
Jung R, Krebbers R, Jourdan JH, Bizjak A, Birkedal L, Dreyer D. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 2018, 28: e20. [doi: 10.1017/S0956796818000151]
Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10): 576–580. [doi: 10.1145/363235.363259]
Dijkstra EW. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 1975, 18(8): 453–457. [doi: 10.1145/360933.360975]
http://www.jos.org.cn/1000-9825/6238.htm]]>
http://www.jos.org.cn/1000-9825/6238.htm]]>
Jones CB. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 1983, 5(4): 596–619. [doi: 10.1145/69575.69577]
Blazy S, Leroy X. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 2009, 43(3): 263–288. [doi: 10.1007/s10817-009-9148-3]
http://www.jos.org.cn/1000-9825/6246.htm]]>
http://www.jos.org.cn/1000-9825/6246.htm]]>