基于PROMELA模型的安全关键软件形式化验证技术

邢亮, 丁成钧, 杜虎鹏, 马春燕

(1.航空工业西安航空计算技术研究所, 陕西 西安 710076; 2.西北工业大学 软件学院, 陕西 西安 710072)

当前安全关键软件在航空、航天、医疗、交通等领域应用广泛，该类软件存在资源竞争、空指针和数组越界等问题，而检测相应故障主要依赖开发人员的经验和技术能力，保障其可靠性存在很大困难。形式化验证[1]是故障检测技术之一，其通过严格的数学语义进行推理以保障代码的可靠性。

形式化建模语言PROMELA支持对任务关键C程序逻辑进行建模以及C程序的嵌入，具有验证C程序的优势。目前，用PROMELA建模C程序时，主要通过人工方式实现，需要较高技术门槛和代价，限制了安全关键软件进行形式化验证的广泛应用。本文提出了从C程序到PROMELA模型的自动生成方法，实现对安全关键C程序中5类故障模式进行一键式形式化验证。本文贡献如下：

1) 制定了C程序到PROMELA模型2类映射规则，提出了PROMELA模型自动生成的方法，并对方法进行理论分析；

2) 针对C程序中违反断言、数组越界、空指针解引用、死锁以及饥饿5类故障，给出形式化验证方法和验证范围；

3) 研制了辅助工具，覆盖每类故障的验证范围，分别选取12个来源于开源代码托管平台GitHub的C程序案例，进行实证研究。

1 相关工作

文献[1]提出了针对并发故障的形式化验证方法，实现了PROMELA模型生成工具C2Spin。Jiang[2]使用语法导向技术，采用PROMELA建模C程序，但缺少并发C程序库函数的建模。Wagner等[3]提出检测缓冲区溢出的方法，但其检测精度较低。文献[4]提出基于插桩的方法验证C程序数组越界，但存在重复和等价插桩点，验证效率较低。Klieber等[5]提出针对缓冲区溢出的自动化修复技术。文献[6]将随机内存分配算法和虚拟内存相结合，改进内存分配策略，避免程序执行时的内存错误。文献[7]综合程序切片和谓词抽象技术，提出C程序断言的静态验证方法。Yong等[8]设计了用于检查空指针解引用的C程序安全工具。Zhe等[9]通过代码插桩技术，设计针对内存漏洞的分析工具，但仅能处理较简单的C程序。

目前，大部分方法存在过多人工干预，并且验证的故障类型较少，也未给出存在故障的反例路径。PROMELA对有限状态分布式系统进行建模[10]。SPIN工具支持PROMELA模型中以断言形式和线性时间逻辑(linear-time logic,LTL)公式形式撰写的验证属性，生成并仿真执行验证程序[11]。

本文基于PROMELA模型，结合SPIN，提出C程序“一键式”形式化验证技术，实现5类故障模式的验证，并给出C程序存在故障的反例路径。

2 基于PROMELA模型的安全关键软件形式化验证方法

2.1 C程序到PROMELA模型的映射机制

2.1.1 C程序到PROMELA模型的映射规则

本节定义了C程序抽象语法树节点(C程序语法结构)到PROMELA模型的19个映射规则，部分规则如表1所示。

表1 抽象语法树节点到PROMELA模型的映射规则

续表1

由于篇幅所限，本文仅阐述循环节点For到PROMELA模型的映射规则：

1) 识别For循环体，生成do...od结构；

2) 递归遍历For第1个子节点，生成PROMELA模型，将返回值作为语句插入do...od结构前；

3) 递归遍历For第2个子节点，生成PROMELA模型，将返回值作为do...od中条件语句；

4) 对For第2个子节点的返回值取反，生成PROMELA模型，作为do...od结构中条件语句；

5) 递归遍历For第4个子节点，生成PROMELA模型，将返回值作为第1个条件语句后的语句；

6) 递归遍历For的第3个子节点，生成PROMELA模型，将返回值按顺序作为第1个条件语句后的语句；

7) 为第2个条件语句添加break。

2.1.2 与验证属性相关的函数到PROMELA模型的映射规则

基于2.1.1生成的PROMELA模型，可以实现对断言违反、数组越界、空指针解引用的验证。为验证死锁、饥饿并发故障，本文进一步提出10条映射规则，部分规则如表2所示。

表2 部分函数节点到PROMELA模型的映射规则

续表2

2.2 PROMELA模型自动生成方法

算法1实现基于映射规则的PROMELA模型自动生成。1至15行对抽象语法树进行递归遍历，获取当前节点及子节点信息，并根据节点名称，应用映射规则，生成PROMELA模型。16至26行以For为例，给出其PROMELA模型生成算法。

算法1PROMELA model instance generator

input:tis the abstract tree root node of a C program; map is the mapping relationships between the abstract tree nodes and mapping rules

output: pr is an instance of PROMELA model

1. while (t!= null) do

2. if(map.containsValue(t.name)) then

3. rule←map.get(t.name)

4. instanceGenerator(rule);

5. end if

6. ift.char is "thr-suspend"

7. return 1

8. end if

9. ift.char is "rand"

10. returnt.char

11. end if

12. returnt.char

13. otherwise do error

14. end if

15. end while

16. Procedure instanceGenerator(rule)

17. if rule is R10 then

18. PROMELAGeneration(node.firstchild)

19. Emit("do")

20. Emit("::")

21. bool var = PROMELAGeneration(node.secondchild)

22. Emit("!var->break")

23. PROMELAGeneration(node.forthchild)

24. PROMELAGeneration(node.thirdchild)

25. Emit("od")

26. end if

27. else if rule is one of other rules then

28. Generator the corresponding instance fragments

29. end procedure

2.3 PROMELA模型生成方法的理论分析

从构建方法的语义保留、确定性和有边界3个方面，证明C程序到PROMELA模型生成方法的合理性。

首先借鉴文献[12]中提出的图同构思想，结合图1对构建方法的语义保留性进行证明。图1中Gramc指C语言的语法规则，Gramp指PROMELA建模语言的语法规则，pro(Gramc)指C程序，pro(Gramp)指PROMELA模型实例。符号h表示C语言语法规则到PROMELA语法规则的映射；符号r表示C程序到PROMELA模型实例的转换函数；符号t和t′分别表示C语言和PROMELA语言语法规则到程序实例之间的映射函数，它们为类型保留映射(type prserve mapping,TPM)，符号F表示C语言语法规则到PROMELA模型实例之间的映射关系。

图1 语法规则和程序实例之间的映射关系

2.1节中29种映射规则是建立在形式化模型与抽象语法树节点语义一致的基础上，所以C程序抽象语法树节点到PROMELA模型的映射规则函数h是同构的。

定义1定义图同构函数f表示从图G到图H的转换：f=G→H。N(G)为图G的节点集合,N(H)为图H的节点集合,E(G)为图G的边的点集合,E(H)为图H的边的集合。f满足公式(1)中的约束。

∀x,y∈N(G)∧f(x),f(y)∈N(H)∧xy

∈E(G)⟹f(x)f(y)∈E(H)

(1)

结合定义1和本文的映射规则可知，图G类似C语言的语法规则，图H类似PROMELA语言的语法规则。而N(G)表示C语言抽象语法树节点，E(G)表示映射规则中的29种抽象语法树节点，N(H)表示PROMELA的语法节点集合，E(H)表示PROMELA语法节点。

命题1Graml为一种程序语言的语法规则，pro(Graml)为该语言对应的程序实例，那么在语法规则及其程序实例之间的TPM函数是图同构的。

由命题1，C语言语法规则到C程序实例之间的映射函数t，以及PROMELA语言到PROMELA模型实例之间的映射函数t′是图同构的。

命题2如果映射函数f是图同构的，并且映射函数g是图同构的，那么f和g的复合运算f∘g也是图同构的。

根据命题2，因为函数h,t′是图同构的，所以F(ht′)是图同构的。

定理1已知Gramc和Gramp之间存在同构映射h，Gramc和它的程序实例pro(Gramc)之间存在类型保留映射函数t，Gramp和它的模型实例之间pro(Gramp)存在类型保留映射函数t′，则pro(Gramc)和pro(Gramp)之间的映射函数r是图同构的。

证明上文已经证明函数h,t,t′,F是图同构的，分别用公式(2)至(5)表示。

h(Gramc)=Gramp

(2)

t(Gramc)=pro(Gramc)

(3)

t′(Gramp)=pro(Gramp)

(4)

F(Gramc)=t′(h(Gramc))=t′(Gramp)=

pro(Gramp)

(5)

根据公式(1)和(2)可得公式(6):

∀x,y∈N(Gramc)∧h(x),h(y)∈N(Gramp)

∧xy∈E(Gramc)⟹h(x)h(y)∈E(Gramp)

(6)

根据公式(1)和(5)可得公式(7):

∀x,y∈N(Gramc)∧F(x),F(y)∈N(pro(Gramp))

∧xy∈E(Gramc)⟹F(x)F(y)∈E(pro(Gramp))

(7)

将公式(7)中的F替换成r∘t，化简得到公式(8):

根据公式(8)，因为TPM函数t是图同构的，结合公式(1)表示的同构函数的约束，因此推断映射函数r也是图同构的，即定理1得证。

C程序到PROMELA模型生成方法是基于C语言和PROMELA建模语言的语法规则提出的，而C语言和PROMELA语言的语法结构是精确无二义性的，且抽象语法树节点的映射规则是一一映射的，所以生成方法是确定性的。由于C程序的抽象语法树节点数量是有限的，所以生成方法是有限的。综上，本文提出的C程序到PROMELA模型生成方法是正确的。

2.4 基于PROMELA模型的C程序验证方法

1) 违反断言的验证方法

在C程序中添加的断言称为基本断言，以检查表达式的合法性。如果表达式中变量值确定，则断言表达式可以直接验证；如果变量值依赖函数参数、函数返回值或全局变量时，例如变量var的地址以实参形式传入函数fun中，则导致C程序转换成PROMELA模型后，断言语句assert(var小于1 000)的逻辑值无法确定，针对变量无法确定取值的情况，本文提出将激励函数插入PROMELA模型的算法2。

算法2Excitation function generation algorithm genStubs()

input:tis the abstract tree root node of a C program;

output: void

1. while (tis not null)

2. if (tis TN-FUNC-CALL) then

3. line←t.cont

4. fun-name←t.lnode.value

5. params =t.rnode

6. for(params hasNext())

7. param = params.next()

8. if param is ASSERT-VAR then

9. param-range←param

10. fun-name=fun-name+"-stubs"

11. for num in param-range

12. fun-body←num

13. new-funcall←line，fun-name

14. end for

15. end if

16. end for

17. end if

18. end while

表3是基于C程序断言的验证范围，对包含规约运算的情况作等价处理，例如，断言表达式assert(i++>0)等价变换为i++和assert(i>0)即可。

表3 C程序断言验证方法的验证范围

2) 数组越界的验证方法

表4是C程序数组越界的验证范围。对于数组长度和索引均确定的情况，可以采用1)中断言的形式进行验证。而当数组长度或索引依赖函数参数或全局变量时，则根据算法2插入激励函数；如果多维数组中每一维度长度和索引范围均静态确定，则插入断言assert(index1

表4 数组越界验证方法的验证范围

3) 空指针解引用的验证方法

本方法对空指针解引用类型的验证范围如表5所示。对于一级静态确定指针，可以采用断言表达式验证。指针变量动态依赖函数参数或全局变量需调用算法2生成静态确定指针变量的激励函数后再进行验证；多级指针与1级指针验证时插入的断言不同，假设二级指针int**p; 则插入断言assert(p &&*p)，即需要对每一级指针进行验证。

表5 空指针解引用验证方法的验证范围

4) 死锁和饥饿的验证方法

死锁及饥饿问题验证是基于C程序Pthread库中线程创建函数pthread_create、互斥锁以及条件变量等。死锁及饥饿问题验证范围如表6所示。

表6 死锁及饥饿验证方法的验证范围

在并发C程序转换为PROMELA模型后，使用“end”标签来标识程序结束状态，如果“end”标签未被执行，则存在死锁问题；使用“progress”标签标记重复被执行的语句，如果存在没有被执行的“progress”，即存在饥饿问题。

3 实验验证

3.1 某实验案例的验证过程

本文以存在数组越界故障的Driver-receiv1553程序为例，阐释验证原理。该程序从1553b总线接收数据，对数据有效性进行判断，读取数据长度、数据块等信息，对无效数据通过调用trans16函数进行处理。该C程序的流程图如图2所示。

图2 Driver-receiv1553程序流程图

本文研制辅助工具完成C程序到PROMELA模型的转换，并与SPIN集成，实现对C程序的验证。辅助工具生成的PROMELA模型原理如图3所示。

图3 PROMELA模型流程图

该模型的验证表达式为c-code[(Pp-receiv1553->ix<32)]，根据本文的验证方法，该程序存在数组越界故障，C程序反例路径如图4所示。由于图2中变量uslength的值为32，因此该有向图中的108→109→108路径会执行32次，此时ix的值为32。而根据验证表达式，ix的值应小于32，所以该程序出现数组越界故障，且故障出现在C程序的第109行。

图4 反例路径有向图示意

3.2 验证方法对比

本文针对违反断言、数组越界、空指针解引用、死锁及饥饿，覆盖各故障类型的所有验证范围，分别使用12个来源于GitHub的C程序案例进行实验验证，并与相关工作中的其他方法进行对比，如表7所示，其中，验证故障类型中的编号为2.4节相应表中的编号。本文方法验证的故障类型多、自动化程度高，并展示C程序故障出现的反例路径，在这三个方面具有明显的优势。

表7 C程序验证方法对比

4 结 论

本文在定义C程序抽象语法树节点到PROMELA模型映射规则的基础上，增加了验证属性相关函数到PROMELA模型的映射规则，提出了一种C程序到PROMELA模型自动生成算法，并给出包含违反断言、数组越界、空指针解引用、死锁、饥饿这5种故障类型的C程序形式化验证方法。在对实验案例分析后，对比现有C程序形式化验证方法的优缺点，本文方法具有明显优势。