基于携带证明代码的IP核安全性验证方法

针对集成电路在RTL代码级设计阶段由于使用第三方IP软核引入的安全性问题,现有的功能测试方法较难实现全覆盖检测无法保障电路安全性。本文在已有基于携带证明代码思想的基础上改进提出一种安全性验证方法。该方法结合形式化验证平台coq,运用形式化逻辑描述电路代码和安全性假设,构造证明过程并采用系统的证明检查器验证证明过程。通过在DES电路代码的实验,说明了该验证方法能有效检测出电路中后门路径类型的硬件木马。相比较于测试类方法覆盖率不能达到100%而无法确定电路是非安全性,本文提出的方法可以确定电路是安全或非安全,能够保证电路代码级的安全可信性。

一种构造代码安全性证明的方法

提出一种构造代码安全性证明的新方法.这种方法的基本思想是,在基础逻辑中定义辅助递归函数来帮助构造证明.这种构造方法在不增加系统信任计算基础的情况下可以极大地减轻构造证明的工作量,并且减小安全性证明的规模同时介绍了该方法在一个FPCC系统中的应用.在这个系统中使用该方法使得代码的安全性证明可以自动产生.全部工作的细节已在证明辅助工具Coq中得以实现.

部分冗余删除的证明变换研究

部分冗余删除优化是一个同时包含有公共子表达式删除和表达式提升的复杂优化,但是对基于部分冗余删除优化的证明变换研究,还停留在对一些简单情况的处理和讨论上.本文在实验室前期优化对证明调整的研究基础上,总结简单优化行为对证明变换的调整过程,通过将部分冗余删除优化细分为简单的PRE、复杂的PRE、复制代码的PRE、前瞻的PRE,给出了不仅是简单的优化调整证明方法,而是包含有基于复杂的部分冗余删除优化的证明变换的方法.

基于提示的移动代码安全检查

基于语言内部安全机制能够有效地保证移动代码的安全执行 ,其思想是要在移动代码中附加详细且足够的满足安全策略检查的注解信息 .基于提示的移动代码的安全检查 ,克服了目前 PCC存在的验证条件必须回送和证明长度过于庞大等缺陷 ,从而获得了更佳的代码安全检查性能 .

一种出具证明编译器中的汇编级断言和证明生成的方法

携带证明代码允许代码消费方通过检查代码生产方提供的证明,来判断代码是否满足相应的安全规范.本文实现了一个类C语言的出具证明编译器原型,它在将带有规范标注的源代码编译成汇编代码的同时,还能产生汇编代码满足相应规范的Coq可检查证明,从而保证汇编代码的安全性.本文设计了一种Hoare风格的汇编级验证框架,并在此框架下提出并实现一种新的自动生成汇编级断言和证明的方法.

基于移动代理计算模型的安全

移动代理可视为由客户机器生成的程序派送到网络中漫游以寻找合适的机器予以执行后将结果返回或送到特定的主机。基于移动代理的计算在诸多方面有着比传统的基于RPC或消息机制的计算更适合实现分布式计算的优势。在对基于移动代理的计算模型简单介绍后，对其优点做出评估。尽管这祥，这种计算模式还是带来了许多显著的安全上的问题．将分析出安全上的威胁．从而从两个方面来得出基于移动代理计算模型的安全需求。之后，将考察现有的该问题的对策．特别是移动加密方案。也将给出一种重要的应用图景作为例子来诠释基于移动代理计算的安全解决方案。基于移动代理的计算安全是一个涉及面广并且远未成熟的研究领域，因此最后将做出一个简要的对此问题更深的考虑和未来工作的可能的方向的评述。

一种用于指针程序验证的指针逻辑

本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合.

基于类型注解的认证编译器设计与实现

基于类型注解的认证编译器是安全策略系统的核心部件 ,它不仅能够用C语言的类型安全子集编写的程序编译成优化的Intelx86 /linux汇编语言程序 ,而且还可以根据类型安全策略的要求产生带注解的汇编程序 实验结果表明 ,新设计的认证编译器可实现 :①类型安全的C语言子集的编译 ;②许多标准的局部优化 ;③可以对数组运行时越界操作进行检查 由于安全策略系统的证明是建立在含注解的代码基础之上的 ,因此 。

动态存储管理安全验证的Coq实现

随着软件规模和复杂度的日益提升,软件安全的问题变得越来越严峻,同时有越来越多的研究工作集中在高可信软件的开发上.由于类型系统表达能力的不足,现有的研究不触及底层软件的验证.由于Hoare逻辑更好的表达能力,采用Hoare逻辑风格的推理,在汇编语言级别,使用Coq形式化与定理证明工具可以实现一个经过安全验证的动态存储管理函数库,这是程序验证技术一次有意义的实践.实践表明,程序验证技术可以应用到高可信软件的开发上.

P2P网络环境下的远程认证技术研究

介绍了适合P2P网络中的不同的远程认证技术,包含密码认证,语义远程认证,基于信任模型的认证和携带代码的证明认证,接着对提出的认证技术的优点和不足之处进行分析,最后讨论如何合理地把提出的技术结合在一起,应用到P2P网络中。

渐进式标记-清扫垃圾收集机制验证

垃圾收集已经成为可靠、高效程序运行平台的一个重要组成部分.渐进式垃圾收集由于在用户程序运行时并行的执行垃圾收集操作,其算法及实现则更为复杂,其可靠性也更难以得到保证.本文论述使用Hoare风格的程序验证框架形式验证渐进式标记-清扫垃圾收集机制及其写拦截器在汇编语言层次上的实现的研究工作.被验证的属性涵括了简单的类型安全到整个内存堆上的数据保持.本文所有的验证工作都实现在Coq辅助定理证明工具中,从而可以迅速的用于构造携带证明的代码包.

远程网络环境下认证技术的研究

在远程网络环境下,认证是建立网络安全系统必不可少的基本组成部分。该文首先介绍了常用的认证技术,包括口令认证、基于生物学信息的认证、基于密钥机制的认证及基于挑战/应答的认证机制,接着对常用的认证技术进行了详细的分析,并指出严重的漏洞,最后讨论了当前较有前景的认证技术,包括携带代码的证明的认证、语义远程认证及可信计算的远程认证机制。