Windows x64无签名驱动程序运行方法

主机监管系统利用过滤驱动程序对系统实现全面监管.随着微软64位操作系统的推出,要求驱动程序经过付费签名后才能正常运行.由种种原因使驱动程序不能被签名时,主机监管系统就不能在WINDOWS 64位操作系统上使用.因此无签名驱动程序问题成为在WINDOWS 64位系统开发最普遍的问题之一,会导致程序难移植、影响用户体验.通过对WINDOWS 64位系统数字签名过程的逆向分析,提出一种能一次性关闭系统数字签名验证机制的方法,从而顺利加载运行未签名驱动程序.     

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

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

基于前后断言法的温度控制系统程序验证

温度控制系统已经广泛地应用于各个领域,温度控制系统对可靠性要求较高,一般来说,温度控制系统的故障将导致灾难性的后果。温度系统的设计直接影响了系统的可靠性,文章利用前后断言法对温度控制系统的设计进行验证,结论表明,该方法可以保证温度控制系统设计的正确性,保证系统可靠运行。     

燃料组件程序ROBIN-1.7的验证和确认

利用国际公开基准题开展ROBIN-1.7燃料组件计算程序的共振计算、输运计算、燃耗计算等模块的验证工作。分别利用临界基准问题、蒙特卡罗程序、OECD NEA燃耗基准问题及其他输运-燃耗基准问题等对ROBIN-1.7程序进行确认。验证及确认结果表明,ROBIN-1.7程序的共振计算、输运计算、燃耗计算等模块及集成计算结果是正确的;ROBIN-1.7程序对各问题主要物理参数(如反应性、棒功率分布以及同位素浓度)的计算精度达到了国际同类商业程序的水平,满足在压水堆中工程应用的要求。     

有界闭区间并上的非线性循环程序的终止性验证

利用符号动力学理论中有关一维离散映射的函数和区间的转换图方法及相关结论,证明一类非线性循环程序不终止的必要条件是在该程序循环区间上有不动点或者周期点存在,并给出相应的终止性验证算法.利用该算法可以验证一维有界闭区间上的非线性循环程序的终止性.最后,给出计算实例演示该算法的算法步骤.     

关于程序验证方法的讨论

一、引言 自从1967年Floyd发表其论文“给程序赋予意义以来,程序自动验证工具的研究持续了数十年。Floyd在文[4]中提出了用“断言式方法”证明程序的正确性。其具体作法是:在程序程图的每一条     

操作系统内核程序函数执行上下文的自动检验

函数执行上下文正确性是操作系统内核程序最容易违反且难以检查的正确性性质.应用传统的技术检查该类错误都有一定的困难和局限性.提出一个验证函数执行上下文正确性的框架PRPF,详细描述了其建模过程和相关算法.PRPF相比传统技术的优势有:直接检查源代码、无须编写形式化的验证规约、较低的时空运行开销、良好的可扩展性等等.该技术已应用在Linux内核2.4.20的网络设备驱动程序检查中.应用表明,PRPF能够自动探测程序中所有执行路径,有效地检查函数执行上下文的正确性.实验发现了Linux内核的23处编程错误,另有     

软件安全漏洞的静态检测技术

软件安全漏洞问题日益严重,静态漏洞检测提供从软件结构和代码中寻找漏洞的方法。该文研究软件漏洞静态检测的两个主要方面：静态分析和程序验证,重点分析词法分析、规则检查、类型推导、模型检测、定理证明和符号执行等方法,将常用的静态检测工具按方法归类,讨论、总结静态检测技术的优势、适用性和发展趋势。     

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

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

XYZ系统在电信领域中的应用

最近几年,在软件工程界内部有一种趋势,这就是开发以面向具体领域的ＣＡＳＥ环境．作为这样的一种ＣＡＳＥ工具,ＸＹＺ系统是由一时序逻辑语言ＸＹＺ／Ｅ和一组基于该语言的工具集构成．在ＸＹＺ系统中有很多的工具,它们被用来满足不同的需要．众所周知,ＳＤＬ（ｓｐｅｃｉｆｉｃａｔｉｏｎａｎｄｄｅｓｃｒｉｐｔｉｏｎｌａｎｇｕａｇｅ）是电信领域中的一个国际标准语言,而且有关基于该语言的环境已在开发,但是有关该语言的验证工作,特别是利用有关时序逻辑语言进行验证的工作还不多．作为一种尝试,本文将利用ＸＹＺ系统中的一个子系统ＸＹＺ／ＶＥＲＩ,对ＳＤＬ所描述的有关电信领域中的例子进行验证．