基于SMT求解器的一阶逻辑公式程序验证方法及系统

摘要

本发明公开了一种基于SMT求解器的一阶逻辑公式程序验证方法及系统，包括接收至少一个客户端中任一客户端发送的程序形式化验证数据交互请求；基于获取的数据验证请求内容，提取数据验证请求中的一阶逻辑公式；基于SMT求解器对上述数据验证请求中的一阶逻辑公式进行可满足性求解。本发明基于SMT求解器实现了一阶逻辑公式的自动证明，使得形式化验证系统能够对程序进行自动化验证，提高软件的可信度。

说明书

技术领域

本发明涉及计算机证明方法的技术领域，具体涉及一种基于SMT求解器的一阶逻辑公式程序验证方法及系统。

背景技术

基于演绎推理的形式化验证主要用于提高软件的可信度，在形式化验证系统的验证过程中，会产生大量的一阶逻辑公式。通过证明一阶逻辑公式的正确性，来证明程序的行为是否符合程序员的形式化描述，进而证明程序的正确性。

现有技术中，why3和boogie在程序验证领域使用都比较广泛，其主要作为程序验证工具的中间层，程序验证工具将验证得到的一阶逻辑公式转换为WhyML或Boogie语言描述，然后再通过将WhyML或者Boogie语言转换为OCaml或者SMT2语言，再调用自动定理证明器证明。其中WhyML和Boogie语言语法复杂，学习曲线大，并且WhyML和Boogie作为中间层语言，与验证者在验证工具中描述的形式化语言差异较大，例如frama-c在前端使用ACSL语言描述，其与WhyML差异较大，验证者需要同时学习ACSL和WhyML语言，不利于减轻程序验证者的负担。同时将WhyML和Boogie转换为后端自动定理证明器输入语言OCaml或者SMT2时，转换后的证明文件内容可读性较差，不利于用户的读取和理解。基于现状，亟待开发一种基于SMT求解器的一阶逻辑公式验证方法及系统，用于C程序的验证，实现自动定理证明。

发明内容

为解决上述现有技术的中的不足，本发明的目的在于克服现有不足，提供基于SMT求解器的一阶逻辑公式程序验证方法及系统，基于SMT求解器实现了一阶逻辑公式的自动证明，使得形式化验证系统对程序进行自动化验证，提高软件的可信度。

本发明的给出了一种基于SMT求解器的一阶逻辑公式程序验证方法，包括：

接收至少一个客户端中任一客户端发送的程序形式化验证数据交互请求；

基于获取的数据验证请求内容，提取验证数据交互请求中的一阶逻辑公式；

基于SMT求解器对上述验证数据交互请求中的一阶逻辑公式求解证明。

作为上述方案的进一步优化，基于SMT求解器对上述数据交互请求中的一阶逻辑公式求解证明具体包括如下步骤：

提取一阶逻辑公式：从验证数据交互请求中获取初始一阶逻辑公式；

一阶逻辑公式预处理：基于获取的SCSL语言描述的一阶逻辑公式进行预处理，通过前端的语法分析生成中间语法树AST，化简一阶逻辑公式，削减变量，并构造一阶逻辑公式的否命题作为证明目标。

SMT2代码生成处理：预处理后输入一阶逻辑公式，遍历语法树，遍历不同的表达式节点，生成节点对应的SMT2语句，并输出到字符缓冲区(或文件缓冲区)；

SMT求解器：使用SMT求解器对一阶逻辑公式生成的SMT2语句进行求解；

结果分析处理：基于SMT求解器对一阶逻辑公式的证明结果进行分析，构建证明子目标，将一阶逻辑公式划分为子目标进行求解；

输出证明结果：输出证明结果，若结果不通过，输出未通过的子目标的一阶逻辑公式。

作为上述方案的进一步优化，在所述SMT2代码生成处理中，引入引理辅助证明一阶逻辑公式。并且实现了引理自动证明，用于对被引入的引理进行自动证明，以保证被引入的引理不会影响一阶逻辑公式证明的可靠性。

作为上述方案的进一步优化，引理自动证明中，设置前驱引理和目标引理，前驱引理用来对目标引理进行辅助证明；并通过语法定义了前驱引理和目标引理间的依赖关系；通过不断添加前驱引理作为当前目标引理的先验知识，以解决当前目标引理无法证明的问题。

作为上述方案的进一步优化，所述一阶逻辑公式预处理包括：

语法树AST生成:通过前端的语法分析将一阶逻辑公式生成中间语法树AST；

消减变量：对一阶逻辑公式中的常量进行代换；对一阶逻辑公式中相等变量，设置同一变量进行代换；

常量表达式计算：对于一阶逻辑公式中的可计算的常量计算表达式进行计算；

移除重复布尔型子式：移除一阶逻辑公式中的重复布尔(bool)型子式；

断言拆分和拼接：对于一阶逻辑公式中的量化断言尝试拆分和拼接处理。经过上述预处理流程，化简断言，削减变量，以提高SMT求解器的证明能力；

证明目标构造：构造一阶逻辑公式的否命题作为证明目标逻辑公式。

作为上述方案的进一步优化，所述引理证明分析包括：

构建引理集合；

分析引理间的依赖关系，对引理集合进行排序；

按照顺序对引理进行证明，按照归纳证明原理构造归纳假设。其中，根据引理的属性将引理的证明分为结构归纳证明和自然数归纳证明：结构归纳证明用于证明代数数据类型的归纳性质证明；自然数归纳证明用于整数类型的归纳性质证明；

将构造的归纳假设，调用SMT2代码生成器，将归纳假设的一阶逻辑公式转换为SMT2语句，再使用SMT求解器证明；

输出引理证明结果。

作为上述方案的进一步优化，所述结果分析处理包括：

若SMT求解器返回的结果值为不满足，直接输出待验证一阶逻辑公式的证明结果为真；

若SMT求解器返回的结果值为满足或未知，拆分待验证一阶逻辑公式的蕴含式右件为合取子式，构建新的一阶逻辑公式作为证明子目标；

求解证明新构建的子目标：

若所有子目标证明结果为通过，输出待验证一阶逻辑公式的证明结果为真；

若存在部分子目标未通过，输出待验证一阶逻辑公式的证明结果为假，且将未通过的子目标输出。

本发明还给出了一种基于SMT求解器的一阶逻辑公式验证系统，该系统应用于一服务器，该服务器与至少一个客户端连接；包括：

第一接收模块，用于接收至少一个客户端中任一客户端发送的程序形式化验证数据交互请求；

第一提取模块：用于根据获取的数据验证请求内容，提取数据验证请求中的一阶逻辑公式；

第一证明模块：用于根据SMT求解器对上述数据验证请求中的一阶逻辑公式求解证明。

作为上述方案的进一步优化，还包括：

一阶逻辑公式预处理模块：基于获取的SCSL语言描述的一阶逻辑公式进行预处理，通过前端的语法分析生成中间语法树AST，化简一阶逻辑公式，削减变量，并构造一阶逻辑公式的否命题作为证明目标。

SMT2代码生成模块：预处理后输入一阶逻辑公式和辅助证明的引理的中间语法树AST，遍历语法树，遍历不同的表达式节点，生成节点对应的SMT2语句；

SMT求解器模块：用于将经过SMT2代码生成处理后的一阶逻辑公式在SMT求解器求解证明；

结果分析处理模块：用于SMT求解器对一阶逻辑公式的证明结果进行分析，构建证明子目标，将一阶逻辑公式划分为子目标进行求解；

输出证明结果模块：用于输出一阶逻辑公式的证明结果和未通过子目标的一阶逻辑公式。

作为上述方案的进一步优化，还包括引理证明分析模块，用于根构建引理集合；分析引理间的依赖关系，对引理集合进行排序；按照顺序对引理进行证明，按照归纳证明原理构造归纳假设；将构造的归纳假设，调用SMT2代码生成器，将一阶逻辑公式转换为SMT2语句，再使用SMT求解器证明；

本发明还给出了一种基于SMT求解器的一阶逻辑公式验证装置，所述装置包括：

一个或多个处理器；

存储器，用于存储一个或多个程序，当所述一个或多个程序被所述一个或多个处理器执行时，使得所述一个或多个处理器执行如权利要求1-9任一所述的基于SMT求解器对包含一阶逻辑公式的程序验证方法。

本发明采用上述的技术方案，与现有技术相比，一种基于SMT求解器的一阶逻辑公式验证方法及系统，具有以下技术效果：

1、本发明的基于SMT求解器的一阶逻辑公式程序验证方法及系统，基于SMT求解器实现了一阶逻辑公式的自动证明，使得形式化验证系统对程序进行自动化验证，提高软件的可信度。

2、本发明的基于SMT求解器的一阶逻辑公式程序验证方法及系统，基于SMT求解器，输入的一阶逻辑公式仍使用SCSL语言描述，与验证者在验证工具中描述程序性质的语言一致，将输入转化为SMT2语言时，尽可能使用一阶逻辑公式中的变量符号，使得转化后的SMT2语句内容与输入对应，具有可读性，且有效减轻程序验证者的负担。

3.本发明的基于SMT求解器的一阶逻辑公式程序验证方法，在将输入转化为SMT2语言前，进行一阶逻辑公式的预处理，替换一阶逻辑公式的常量，采用同一变量代换相等变量，移除一阶逻辑公式的重复布尔型子式，针对一阶逻辑公式存在的量化断言进行拆分和拼接，以提高SMT求解器的证明能力。

4.本发明的基于SMT求解器的一阶逻辑公式程序验证方法，还通过引入引理解决SMT求解器证明能力不足的问题。为了对被引入引理的正确性进行自动证明，还实现了引理自动证明模块。在引理的自动证明中，目标引理可能由于SMT求解器的限制，本身无法得到证明，这就失去了引入引理的意义。通过设置多个前驱引理辅助目标引理的证明，通过不断添加前驱引理作为目标引理的先验知识，解决目标引理无法证明的问题，进而确保SMT求解器的证明能力。

附图说明

通过阅读参照以下附图所作的对非限制性实施例所作的详细描述，本申请的其它特征、目的和优点将会变得更明显：

图1为本发明的基于SMT求解器的一阶逻辑公式程序验证方法的预处理流程图；

图2为本发明的基于SMT求解器的一阶逻辑公式程序验证方法的代码生成流程图；

图3为本发明的基于SMT求解器的一阶逻辑公式程序验证方法的引理证明流程图；

图4为本发明的基于SMT求解器的一阶逻辑公式程序验证方法的结果分析流程图；

图5为本发明的基于SMT求解器的一阶逻辑公式程序验证系统的结构框图；

具体实施方式

应当理解，此处所描述的具体实施例仅用以解释本发明，并不用于限定本发明。

本发明的给出了一种基于SMT求解器的一阶逻辑公式验证方法，该方法应用于一服务器，该服务器与至少一个客户端连接；包括：

接收至少一个客户端中任一客户端发送的程序形式化验证数据交互请求；

基于获取的数据验证请求内容，提取数据交互请求中的一阶逻辑公式；

基于SMT求解器对上述数据交互请求中的一阶逻辑公式求解证明。

本发明的一种基于SMT求解器的一阶逻辑公式验证方法，基于SMT求解器实现了一阶逻辑公式的自动证明，使得形式化验证系统可以对程序进行自动化验证。

现有技术中，普遍采用why3和boogie在程序验证领域使用：

why3：提供一种丰富的语言，称为WhyML，将其作为C程序验证的中间语言，然后通过调用其他自动证明器或者交互式证明器证明，法国的软件安全实验室开发Frama-c平台用于程序的分析及其验证，其用于程序的形式化验证的WP(Weakest Precondition)工具，将形式化描述的语言，转化为WhyML，并将why3等工具作为自动定理证明器。

boogie：提供Boogie语言，用以描述一阶逻辑公式，并通过SMT求解器证明，其主要作为其他程序验证工具(如VCC和Dafny等)的中间层。

通过程序验证工具将验证得到的一阶逻辑公式转换为WhyML或Boogie语言描述，再将WhyML或Boogie语言转换为OCaml或者SMT2语言，从而调用自动定理证明器进行证明。

参见图5，图5为本发明的基于SMT求解器的一阶逻辑公式验证系统的结构框图；基于SMT求解器对上述数据交互请求中的一阶逻辑公式求解证明具体包括如下步骤：

提取一阶逻辑公式：从数据交互请求中获取初始一阶逻辑公式；

一阶逻辑公式预处理：基于获取的SCSL语言描述的一阶逻辑公式进行预处理，通过前端的语法分析生成中间语法树AST，化简一阶逻辑公式，削减变量，并构造一阶逻辑公式的否命题作为证明目标。

SMT2代码生成处理：预处理后输入一阶逻辑公式和辅助证明的引理的中间语法树AST，遍历语法树，遍历不同的表达式节点，生成节点对应的SMT2语句，并输出到字符缓冲区(或文件缓冲区)；

SMT求解器：使用SMT求解器对一阶逻辑公式生成的SMT2语句进行求解；

结果分析处理：基于SMT求解器对一阶逻辑公式的证明结果进行分析，构建证明子目标，将一阶逻辑公式划分为子目标进行求解；

输出证明结果：输出证明结果，若结果不通过，输出未通过的子目标的一阶逻辑公式

引理自动证明：用于一阶逻辑公式证明中引入的辅助引理的自动证明。

参见图1和图2，图1为本发明的基于SMT求解器的一阶逻辑公式验证方法的预处理流程图；图2为本发明的基于SMT求解器的一阶逻辑公式验证方法的SMT2代码生成流程图。一阶逻辑公式预处理包括：

语法树AST生成:通过前端的语法分析将一阶逻辑公式生成中间语法树AST；

消减变量：对一阶逻辑公式中的常量进行代换；对一阶逻辑公式中相等变量，设置同一变量进行代换；

常量表达式计算：对于一阶逻辑公式中的可计算的常量计算表达式进行计算；

移除重复布尔型子式：移除一阶逻辑公式中的重复布尔(bool)型子式；

断言拆分和拼接：对于一阶逻辑公式中的量化断言尝试拆分和拼接处理。经过上述预处理流程，化简断言，削减变量，以提高SMT求解器的证明能力。

证明目标构造：构造一阶逻辑公式的否命题作为证明目标逻辑公式。

更具体的，主要通过常量替换和变量代换后，对一阶逻辑公式中的可计算的常量进行计算；针对一阶逻辑公式中的相等变量，使用同一变量进行代换，消除变量；优选实施例中，对于一阶逻辑公式中的可计算的常量计算表达式进行计算，如1+5，替换为6；a＝＝>ture代换为true。优选实施例中，对于一阶逻辑公式中的量化断言尝试拆分和拼接，如(forall i.0<＝i<＝10＝＝>P(i))&&P(11)转化为forall i.0<＝i<＝11＝＝>P(i)。

具体的，经过预处理的一阶逻辑公式生成并输出SMT2语句具体包括如下内容：

传输基于SCSL语言描述的一阶逻辑公式至可执行平台；在此需特别说明的是，本发明实施例公开的可执行平台具体为具备程序运算和数据处理能力的设备；

获取一阶逻辑公式，根据语法分析生成中间语法树；

遍历中间语法树的表达式节点，标记节点对应的变量、变量类型和谓词，对应生成节点的SMT2语句缓存并输出可执行平台。

本发明通过公开一种基于SMT求解器的一阶逻辑公式验证方法，在其输入的一阶逻辑公式使用SCSL语言描述，与用户在验证工具中描述程序性质的语言保持一致，便于验证工具描述；并在转换为SMT2语言时，尽可能采用一阶逻辑公式中的变量符号，便于读写。

作为上述方案的进一步优化，参见图3，图3为本发明的基于SMT求解器的一阶逻辑公式验证方法的引理证明流程图。在所述SMT2代码生成处理中，引入引理辅助证明一阶逻辑公式。并且实现了引理自动证明，用于对被引入的引理进行自动证明，以保证引入的引理不会影响一阶逻辑公式证明的可靠性。引理自动证明中，设置前驱引理和目标引理，前驱引理用来对目标引理进行辅助证明；并通过语法定义了前驱引理和目标引理间的依赖关系；通过不断添加前驱引理作为当前目标引理的先验知识，以解决当前目标引理无法证明的问题。

引理自动证明包括：

构建引理集合；

分析引理间的依赖关系，对引理集合进行排序；

按照顺序对引理进行证明，按照归纳证明原理构造归纳假设。其中，根据引理的属性将引理的证明分为结构归纳证明和自然数归纳证明：结构归纳证明用于证明代数数据类型的归纳性质证明；自然数归纳证明用于整数类型的归纳性质证明；

将构造的归纳假设，调用SMT2代码生成器，将归纳假设的一阶逻辑公式转换为SMT2语句，再使用SMT求解器证明

输出引理证明结果。

一阶逻辑公式的验证通过SMT求解器进行可满足性判定，由于满足性判定问题是NP-完全问题，无法在理论上对所有一阶逻辑公式进行可满足性判定，即SMT求解器理论上具有局限性，无法判定所有问题，导致部分一阶逻辑公式无法证明验证，为此本方法和系统添加了一阶逻辑公式的预处理和引入引理，来解决SMT求解器证明能力不足的问题。同时为了保证引入引理后证明结果的可靠性，本方法和系统还对引入引理的正确性进行了自动证明。

在实际进行引理的自动证明过程中，由于引理可能由于SMT求解器的限制，本身无法得到证明；本发明为了能够有效避免该问题，通过添加其他引理作为前驱引理来辅助当前目标引理的证明；如，设置目标引理p1的证明需要p2作为前驱引理，则定义p1依赖于p2；在SCSL语言中，使用依赖语法进行描述；在此需要特别说明的是，前驱引理包括但不限于一条引理，即根据实际需要的目标引理，可添加多条前驱引理进行证明。

本发明基于引理证明，根据归纳证明原理构造归纳假设，并且调用SMT2代码生成器，转换为SMT2文件，使用SMT求解器证明。

参见图4，图4为本发明的基于SMT求解器的一阶逻辑公式验证方法的结果分析流程图；具体的，SMT求解器的证明分析结果包括如下：

若SMT求解器返回的结果值为不满足，直接输出待验证一阶逻辑公式的证明结果为真；

若SMT求解器返回的结果值为满足或未知，拆分待验证一阶逻辑公式的蕴含式右件为合取子式，构建新的一阶逻辑公式作为证明子目标；

求解证明新构建的子目标：

若所有子目标证明结果为通过，输出待验证一阶逻辑公式的证明结果为真；

若存在部分子目标未通过，输出待验证一阶逻辑公式的证明结果为假，且将未通过的子目标输出。其中，求解证明新构建的子目标，通过SMT2代码生成处理，生成对应的SMT2语句；再将对应的SMT2语句通过在SMT求解器中求解证明。

参见图5，图5为本发明的基于SMT求解器的一阶逻辑公式验证系统的结构框图；本发明还给出了一种基于SMT求解器的一阶逻辑公式验证系统，该系统应用于一服务器，该服务器与至少一个客户端连接；包括：

第一接收模块，用于接收至少一个客户端中任一客户端发送的程序形式化验证数据交互请求；

第一提取模块：用于根据获取的数据验证请求内容，提取验证数据交互请求中的一阶逻辑公式；

第一证明模块：用于根据SMT求解器对上述验证数据交互请求中的一阶逻辑公式求解证明。

参见图5，

一阶逻辑公式预处理模块100：基于获取的SCSL语言描述的一阶逻辑公式进行预处理，通过前端的语法分析生成中间语法树AST，化简一阶逻辑公式，削减变量，并构造一阶逻辑公式的否命题作为证明目标。

SMT2代码生成模块200：预处理后输入一阶逻辑公式和辅助证明的引理的中间语法树AST，遍历语法树，遍历不同的表达式节点，生成节点对应的SMT2语句；

SMT求解器模块：用于将经过SMT2代码生成处理后的一阶逻辑公式在SMT求解器求解证明；

结果分析处理模块400：用于SMT求解器对一阶逻辑公式的证明结果进行分析，构建证明子目标，将一阶逻辑公式划分为子目标进行求解；

输出证明结果模块：用于输出一阶逻辑公式的证明结果和未通过子目标的一阶逻辑公式。

引理证明分析模块300，用于被引入引理的自动证明。根构建引理集合；分析引理间的依赖关系，对引理集合进行排序；按照顺序对引理进行证明，按照归纳证明原理构造归纳假设；将构造的归纳假设，调用SMT2代码生成器，将归纳假设的一阶逻辑公式转换为SMT2语句，再使用SMT求解器证明。

本发明的基于SMT求解器的一阶逻辑公式程序验证系统用于安全C验证系统产生的一阶逻辑公式的自动证明，基于SMT求解器实现，常用的SMT求解器有Z3、CVC4、Yices。通过求解一阶逻辑公式的非的可满足性，若返回结果为不可满足，则说明该一阶逻辑公式永真。为了解决SMT求解器证明能力不足的问题，实现了一阶逻辑公式的预处理，证明策略调整和引入引理等辅助证明方案。并实现了引入引理的自动证明。

本发明的基于SMT求解器的一阶逻辑公式程序验证系统实现的系统输入为SCSL语言描述的一阶逻辑公式和SCSL语言描述的引理。输出为转化后的SMT2语句、一阶逻辑公式证明结果和引理证明结果。基于SMT求解器实现了一阶逻辑公式的自动证明，使得形式化验证系统对程序进行自动化验证，提高软件的可信度。

以上描述仅为本申请的较佳实施例以及对所运用技术原理的说明。本领域技术人员应当理解，本申请中所涉及的发明范围，并不限于上述技术特征的特定组合而成的技术方案，同时也应涵盖在不脱离所述发明构思的情况下，由上述技术特征或其等同特征进行任意组合而形成的其它技术方案。例如上述特征与本申请中公开的(但不限于)具有类似功能的技术特征进行互相替换而形成的技术方案。