临沂罗庄建设局网站,网站建设要在哪学,传奇网页版游戏开服表,seo黑帽是什么摘要#xff1a;形式化验证是证明软件、硬件或系统正确性的一种方法#xff0c;近年来受到了越来越多的关注。 本文对形式化验证的研究进行了综述。首先介绍了形式化验证的基本概念#xff0c;然后重点介绍了形式化验证的三种技术#xff0c;包括模型检测、定理证明和等价性…摘要形式化验证是证明软件、硬件或系统正确性的一种方法近年来受到了越来越多的关注。 本文对形式化验证的研究进行了综述。首先介绍了形式化验证的基本概念然后重点介绍了形式化验证的三种技术包括模型检测、定理证明和等价性验证等。此外通过两篇论文介绍了形式化验证在软件和硬件系统开发中的应用和实现、形式化验证工具的发展和使用。最后对形式化验证的未来发展进行了展望认为人们应该不断探索新的理论和工具以提高形式化验证的效率和可用性。 关键词 形式化验证形式化方法软件开发研究综述 一、引言 现如今计算机硬件性能变得越来越高、运算速度变得越来越快、体系结构变得越来越复杂软件的功能也变得越来越强大而复杂如何开发可靠的软、硬件系统已经成为计算机科学发展的巨大挑战特别是现在计算机系统已广泛应用于许多关系国计民生的安全攸关系统中例如高速列车控制系统、航空航天控制系统、核反应堆控制系统、医疗设备系统等等这些系统中的任何错误都可能导致灾难性后果。 计算机系统的设计开发需要分析、处理、证明计算机硬件和软件系统的性质。 形式化方法以形式(逻辑)系统为基础支持对计算机系统进行严格的规约、建模和验证并且为此设计算法从而建立计算机辅助工具。在现代计算机系统的开发过程中形式化方法在不同的阶段、以不同的形式和程度得以应用例如在基于模型的软件开发中建模 、模型精化和基于模型的测试都是基于形式化方法的思想和技术发展起来的程序语言的类型设计、程序分析的算法都是形式化方法中的基本技术[1]。 形式化方法最显著的作用是能够对形式规约进行验证。形式验证常见的有两种形式一种是推理“系统模型规约是否满足其性质规约”此时模型规约偏向操作型性质往往是说明型的另一种是推理“系统的一个模型规约是否与另一模型规约有精化或等价关系”。这些推理过程给出了一套静态方法来预测系统的行为用户可以描述系统行为的所期望性质或者开发过程中不同抽象之间关系的猜想形式验证通过机械化的方式来证实或者证伪这个性质或者猜想从而提高用户对规约和系统的可信程度。 二、形式化验证方法 形式验证方法主要包括定理证明、模型检验和模型等价性验证下面笔者将从上述三种方法进行详细介绍。 2.1 定理证明 基于定理证明的形式验证将“系统满足其规约”这一论断作为逻辑命题通过一组推理规则以演绎推理的方式对该命题开展证明。基于定理证明的验证大部分是以程序逻辑为理论基础的但是程序逻辑并非唯一的验证方法例如我们可以基于程序的操作语义直接表达程序执行的安全性、正确性等各种性质并证明相关定理[2]。 按照证明方式和自动化程度的不同基于定理证明的验证又可以分为两类即基于自动定理证明器的自动验证和基于人机交互的半自动验证。 2.1.1 基于自动定理证明器的自动验证 随着自动证明理论的发展和计算机处理器能力的大幅增强自动定理证明器的能力得到大幅提升基于自动定理证明的验证也得到很大发展。目前常见的程序证明器包括 Dafny、Why3、VeriFast、Smallfoot 等。这些程序证明器大多基于某种具体的程序逻辑。给定程序及其规约证明器能够自动决定针对程序的每条语句使用程序逻辑中的何种公理或规则并产生相应的验证条件作为证明义务。最终产生的验证条件被送到自动定理证明器中由定理证明器完成对验证条件的证明。目前使用最广泛的定理证明器是微软开发的Z3其他常见的证明器还包括CVC4、Yices2 等。使用各种定理证明器和自动化程序验证技术人们已经实现了对一些相对实用的、较大规模的具体系统的验证。 基于自动定理证明的验证工作的优点在于验证的效率较高不需要人手工写证明。然而由于自动定理证明中很多问题是不可判定问题而且各个定理证明器又有各自的能力限制因此能够表达和证明的性质有限。为了 能够实现自动证明很多时候需要对待证明的性质和待验证的代码本身都进行重写甚至为了迁就验证的自动化而牺牲待验证的性质以及代码的功能。 2.1.2 基于人机交互的半自动验证 基于定理证明的另一类验证工作则不强调使用计算机实现验证的自动化而是利用计算机来解决证明在计算机中的表示问题以及自动检查证明的正确性的问题证明的构造则由人手工和机器交互以半自动化的方式完成。很多辅助定理证明工具如Coq[3]和Isabelle/HOL等都是针对这一目的进行开发的。这类工具往往是利用类型系统和逻辑之间的Curry-Howard 同构关系[4]将构造证明的过程转化为编写程序的过程而证明的正确性检查也变成了类型检查问题。 这类人机交互的半自动化验证工作往往需要大量的手工劳动来构造证明虽然在辅助定理证明工具中提供了一些基本的证明策略和引理库来减少证明负担但在实际代码的验证中往往平均一行程序需要手工书写20~30行证明脚本。然而这种方法的优点在于无需牺牲规约和代码的表达能力特别是程序规约可用表达能力很强的逻辑(如在Coq[3]和Isabelle/HOL中使用的高阶逻辑)来表示。而且证明自身在机器中有显式表示其正确性可以被自动检查因而我们无需依赖自动定理证明算法的正确性验证的结论也就更加可信。 2.2 模型检验 定理证明中形式验证把待证明的性质直接作为了一个数学定理来证明也称为演绎式验证。与演绎式相对应的一种方式是模型检验。模型检验的其基本思想是检验一个结构是否满足一个公式要比证明公式在所有结构下均被满足容易得多进而面向并发系统创立了在有穷状态模型上检验公式可满足性的验证新形式[5]。 图1[6]是模型检测验证方法示意图。首先根据设计搭建形式验证模型然后根据设计要求编写断言属性和相关的约束再将模型和约束合并成为符合验证需求的形式验证模型。接着加入需要验证的设计运用形式验证工具进行验证此时形式验证工具会根据约束自动遍历所有需要被验证的状态如果所有的断言都成立则设计正确反之设计错误工具发现错误时可以提供错误场景帮助验证人员分析错误。根据形式验证结果分析覆盖率状况并通过分析后的结果优化形式验证环境提高形式验证覆盖率。 图2[6]是模型检测查错示意图在模型检测时首先是根据设计需求定义输入可以搜索的状态范围在状态搜索过程中工具会首先建立一个初始状态并进行扩展进入下一个状态除非有明确的状态约束否则扩展将一直进行。在查找过程中可能会出现状态重复的情况但是不管过程如何工具都会遍历所有的状态空间然后工具会将所有状态的输出值和模型检测中的标准值进行对比检查在进行断言检查的过程中如果出现了输出值不符合断言属性的状况模型检测工具会反方向运行推导出出错时的输入状态这就是上文中提到的工具给出反例的原理。 设计建模和形式规约是模型检测方法搭建形式验证环境的重要环节。在模型检测中为了验证设计首先需要理解设计规范和验证需求在此基础上编写设计等价参考模型。通常情况下参考模型会比设计更加抽象模型仅仅是为了描述预期的结果。在验证的过程中可以把设计模块分解成小的、方便验证的模块但同时也要保证分解后的任意模快之间状态逻辑和状态空间的吻合[7]。因此在验证时为了防止产生状态爆炸在保证验证合理性的前提下可以对状态空间进行划分使得验证更加简单快速。模型检测时形式验证工具将根据形式规约来判断相关属性的正确性。形式规约是用具有精确语义的形式化语言描述设计性质形式规约的状态将影响模型检测的一致性和完备性。一致性指的是与验证目标无矛盾完备性指的是是否完全无遗漏地描述出了目标属性。 2.3 等价性检验 等价性验证是目前形式验证方法中运用最为普遍的验证技术。等价性验证不仅拥有形式验证全遍历和验证速度快的特点而且等价性验证的自动化程度也很高验证工具操作简单。虽然等价性验证的优点很多但是这种验证方法不能用来验证设计的功能正确性因为等价性验证方法的原理是通过对比不同阶段设计之间的等价性从而达到验证的目的。在形式验证中由于数学逻辑分析的方法是抽象的所以验证不会受到不同描述语言的限制可以验证不同描述方式之间设计的等价性[8]。即等价性验证只能检测芯片不同设计阶段之间有没有产生错误而不能检测出不同阶段设计的共同错误。等价性验证在芯片设计流程中通常用于RTL和RTL、门级与RTL、门级和门级以及版图和门级之间的错误分析[9]。 三、相关论文研究 本章将简单介绍笔者阅读过的两篇关于形式化验证的论文在介绍的过程中着重阐述文献中具体的案例分析。 3.1 Ptolemy离散事件模型形式化验证方法[10] 3.1.1 基本思想 Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包主要通过仿真的方式保证所建模型的正确性。文中提出了一种基于形式模型转换的方法来验证离散事件模型的正确性。离散事件模型根据不同事件的时间戳触发组件时间自动机模型能够表达这个特征因此选用Uppaal作为验证工具。首先定义了离散事件模型的形式语义其次设计了一组从离散事件模型到时间自动机的映射规则然后在Ptolemy环境中实现了一个插件可以自动将离散事件模型转换为时间自动机模型并通过调用Uppaal验证内核完成验证。与现有研究工作相比,该方法定义了更为完整的Ptolemy组件转换规则可以支持更多的组件保留了模型层次化的特点有效避免了状态空间爆炸避免使用tick计时降低验证的复杂度在Ptolemy环境中设计实现了一个自动转换验证的插件,完善了使用Ptolemy进行模型驱动开发的工具链。 其中Ptolemy DE模型验证整体框架如图3[10]所示可分为转换模型和形式化验证两部分 1在模型的自动转换阶段将Ptolemy DE模型和根据模型提取的属性验证公式作为输入首先对Ptolemy DE模型进行解析,获得各个组件的结构信息然后根据定义的映射规则将各个组件转换为对应的时间自动机最终将时间自动机与属性验证公式共同构成一个可进行验证的时间自动机网络结构。 2将内存中的时间自动机网络结构输出文件即可调用Uppaal验证引擎进行验证。 3.1.2 交通信号灯案例分析 在一个交通信号灯系统中指示车辆行动的信号灯有红、黄、绿这3种指示行人行动的指示灯有红、绿这两种。当系统正常工作时汽车指示灯按照红、黄、绿、黄的顺序变换分别停留3121个时间单元行人指示灯根据汽车指示灯的变换而变换当汽车指示灯由红变黄时行人指示灯变红当汽车指示灯由黄变红时行人指示灯变绿。有时系统会出现故障此时只有指示汽车暂停行驶的黄灯闪烁其他指示灯都灭。 如图4[10]所示Ptolemy DE模型中定义了5个参数PredPgrnCredCyel和Cgrn分别表示不同的交通灯当值为1时表示其对应的交通灯亮值为0时表示其对应的交通灯灭。如图中参数Pred和Cyel值为1则行人红灯和车辆黄灯亮。DiscreteClock是一个事件源组件以1为周期产生输出信号Decision是一个异常生成器TrafficLight是交通灯控制器SetVariable组件用于更新参数值。其中组件TrafficLight交通灯控制器是一个模态模型有两个状态normal和error状态normal和error各有一个细化模型。TrafficLight normal是TrafficLight中normal状态的一个细化模型表示系统在正常情况下交通灯控制器的详细模型包含两个控制器车辆交通灯控制器CarLightNormal和行人交通灯控制器PedestrianLightNormal。 通过提取Ptolemy DE模型中的属性特征形式化描述为CTL公式进而使用Uppaal验证的引擎对模型的可靠性、安全性、死锁进行形式化验证。表1[10]是上述验证公式详细的验证情况当时间自动机模型中有不满足的属性时Uppaal验证引擎可以返回异常路径。 3.2 面向MSVL的智能合约形式化验证[11] 3.2.1 基本思想 智能合约是运行在区块链上的计算机协议被广泛应用在各个领域中但是其安全问题层出不穷因此在智能合约部署到区块链上之前需要对其进行安全审计。然而传统的测试方法无法保证智能合约所需的高可靠性和正确性。文章提出一种基于时序逻辑语言(MSVL)的智能合约安全性的模型检测方法首先使用MSVL对智能合约程序进行建模为了减少建模时大量的人工操作开发了将智能合约语言Solidity转换为MSVL的转换器工具SOL2M实现了智能合约建模程序的自动化生成然后使用命题投影时序逻辑(PPTL)公式描述该智能合约的安全性性质最后在统一模型检测器(简称UMC4M)中自动化验证建模程序是否满足给定的安全性性质并通过实例说明该方法运用到智能合约验证中的可行性和实用性。 其中转换器工具SOL2M的具体结构以及工作流程如图5[11]所示。SOL2M转换器主要分为4个部分 (1)预处理处理Solidity源程序中的版本标识语句和导入其他源文件语句 (2)词法分析通过JavaCC工具生成词法分析器对Solidity程序进行词法分析将源程序识别为特定的单词流 (3)语法分析通过JavaCC工具生成语法分析器对Solidity程序进行语法分析把词法分析生成的单词流识别为程序语句 (4)程序转换通过分析Solidity和MSVL的词法以及语法的异同制定出Solidity到MSVL的转换规则并将转换代码嵌套在语法分析的BNF范式中实现Solidity程序到MSVL程序的动态转换。 3.2.2 银行转账合约案例分析 以具体的银行转账智能合约与常见的重入攻击漏洞为例给出SOL2M对转账合约与重入攻击进行建模的详细流程以及验证过程。建模时在银行转账合约中抽象加入了重入攻击操作即将转账合约与重入攻击代码抽象为合约。如图6[11]所示其中deposit函数的功能是用户把钱存入银行withDraw函数实现了转账功能用户通过withDraw函数与send函数从银行取钱。Attack函数实现了重入攻击的功能其具体步骤为首先攻击者调用Attack函数通过deposit函数向银行转账合约中存入一些以太币之后调用withDraw函数从银行转账合约中取钱使用require语句判断用户余额以及银行总余额是否足够最后调用send函数给用户地址转账。 对合约进行建模将银行转账合约与重入攻击合并为一个合约并作为SOL2M转换器的输入转换结果如图7[11]所示。从功能一致性、逻辑正确性以及合约完备性3个层面使用PPTL公式描述银行转账合约应满足的性质此处便不再详细阐述。 四、总结 形式化验证是一种通过数学方法来证明软件、硬件或系统的正确性的技术。它采用形式化语言、逻辑和证明技术通过对系统建模、规约和验证从而达到证明系统行为是否满足给定规定的目的的目的。 形式化验证的优势在于它可以对系统进行全面、自动、形式化的测试和验证从而发现和纠正系统设计的缺陷。它的结果可以得到精确、确定的结论可以帮助开发人员减少迭代设计和测试的时间和成本。因此形式化验证在现代软件和硬件系统的开发过程中已经得到广泛应用。 尽管形式化验证具有强大的验证功能但是它在实际应用中也存在一些挑战。形式化验证需要专业的证明人员和高水平的数学和计算机科学知识因此成本较高。此外由于复杂性问题形式化验证的规模通常在实际系统的规模上有所限制。 综上所述形式化验证是一种非常有价值的技术它对提高软件和硬件系统质量的保障作用不可忽视。但是为了使其更广泛应用于实际开发过程中还需要不断提高形式化验证的效率和可用性。 参考文献