基于分离逻辑的程序验证技术

介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入应用所面临的问题和解决方向.     

一个程序验证器的设计和实现

形式验证是提高软件可信程度的重要方法,基于逻辑推理对程序性质进行严格的自动证明是当前的研究热点,但尚无可供工业界使用的产品,其根源在于自动定理证明方面的困难.介绍在通过程序分析建立起各程序点的形状图的基础上,如何利用形状图提供的信息来支持程序验证的方法.提出一种利用形状图信息来消除访问路径别名,使得指针程序中非指针部分的性质仍然可以用Hoare逻辑来进行验证的方法,并证明了该方法的可靠性.还提出一种在不使用自定义谓词的情况下,易变数据结构上数据性质的描述和验证方法.另外,介绍所设计并实现的基于上述方法的PointerC语言的程序验证器的原型.它不仅能自动验证操作易变数据结构程序的性质,也能自动验证使用一维数组的程序的性质.     

时态逻辑与程序验证

近年来,时态逻辑大量应用于程序验证,采取的途径随使用的时态逻辑的形式和方法的不同而异。本文用自动机理论研究几种时态逻辑(LTL,BTL,POTL)的模型和模型生成子,并讨论用时态逻辑进行程序验证的的重要途径。     

断言语言支持自定义谓词的程序验证器原型

基于逻辑推理的方法进行程序验证是形式化程序验证的研究热点.目前的自动验证工具为了保证自动性,对描述程序性质的断言语言都有较多限制,导致程序的某些递归性质难以用断言语言表述.本文在一个面向指针程序、基于先前自行设计的形状图逻辑、依赖于自动定理证明工具Z3的自动程序验证原型系统上,通过在断言语言中引入自定义谓词来增强断言语言的表达能力,使得该原型系统不仅能自动验证含操作易变数据结构的程序的性质,也能自动验证一些不含指针的程序的性质.     

基于插桩和布尔逻辑的运行时程序验证框架

针对软件测试和静态程序验证中存在的连续性程序执行验证和推理问题,提出一个基于程序插桩和布尔逻辑的运行时程序验证框架——RPA。定义一种用于描述运行时程序性质和规范的动态逻辑语言RPAL,实现自动化插桩以收集运行时程序状态信息,设计一个支持高效验证的句子调度算法。实验结果表明,结合合适的谓词扩展,RPA可以有效地验证和分析软件逻辑,发现潜在的软件错误。     

基于交互式定理证明的并发程序验证工作综述

并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用。但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果。同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难。在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证。本文对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性。交互式定理证明方法中常用程序逻辑对程序进行验证,本文分析了基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用了这些方法的程序验证工具和程序验证成果进行了总结。     

基于Coq的微内核操作系统程序验证方法研究

机载嵌入式程序的可信属性验证是新一代飞机研制最关注的软件质量保障问题;基于定理证明的程序形式化验证方法是一种可靠和严格的软件正确性验证技术;文中在深入分析微内核操作系统的基础上,应用霍尔逻辑针对机载嵌入式软件核心代码开展程序验证技术研究,根据霍尔逻辑的相关推理规则进行程序验证,并在定理证明辅助工具Coq中形式化表示霍尔逻辑的推理规则,针对机载操作系统的部分程序代码实例进行验证;实验结果表明基于定理证明的程序验证方法可以对软件程序代码的正确性进行验证,从而帮助软件提供商开发高可信的机载嵌入式软件。     

面向程序验证的并行程序状态空间态约简技术综述

程序验证是保证程序安全性的重要手段.随着采用多核技术的硬件环境日渐普及,越来越多的软件正通过转向基于共享内存的并行程序模型来充分利用现有的计算资源.各线程在并行执行时通过共享内存的访问互相干扰执行状态,导致可能执行路径数成几何级数增长,进而产生可达状态空间爆炸问题.由于验证并行程序安全性主要通过分析程序可达状态来实现,因此,对并行程序可达状态空间的约简是决定并行程序验证效率的关键因素.首先对面向并行程序验证的并行程序可达状态空间约简方法进行了分类,然后对各类可达状态空间约简方法分别进行了分析和总结,最后指出了当前存在的问题和未来解决这些问题的研究方向.     

基于逻辑的访问控制研究

描述了访问控制和逻辑的关系,并将访问控制授权判决问题归约成逻辑蕴涵问题;总结了基于逻辑的访问控制的基本逻辑问题,即逻辑基础、可判定性和安全性分析;分析了一些访问控制模型的基本逻辑问题,包括基于身份的访问控制模型、基于信任管理的访问控制模型和基于属性的访问控制模型;指出了结构化属性描述能力和安全性分析是基于逻辑的访问控制需要进一步研究的问题.     

基于逻辑分离的无人机仿真系统设计

针对在无人机仿真系统开发过程中的结构复杂问题,以及时间、经济成本等问题,提出一种ROS环境下基于逻辑分离思想的体系结构,并设计了一款基于PX4开源固件的交互式工具包应用到仿真系统.首先,根据逻辑分离思想进行系统整体设计;其次,在单机和多机的条件下进行仿真并验证;最后对仿真进行分析,结果表明该系统可实现表示层、业务层、控制层逻辑分离的无人机仿真测试,体现出系统设计的正确性与可用性.由于逻辑分离思想的应用,使得系统各部分职能明确,具有更高的开放性和可控性.     

基于隔离逻辑的并行程序可靠性验证方法

并行程序验证的复杂性在于执行流程的不确定性以及由此导致的执行规模变大,使得验证的内容和目标之间的关系不明确。为解决该问题,提出一种基于隔离逻辑的并行程序可靠性验证方法。通过变量的执行关系图,描述变量相关的语句及执行关系,将所需验证的程序性质逻辑式转换为变量并行语句序列的逻辑组合式,使得性质表达式与并发程序的语句相关联。根据逻辑组合式确定语句执行序列和前后件逻辑表达式,基于并发隔离逻辑的公理系统对语句执行序列进行验证,并根据验证结果对并发程序进行修改和完善。通过对银行柜台业务办理的功能模块验证结果表明该方法是有效的。     

Verification of an Incremental Garbage Collector in Hoare-Style Logic

Many of the current software systems rely on garbage collectors for automatic memory management. This is also the case for various software systems in real-time appli-cations. However, a real-time application often requires an incremental working style of the underlying garbage collection, which renders the garbage collector more complex and less trustworthy. We present a formal veriˉcation of the Yuasa incremental garbage collector in Hoare-style logic. The speciˉcation and proof of the collector are built on a concrete machine model and cover detailed behaviors of the collector which may lead to safety prob- lems but are often ignored in high-level veriˉcations. The work is fully implemented with the Coq proof assistant and can be packed as foundational proof-carrying-code packages.Our work makes an important step toward providing high-assurance garbage collection for mission-critical real-time systems.     

基于逻辑程序的安全协议验证

安全协议本质上是分布式并发程序,可以自然地描述为多个子进程的并发合成系统．将安全协议对应的并发合成系统抽象为逻辑程序进行消解,能够对安全协议无穷多个会话的交叠运行进行验证．该文提出了安全协议逻辑程序中逻辑规则的一个分类方法,基于该分类方法提出了安全协议逻辑程序不动点的迭代计算方法．逻辑规则的分类优化了安全协议逻辑程序不动点的迭代计算和安全性质验证过程中的计算．由于安全协议逻辑程序不动点迭代计算过程不一定终止,文中提出了每进行k≥1步安全协议逻辑程序不动点迭代计算验证一次安全性质的验证策略．     

基于分离逻辑的并行程序性质验证方法

随着多核多线程并行执行方式的普及,并行程序形式化验证的需求日显突出.并行程序验证中执行流程的不确定性使验证的内容与目标的关系难以确定,且从并行程序直接进行性质验证会导致验证规模大.为此,提出一种基于分离逻辑的新的验证方法.该方法根据分离逻辑的程序语义描述兼有解释语义和公理语义的特点,从验证的性质出发,把要验证的性质式转换成并行语句序列的逻辑组合式,并进行整理和化简;然后,利用分离逻辑公理系统对语句序列进行验证,用验证了的断言集来求出性质的真值.实例进一步说明,此方法更有效,同时也简化了验证的规模.     

多agent逻辑程序及其在协议验证中的应用

提出一种多agent逻辑程序,每个agent具有一个相信算子,讨论了其不动点语义和操作语义,证明了两种语义之间的等价性.提出了一种基于多agent逻辑程序的协议验证方法,以一种多方非否认安全协议为例,对该协议进行了形式化描述,验证了其具有不可否认性.     

A Program Logic for Bytecode

Program logics for bytecode languages such as Java bytecode or the .NET CIL can be used to apply Proof-Carrying Code concepts to bytecode programs and to verify correctness properties of bytecode programs. This paper presents a Hoare-style logic for a sequential bytecode kernel language similar to Java bytecode and CIL. The logic handles object-oriented features such as inheritance, dynamic method binding, and object structures with destructive updates, as well as unstructured control flow with jumps. It is sound and complete.