面向计算机并发程序的形式化验证方法设计
面向计算机并发程序的形式化验证方法设计
摘 要：
计算机并发性程序形式化验证一直是软件安全领域的难题。软件并发性漏洞难以被发现，一旦发生问题，会造成不可估量的安全问题。形式化验证基于严格的数学推导基础，采用语言、语义、推理证明三位一体方法，构建形式逻辑系统，以确保被验证系统的安全性能。传统的形式化验证方法由于人工参与多、验证工作量大、验证效率低等不足，难以对计算机并发程序进行严谨高效的模型描述与验证。研究了一种可双向转换的并发性程序形式化验证方法，解决了人工抽象建模存在的工作量大且易出错的问题，并且保证了源码层与抽象层验证的一致性，大幅提升了形式化验证的效率。
内容目录：
1 并发性验证基本路线
2 并发性验证方法设计
2.1 中间层规范生成模块
2.2 自动化并发性验证模块设计
2.3 自动化功能性验证模块设计
2.4 集成模块设计
3 实验过程和结果
3.1 中间层规范生成
3.2 自动向上映射及并发属性验证
3.3 自动向下映射及功能性验证
3.4 验证结果分析
4 结 语
形式化验证作为一种基于严格数学推理的计算机软件安全性和可靠性保障技术，近年来已经取得了巨大的进展。但是，随着计算机系统越来越复杂，提供的功能越来越强大，其蕴含的安全性问题也日益严峻，因此对形式化验证方法提出了更高的要求。计算机并发技术在高效利用计算机资源的同时，可能存在对计算机软件安全造成很大威胁的并发错误。利用形式化验证找出软件中的并发错误并排除其带来的安全隐患成为形式化方法研究领域的一个重点方向。
基于形式化验证并发错误的研究主要包含两个方面：以定理证明为例的演绎推理方法和以模型检测为例的建模和验证方法。前者通常利用从系统生成的一组规则并进行推理证明，以验证系统是否满足指定的规则。而模型检测是一种对有限状态的并发软件系统进行自动化验证的技术，其实现方式是使用过程建模语言将需要验证的软件系统进行重新建模，将软件系统内部的数据、行为和实体进行抽象，并在系统模型代码中加入相应的并发性验证代码，最后输入到模型检查引擎中得出并发性验证结果。
经过相关工作人员的大量研究，目前针对并发程序的形式化验证工作已经有部分成效。在早期的研究中，Taylor给出并发状态、并发历史等相关概念，并且提出了一种基于并发历史的并发错误分析方法。Foster 等人将定理证明这一形式化方法引入并发问题检测中，通过对程序的形式化规约进行静态分析以检测并发性漏洞。Enans在工具 LCLint 中实现了静态检测方法，并通过内存标注来检测并发错误。在并发性形式化验证的早期研究中，检测目标的规模一般较小，复杂度不高，验证过程的自动化程度较低，难以验证大型并发软件。
在近年针对软件并发性验证的研究中，研究人员基于验证对象提出了不同的框架和方法。例如，采用符号执行、进程代数分析以及模型检测等方式和思路，对软件的并发性进行了形式化验证。相较于早期的研究，其在自动化程度上有了进一步的提升。Kaki 等人利用进程代数，提出了一种针对并发和分布式程序行为特性的验证技术，这种技术使用进程代数对建模程序行为进行自动抽象，弥补了程序实现与其模型之间的典型差距。吴亚楠设计了一个动态数据竞争检测工具，提出了一种分层过滤的方法，可以减少动态监视程序执行行为的高性能开销，以实现高效检测多线程程序的数据竞争和验证有害竞争。Foster 等人提出了一种具有大或无限状态空间的并行反应程序的代数验证策略，并利用反应关系和克莱尼代数证明了该策略的可行性。进程代数分析和符号执行的引入使得并发系统定义的精确程度有了进一步的提高，但在验证效率方面依然无法支持大型复杂软件的并发性验证工作。
随着形式化方法中模型检测技术的发展和完善，不断有研究人员将其应用在并发性形式化验证上。Guellati 等人 改进了自动状态机的模型检测算法，将基于时间计算树逻辑（Time Computation Tree Logic，TCTL）模型检查算法应用于持续动作定时自动机模型，对模型检验算法和可表达及验证的性质范围进行了改进和扩展，使得模型可以捕捉系统行为中真正的并发性。David 等人 研究了一套基于依赖保证的并发程序验证框架（CSim2），可实现对并发系统进行自顶向下的组合验证，通过使用模拟框架，在顶层上进行验证的属性被组合传播到系统每个并发组件中的最低源码层。
目前针对系统并发性形式化验证的研究在许多层面已有突破，但仍存在一些难点和问题。首先，推理低效困难，普通验证过程通常采用单一的源码或者字节码进行底层验证，并发性验证需要证明高层的安全属性，如死锁、可达性、无散度判别等。而源码级别涉及太多的无意义变量与逻辑，导致验证效率很差。其次，验证系统存在模型间的语义鸿沟，功能验证和行为验证所用的方法不同，缺乏抽象端到源码端的一致性证明。
针对计算机软件并发性验证的难点，本文提出了一种可双向转换的并发性形式化验证方法，解决了普通抽象过程中建模验证缺乏灵活性的问题，避免了对系统进行重复抽象建模，并且保证了源码层与抽象层验证的一致性。文章首先介绍了验证方法的基本路线，路线分别从代码功能正确性和行为功能正确性两方面进行程序的验证，以保证最终的验证一致性。其次对框架的整体设计思路进行了详尽的描述，方法根据输入的源码应用程序接口（Application Programming Interface，API）与功能需求文档，通过模型规范提取器和形式化命题生成器抽取规范表示并输入到中间映射层，自动向上映射 生 成 相 应 的 通 信 顺 序 进 程（Communication Sequential Process，CSP）模型，向下映射生成相应的功能性规范。经过自动验证器完成并发性验证和功能性验证。最后基于该并发性验证方法进行应用案例分析。
1并发性验证基本路线
以 CSP 过程建模为例的并发性形式化验证方法使用模型检查技术，通过系统抽象获取整体模型，利用自动化验证器完成并发性验证。为保证系统整体的安全性，还需要对计算机软件的功能正确性进行验证，但是因为系统中存在模型间的语义鸿沟，无法保证并发性验证模型和功能正确性验证模型的一致性。如果交由人工编写功能规范再进行复杂的一致性推理，则会严重影响验证效率。为此，本文提出了一种可以保证源码端和抽象端一致性的可双向转换的并发性验证方法。方法路线如图 1 所示。
图 1 方法路线
基于输入的源码 API 及其用自然语言给出的功能规范，路线分为代码端的功能正确性验证和抽象端的行为并发性验证。整体的验证路线为首先根据提供的函数 API以及需求规范说明文档进行规范提取，然后转化为一种抽象度居中的中间层规范。这种中间层规范既可以自动向上映射为高层规范并输入到并发性验证模块中进行并发属性验证，也可以自动向下映射为源码层规范并输入到功能性验证模块中进行功能正确性验证，经过两条路线验证后，最终得到验证结果。整体的验证步骤如图 2 所示。
图2 验证步骤
中间层规范是指对源码规范与需求进行了适度抽象的形式化表示。一方面，中间层规范不仅完整地描述了底层程序功能，而且过滤了程序实现细节，使得程序安全验证可同时映射高层与底层两个方向，解决了高层抽象验证与源码级验证之间存在的语义鸿沟，提供了高层属性端到源码端的一致性验证。另一方面，生成中间层规范时可以一次性覆盖所有源码 API，从中间层规范自动向上映射出过程模型分析系统并发属性，避免了对整个系统进行人工的重复建模，提高了系统灵活性。
2并发性验证方法设计
可双向转换的并发性验证方法设计架构整体可分为中间层规范生成模块、自动化功能性验证模块、自动化并发性验证模块以及集成模块。其中，中间层规范生成模块主要用于将源码 API信息与文档功能需求整合并生成一种可以双分支映射的中间层规范；自动化功能性验证模块主要通过自动向下映射机制使中间层规范转化为源码级验证模型，再通过自动化功能性验证工具进行功能性验证，并得出功能正确性验证结果；自动化并发性验证模块主要通过自动向上映射机制使中间层规范转换为抽象过程模型，再通过自动化并发性验证工具进行并发属性验证，得到并发性验证结果；集成模块根据并发属性验证与功能性验证的结果，最终生成具有跨模型逻辑一致性的安全验证结果。
2.1 中间层规范生成模块
设计中间层规范模块由形式化命题生成器、模型规范提取器和中间层规范生成器组成。模块结构设计如图 3 所示。
图 3 中间层规范模块结构设计
形式化命题生成器用于对输入的源码进行形式化表示，通过分析待验证程序中所有的变量，将其作为所述中间层规范中的行为载体；确定待验证程序中的主要状态变迁依靠的函数，将其设置为功能元素；隐藏底层内存状态，引入等价的抽象状态用于表述底层完整功能逻辑，忽略函数变量具体的取值，只考虑相应的状态变迁及变迁条件，并描述出函数具体内部逻辑。模型规范提取器根据提供的代码流程以及相应的需求说明文档，将文档中关于代码的逻辑限制转化为便于进行形式化描述的模型规范。获得的模型规范为一种抽象度居中的形式化描述，用于输入到中间层规范生成器中。中间层规范生成器根据输入的形式化命题与相应的模型规范，整合成为一种抽象度居中的中间层规范。从整体而言，中间层规范模块一次性处理所有的 API，转化为所述中间层规范。
将中间层规范输入到自动化功能性验证模块与自动化并发性验证模块，即可进行自动化验证和并发性验证。
2.2 自动化并发性验证模块设计
自动化并发验证模块主要负责提供抽象端的并发性验证，通过双向转换器将中间层规范自动向上映射为抽象层规范。其完成并发性验证的具体步骤描述如下：
步骤 1：根据所述中间层规范表现出的状态间逻辑关系进行抽象；
步骤 2：确定状态间转移条件，形成不同的抽象路径，每条路径包含相应的前置后置状态；
步骤 3：对所述中间层规范进行分析，确定路径相关性，将并发的路径并列起来，生成相应的高层规范；
步骤 4：根据高层规范得到高层抽象状态机，并参考系统的状态迁移属性，推理出状态迁移合法性规则，编写高层属性规范；
步骤 5：依据所述高层抽象状态机中的状态、行为及逻辑信息，形成可用于并发推理的抽象过程模型，再根据所述高层规范与所述高层属性规范，生成并插入并发安全属性语句，最后进行并发属性验证。
2.3 自动化功能性验证模块设计
自动化功能性验证模块主要负责提供源码级的功能正确性验证，在生成可双向映射的中间层规范后，经由双向转换器自动向下映射为源码级规范，经过细节抽取、验证函数生成、规范生成和最终验证 4 个步骤完成功能性验证。关键步骤描述如下：
步骤 1：根据所述中间层规范给出的函数调用关系，抽取函数实现逻辑以及函数内部变量的数据结构和传递条件；
步骤 2：根据所述数据结构和传递条件，分析函数应达到的安全标准，将其生成为一个源码级形式化规范；
步骤 3：将生成的所述源码级形式化规范插入到源码中，形成源码级验证模型；
步骤 4：将转换输出的所述源码级验证模型进行功能性验证。系统整体的工作流程图如图4所示。
图 4 自动并发验证工作流程
2.4 集成模块设计
集成模块由结果生成器组成。结果生成器根据中间层规范模块中的并发属性验证与功能性验证情况，生成具有跨模型逻辑一致性的安全验证结果。
集合模块整合了属性并发性和功能正确性的验证结果，最后生成一份源码安全性报告。
3实验过程和结果
本文以一个 C 语言实现的融资程序为案例，采用第二节所述的双向并发性验证方法对程序进行验证：
案例程序主要的功能为控制融资金额，预先给定一个最低融资目标，当实际融资金额小于融资目标时，可以进行相应的融资操作；当融资金额大于或等于相应的融资目标时，更新融资状态为关闭状态。此案例涉及金融安全领域，对代码安全性要求较高，因此需要采用形式化验证方法使程序满足相应的安全性需求。本文将对该程序生成抽象度居中的中间层规范，再进行双向自动化映射以及验证器验证，最后根据结果分析说明本文所述方法的有效性。
3.1 中间层规范生成
步骤 1：首先对于案例程序来说，确定声明中 goal 与 raised 为函数变量，在中间层规范中体现为实际的行为载体；再确定程序内部状态变迁的主要逻辑依靠 invest 函数内部行为来实现，则将 invest 定义为中间层规范中的 FUNCTION元素。
步骤 2：函数内部逻辑为当融资金额小于目标时，进行融资操作；考虑到中间层规范既要隐藏底层具体繁杂的内存状态，又要引入等价的抽象状态用于表述底层完整功能逻辑，raised涉及两种状态，则将其声明为一个 old(raised) 带有时间性质的元素类型，当 old(raised)
步骤 3：根据上述操作，将程序中所有 API都整合为中间层规范；本例中 invest 整合出的中间层规范为：
3.2 自动向上映射及并发属性验证
步骤 1：根据中间层规范中表现出的状态间逻辑关系进行抽象。
步骤 2：确定每个状态之间的转移条件，形成不同的抽象路径，每条路径包含相应的前置后置状态。对于本例来说，中间层规范中的 invest函数抽象出的路径为两条，以第一条路径为例，前 置 条 件 为 (raised
步骤 3：对完整的中间层规范进行分析，确定每一条路径的相关性，将可并发产生的路径并列起来；经过对所有路径的分析，得到的 invest高层规范代码为：
步骤 4：根据高层规范得到 invest 函数高层抽象状态机，参考整个系统的状态迁移属性，推理出状态迁移合法性规则，编写高层属性规范。在本例中，参考 invest 函数路径，考虑到一旦募集成功，融资金额不能低于最低融资目标，则本例得到的高层属性规范代码为：
步骤 5：根据高层规范，生成相应的 CSP 模型代码；根据相应的高层属性规范及系统需求文档给出的并发性要求，编写相应的并发属性判 断 语 句， 如：#assert P() deadlock，#assert P() deterministic 等；并将判断语句插入到 CSP 抽象过程模型代码中，最后输入到自动化并发验证模块进行系统并发模拟验证，并得出并发性验证结果。
3.3 自动向下映射及功能性验证
步骤 1：根据中间层规范给出的函数调用关系，抽取具体的函数实现逻辑，以及函数内部变量的数据传递结构和传递条件。
步骤 2：根据具体的数据传递结构及条件，自动化分析函数模块应该达到的安全标准，将其生成为一个单独的验证函数。在本例中，参考中间层规范中表述当 raised 旧值小于最低目标融资时，函数会进行融资操作，自动生成一条判断函数语句：assert(raised == old_raised + value)。
步骤 3：将自动生成的单独验证函数插入到源码中，形成最后输出的源码级规范，本例生成代码为：
步骤 4：将生成的源码级规范输入到功能性验证工具中，根据规范中单独的验证函数为功能性验证工具调整参数，使其可以完全覆盖函数本身的逻辑分支，并得出功能性验证结果。
3.4 验证结果分析
上述案例首先通过代码逻辑信息及功能需求整合出了相应的中间层规范，描述了行为载体goal，raised，state 与功能元素 invest，close 之间的逻辑关系。一方面，通过自动向上映射生成了高层规范，根据 invest 元素的功能逻辑编写了高层属性规范，最终插入相应并发性断言进行了自动化并发性验证。另一方面，通过自动向下映射生成了相应的源码级规范，根据 raised 行为载体的逻辑需求插入了功能性断言并进行了自动化功能性验证。
在本例中，自动化并发性验证模块与功能性验证模块给出的验证结果均为正确，表示验证过程中生成规范与断言均得到了满足，源码层的功能性规范与抽象层的并发属性规范通过了验证。验证结果表明，本例设计的形式化验证方法成功证明了融资程序的源码级实现与相应抽象层属性之间的逻辑一致性。
在验证流程中，一方面，通过中间层规范双向映射的验证方法，消除了高层抽象验证与源码级验证的语义鸿沟。另一方面，生成中间层规范时一次性覆盖了所有源码 API，避免了对系统进行人工重复建模。在实际验证流程中，双向映射过程采用自动化工具完成，相较于传统并发程序验证采用的手动验证方式，降低了人工参与度，提高了验证效率。
４结 语
本文以 C 语言程序源码的并发性验证方法为研究对象，提出了一种可双向转换的并发性验证方法，针对传统并发性验证建模缺乏灵活性的问题进行了改进，并在整个验证过程中提供了从抽象端到源码端的一致性保证。首先，根据可双向转换的并发验证思路设计了验证系统的框架；其次，根据整体验证思路设计了一种中间层规范生成器，将提供的代码及需求说明文档转化为中间层规范；最后，设计了一种自动化双向转换器，将中间层规范自动映射为高层规范与功能性规范并分别进行验证。根据对融资程序的试验验证，证明了此双向转换并发性验证方法的有效性及可用性。未来主要是在面向更复杂的验证目标时能更好地提供效率保障，并且在实际的验证工作中提高自动化程度，减少人工参与度。
引用格式：谢小赋 , 曾梦岐 , 庞飞 . 面向计算机并发程序的形式化验证方法设计 [J]. 信息安全与通信保密 ,2022(3):54-62.