形式化验证方法研究综述

摘要：形式化验证是证明软件、硬件或系统正确性的一种方法，近年来受到了越来越多的关注。本文对形式化验证的研究进行了综述。首先介绍了形式化验证的基本概念，然后重点介绍了形式化验证的三种技术，包括模型检测、定理证明和等价性验证等。此外，通过两篇论文介绍了形式化验证在软件和硬件系统开发中的应用和实现、形式化验证工具的发展和使用。最后，对形式化验证的未来发展进行了展望，认为人们应该不断探索新的理论和工具，以提高形式化验证的效率和可用性。

关键词： 形式化验证；形式化方法；软件开发；研究综述

一、引言

现如今计算机硬件性能变得越来越高、运算速度变得越来越快、体系结构变得越来越复杂，软件的功能也变得越来越强大而复杂，如何开发可靠的软、硬件系统已经成为计算机科学发展的巨大挑战，特别是现在计算机系统已广泛应用于许多关系国计民生的安全攸关系统中，例如高速列车控制系统、航空航天控制系统、核反应堆控制系统、医疗设备系统等等，这些系统中的任何错误都可能导致灾难性后果。

计算机系统的设计开发需要分析、处理、证明计算机硬件和软件系统的性质。形式化方法以形式(逻辑)系统为基础，支持对计算机系统进行严格的规约、建模和验证，并且为此设计算法从而建立计算机辅助工具。在现代计算机系统的开发过程中，形式化方法在不同的阶段、以不同的形式和程度得以应用，例如：在基于模型的软件开发中，建模、模型精化和基于模型的测试都是基于形式化方法的思想和技术发展起来的；程序语言的类型设计、程序分析的算法都是形式化方法中的基本技术[1]。

形式化方法最显著的作用是能够对形式规约进行验证。形式验证常见的有两种形式：一种是推理“系统模型规约是否满足其性质规约”，此时模型规约偏向操作型，性质往往是说明型的；另一种是推理“系统的一个模型规约是否与另一模型规约有精化或等价关系”。这些推理过程给出了一套静态方法来预测系统的行为：用户可以描述系统行为的所期望性质或者开发过程中不同抽象之间关系的猜想，形式验证通过机械化的方式来证实或者证伪这个性质或者猜想，从而提高用户对规约和系统的可信程度。

二、形式化验证方法

形式验证方法主要包括定理证明、模型检验和模型等价性验证，下面笔者将从上述三种方法进行详细介绍。

2.1 定理证明

基于定理证明的形式验证将“系统满足其规约”这一论断作为逻辑命题，通过一组推理规则，以演绎推理的方式对该命题开展证明。基于定理证明的验证大部分是以程序逻辑为理论基础的，但是程序逻辑并非唯一的验证方法，例如我们可以基于程序的操作语义直接表达程序执行的安全性、正确性等各种性质并证明相关定理[2]。

按照证明方式和自动化程度的不同，基于定理证明的验证又可以分为两类，即基于自动定理证明器的自动验证和基于人机交互的半自动验证。

2.1.1 基于自动定理证明器的自动验证

随着自动证明理论的发展和计算机处理器能力的大幅增强，自动定理证明器的能力得到大幅提升，基于自动定理证明的验证也得到很大发展。目前常见的程序证明器包括 Dafny、Why3、VeriFast、Smallfoot 等。这些程序证明器大多基于某种具体的程序逻辑。给定程序及其规约，证明器能够自动决定针对程序的每条语句使用程序逻辑中的何种公理或规则，并产生相应的验证条件作为证明义务。最终产生的验证条件被送到自动定理证明器中，由定理证明器完成对验证条件的证明。目前使用最广泛的定理证明器是微软开发的Z3，其他常见的证明器还包括CVC4、Yices2 等。使用各种定理证明器和自动化程序验证技术，人们已经实现了对一些相对实用的、较大规模的具体系统的验证。

基于自动定理证明的验证工作的优点在于验证的效率较高，不需要人手工写证明。然而由于自动定理证明中很多问题是不可判定问题，而且各个定理证明器又有各自的能力限制，因此能够表达和证明的性质有限。为了能够实现自动证明，很多时候需要对待证明的性质和待验证的代码本身都进行重写，甚至为了迁就验证的自动化而牺牲待验证的性质以及代码的功能。

2.1.2 基于人机交互的半自动验证

基于定理证明的另一类验证工作，则不强调使用计算机实现验证的自动化，而是利用计算机来解决证明在计算机中的表示问题以及自动检查证明的正确性的问题，证明的构造则由人手工和机器交互，以半自动化的方式完成。很多辅助定理证明工具如Coq[3]和Isabelle/HOL等，都是针对这一目的进行开发的。这类工具往往是利用类型系统和逻辑之间的Curry-Howard 同构关系[4]，将构造证明的过程转化为编写程序的过程，而证明的正确性检查也变成了类型检查问题。

这类人机交互的半自动化验证工作往往需要大量的手工劳动来构造证明，虽然在辅助定理证明工具中提供了一些基本的证明策略和引理库来减少证明负担，但在实际代码的验证中，往往平均一行程序需要手工书写20~30行证明脚本。然而这种方法的优点在于无需牺牲规约和代码的表达能力，特别是程序规约可用表达能力很强的逻辑(如在Coq[3]和Isabelle/HOL中使用的高阶逻辑)来表示。而且证明自身在机器中有显式表示，其正确性可以被自动检查，因而我们无需依赖自动定理证明算法的正确性，验证的结论也就更加可信。

2.2 模型检验

定理证明中，形式验证把待证明的性质直接作为了一个数学定理来证明，也称为演绎式验证。与演绎式相对应的一种方式是模型检验。模型检验的其基本思想是：检验一个结构是否满足一个公式要比证明公式在所有结构下均被满足容易得多，进而面向并发系统创立了在有穷状态模型上检验公式可满足性的验证新形式[5]。

图1[6]是模型检测验证方法示意图。首先根据设计搭建形式验证模型，然后根据设计要求编写断言属性和相关的约束，再将模型和约束合并成为符合验证需求的形式验证模型。接着加入需要验证的设计，运用形式验证工具进行验证，此时形式验证工具会根据约束自动遍历所有需要被验证的状态，如果所有的断言都成立则设计正确，反之设计错误，工具发现错误时可以提供错误场景帮助验证人员分析错误。根据形式验证结果分析覆盖率状况，并通过分析后的结果优化形式验证环境，提高形式验证覆盖率。
在这里插入图片描述
图2[6]是模型检测查错示意图，在模型检测时首先是根据设计需求定义输入可以搜索的状态范围，在状态搜索过程中工具会首先建立一个初始状态，并进行扩展进入下一个状态，除非有明确的状态约束，否则扩展将一直进行。在查找过程中可能会出现状态重复的情况，但是不管过程如何，工具都会遍历所有的状态空间，然后工具会将所有状态的输出值和模型检测中的标准值进行对比检查，在进行断言检查的过程中，如果出现了输出值不符合断言属性的状况，模型检测工具会反方向运行，推导出出错时的输入状态，这就是上文中提到的工具给出反例的原理。
在这里插入图片描述
设计建模和形式规约是模型检测方法搭建形式验证环境的重要环节。在模型检测中为了验证设计首先需要理解设计规范和验证需求，在此基础上编写设计等价参考模型。通常情况下参考模型会比设计更加抽象，模型仅仅是为了描述预期的结果。在验证的过程中可以把设计模块分解成小的、方便验证的模块，但同时也要保证分解后的任意模快之间状态逻辑和状态空间的吻合[7]。因此在验证时为了防止产生状态爆炸，在保证验证合理性的前提下，可以对状态空间进行划分，使得验证更加简单快速。模型检测时形式验证工具将根据形式规约来判断相关属性的正确性。形式规约是用具有精确语义的形式化语言描述设计性质，形式规约的状态将影响模型检测的一致性和完备性。一致性指的是与验证目标无矛盾，完备性指的是是否完全无遗漏地描述出了目标属性。

2.3 等价性检验

等价性验证是目前形式验证方法中运用最为普遍的验证技术。等价性验证不仅拥有形式验证全遍历和验证速度快的特点，而且等价性验证的自动化程度也很高，验证工具操作简单。虽然等价性验证的优点很多，但是这种验证方法不能用来验证设计的功能正确性，因为等价性验证方法的原理是通过对比不同阶段设计之间的等价性，从而达到验证的目的。在形式验证中由于数学逻辑分析的方法是抽象的，所以验证不会受到不同描述语言的限制，可以验证不同描述方式之间设计的等价性[8]。即等价性验证只能检测芯片不同设计阶段之间有没有产生错误，而不能检测出不同阶段设计的共同错误。等价性验证在芯片设计流程中通常用于RTL和RTL、门级与RTL、门级和门级以及版图和门级之间的错误分析[9]。

三、相关论文研究

本章将简单介绍笔者阅读过的两篇关于形式化验证的论文，在介绍的过程中着重阐述文献中具体的案例分析。

3.1 Ptolemy离散事件模型形式化验证方法[10]

3.1.1 基本思想

Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包，主要通过仿真的方式保证所建模型的正确性。文中提出了一种基于形式模型转换的方法来验证离散事件模型的正确性。离散事件模型根据不同事件的时间戳触发组件，时间自动机模型能够表达这个特征，因此选用Uppaal作为验证工具。首先定义了离散事件模型的形式语义；其次设计了一组从离散事件模型到时间自动机的映射规则；然后在Ptolemy环境中实现了一个插件，可以自动将离散事件模型转换为时间自动机模型，并通过调用Uppaal验证内核完成验证。与现有研究工作相比,该方法定义了更为完整的Ptolemy组件转换规则，可以支持更多的组件；保留了模型层次化的特点，有效避免了状态空间爆炸；避免使用tick计时，降低验证的复杂度；在Ptolemy环境中设计实现了一个自动转换验证的插件,完善了使用Ptolemy进行模型驱动开发的工具链。

其中Ptolemy DE模型验证整体框架如图3[10]所示，可分为转换模型和形式化验证两部分：
（1）在模型的自动转换阶段，将Ptolemy DE模型和根据模型提取的属性验证公式作为输入，首先对Ptolemy DE模型进行解析,获得各个组件的结构信息；然后根据定义的映射规则，将各个组件转换为对应的时间自动机；最终将时间自动机与属性验证公式共同构成一个可进行验证的时间自动机网络结构。
（2）将内存中的时间自动机网络结构输出文件，即可调用Uppaal验证引擎进行验证。
在这里插入图片描述
3.1.2 交通信号灯案例分析

在一个交通信号灯系统中，指示车辆行动的信号灯有红、黄、绿这3种，指示行人行动的指示灯有红、绿这两种。当系统正常工作时：汽车指示灯按照红、黄、绿、黄的顺序变换，分别停留3，1，2，1个时间单元；行人指示灯根据汽车指示灯的变换而变换：当汽车指示灯由红变黄时，行人指示灯变红；当汽车指示灯由黄变红时，行人指示灯变绿。有时系统会出现故障，此时只有指示汽车暂停行驶的黄灯闪烁，其他指示灯都灭。

如图4[10]所示，Ptolemy DE模型中定义了5个参数：Pred，Pgrn，Cred，Cyel和Cgrn，分别表示不同的交通灯：当值为1时，表示其对应的交通灯亮；值为0时，表示其对应的交通灯灭。如图中参数Pred和Cyel值为1，则行人红灯和车辆黄灯亮。DiscreteClock是一个事件源组件，以1为周期产生输出信号，Decision是一个异常生成器，TrafficLight是交通灯控制器，SetVariable组件用于更新参数值。其中，组件TrafficLight交通灯控制器是一个模态模型，有两个状态normal和error，状态normal和error各有一个细化模型。TrafficLight normal是TrafficLight中normal状态的一个细化模型，表示系统在正常情况下，交通灯控制器的详细模型，包含两个控制器：车辆交通灯控制器CarLightNormal和行人交通灯控制器PedestrianLightNormal。
在这里插入图片描述
通过提取Ptolemy DE模型中的属性特征，形式化描述为CTL公式，进而使用Uppaal验证的引擎对模型的可靠性、安全性、死锁进行形式化验证。表1[10]是上述验证公式详细的验证情况，当时间自动机模型中有不满足的属性时，Uppaal验证引擎可以返回异常路径。

在这里插入图片描述
3.2 面向MSVL的智能合约形式化验证[11]

3.2.1 基本思想

智能合约是运行在区块链上的计算机协议，被广泛应用在各个领域中，但是其安全问题层出不穷，因此在智能合约部署到区块链上之前，需要对其进行安全审计。然而，传统的测试方法无法保证智能合约所需的高可靠性和正确性。文章提出一种基于时序逻辑语言(MSVL)的智能合约安全性的模型检测方法：首先使用MSVL对智能合约程序进行建模，为了减少建模时大量的人工操作，开发了将智能合约语言Solidity转换为MSVL的转换器工具SOL2M，实现了智能合约建模程序的自动化生成；然后使用命题投影时序逻辑(PPTL)公式描述该智能合约的安全性性质；最后在统一模型检测器(简称UMC4M)中自动化验证建模程序是否满足给定的安全性性质，并通过实例说明该方法运用到智能合约验证中的可行性和实用性。

其中，转换器工具SOL2M的具体结构以及工作流程如图5[11]所示。SOL2M转换器主要分为4个部分：
(1)预处理：处理Solidity源程序中的版本标识语句和导入其他源文件语句；
(2)词法分析：通过JavaCC工具生成词法分析器，对Solidity程序进行词法分析，将源程序识别为特定的单词流；
(3)语法分析：通过JavaCC工具生成语法分析器，对Solidity程序进行语法分析，把词法分析生成的单词流识别为程序语句；
(4)程序转换：通过分析Solidity和MSVL的词法以及语法的异同，制定出Solidity到MSVL的转换规则，并将转换代码嵌套在语法分析的BNF范式中，实现Solidity程序到MSVL程序的动态转换。
在这里插入图片描述

3.2.2 银行转账合约案例分析

以具体的银行转账智能合约与常见的重入攻击漏洞为例，给出SOL2M对转账合约与重入攻击进行建模的详细流程以及验证过程。建模时，在银行转账合约中抽象加入了重入攻击操作，即将转账合约与重入攻击代码抽象为合约。如图6[11]所示，其中deposit函数的功能是用户把钱存入银行，withDraw函数实现了转账功能，用户通过withDraw函数与send函数从银行取钱。Attack函数实现了重入攻击的功能，其具体步骤为：首先攻击者调用Attack函数，通过deposit函数向银行转账合约中存入一些以太币；之后调用withDraw函数，从银行转账合约中取钱，使用require语句判断用户余额以及银行总余额是否足够；最后调用send函数给用户地址转账。
在这里插入图片描述