形式化验证技术在核电厂DCS中的应用研究

侯荣彬，马 权，兰 林，李 勇，杨 斐，薛 凯，吴亚波

（中国核动力研究设计院 核反应堆系统设计技术重点实验室，成都 610213）

0 引言

目前保证软件可靠性的方法主要有两类：①传统方法：测试和软件过程管理；②形式化方法：主要包括定理证明、模型检测、翻译确认等。传统测试方法，实施过程较为简单，但测试用例数量庞大，并且测试只能发现软件错误，不能证明其没有错误。采用形式化方法是提高软件可靠性的有效途径，随着形式化验证技术的成熟，人们逐渐意识到形式化方法的发展潜力。在一些安全攸关领域的软件开发标准中也逐步新增了与形式化方法相关的要求和建议，如安全评估标准[1]、DO-178C[2]、ISO26262-6[3]推荐在系统软件开发中运用形式化方法。在核领域IAEA 的核能系列《核电厂仪控系统安全级软件可靠性评估》[4]将形式化方法作为重要的评估证据来源。近年来随着形式化技术的普及和开发工具的进步，已经达到了实用化水平，因此在未来新的工业标准中极有可能引入形式化方法的要求。对此有必要在核电厂安全软件中引入形式化方法，一方面提高开发可靠性；另一方面满足未来需求。基于对形式化方法的理论研究和核安全级DCS 系统的实际需求，本文主要讨论形式化技术在核电厂仪控工程应用软件、代码生成器、操作系统的应用。

1 核电厂仪控工程应用软件的正确性验证

1.1 模型检测

模型检测：通过搜索待验证软件系统模型的有穷状态空间来检查系统的行为是否具备预定属性的一种自动验证技术。模型检测方法最初由E.M.Clark 等人于1981 年提出，他们设计了检验有穷状态并发系统是否满足给定分支时序逻辑公式的算法。模型检测方法大致可以分为以下3 个基本步骤：建模——将实际的系统转换为模型检测工具所能够接受的形式；规约——采用逻辑公式描述系统的属性；验证——基于状态空间搜索的方法对系统进行形式验证。该方法的优点为验证过程自动化，缺点为因其基础状态空间搜索，会引起状态空间爆炸。

比较著名的模型检测工具包括：针对C 语言的模型检测器CBMC[5]、基于时间自动机的UPPAAL[6]、用于验证线性时序逻辑的SPIN 和开源模型检测工具NuSMV。

1.2 程序验证

程序验证是使用逻辑推理的方法来证明程序满足其规范所描述的性质。可以通过对程序进行归纳证明避免状态搜索，进而避免状态空间爆炸。程序规范是某种逻辑表达式构成的断言，用于描述程序应满足的性质。根据程序的语义可以建立一套特定的推理规则用于程序验证。如果能得到程序的一个证明，则表示程序满足程序规范。形式化程序验证研究始于Hoare 等提出的霍尔逻辑理论。经典霍尔三元组：{P}C{Q}是一个数理逻辑断言。把状态断言对（P，Q）看作描述程序行为的规范，那么证明霍尔三元组为真的数理逻辑证明也就是对应程序满足其规范的证明。为了表述复杂数据类型和指针，在霍尔逻辑的基础上建立了离散逻辑，但其基本思想相同，只不过引入离散算术以适应高级语言特性。常见的程序验证工具包括Smallfoot[7]、Boogie[8]等。

核电厂仪控工程应用软件属于安全级软件，主要实现反应堆监测、控制、保护功能逻辑。其开发过程如图1 所示，包括：需求分析阶段、设计阶段、实现阶段、测试阶段。其中，需求分析阶段主要对软件的需求进行描述，包括非形式化描述和形式化描述；设计阶段将需求定义转化为功能块图的形式；实现阶段将功能块图转化为C 代码，再经过编译器编译为嵌入式设备中可运行的二进制文件；最后，在硬件设备上对程序进行测试，或对功能块图进行仿真测试。核电厂仪控工程应用软件控制逻辑相对简单，很适合使用形式化方法进行验证。如图1 所示，可考虑将模型检测方法应用于需求阶段的形式化需求模型和设计阶段的功能图块，在开发早期对模型进行验证，尽早发现问题。这一过程可以替代测试阶段对功能块图的测试，另一方面也可以考虑对实现阶段的C 代码进行程序验证，以替代C 代码的测试。

图1 模型检查和程序验证在核电厂仪控工程应用软件开发过程中的应用Fig.1 Application of model check and program verification in the development process of application software for nuclear power plant instrumentation and control engineering

图2 代码生成器和编译器关系示意图Fig.2 Schematic diagram of the relationship between code generator and compiler

2 可信编译器的开发

通常可信编译程序分为两种，一种是实现两种高级语言之间的转化程序，通常称为代码生成器。另一种是实现高级语言到机器语言的翻译称为编译器。二者关系如图2所示。

图3 可信编译技术在核电厂仪控工程应用软件开发过程中的应用Fig.3 Application of trusted compilation technology in the development process of nuclear power plant instrumentation and control engineering application software

采用形式化方法构造可信编译器或代码生成器的方法主要有以下3 种：①携带证明的编译器：不但能够编译器生成目标代码，另外还生成与之对应的证明，通过一个额外的验证器来检查证明目标代码是否满足给定的性质。提出携带证明代码的概念最先由Necula 等提出[9]，并为一个类型安全的C 语言子集实现了一个携带证明的编译器[10]。Colby 等人采用同样的方法实现对java 语言的字节码编译到目标代码的携带证明编译器[11]；②翻译确认：翻译确认的方法不是对编译本身进行验证，而是自动验证源代码和目标代码满足相同的规范，主要做法是用同一语义框架为翻译过程的源代码和目标代码建模，通过实现一个额外的验证器来自动验证源程序和目标程序满足相同的规范。翻译确认方法可用于完整编译器的构建，也可用于编译器的优化。Pnueli[12,13]等最早提出了翻译确认的概念并用于实现同步数据流语言Signal 到C 的编译器的翻译确认。Ngo和Talpin[14-19]等采用翻译确认方法，针对同步数据流语言Signal 到C 的编译器，为源代码和目标代码建立了一套统一的语义框架；定义了一种源和目标之间的抽象时钟等价关系；通过对等价关系进行验证来保证编译器时钟语义的一致性。翻译确认方法的优点在于不依赖于翻译的具体过程，相比对翻译过程进行验证的方法更轻便和灵活并具有较高的自动化水平，更适合用于编译器的局部优化；③定理证明：该方法是对翻译过程进行证明，也是最为直接彻底的方法。该方法需要严格定义源语言和目标语言的操作语义，并基于一种单向模拟原理定义源语言和目标语言的语义一致性。根据操作语义进行推理证明源语言和目标语言的语义一致性，这一过程可以通过定理辅助证明工具来实现。使用定理证明方法开发的编译器的成功案例为Compcert[20]和Velus[21]。国内王生原团队用此方法开发一个针对一种同步数据流语言到C 的代码生成工具[22,23]。

上节介绍了核电厂仪控系统应用软件的开发流程，在需求、设计和实现阶段分别对应着一种模型描述语言，需求阶段对应形式化需求定义语言、设计阶段对应功能图块语言、实现阶段对应C 语言和机器语言。在实际开发过程中，可以使用代码生成工具实现上述语言的自动转化。通常代码生成工具不仅需要完成语言的转换，还要求保证转换前后语义具有一致性，使用可信编译技术开发的代码生成工具恰好具备上述性质。如图2 所示，可考虑可信编译技术在需求定义语言到功能图块和功能图块到C 语言的转换过程的应用，至于C 到二进制文件的编译可使用著名的Compcert，这样一来就构成一套完整的可信编译工具链，另外代码生成技术还可应用于测试用例的自动生成。

图4 操作系统的微内核架构Fig.4 The microkernel architecture of the operating system

3 操作系统验证

操作系统的安全性对信息安全和嵌入式系统功能安全至关重要。操作系统作为基础软件，因其复杂性，往往存在系统漏洞，因此无法提供安全服务和安全保障。造成这些文题的主要原因包括两个方面：①操作系统的顶层设计和代码实现不一致；②操作系统功能定义与实际安全目标不一致。通过采用形式化的方法对操作系统进行设计和验证可有效提高设计和实现的一致性，保证操作系统的安全目标。

国内相关机构开展了有关操作系统形式化验证的研究工作。陈超超[24]等对L4 内核操作系统的内存管理机制进行了形式化验证。钱振江等[25-27]提出了操作系统对象语义模型（OSOSM），验证了操作系统的安全属性和微内核架构的中断机制的正确性。程亮[28]针对SELinux 的安全策略，使用模型检测方法验证策略实现与安全需求之间的一致性。张忠秋等[29]应用霍尔逻辑，以定理证明的方式完成机载嵌入式操作系统软件的形式化验证。

图5 操作系统的形式化设计和验证框架Fig.5 Formal design and verification framework of operating system

目前，核电厂仪控系统的操作系统一般是使用自主研发微内核的操作系统，任务顺序执行无中断，要求具有确定性，相较于传统的操作系统有所简化。操作系统的微内核架构如图4 所示，包括硬件层，运行在特权模式下的微内核与运行在用户模式下的应用程序、驱动程序、文件系统等。微内核的优点在于驱动程序和文件系统等从操作系统中剥离出来，运行在自己单独的内存区域中，因此驱动程序和文件系统的错误只会涉及到自身的区域，不会对整个系统造成大的危害。操作系统是一个很复杂的软件，因此难免出现需求与设计、设计与实现的不一致问题。图5给出了操作系统的形式化设计和验证的框架。主要包括三层：分别是需求概念层、形式化描述层、代码实现层。需求概念层包括操作系统的设计描述和功能需求，涉及操作系统的工作原理、安全属性、策略等。形式化描述层主要实现操作系统的形式化建模和规范的形式化定义（规范说明和系统安全属性），这一过程需要对操作系统形式化模型是否满足操作系统的规范说明和安全属性进行验证。最后，验证操作系统的代码实现与操作系统形式化模型是否一致。

4 开发工具-高阶逻辑和证明助手

高阶定理证明器也称为证明助手。使用证明助手进行证明的过程类似在纸面上进行证明的过程，证明者需要定义相关的引理，并可以借助于证明策略提高证明的效率，每个命题的证明通常采用从后向前推理证明方法。复杂的证明目标可通过分解成子目标，子目标再分解成更小的目标，直到公理级别和已知前提，最后完成证明。如果一个子目标不容易被直接证明，则可引入一条辅助引理，单独进行证明。证明策略用于对子目标进行组织、分解及证明。证明助手不仅提供基本的证明策略，还提供证明策略的构造方法即泛策略，用户可以通过构造新的证明策略加速证明过程，也可以通过定义复杂策略，可实现一类问题的自动化证明，这些复杂策略中可以融合一些自动证明算法。常用的机械化定理证明器如下：

1）德克萨斯大学奥斯汀分校：ACL2

2）INRIA：Coq

3）剑桥大学：HOL

4）剑桥大学：Isabelle

5）MIT：Larch 系统

6）康奈尔大学：Nuprl

7）斯坦福研究所：PVS

8）卡耐基-梅隆大学：TPS

5 结束语

本文首先通过调研相关标准和文献，论述形式化方法在软件可靠性中的意义和必要性。接下来主要考虑模型检测和程序验证方法在核电厂控制逻辑验证中的应用，主要是简述模型检测和程序验证方法的原理、应用实例及相关工具。代码生成器和编译器作为工具软件在安全关键领域至关重要，根据现有可信编译技术包括出具证明编译器、翻译确认方法、定理证明方法，考虑将可信编译技术应用到核电厂仪控工程组态程序的自动生成中，拟使用形式化方法开发代码生成器。操作系统作为仪控系统中的基础软件，目前仪控系统使用的是微内核的操作系统。调研发现目前有很多关于操作系统形式化验证的研究，可以将形式化技术应用到仪控系统的微内核的验证中，进一步增加仪控系统的安全性。最后，介绍应用于形式化验证的工具，简要介绍了其原理。总而言之，形式化方法在提高核电厂仪控系统软件可靠性方面有很多的应用场景，但是形式化方法涉及很多的技术分支，并且形式化方法的实施有技术上的难度，从技术理论到实际应用仍然需要进一步探索研究。