面向C源码的自动化形式化验证工具及方法

摘要

本发明公开了面向C源码的自动化形式化验证工具及方法，将编写好的代码功能规范插入C源码中，然后将功能规范和C源码自动转换成程序验证器可处理的中间表示，接着程序验证器将中间表示转换成中间验证语言代码，供形式化验证输入使用；采用形式化方法，可对转换的源代码进行自动化的形式化验证，以验证源代码的功能性和安全性。在各接口函数通过代码功能正确性验证的基础上，利用行为建模语言和组合验证技术构建抽象模型；然后利用模型仿真引擎和属性检测引擎模拟交互行为，验证安全属性，判断代码是否满足安全属性规范。本发明能够以自动化的形式，实现对C源码的形式化验证，其中使用的中间表示生成器可以自动化生成中间表示，程序验证器可以自动化生成中间验证语言代码，模型仿真引擎和属性检测引擎可以自动化验证安全属性，这些措施可以极大的提高C源码验证的效率，减少人工参与度。

说明书

技术领域

本发明涉及C语言源代码安全技术领域，具体涉及面向C源码的自动化形式化验证工具及方法。

背景技术

形式化验证方法是使用数学的公式、定理和系统来验证一个系统的正确性。形式化验证过程可以证明一个系统不存在某个缺陷或符合某个或某些属性。软件测试无法证明系统不存在缺陷，也不能证明它符合一定的属性。系统无法被证明或测试为无缺陷，这是因为不可能形式地规定什么是“没有缺陷”。所有可以做的，就是证明一个系统没有任何可以想到的缺陷，并且满足所有的功能规范和安全属性。

C语言是一种通用的编程语言，由于具有高效、灵活、功能丰富、表达力强和较高的可移植性等特点，在程序设计中备受青睐，应用于许多重点领域。如果C语言程序设计出现漏洞，或将产生重大损失。形式化验证方法可以很好的检验和验证C语言代码的漏洞，但传统的形式化验证方法主要依赖于手工验证，工作量大，效率较低，并且对使用形式化验证方法的程序员要求较高。

发明内容

本发明的目的在于提供一种面向C源码的自动化形式化验证工具及方法，解决上述C语言代码面临的安全问题以及传统形式化验证工作量大、验证效率低的问题。

本发明通过下述技术方案实现：

面向C源码的自动化形式化验证工具，包括：

中间表示生成器：用于将C源码和插入的功能规范转换成中间表示，并输入到程序验证器；程序验证器：用于接收中间表示，并将中间表示转换成C代码类型、语义一致的中间验证语言代码，并输入到自动化验证模块，由自动化验证模块的自动化验证器对该中间验证语言代码进行自动化的形式化验证，得出验证结果；

自动化验证模块：用于提供多种自动化验证器，可根据用户的输入参数对自动化验证进行配置；

抽象模型编译器：用于接收建模语言编写的代码，并将建模代码编译成为抽象模型；

模型仿真引擎：用于根据仿真的输入参数对抽象模型进行仿真模拟，输出仿真模拟的过程中抽象模型的各种状态和属性；

属性检测引擎：用于接收用特定语法编写的安全属性公式，并利用模型仿真引擎和生成的抽象模型模拟交互行为，验证安全属性公式定义的安全属性，得出验证结果。

本发明面向C源码的自动化形式化验证工具，将C源码和根据其功能要求编写的功能规范导入形式化验证工具的中间表示生成器，能够自动化地生成程序验证器所需的中间表示，程序验证器接收中间表示后自动转换成中间验证语言代码，然后输入到自动化验证模块进行验证，能够得出代码功能正确性的验证结果；在各接口函数通过代码功能正确性验证的基础上，利用行为建模语言编写建模代码，输入到抽象模型编译器中生成抽象模型，然后利用模型仿真引擎和属性检测引擎模拟交互行为，验证安全属性，能够判断代码是否满足安全属性规范。本发明工具能够以较高程度的自动化，对C源码进行形式化安全验证，其中使用的中间表示生成器可以自动化生成中间表示，程序验证器可以自动化生成中间验证语言代码，模型仿真引擎和属性检测引擎可以自动化验证安全属性，这些措施可以极大的提高C源码验证的效率，减少人工参与度。

面向C源码的自动化形式化验证方法，包括以下步骤：

步骤001：使用自然语言编写C源码的功能需求描述文档，C源码的功能需求描述文档包括目标C源码功能规范描述和安全属性描述；

步骤002：根据C源码函数之间的交互关系，抽象出一个有限状态机；

步骤003：借助步骤001中文档描述的目标C源码功能规范和霍尔逻辑，生成C语言描述的C源码功能规范；

步骤004：将C语言描述的C源码功能规范插入C源码中，然后进行代码功能正确性自动化形式化验证，得到功能正确性验证报告；

步骤005：在各接口函数通过功能正确性验证的基础上，借助步骤002中所得到的有限状态机，定义出状态变量和转移关系，然后用建模语言编写建模代码；

步骤006：借助步骤001中文档描述的安全属性，利用线性时序逻辑(LTL)构建安全属性公式；

步骤007：借助步骤005中得到的建模代码和步骤006中得到的安全属性公式，进行安全属性自动化形式化验证，得到安全属性验证报告。

进一步地，代码功能正确性验证的自动化形式化验证步骤包括：

步骤101：接收插入功能规范后的C源码，并将其输入到中间表示生成器，以生成中间表示；

步骤102：将步骤101中产生的中间表示导入到程序验证器中，转换成C代码类型、语义一致的中间验证语言代码，并输入到自动化验证器模块中；

步骤103：由自动化验证器根据输入参数的配置对步骤102中生成的中间验证语言代码进行验证，如果验证失败，生成验证失败报告，给出反例，说明该C源码不符合功能规范，再修改源代码，然后从步骤101开始重新对代码进行功能正确性验证；如果验证成功，则生成验证成功的结果，如果验证失败，再次重复此步骤，直到验证通过，生成正确的验证结果为止。

进一步地，安全属性验证的自动化形式化验证步骤包括：

步骤201：接收建模代码，并将其输入到抽象模型编译器，生成抽象模型；

步骤202：将步骤201中产生的抽象模型导入模拟仿真引擎中；

步骤203：将安全属性公式输入到属性检测引擎中，属性检测引擎会调用模拟仿真引擎对抽象模型进行模拟仿真，并在仿真模拟过程中验证公式定义的安全属性，如果验证失败，说明该C源码不符合安全属性的定义，再修改源代码，然后从步骤201开始重新对代码进行安全属性验证；如果验证成功，则生成验证成功的结果，如果验证失败，再次重复此步骤，直到验证通过，生成正确的验证结果为止。

进一步讲所述步骤203是：属性检测引擎接收人工编写的安全属性公式，判断该安全属性公式是否符合公式的语法要求，然后接收待检测的抽象模型，该抽象模型是由根据待检测代码的抽象状态机编写的建模代码编译而来。为提高验证效率，属性检测引擎会调用仿真模拟引擎来模拟抽象模型的交互行为，在用户设定的模拟参数下检测抽象模型的每一个状态转移路径是否满足安全属性定义，如果在检测的所有状态转移路径中安全属性的定义都被满足，则表明被验证的程序符合所期望的验证属性，会生成一个验证属性为真的验证结果；否则验证失败，说明源程序不符合用户设定的安全属性，存在安全问题。对于验证失败的情况，将重新修改C源码程序，并重新修改建模代码重新生成抽象模型，并重新验证，多次反复，直到验证通过为止。

本发明与现有技术相比，具有如下的优点和有益效果：

1、本发明面向C源码的自动化形式化验证系统，能够以较高程度的自动化，实现对C源码的形式化验证，其中使用中间表示生成器能够自动化生成程序验证器所需要的中间表示，程序验证器则能够自动生成中间验证语言供自动化验证器进行验证，属性验证引擎能够自动调用模拟仿真引擎模拟抽象模型的交互行为以自动化的检测程序的安全属性，这些措施能够极大的提高C源码形式化验证的效率，减少人工参与度；

2、本发明面向C源码的自动化形式化验证方法，能够对转换后的中间验证语言代码进行自动化的验证，证明源码的功能性是否符合预期，并且证明源代码是否存在逻辑漏洞，同时还能够利用抽象建模和安全属性检测证明源代码的实现是否符合安全属性的定义，是否存在安全问题；

3、本发明所提的验证系统和方法，不仅仅适用于C源码的验证，对于其他语言源码的验证，同样有效。

附图说明

此处所说明的附图用来提供对本发明实施例的进一步理解，构成本申请的一部分，并不构成对本发明实施例的限定。在附图中：

图1为本发明原理框图；

图2为示例C源码；

图3为示例简单有限状态机。

具体实施方式

为使本发明的目的、技术方案和优点更加清楚明白，下面结合实施例对本发明作进一步的详细说明，本发明的示意性实施方式及其说明仅用于解释本发明，并不作为对本发明的限定。

实施例

如图1所示，本发明面向C源码的自动化形式化验证工具及方法，本发明开的的面向C源码的自动化形式化验证工具，验证C源码的功能正确性以及是否存在逻辑漏洞。为了能够更容易让本领域技术人员理解，以下将用图2所示的简单C源码的形式化验证为例进行说明。其并不构成对本发明的任何限制。本领域技术人员可在本发明公开的技术内容启示下，将其应用于其他语言的形式化验证，如java、Go等。本例中以图2所示的简单C源码的形式化验证为例，结合图1，使用本发明工具对C源码的功能正确性进行形式化验证的流程进行详细阐述，主要步骤如下：

步骤S01：根据用户给出的函数功能要求，此处函数功能要求为输入参数n大于100时，输出结果为n-10，输入参数n小于100时，输出结果为91，基于霍尔逻辑用C语言描述C源码函数的功能规范，写成assert的形式，插入C源码中，并将输入参数n设置为一个验证用的特殊int值；

步骤S02：中间表示生成器接收插入功能规范后的C源码转化成中间表示；

步骤S03：将步骤S02中产生的中间表示导入到程序验证器中，生成中间验证语言规范与代码；

步骤S04：将步骤S03中产生的中间验证语言规范与代码导入到自动化验证器模块中；

步骤S05：通过函数特点设定自动化验证参数对自动化验证器进行配置，例如这段C源码包含递归调用，需要设定自动化验证的展开次数，设定好之后由自动化验证器对中间验证语言规范和代码进行自动化的验证，若在验证过程中发现不符合功能规范的执行路径，那么验证将停止，然后把此执行路径的输入参数x作为反例输出到验证报告中，同时还将输出此执行路径的函数调用情况，包括函数的输入参数以及返回值到验证报告中，给出一个验证失败的验证报告，这说明C源码对应函数不符合用户给定的函数功能要求，源码的功能性不符合预期；如果在验证过程中未发现不符合功能规范的执行路径，那么表示验证成功，给出验证成功的验证报告。

本发明开的的面向C源码的自动化形式化验证工具，验证C源码的安全属性是否被满足。为了能够更容易让本领域技术人员理解，以下将用图3所示的简单有限状态机的建模和形式化验证为例进行说明。其并不构成对本发明的任何限制。结合图1，使用本发明工具对C源码的安全属性进行形式化验证的流程进行详细阐述，主要步骤如下：

步骤P01：根据有限状态机，定义出状态变量和转移关系，并用建模代码表示，例如s_leave表示出场态、s_initass表示初装态、s_ready表示就绪态、s_run表示工作态；a_init_ass表示初装动作、a_con_ass表示配装动作、a_start表示开机动作、a_shutdown表示关机动作、a_fst_des表示一级销毁动作、a_snd_des表示二级销毁动作。再由上述解析出的状态机中存在的状态和转移动作，编写建模代码；

步骤P02：根据用户描述的安全属性，例如此处用户描述的一条安全属性为“工作态”终将可达且所需资源均已配置完成，利用线性时序逻辑(LTL)构建安全属性公式如下所示：G{n}(CtrlProtocol.a＝＝a_snd_dex＝>F{1}(CtrlProtocol.s＝＝s_initass))

步骤P03：接收建模代码，并将其输入到抽象模型编译器，抽象模型编译器会自动编译生成抽象模型；

步骤P04：将步骤P03中产生的抽象模型导入模拟仿真引擎中；

步骤P05：将安全属性公式输入到属性检测引擎中，属性检测引擎会调用模拟仿真引擎对抽象模型进行模拟仿真，并在仿真模拟过程中验证公式定义的安全属性，若在验证过程中发现有某条路径不符合安全属性的定义，那么将会把这条路径统计下来，最后给出一个验证失败的验证报告；如果在验证过程中未发现发现有某条路径不符合安全属性的定义，那么表示验证成功，给出验证成功的验证报告。

以上所述的具体实施方式，对本发明的目的、技术方案和有益效果进行了进一步详细说明，所应理解的是，以上所述仅为本发明的具体实施方式而已，并不用于限定本发明的保护范围，凡是在本发明的精神和原则之内，所做的任何修改、等同替换、改进等，均应包含在本发明的保护范围之内。