一种基于Isabelle/HOL的安全通信协议验证方法

传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢。为解决上述问题,结合对称和非对称密钥加密方式,构建D_protocol混合密钥加密协议。使用Isabelle/HOL定理证明辅助工具对D_protocol协议建立通信代理和消息序列的形式化模型,采用形式化操作语义描述用户行为,通过归纳分析方式对通信协议消息交互过程涉及的相关定理展开验证,结果表明D_protocol协议在提高通信效率的同时具有较高的安全性,并且可在一定程度上抵抗外部攻击和中间人攻击。

文件比较算法fcomp在Isabelle/HOL中的验证

基于机器定理证明的形式验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.文件比较算法(file comparison algorithm)是一类成员众多,应用极为广泛,跨越生物信息学、情报检索、网络安全等多个应用领域的基础算法.在交互式定理证明器Isabelle/HOL中对Miller和Myers在1985年提出的基于行的文件比较算法fcomp做了形式化,改正了算法关于边界变量迭代的一个小错误,证明了改正后算法的可终止性和正确性;对算法时间复杂性做了完全形式化的分析,印证了算法的非形式化分析结论,为今后更多文件比较算法的形式验证提供了可供借鉴的经验.

VSOS-HAM:基于Isabelle/HOL的OS内核硬件抽象模型和形式化验证方法研究

形式化方法是保证操作系统设计和实现的正确性的可靠方法.操作系统的形式化设计和验证过程仍然是一个极其复杂的过程.由于汇编语言过于底层,对其进行形式化验证的难度较大,如何有效地对汇编语言代码进行建模,便于对其语义和功效的正确性进行验证成为操作系统形式化领域的研究热点.在汇编级提出对操作系统的设计和实现的正确性进行形式化验证的方法.通过建立操作系统内核硬件抽象模型,形式化地描述指令的操作语义,在此内核硬件抽象模型的基础上界定影响系统状态变化的数据对象,建立系统状态空间,结合指令的操作语义的定义来描述系统的状态转换函数.在Isabelle/HOL定理证明器环境中描述该内核硬件抽象模型,以实现的可信操作系统VSOS为例,在汇编级对系统设计和实现的正确性进行验证.结果表明,该方法是可行的和高效的.

命题演算形式系统在Isabelle/HOL中的形式化

本文针对命题演算形式系统,在机器辅助定理证明系统Isabelle/HOL中为其建立逻辑模型,并分别形式化验证了PC和ND的主要性质,以及完备性定理的证明。通过对PC和ND的分析和验证表明,采用机器辅助定理证明系统,对以数理逻辑为平台的各种形式系统进行严格的分析和证明是可行的。

堆栈机器简单编译器在Isabelle/HOL中的验证

堆栈机器(stack machine)作为一种计算模型,不仅执行部分高级语言的效率很高,而且其编译器也简单、快速.在形式化领域,目前已有不少定理证明器用来验证模型的正确性.本文对堆栈机器的简单编译器进行介绍,对布尔表达式和算术表达式、机器指令、编译器、机器运行行为在Isabelle/HOL中进行形式化,验证编译器的正确性.

格林定理的形式化及其初步应用

格林定理广泛应用于物理学、流体力学和化学等领域。通常使用传统的计算机仿真和数值计算方法构建基于格林定理的系统模型。然而,由于工具软件可能存在的系统缺陷导致模型出现偏差,从而使任务失败。为解决上述问题,采用基于高阶逻辑的形式化方法,在定理证明器HOL Light中实现了格林定理相关内容的高阶逻辑建模与验证。首先,对梯度、散度等基本概念和性质进行了形式化描述;其次,对格林定理及其性质进行了形式化建模与验证;最后,基于格林定理的形式化模型完成了地下水控制模型的高阶逻辑推导,进而确保系统模型的安全性。

算法的形式化推导与基于Isabelle的自动化验证

可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化验证,避免了手工验证过程繁琐和易出错等问题.研究表明:基于递推关系的算法形式化方法不仅可以提高开发算法的效率,而且通过数学变换保证推导过程的正确性,从而有效保证了算法和程序的正确性.

LLRB算法的函数式建模及其机械化验证

基于机器定理证明的形式化验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.LLRB(left-leaning red-black trees)是一种二叉搜索树变体,其结构比传统的红黑树添加了额外的左倾约束条件,在验证时无法使用常规的证明策略,需要更多的人工干预和努力,其正确性验证是一个公认的难题.为此,基于二叉搜索树类算法Isabelle验证框架,对其附加性质部分进行细化,并给出具体化的验证方案.在Isabelle中对LLRB插入和删除操作进行函数式建模,对其不变量进行模块化处理,并验证函数的正确性.这是首次在Isabelle中对函数式LLRB插入和删除算法进行机械化验证,相较于目前LLRB算法的Dafny验证,定理数由158减少至84,且无需构造中间断言,减轻了验证的负担;同时,为复杂树结构算法的函数式建模及验证提供了一定的参考价值.

基于HOL4的形式化方法

针对计算机系统设计的正确性问题,研究了一种在测试空间上完备的形式化方法,探讨了硬件系统在定理证明器HOL4中进行形式化验证的一般方法,其中包括如何采用高阶逻辑形式化描述系统的实现与规范,以及在HOL4中证明目标的一般过程.同时,以乘法器为实例,提出一种功能分解法对需要分析的电路进行形式化建模,并对模型的性质在HOL4中进行推理与验证,从而证明了乘法器电路设计的模型满足所提取的性质.

Gauge积分在HOL4中的形式化

积分是许多数学理论的基础,如实数分析、信号与系统中微分方程的求解等等。Gauge积分是黎曼积分在闭区间上的推广,应用更加方便。将Gauge积分的运算性质在HOL4(Higher-Order Logic 4)中形式化,包括积分的线性运算性质、积分不等式、分部积分、积分分裂定理、子区间的可积性、对特殊函数的积分的形式化及积分极限定理、柯西可积准则,并根据相关性质对反相积分器进行了验证。

SpaceWire译码电路在HOL4中的形式化验证

SpaceWire是在苛刻环境下的高速通信总线协议,译码电路是其接收端的关键电路,对该电路进行形式化验证具有重要的现实意义.形式化验证方法中的定理证明将需要分析的电路进行形式化建模,结合定理证明器,对模型的性质进行严格推理从而完成验证.本文运用定理证明的方法,在高阶逻辑证明工具HOL4中对SpaceWire总线的译码电路进行形式化验证.首先根据SpaceWire标准规范抽取相关性质,用高阶逻辑语言形式化描述;然后分析电路设计中的VHDL代码,依据代码实现的功能用相应的逻辑谓词建模;最后在HOL4中证明了译码电路设计的模型能满足所提取的性质.本文同时给出了形式化建模的方法和验证过程.

拉普拉斯变换微积分性质在HOL4中的形式化

拉普拉斯变换是系统时域频域分析转换的基本工具,基于拉普拉斯变换的数值计算广泛用于信号传输的评估和重要安全系统的分析等,但是其存在计算不精确等问题.高阶逻辑定理证明是验证系统的一种严密的形式化方法.本文在高阶逻辑证明工具HOL4中使用积分、微分、超越函数、复数等定理建立了拉普拉斯变换形式化模型,并且对拉普拉斯变换的线性性质、微分性质、积分性质、频移性质进行了逻辑推理证明.最后通过对电机传递函数的形式化验证说明拉普拉斯变换形式化的有效性和正确性.

实数二项式系数在HOL4中的形式化

定理证明是一种形式化方法,在高可靠性系统验证中起着越来越重要的作用。分数阶微积分是高可靠性系统分析的基础,实数二项式系数是分数阶微积分定义的重要组成部分。在高阶逻辑定理库中还没有实数二项式系数的形式化。提出实数二项式系数高阶逻辑形式化方法。首先研究阶乘幂在HOL4中的形式化,然后利用阶乘幂的高阶逻辑形式分析实数二项式系数,最后将实数二项式系数应用于分数阶微积分的形式化。分数阶微积分的形式化分析表明了实数二项式系数及其运算性质形式化的正确性和有效性。

基于Isabelle的证明信息系统设计

Isabelle定理证明器中的证明步骤和证明状态是非常具有参考价值的证明信息。然而目前没有工具可以有效管理这些信息。本文给出一个基于Isabelle的信息系统设计方案。利用该系统的实现,用户可以提取、保存和搜索这两种证明信息。

操作系统对象语义模型(OSOSM)及形式化验证

操作系统的复杂性使得其安全性问题日益突出.有不少的研究工作采用形式化的方式对现有的操作系统进行了正确性的验证,这些工作主要是采用程序形式逻辑验证代码级的功能实现性.从系统设计的角度,以高阶逻辑和类型论为基础,提出了操作系统对象语义模型(OSOSM).OSOSM采用分层结构,包括基本功效层、实现层和优化层.OSOSM将操作系统中的行为主体和资源抽象为操作系统对象,建立操作系统的论域,利用以操作系统对象变元集合为定义域到论域的映射表示操作系统的状态,描述操作系统系统调用等行为的语义,使用逻辑系统的谓词公式表达操作系统的安全属性,给出如何验证操作系统在运行过程中保持安全策略和属性的形式化描述方法.以实现并经过形式化验证的可信操作系统(VTOS)为例,阐述OSOSM的语义正确性.使用Isabelle定理证明工具验证设计和安全需求的一致性,以说明VTOS具有预期的安全属性.

程序求精新策略及自动验证方法研究

传统的程序求精策略无法求精至可执行程序,且存在验证的可信度低和自动化程度不高的问题。针对上述问题,提出一种较完整的程序求精策略并给出自动验证方法。使用递归定义函数技术刻画问题规约,基于Morgan精化规则程序求精至IMP程序,并使用验证条件生成器(verification condition generator,VCG)自动生成验证条件,通过Isabelle定理证明器验证IMP程序的正确性,最后利用开发平台自动生成C++可执行程序。以最长标志基因序列问题为实例进行程序求精和自动验证,检验了所提策略的有效性。该策略提高了算法程序开发的正确性,减轻了传统验证烦琐的工作量。

Xen混合多策略模型的设计与形式化验证

Xen作为一种虚拟化工具因开源、高效等特点而受到越来越多的关注。作为Xen安全的基础,XSM决定了其安全性。原生XSM没有对系统资源进行安全分级,并且以虚拟机为管理对象使得Dom0作为一个唯一管理域不符合最小特权,文中设计了一种混合多策略模型SV_HMPMD。在该模型中,针对BLP引入多级安全标签,从而增加BLP的实用性,并通过DTE和RBAC对特权进行更细致的划分,从而对Dom0特权进行合理限制。提出了一种分层模型,利用该模型对混合模型进行形式化的描述。运用系统不变量构造访问规则的安全属性需求,通过Isabelle/HOL对模型设计与安全需求的一致性进行验证。

基于形式化方法的有限域乘法器的建模与验证

针对有限域乘法器设计正确性的问题进行研究,阐述了有限域乘法器在高阶逻辑定理证明器HOL4中进行形式化建模和验证的过程。通过分析电路的结构特性和时序特性,提出了结合层次化和基于周期的形式化建模方法,构建4位多项式基有限域乘法器的形式化模型;最后在HOL4系统中完成对其相关性质的验证。实验结果证明了该有限域乘法器设计的正确性,同时表明所提出的建模方法对时序逻辑电路的验证是有效的。

一种水下群机器人路径规划算法的形式化研究

为了增强基于遗传算法的水下群机器人路径规划算法正确性的说服力,使用定理证明对其进行形式化研究,给出算法在定理证明器HOL4中的形式化模型。基于算法形式化的一般步骤,对算法的设计进行了详细的分析,指出算法设计的核心步骤和建模难点。在此基础上建立了总体形式化建模框架,然后对其进行化简,得到种群初始化、选择、交叉三个核心模块。给出了模型中要用到的基本数据类型的形式化描述,并分别对三个模块进行形式化描述,最终得到算法的形式化模型。通过证明与模型相关的97条性质,说明了模型的合理性及有效性,在此模型的基础上,可以完成对算法的形式化验证,同时还能拓展HOL4的应用范围。

并发系统概率空间的形式化构造方法

本文用Paulson归纳法描述并发系统,对系统执行的不确定性进行建模,给出了一种适合定义测度的产生集合,利用测度评估函数将产生集合的测度与有限执行序列的测度联系起来;证明执行序列集合上的测度满足非负性和可列可加性,利用测度扩张定理构造并发系统执行序列集合上的概率空间。所有证明脚本经过定理证明工具Isabelle/HOL/Isar的检查。