共查询到19条相似文献,搜索用时 93 毫秒
1.
2.
随着软件运行时验证技术的发展,出现了许多面向C语言的运行时内存安全验证工具。这些工具大多是基于源代码或者中间代码插桩技术来实现内存安全的运行时检测。但是,其中一些没有经过严格证明的验证工具往往存在两方面的问题,一是插桩程序的加入可能会改变源程序的行为及语义,二是插桩程序并不能有效保证内存安全。为了解决这些问题,文中提出了一种使用Coq定理证明器来判定内存安全验证工具算法是否正确的形式化方法,并使用该方法对C语言运行时验证工具Movec的动态检测算法的正确性进行了证明。对安全规范性质的证明结果表明了Movec的内存安全性动态检测算法是正确的。 相似文献
3.
安全协议认证的形式化方法研究 总被引:6,自引:0,他引:6
安全协议认证是网络安全领域中重大课题之一。形式化方法多种多样。该文首先论述了模型检测技术及其在安全协议验证中的应用,然后介绍了各种定理证明方法和定理证明工具,接着讨论其它形式化验证方法,最后论述形式化方法的一些研究方向。 相似文献
4.
形式化方法是分析与验证安全协议属性的强有力的工具.在对一阶定理证明器ProVerif深入研究的基础上,对简化的Needham-Schroeder认证协议进行了形式化分析. 相似文献
5.
各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础. 相似文献
6.
7.
针对完整性报告协议(IRP)存在局部和全局攻击的安全隐患,对StatVerif进行语法扩展,增加了与完整性度量相关的构造算子和析构算子,通过对平台配置证明(PCA)安全进行分析,发现其存在的局部攻击和全局攻击,包括通过未授权命令对平台配置寄存器和存储度量日志进行篡改。对攻击者能力进行了建模,详细说明了攻击者如何通过构造子和析构子形成知识,进而对平台配置证明进行攻击。最后,在平台配置证明不满足对应性属性的情况下,从理论上证明了攻击序列的存在,并给出了平台配置证明满足局部可靠和全局可靠的条件,通过形式化验证工具Proverif证明了命题的合理性。 相似文献
8.
一种安全协议的形式化设计方法 总被引:1,自引:0,他引:1
文章以协议分析器为辅助工具,结合定理证明方法,给出了一个安全协议形式化设计方法。该方法首先根据协议规范构造全信息项及冗余协议,使用定理证明保证冗余协议的安全性。对冗余协议利用安全性保持约简规则和随机约简规则进行约简,从而得到最优约简协议。该方法实现了安全协议的自动设计,具有良好的扩展性,可以根据需求和协议的发展增加设计规则和约简规则。 相似文献
9.
10.
SpaceWire是在苛刻环境下的高速通信总线协议,译码电路是其接收端的关键电路,对该电路进行形式化验证具有重要的现实意义.形式化验证方法中的定理证明将需要分析的电路进行形式化建模,结合定理证明器,对模型的性质进行严格推理从而完成验证.本文运用定理证明的方法,在高阶逻辑证明工具HOL4中对SpaceWire总线的译码电路进行形式化验证.首先根据SpaceWire标准规范抽取相关性质,用高阶逻辑语言形式化描述;然后分析电路设计中的VHDL代码,依据代码实现的功能用相应的逻辑谓词建模;最后在HOL4中证明了译码电路设计的模型能满足所提取的性质.本文同时给出了形式化建模的方法和验证过程. 相似文献
11.
Shaoying Liu 《Computer Languages, Systems and Structures》1993,18(4):273-282
The realization of an abstract programming language is a good approach for automating the software production process and facilitating the correctness proof of a software system.
This paper introduces a formal language for programming at the abstract level by combining Pascal with VDM (Vienna Development Method). The notation provided by the language obliges programmers to consider the correctness of programs throughout the whole process of programming, and the proof axiom and rules presented in this paper may be used to prove the correctness of programs. A complete example is given to illustrate how to program using APL and how to prove the correctness of programs using the given axiom and rules. 相似文献
12.
13.
随着软件规模和复杂度的日益提升,软件安全的问题变得越来越严峻,同时有越来越多的研究工作集中在高可信软件的开发上 .由于类型系统表达能力的不足,现有的研究不触及底层软件的验证 .由于Hoare逻辑更好的表达能力,采用Hoare逻辑风格的推理,在汇编语言级别,使用Coq形式化与定理证明工具可以实现一个经过安全验证的动态存储管理函数库,这是程序验证技术一次有意义的实践 .实践表明,程序验证技术可以应用到高可信软件的开发上 . 相似文献
14.
15.
16.
The research described in this paper involved developing transformation techniques that increase the efficiency of the original program, the source, by transforming its synthesis proof into one, the target, which yields a computationally more efficient algorithm. We describe a working proof transformation system that, by exploiting the duality between mathematical induction and recursion, employs the novel strategy of optimizing recursive programs by transforming inductive proofs. We compare and contrast this approach with the more traditional approaches to program transformation and highlight the benefits of proof transformation with regards to search, correctness, automatability, and generality. 相似文献
17.
18.
Proof planning extends the tactic-based theorem proving paradigm through the explicit representation of proof strategies.
We see three key benefits to the proof planning approach to the development of proof strategies: flexibility, re-usability
and synergy. Here we demonstrate these benefits in terms of reasoning about imperative programs where we reuse strategies
developed previously for proof by mathematical induction. In particular, we focus upon strategies for automating the discovery
of loop invariants. Our approach tightly couples the discovery of invariants with the process of patching proof strategy failures.
This revised version was published online in June 2006 with corrections to the Cover Date. 相似文献
19.
形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高,而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.本文结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减轻用户手动验证程序的开销. 相似文献