一种航天嵌入式C语言软件运行时错误的静态分析方法

摘要

本发明公开了一种航天嵌入式C语言软件运行时错误的静态分析方法。包括：(1)将航天嵌入式C语言软件运行时错误按照错误的发生机制进行分类，根据每类错误构造属性状态机的步骤。(2)根据构造的待检测软件源代码的程序控制流图和属性状态机获得程序控制流图中各节点的属性状态和路径条件的步骤。(3)根据获得的属性状态和路径条件对运行时错误进行分析的步骤。采用本发明提高了对航天嵌入式C语言软件运行时错误进行检测的准确度和效率。

说明书

技术领域

本发明涉及一种航天嵌入式C语言软件运行时错误的静态分析方法，属于 软件测试技术领域。

背景技术

目前在航天领域，C语言被普遍应用于编写嵌入式软件，C语言已经成为嵌 入式系统高级编程语言的标准。C语言有很多优点但是对于开发高安全软件来 说它缺少必要的安全措施，主要缺陷有：C语言的非强制类型特性降低了它的 可靠性；C语言的另一个特性是没有对指针操作进行严格的限定；此外，C语言 不提供对数组和字符串的边界检查。正是由于C语言的这些缺陷，C程序中会 存在一些漏洞和错误，其中一类为运行时错误。运行时错误(Run-time Error) 就是软件在动态运行时出现的错误。根据ANSIC定义，运行时错误是指那些能 导致预定义之外的不正确结果或者处理器停机的错误。

运行时错误是所有软件错误中最具风险的，同时也是最难发现的。对于航 空航天、汽车以及医疗设备等安全级别要求非常高的系统来说，一旦出现这样 的运行时错误，损失就是不可估量的。

对运行时错误进行检测的方法主要有动态测试和静态分析两种。动态测试 是传统的方法，通过软件的实际执行来发现软件中的错误。其检测结果高度依 赖于测试用例的选择，同时，由于只能对有限的测试用例进行检查，所以动态 测试方法不能保证发现软件的所有安全漏洞。静态分析方法是在程序不执行的 状态下，通过对被检测软件进行建模，发现满足所有可能执行状态的软件属性， 再通过对事先预定的规则库的分析来检测软件中的错误漏洞。

静态分析主要有定理证明，模型验证和抽象解释等方法。定理证明和模型 检验都属于形式化验证方法，可以精确地确定软件的属性。定理证明方法将程 序转换为逻辑公式，然后使用公理和规则证明程序是一个合法的定理。由于定 理证明过程难以完全自动化，需要高素质分析人员的大量参与，证明过程非常 耗时费力，一般只用于验证设计阶段的程序规范而非实际代码。模型检验用状态 迁移系统(S)描述软件的行为，用时序逻辑、计算树逻辑或μ-演算公式(F)表示 软件执行必须满足的性质，通过自动搜索S中不满足公式F的状态来发现软件 中的漏洞。由于需要穷尽程序的所有实际执行状态，所以模型检验的效率很低， 并且不能检验无穷状态系统。抽象解释是用于构造和逼近程序不动点语义的理 论，它使用抽象对象域上的计算抽象来逼近程序指称的具体对象域上的计算， 使得程序抽象执行的结果能够反映出程序真实运行的部分信息。它仅跟踪用户 关心的程序属性，所以它对程序语义的解释是程序实际语义的近似。错误检测 的两个标准是准确度和效率。静态分析各个方法都有自己的局限性，定理证明 和模型验证方法的准确度比较高，但效率却比较低。抽象解释方法的效率比较 高，但准确度却比较低。如何在准确度和效率上取得一个好的平衡是静态分析 的难点，也是目前研究热点。

发明内容

本发明的技术解决问题是：克服现有技术的不足，提供了一种航天嵌入式 C语言软件运行时错误的静态分析方法。采用本发明提高了对航天嵌入式C语 言软件运行时错误进行检测的准确度和效率。

本发明的技术解决方案是：

本发明所述的一种航天嵌入式C语言软件运行时错误的静态分析方法，通 过以下步骤实现：

(1)对航天嵌入式C语言软件运行时错误进行分类，按照分类后每类错误 的属性模式构造属性状态机，所述属性状态机包括程序运行过程中可能出现的 属性状态D_i，i＝{1，…n}，n为每类错误中的属性状态总数，D_i包括程序运行过 程中可能的出现的错误状态；

(2)按照程序的控制流程图和运行时错误的属性状态机，根据控制流程图 中位置l处的节点信息和输入属性状态σ_{l_in}，获得经位置l处的节点处理后的输 出属性状态σ_{l_out}和路径条件C_s，l，其中，s为到达位置l处的路径；

(3)判断σ_{l_out}与属性状态D_i的关系：

若σ_{l_out}为D_i中的错误状态，则将路径条件C_s，l作为可能出现的错误提示输 出，并不再对C_s，l进行后续分析；否则，将σ_{l_out}作为下一个位置处的输入属性状 态返回步骤(2)，直到程序出口。

所述属性状态机由状态转移集合T组成，所述状态转移集合T为 D_i×conditions_i→D_k，i，k＝{1，…n}，其中，D_i和D_k为属性状态，D_k为源属性状态D_i在转移条件为conditions_i时的目标属性状态；所述转移条件conditions_i为根据C语 言确定的对数据流的操作。

在所述步骤(2)中，对控制流程图中位置l_j处的节点信息进行判断：

若位置l处的节点为汇合节点，则将相同的输入属性状态σ_{l_in}的路径条件进 行合并，然后获得经位置l处的节点处理后的输出属性状态σ_{l_out}和合并后的输出 路径条件C_s，l；

若位置l处的节点为分支节点，比较路径条件C_sl中的变量取值与当前判断 谓词取值的交集，若交集为空，表示该位置的输入属性状态σ_{l_in}的路径条件C_s，l和当前分支组合后为不可达路径，则不记录不可达路径上的属性数据流信息。

所述属性状态机根据错误的属性模式可分为：空指针解引用属性状态机、 资源泄露属性状态机、未初始化变量引用属性状态机和除零错误属性状态机。

本发明与现有技术相比具有如下优点：

(1)属性有限状态机是一种易于理解的对错误产生机制和过程的抽象表示， 用属性有限状态机对运行时错误进行描述，可以使描述更加准确、无二义性。 在程序分析过程中，依据属性状态机和程序控制流图对某类错误进行检测。该 方法针对性强，能检测出一些小概率错误。

(2)在程序分析过程中，跟踪的数据流信息包括属性状态和路径条件。若 属性状态中包括错误状态，则报告一个错误并输出相应路径条件作为错误提示。 根据报告的路径条件，可以从程序入口沿着错误发生的路径一直追踪到错误发 生的位置。该方法能准确地定位错误，找到错误发生的根源。

(3)当程序分析到达控制流图中的汇合节点时，若不同属性数据流信息中 的属性状态相同时，合并属性数据流信息中的路径条件，进而组成一个新的属 性数据流信息。该方法剔除了与待测属性无关的路径，降低了分析的复杂度， 提高了分析的效率。

(4)当程序分析到达控制流图中的汇合节点时，通过比较路径条件中的变 量取值与当前判断谓词取值是否为空来判断该输入属性状态的生成路径与当前 分支组合后是否为不可达路径。剔除不可达路径，不记录其上的属性数据流信 息。该方法对路径实现敏感分析，提高了分析的准确度，降低了误报率。

附图说明

图1为本发明的流程图；

图2为待检测的代码片段；

图3为空指针解引用属性有限状态机；

图4为待检测代码片段的控制流图；

图5为资源泄露属性有限状态机；

图6为未初始化变量引用属性状态机；

图7为除零错误属性有限状态机；

具体实施方式

下面就结合附图对本发明做进一步介绍。

将航天嵌入式C语言软件运行时错误分类，提取每类错误的属性模式，将 属性模式用属性有限状态机表示。然后，构造待检测软件源代码的控制流图， 在控制流图的每个节点上对被测软件中的属性状态信息进行跟踪，依据属性状 态中是否有错误状态来判断是否存在该类属性模式的运行时错误。其流程如图 1所示，具体步骤如下：

(1)将航天嵌入式C语言软件运行时错误按照错误的发生机制进行分类， 具体细化后的每类运行时错误对应于软件编码中的某个错误。错误类别包括空 指针解引用、资源泄露、未初始化变量引用和除零错误。

每类错误的属性模式都是对程序某个属性的一种描述，将运行时错误的属 性模式转化为有限状态的属性状态机(Finite State Machine，FSM)。FSM由 状态转移集合T组成，T：D_i×conditions_i→D_k，i，k＝{1，…n}。其中，D_i和D_k为属性 状态，对应于一类错误的所有属性状态组成状态集合D，可表示为 D＝{$start，$error}∪D_other，$start为开始状态，$error为错误状态，D_other为在属性 模式下其他可能出现的属性状态的集合；conditions_t为转移条件，为根据编程语 言确定的对数据流的操作，所有的conditions_i组成转移条件集合Conditions。

空指针解引用的属性模式如图3。其中，D＝{$start，$error，may-null， non-null }，Conditions＝{肯定不为空，可能为空，解引用，其他}，T＝{$start×其 他→$start，$start×肯定不为空→non-null，$start×可能为空→may-null， non-null×其他→non-null，non-null×可能为空→may-null，may-null×其他 →may-null，may-null×肯定不为空→non-null，may-null×解引用→$error}。

资源泄露的属性模式如图5。其中，D＝{$start，$error，opened，closed}， Conditions＝{打开，关闭，其他，任何}，T＝{$start×其他→$start，$start×打开 →opened，$opened×关闭→closed，opened×其他→opened，closed×任何→closed， opened×资源不被任何变量访问→$error}。

未初始化变量引用的属性模式如图6，其中，D＝{$start，$error，init}， Conditions＝{初始化/赋值，引用，其他}，T＝{$start×其他→$start，$start×初始 化/赋值→init，init×任何→init，$start×引用→$error}。

未初始化变量引用的属性模式如图7，其中，D＝{$start，$error，safe，unsafe}， Conditions＝{值为零，值非零，作为除数，其他}。T＝{$start×其他→$start，$start× 值非零→safe，$start×值为零→unsafe，safe×其他→safe，safe×值为零→unsafe， unsafe×值非零→safe，unsafe×其他→unsafe，unsafe×作为除数→$error}。

(2)根据被测程序源代码构建程序控制流图(Control Flow Graph，CFG)。 在一个被测程序的函数内部，根据属性状态机创建属性状态机实例，刚创建的 属性状态机实例处于$start状态，然后沿着控制流方向计算各属性状态机实例 的可能状态集合。过程如下：

1)构造程序的控制流图，其可表示为一个有向图G＝<N，E，n_entry，n_exit>。其中， N是节点集，程序中的每个语句都对应图中的一个节点；E为边集， E＝{<n₁，n₂>|n₁，n₂∈N}(n₁为源节点，n₂为目标节点)，n_entry和n_exit分别为控制流 图的入口和出口节点。

2)将控制流图中的节点分类为汇合节点(Merge Nodes)，分支节点(Branch Nodes)和计算节点(Computation Nodes)。汇合节点有2个前驱节点，分支节 点有一个前驱节点和2个后继节点(一个为真分支，一个为假分支)，计算节点 有一个前驱节点和一个后继节点。通过跟踪各个节点的输入、输出数据流信息 来判断程序是否存在运行时错误。

3)对于每个节点，记录被测属性的数据流信息。属性的数据流信息包括位 置l节点的输出属性状态σ_{l_out}和到达该属性状态的路径条件C_s，l。输出属性状态 σ_{l_out}对应于属性状态机的状态集合D中的某个元素，是输入属性状态σ_{l_in}经l处 的节点处理后的输出。路径条件C_s，l是到达该属性状态的相关变量的取值集合， 即程序通过路径s执行到位置l时，s_j上的相关判断谓词和赋值操作组成的抽象 上下文。属性状态σ_{l_out}和路径条件C_s，l的组合构成属性的数据流信息，即 {σ_{l_out}:C_s，l}。

4)在控制流图的入口节点n_entry上，将被测属性的属性状态置为$start，路径 条件置为(代表开始节点)，属性数据流信息为

5)在控制流图中的所有汇合节点(Merge Nodes)上，将具有相同属性状态 的属性数据流信息中的路径条件进行合并，形成新的属性数据流信息。例如： 程序通过路径s₁到达汇合节点l_j时的属性状态为此属性数据流信息P₁为 程序通过路径s₂到达汇合节点l_j时的属性状态也为此属性数 据流信息P₂为由于P₁和P₂具有相同的属性状态，所以可以将P₁和P₂的路径条件进行合并，形成新的属性数据流信息由于只进行 了路径的合并，并没有属性状态的转移，因而

6)在控制流图中的所有分支节点(Branch Nodes)上，比较路径条件中的 变量取值与当前判断谓词取值的交集。若交集为空，表示该位置的输入属性状 态的路径条件和当前分支组合后为不可达路径。剔除不可达路径，不记录该路 径上的属性数据流信息。例如：程序通过路径s到达分支节点l_j，属性状态的路径条件为分支节点l_j的判断语句为if(m)。比较路径条件中的变量m 的取值与当前判断谓词m取值的交集。假设中的变量m取值为真，判断谓词 m取值为假。由于它们的交集为空，表示路径条件和当前假分支组合后为 不可达路径。剔除该组合路径，不记录其上的属性数据流信息。

(3)当程序沿着路径条件C_s，l到达控制流图中的节点l时，比较节点l的输出 属性状态σ_{l_out}与属性状态D_i的关系：

若σ_{l_out}为D_i中的错误状态，则将路径条件C_s，l作为可能出现的错误提示输 出，并销毁该属性状态机实例；否则，将σ_{l_out}作为下一个位置处的输入属性状 态，根据步骤(2)中的相关步骤计算下一位置的输出属性数据流信息，直到程 序出口。

以某卫星的中央处理单元软件为例，说明本发明的实施步骤：

(1)首先给定一个简单的需求，验证该软件的某代码片段(图2)是否存 在空指针解引用这类运行时错误。空指针解引用是指对一个指向空地址单元的 指针表达式进行解引用操作(dereference)而引起的错误。

(2)空指针解引用的属性模式如下：首先，指针的属性状态处于开始状态 ($start)，若有能让指针肯定不指向空地址的操作序列T₁，指针的属性状态转 化为非空状态(non-null)，若有能让指针可能指向空地址的操作序列T₂，指针 的属性状态转化为可能为空状态(may-null)，否则指针的属性状态维持开始状 态($start)。在非空状态(non-null)下，若有能让指针可能指向空地址的操作 序列T₂，指针的属性状态转化为可能为空状态(may-null)，否则，指针的属性 状态继续维持非空状态(non-null)。同理，在可能为空状态(may-null)下， 若有能让指针肯定不指向空地址的操作序列T₁，指针的属性状态转化为非空状 态(non-null)，否则，指针的属性状态继续维持可能为空状态(may-null)。同 时，若指针处于可能为空状态(may-null)，而对该指针进行了解引用操作T₃， 指针的属性状态将转化为错误状态($error)，则证明该代码片段中存在空指针 解引用的运行时错误。

(3)将空指针解引用的属性模式转化为属性有限状态机FSM。FSM中的属 性状态集合D为{$start，non-null，may-null，$error}，转移条件集合Conditions为 Conditions＝{肯定不为空，可能为空，解引用，其他}，T＝{$start×其他→$start， $start×肯定不为空→non-null，$start×可能为空→may-null，non-null×其他 →non-null，non-null×可能为空→may-null，may-null×其他→may-null， may-null×肯定不为空→non-null，may-null×解引用→$error}。属性状态机FSM 以一个有向图表示，具体如图3。

(4)构造待检测源代码片段(图2)的程序控制流图(CFG)，如图4所示。 构造指针ptr的属性状态机实例，沿着控制流方向计算各个节点处ptr的属性 数据流信息。

1)在entry节点上，指针的属性数据流信息为

2)在n1节点上，n1节点是一个分支节点。对于真分支m＝true，属性数据 流信息为{$start:m＝true}；对于假分支m＝false，属性数据流信息为 {$start:m＝false}。

3)真分支到达n2节点，n2节点有i＝1；ptr＝&i的操作，因而属性数据流信 息变为{non-null:m＝true}。假分支到达n3节点，n3节点有ptr＝NULL的操作， 因而属性数据流信息变为{may-null:m＝false}。

4)到达n4节点，n4节点是汇合节点，属性数据流信息为{non-null:m＝true}， {may-null:m＝false}。由于属性状态不同(一个为non-null，另一个为may-null)， 这两个属性数据流信息不能合并。

5)到达n5节点，n5是分支节点。对于真分支p＝true，属性数据流信息为 {non-null:m＝true，p＝true}，{may-null:m＝false，p＝true}。对于假分支p＝false，属 性数据流信息为{non-null:m＝true，p＝false}，{may-null:m＝false，p＝false}。

6)真分支到达n6节点，n6节点的操作q＝0不影响属性数据流信息，因而 属性数据流信息依然为{non-null:m＝true，p＝true}，{may-null:m＝false，p＝true}。 假分支到达n7节点，n7节点的操作q＝1也不影响属性数据流信息，因而属性 数据流信息依然为{non-null:m＝true，p＝false}，{may-null:m＝false，p＝false}。

7)到达n7节点，n7节点是汇合节点。对于有相同属性状态的属性数据流 信息可以合并，因而{non-null:m＝true，p＝true}，{non-null:m＝true，p＝false}可以 合并，{may-null:m＝false，p＝true}，{may-null:m＝false，p＝false}可以合并。合并 后的属性数据流信息为{non-null:m＝true}，{may-null:m＝false}。

8)n9节点是一个分支节点。对于真分支m＝true，属性数据流信息为 {non-null:m＝true}；对于假分支m＝false，属性数据流信息为{may-null:m＝false}。

9)真分支到达n10节点，n10节点有j＝*ptr操作，操作完成后的属性数据 流信息为{non-null:m＝true}。假分支没有操作，属性数据流信息依然为 {may-null:m＝false}。

10)到达n11节点，n11是汇合节点。合并后的属性数据流信息为 {non-null:m＝true}，{may-null:m＝false}。

11)到达exit节点，属性数据流信息为{non-null:m＝true}， {may-null:m＝false}。因为属性数据流信息中的属性状态没有$error状态，所以 证明该代码片段中没有空指针解引用错误。

本发明未详细说明部分属本领域技术人员公知常识。