鉴源论坛 · 观模丨形式化验证——以操作系统任务调度算法验证为案例

作者 |蔡雄 上海控安可信软件创新研究院研发工程师

版块 | 鉴源论坛 · 观模

形式化方法是基于严格的数学基础，通过采用数学逻辑证明来对计算机软硬件系统进行建模、规约、分析、推理和验证，是用于保证计算机软硬件系统正确性以及安全性的一种重要方法。形式化方法是基于严格定义的数学概念和语言，其描述软件及其性质的语言是无歧义的，构造和验证方法是严格的。加上形式化方法在开发过程具备良好的可重复性，并且相应的模型软件也具有比较强的可分析性和可验证性，可以很好地支持抽象模型建立、系统精化、模型和证明重用，有效地提高和保障系统的可信性。

图1 验证与分析框架

其中主要将验证与分析框架划分为三个部分：

（1）利用VCC做单元级别的函数验证，基于软件架构设计规范及软件详细设计规范等文档，选取适用的审查、分析或测试等方法，验证软件单元设计和实施的正确性和一致性；

（2）利用CBMC做多个函数的集成验证，集成验证主要是针对软件高层设计进行验证，一般来说是对模块和子系统为单位进行验证，验证每个函数调用其他函数时，调用者的规范能否满足；

（3）利用PAT做系统验证，确认整个系统是否满足了软件规格说明中的功能性和非功能性的各项需求，以及满足的程度，系统验证应能够发现和找出因需求不正确、不完整或实现与需求之间的不一致而引起的失效，并识别在没有文档化时或被遗失的那些需求，验证系统在运行时能否满足要求的性质。

01

VCC

VCC(Verified C Compiler)是一个针对C语言程序的验证工具。VCC提供了用于描述C语言函数的前置条件、后置条件、不变式等函数规约的接口。VCC是在原始C语言的基础上进行撰写函数约束对C代码进行进一步的完善C语言更深层次的属性。其对约束内容可以划分为对一阶逻辑表达式的约束和指针的约束。

为了验证程序的正确性，VCC使用演绎验证模式。它生成一定数量的数学表达式(称为验证条件)，并试图使用一个自动定理验证器来验证这些数学表达式。如果验证失败，VCC会将失败的原因反映到用户的程序代码身上。因此，用户通常是在代码和程序状态层面与VCC交互的。通常情况下，用户可以忽略在VCC内部的数学推理。例如，如果待验证的程序使用了除法，如果VCC无法证明除数一定非零，它会报告待验证的程序有(潜在的)错误。这并不意味着程序必然是不正确的。通常，可以通过增加注释和断言来解决这个“错误”。不过这可能又会导致其他的错误报告，迫使用户添加更多的注释。所以实际的验证是一个迭代的过程。

如图2所示，VCC的主要工作过程分为两个步骤。

第一步，VCC工具将注释的C代码转换为用于验证的 BoogiePL中间语言，然后通过Boogie工具将其继续转化为一阶逻辑表达式。其中，BoogiePL 是一种带有嵌入式断言的简单命令式语言，它很容易生成一组一阶逻辑公式，表明程序应该满足性质，这里以断言的形式呈现。

第二步，利用 SMT 求解器 Z3（自动化定理证明器）对转换后的一阶逻辑表达式进行验证。Z3 求解器会返回两种结果：（1）一阶逻辑表达式通过验证；（2）Z3 返回一个反例或者提示超时。

图2 VCC的工作流程

VCC可以自动验证函数是否满足用户书写函数规约。用户使用时操作步骤如下：

（1）根据设计规约，利用VCC提供的接口，编写前置条件、后置条件等函数契约；

（2）使用VCC自动验证函数是否满足这些契约；

（3）如果VCC报告验证失败，那么根据错误报告，修改代码，或重写函数契约；

（4）如果VCC报告验证成功，则说明函数符合契约。

以下一个返回两者之间更小的数的一个函数为例，进一步分析如何使用VCC工具对一个C语言代码进行单元验证。

表 1

在表1中，表左边展示的是使用VCC标记过的源代码，表右边展示的是C语言转化后的BoogiePL中间语言，其中为源代码添加了一个前置条件和后置条件。前置条件表示在进入函数前假定满足的条件，后置条件表示在执行完函数后所需要满足的条件。BoogiePL中间语言转化过程会将返回结果赋值给result；将前置条件转化成assume语句来假定前置条件满足；将后置条件转化成assert语句对提出的后置条件进行验证。

02

CBMC

CBMC是Bounded Model Checker for ANSI-C and C++ programs的缩写，CBMC是C和C ++程序的绑定模型检查器。CBMC实现了一种称为边界模型检查（BMC，Bounded Model Checker）的技术。在BMC中，通过联合解开复杂状态机的转换关系及其规范以获得布尔公式，然后使用有效的SAT程序检查布尔公式的可满足性。如果该公式是可满足的，则从SAT过程的输出中提取一个反例。如果公式无法满足要求，则可以展开更多程序以确定是否存在更长的反例。

在许多工程领域中，实时保证是严格的要求。例如是嵌入在汽车控制器中的软件，这些类型的程序中的循环构造通常对迭代次数有严格的限制。CBMC能够通过展开断言来严格验证这种范围。建立迭代次数的界限后，CBMC便可以证明是否存在错误。

CBMC能够验证内存安全性（包括数组范围检查和指针是否安全使用的检查）、检查异常、检查未定义行为的各种变体以及用户指定的断言。通过展开程序中的循环并将结果方程式传递到决策程序来执行验证。CBMC像编译器一样，从命令行接收.c命名的文件，然后编译程序并将不同文件定义的函数组合起来。但CBMC不像编译器生成可执行二进制代码，而是符号执行程序。

CBMC 的目标是分析 C/C++ 或者 JAVA 程序。CBMC 分析的过程是将输入程序，生成对应的控制流图，当获取到程序的CFG时，就可以获取每条路径对应的公式 ，也就是说路径能够执行的条件是使路径对应的公式能够成立。然后针对获得的公式，使用SAT求解命题逻辑，其中分析流程如图3所示。

图3 CBMC的验证流程

使用CBMC工具进行分析的过程可以划分成如下四步：

（1）对源代码进行插桩，放入部分约束或者标签；

（2）将程序解析为语法树，并基于语法树转换成CFG；

（3）在获得程序的CFG后，我们计划通过收集程序路径，得到路径对应的公式；

（4）结合程序插桩信息，进而通过SMT求解器得到验证结果。

表2所示的是一个CBMC的示例，往代码中注入了一个error标签，可按照其CFG到断言并建立与路径对应的一阶路径进行验证。

表 2

对于上表所示的代码片段，构建的CFG，如图4所示。

图4 CFG图示

图5 路径图示

对于图5所示的标红路径，可以得到公式0 ≤ t ≤ 79 ∧ t/20 != 0 ∧ t/20 == 1 ∧ TEMP2 = B ⊕ C ⊕ D ∧ TEMP3 = K 2，将这组公式放入SMT求解器进行求解时，可以得到一组解。当我们针对error标签进行可达性验证时、可以得到公式 0 ≤ t ≤ 79 ∧ t/20 != 0 ∧ t/20 != 1∧ t/20 != 2 ∧ t/20 != 3，使用SMT求解器进行求解时发现该公式不能得到满足，即该路径不可达。

03

PAT

PAT是Process Analysis Toolkit的简称，是由新加坡国立大学开发的一款形式化建模与验证工具集，支持进程代数、实时进程代数、时间自动机等多种建模语言。此外，PAT工具的人机交互界面友好，支持多种验证方法，包括精化验证、死锁验证、可达性验证、LTL性质验证等。以PAT工具中最常使用的是语言CSP#为例，对如何使用PAT建模进行讲解。

PAT的进程代数(Communication Sequential Process, 简称CSP)模块。该模块使用CSP#，作为建模语言，描述待验证的系统。

CSP#在经典的CSP的基础上，增加了数据状态与相关的操作，使得建模更加方便、直观。CSP#描述的系统主要包括下面三个部分：

（1）全局量：定义常量和全局变量，支持多维数组；

（2）进程：定义系统中的各个进程；

（3）断言：描述系统应当满足的性质，可以使用全局定义中的变量。

进程的定义如下：

图 6

其中事件前缀可以和数据操作组合使用，例如：

P=  add{x=x+1;}→Skip;

其中P是一个进程，add代表一个事件，x是全局变量，伴随着事件add的发生, 执行赋值操作x=x+1。在PAT的建模过程中，我们广泛使用这种机制表示数据的传输。

此处解释关于外部选择以及内部选择：

（1）对于一个外部选择：

P[]Q

选择运算符[]指出可以执行P或Q。但该选择由环境解决，如果P中事件首先发生，那么由P接管进程，否则是由Q接管进程。

（2）对于一个内部选择：

P<>Q

其中P或Q可以执行。该选择是内部确定的，意味着随机执行进程P或者 Q。在建模阶段，它对于隐藏不相关的信息很有用。它可以用于对黑盒过程的行为进行建模，而不用了解黑盒的具体实现。

对于内部选择和外部选择可以写出它们的广义形式：

[]x:{1..n}@ P(x) 等价于  P(1)[]...[]P(n)

<>x:{1..n}@ P(x) 等价于 P(1)<>...<>P(n)

图 7

在PAT工具中，创建CSP#模型之后，然后就可以进行验证。待验证的性质可以划分为两类，一类是LTL性质，另一类是refine性质。PAT工具将验证性质是否满足。如果不满足，可以查看反例。图7展示的是一个操作系统任务调度算法建模的模型。模型中详细描述了操作系统任务调度过程中创建进程、进程执行、进程抢占、进程挂起、进程中断、进程调度等过程，以及进程各个状态之间的迁移关系。并且在使用PAT工具进行验证的时候，也可以验证出该模型存在死锁，并针对死锁情况给出了一系列行为对应的反例，在此操作系统的任务调度算法中没有发现死锁，因此也不会给出反例。

04

基于形式化验证与分析框架的应用

此套形式化验证与分析框架曾用于某操作系统的调度算法验证。在使用VCC工具进行验证的合计77个函数、其中64个验证通过，13个验证不通过。在13个验证不通过的函数中有6个类型不匹配问题、6个数组溢出问题以及一个指针内容可能为空问题。在使用CBMC工具进行验证的77个函数中，其中21个未添加约束验证通过，7个提示内存不足无法验证，2个验证崩溃。在添加了约束后77个函数中75个验证成功、2个验证崩溃。在使用PAT工具对其建模后，对操作系统内的调度算法进行了无死锁验证，在模拟6935684了状态后得到了该操作系统无死锁的结论。

参考资料：

[1] Ankit S ,  Arnab B ,  Lakshmanan K , et al. An overview of model checkers and CBMC as a tool. , 2017.

[2] Liu, Y., Sun, J., Dong, J. S.: Developing model checkers using PAT. In: International symposium on automated technology for verification and Analysis, pp. 371–377. Springer, Berlin, Heidelberg (2010).

[3] Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. 2009. VCC: A Practical System for Verifying Concurrent C. In TPHOLs (LNCS, Vol. 5674). Springer, 23–42.

[4] 缪淮扣,陈怡海.《软件形式规格说明语言—Z》,清华大学出版社出版,2012年11月.

[5] Wing J M. A specifier's introduction to formal methods[J]. Computer, 1990, 23(9): 8-22.

[6] Miao, W. and S. Liu, A Formal Engineering Framework for Service-Based Software Modeling. IEEE Transactions on Services Computing, 2013. 6(4): p. 536-550.

审核编辑 黄昊宇