基于串空间的Kao Chow加密协议形式化验证

Kao Chow加密协议是由Kao和Chow提出的,他们利用BAN逻辑证明了该协议的认证性,但没有证明该协议的保密性,而且没有说明协议参与实体间得到的新会话密钥是否一致.事实上,由于BAN逻辑自身的缺陷,它无法用于证明加密协议的保密性.基于此,给出了Kao Chow加密协议的串空间模型,这个模型不仅验证了该协议的认证性,还验证了它的保密性及新会话密钥的一致性.     

操作系统形式化验证综述

介绍操作系统验证理论、语言和工具等技术基础,阐述验证路径、精化关系验证和大规模验证等新的验证方法和理念.比较分析多个操作系统验证项目研究内容、验证方法、主要贡献以及最新进展.分析操作系统验证过程中存在的问题,认为验证成本高、验证工具局限性是制约操作系统形式化验证的关键因素,随着验证工具、框架和定理库的完善,以及深度学习...     

基于原型验证系统的自稳定算法形式化验证

介绍了分布式系统的自稳定性以及原型验证系统(PVS),阐述了从形式化角度验证系统性质的方法.使用PVS对分布式系统及系统中的自稳定算法进行形式化描述和建模,并成功地证明了系统的自稳定性.同时,通过机械化的验证和分析结果,可以得出形式化证明的优势.     

实时系统形式化描述和自动验证

实时系统是一种带有时间约束的计算机系统,这些系统许多动作的完成是与时间相关的,即要满足一定的时间限制,它需要在特定的时间范围内的对某些输入及时做出反应。例如,碰撞中汽车的安全气囊须在300毫秒膨胀开。它的许多嵌入式应用,都有一个共同的特点就是对实时性、安全性要求很高,都需要实时的形式化规范技术。     

基于LSC的形式化验证方法

调查研究了LSC在形式化验证方法中的作用的研究发展现状,包括LSC在从系统行为需求描述转换形成模型检验的系统行为模型中的作用的研究现状,LSC在抽取待验证系统性质的作用的研究现状,LSC在模型检验中的作用的研究现状,展望了LSC在未来模型检验中的发展方向——概率模型检验.     

基于攻击者的“角色冒充”的协议验证方法

网络的普及使得网络安全问题日益重要 ,协议的安全性和密码算法的安全性是网络数据安全的两个最基本的概念。介绍了几种具有代表性的安全协议的形式化验证工具 ,并提供了用 JAVA语言实现的基于攻击者和秘密的安全协议验证算法。提出了身份验证协议必须交换秘密的概念 ,还为协议的形式化验证过程设计了框架。实现的验证工具是证伪的     

模型驱动的Dafny程序形式化生成与自动验证

Dafny是一种内置规范结构的编程语言和静态程序证明器,它能验证程序的功能正确性以及将证明过程自动化,这既提高了软件开发的效率,又极大增强了软件开发的可靠性.该文探索了一种模型驱动的Dafny程序形式化生成的方法.首先,从问题的Radl规约出发,根据规约变换技术得到其Radl算法;然后,根据PAR方法中循环不变式开发新策略得到问题的循环不变式;最后,在Radl算法和循环不变式基础上利用模型等价转换规则生成Dafny程序,并由Dafny证明器自动验证其功能正确性.用该方法解决了2个典型问题的算法程序开发与验证,证实了该方法能够有效地提高Dafny程序的生成效率和可靠性.     

硬件设计的形式化验证技术

形式化验证用数学可证明的方式来验证系统.硬件设计的形式化验证通常有三种方法：定理证明、等价性检验和模型检验.文章着重分析了这三种方法的优缺点，探讨了形式化验证技术所面临的挑战，以及目前形式化验证技术可能的一些研究方向.     

基于逻辑的形式化验证方法: 进展及应用

近年来, 形式化方法发展很快, 一些技术已经产生工业应用。以逻辑系统为主线, 分析几个影响力比较大的形式化验证技术和验证工具, 以帮助应用工程师选择并使用形式化工具。主要包括命题演算和时态逻辑方面的SAT、BDD、模型检测和SMT, 谓词逻辑方面的ACL2、VDM方法和B方法, 以及高阶逻辑方面的HOL、PVS 和COQ。还介绍形式化方法在学术界和工业界的应用情况, 最后给出几个商业化的形式化验证工具。     

概率模型检验的CBTC系统通信协议的形式化验证

通信协议是CBTC系统重要的组成部分,它的正确性、稳定性和安全性对整个CBTC系统有重要影响.鉴于通信协议中某些参数具有随机特征,本文采用概率模型检验对其进行形式化验证.分析了概率模型检验的语义及语法,建立了通信协议的概率模型,用概率模型检验工具PRISM验证了典型的概率规范.结果证明,当信道正常概率为99%,系统无延时概率为99%时,通信协议失效率小于1.5×1010.说明了用概率模型检验验证具有随机特征参数的通信协议,方法简单快捷,结论清晰明了.     

用于密码协议安全性证明的串空间模型

形式化分析是密码协议安全性证明的一个有效途径。串空间模型是在Dolev-Yao代数模型的基础上,结合Woo-Lam模型、CSP、Schneider秩函数和Paulson归纳法等方法的优点所提出的一种新的密码协议形式化模型,它可为密码协议安全性的证明提供新的方法。文章介绍了串空间模型的研究背景,分析它的架构和特点,综述有关研究工作,并分析其进一步的研究趋势。     

通信协议形式验证中的Petri网方法

Petri网,尤其是扩充类的Petri网对通信协议有很强的模拟能力.同时,Petri网能支持十分有效的验证技术.本文分析了需要验证的协议性质,提出了用线性不变量和标志机状态法全面分析这些性质的综合验证方法,并给出了对HDLC通信协议的验证实例.     

基于事务形式验证(TBFV)及8051的TBFV模型

提出了一种基于事务的形式验证方法(TBFV)，为待验证的系统构造功能验证模型，每个模型包括指令序列、输入变量、输出变量、输出函数、输出判定函数．这些可用Kripke结构来描述．这些功能验证模型实现了特定的事务，从而可以将一般的验证要求映射为具体的实现属性．这样，验证者无需了解设计的细节，可在较高层次上对系统行为进行验证．为了证明该方法的效率，分别用该方法和传统的形式验证方法验证了8051的RTL实现．8051中所有的指令都进行了验证，并给出了相应的功能验证模型．实验结果表明，采用该方法可大大节省验证工程师的时间．功能验证模型和验证指令可以在其他设计中复用．     

一种改进的新型说话人确认算法

在单芯片上实现的说话人确认系统是说话人识别应用的重要方向。该文面向片上应用,在使用DTW(dynamictime-warping)匹配方法的确认系统基础上提出一种改进的说话人确认算法,结合说话人确认的任务特点对DTW算法进行了改进:1)引入分层判决思想,2)在判决中结合单帧说话人区分能力估计,使系统的识别性能得到改进。新系统能够在对模板应用压缩处理后仍然保持良好的识别性能。测试表明新确认系统不做模板压缩时的等错误率为1.81%,经过1:8模板压缩处理后新系统的等错误率为2.35%。     

Ad Hoc网络安全路由协议形式化分析模型

为了能够对Ad Hoc网络安全路由协议进行有效的安全性证明,需要形式化的分析方法.针对目前缺乏有效方法的现状,结合Ad Hoc网络安全路由协议特点,利用图论理论,对传统安全协议分析方法Meadows模型进行扩展,扩展后的Meadows模型具有了路由描述和分析能力.使用扩展后的Meadows模型对Ad Hoc网络安全路由协议Ariadne进行了分析.分析结果显示,Ariadne协议存在产生虚假路由的漏洞,从而也说明了扩展后的Meadows模型能够用于Ad Hoc网络安全路由协议的安全性分析.     

一种本体的形式描述方法及其应用

针对目前还没有一种公认的形式本体描述方法的问题,在对本体的概念、性质进行分析的基础上,结合应用实际,提出了一种本体的形式描述方法DecDef(Declare Define).在这种描述方法中,把本体抽象成外部声明和内部表示两部分,在外部声明中说明本体中的概念、关系;在内部表示中说明这些概念和关系的语义,建立了本体内的简单推理模型.给出了这种形式描述的一个基于XML(Extensibble Makeup Language)的系统模型以及一个具体的应用实例,说明该方法在实际中是可行的.     

面向MANETs按需路由协议的黑洞攻击解析改进模型

传统移动Ad Hoc网络(mobile Ad Hoc network,MANETs)黑洞攻击解析模型存在网络拓扑结构固定、网络传输性能预测精确度低的问题.针对使用按需路由协议的MANETs网络,提出一种基于随机拓扑近似技术的黑洞攻击解析改进模型(improved black hole attack analytical model,IBAAM).IBAAM协议使用随机模型代替传统解析模型使用的n元2立方体模型,并将网络结构扩展至随机拓扑结构,使用最短跳距离概率描述表示网络拓扑结构的随机拓扑信息,再使用K均值聚类法实现跳距离文件配置以求解任意拓扑结构下的攻击概率问题,从而在不利用任何实际拓扑先验信息条件下有效预测MANETs网络平均丢包数目.IBAAM实验结果表明,在多种不同固定Ad Hoc拓扑结构下,IBAAM的网络丢包预测精确度在仿真结果的95%置信区间内,能够有效预测网络传输性能.     

GM(1,1)模型改进算法及其应用研究

原始序列规律、一次累加生成序列光滑度及其初始值是影响GM（1,1）模型预测精度的主要原因.为了获得较高的预测精度,在原有改善序列光滑度方法的基础上,给出一种基于加权和最小平均相对误差的灰色改进算法.该改进算法不但能够提高拟合及预测精度,而且拓展了传统GM（1,1）预测模型的适用范围.将传统方法与改进算法应用于实际设备故障诊断和寿命预测,结果表明,改进算法对于机械设备的预知维修具有较好的参考价值.