一种基于模型检测的二进制程序脆弱性分析框架

针对二进制程序脆弱性分析的实际需求,提出了一种基于模型检测的二进制程序脆弱性分析框架。首先定义了二进制程序的抽象模型,描述了基于有限状态自动机的软件脆弱性形式化表示和基于事件系统的软件安全属性表示方法。在此基础上,提出了基于模型检测的脆弱性分析过程和算法。根据该分析框架,设计并实现了二进制程序脆弱性分析工具原型。通过脆弱性分析实验,详细说明了该框架的工作原理,验证了该分析方法的有效性。     

一种层次式时间自动机模型检测方法

层次式时间自动机在软件系统建模过程中有着重要的应用.由于层次嵌套带来额外的复杂度,难以对之进行直接的形式化验证工作.提出一种平展算法,将层次式时间自动机转化为一组并行的顺序时间自动机,应用广播通道同步该自动机集合执行.在此基础之上实现一个原型系统可以将层次式时间自动机模型自动转化为模型检测工具UPPAAL的输入,从而可以对之进行验证.结合实时UML状态机图实例,证明了该方法的有效性.     

一种基于模型的特征交互检测方法

为了适应业务的不断更新,许多软件系统通过向公共的基础系统插入新的扩展来实现演化.这种演化策略虽然有利于并行开发和部署,但也面临着扩展间可能发生非预期特征交互的问题.目前,形式化方法在检测特征交互问题方面仍然是最有效的方法之一.这类方法着眼于检测扩展之间是否会发生冲突.虽然在小规模实验上较为成功,但是它们也面临着一些挑战.例如:扩展的非单调性、扩展组合的激增以及扩展模型可能无法获知的问题.实际上,许多特征交互都源于新扩展对基系统和已有扩展造成的不恰当影响.基于这种认识,集中关注由于扩展的不恰当影响所导致的交互冲突问题,提出了如何从已知的特征交互实例来分析产生冲突的原因的具体方法,并说明了如何制定约束以限制扩展中易导致冲突的行为,从而预防同一类行为可能导致的各种冲突.该方法被应用到电信系统特征交互的分析上,实验结果表明,大部分特征交互中导致冲突的行为都可以被检测出来.该方法不仅能够保证原有基系统或扩展模型的稳定、有效,避免扩展组合带来的问题,而且它无须公布扩展的模型细节.     

Petri网模型的扩展与检测

扩展了基本Petri网,提出了更加适合模型检测的MCPN方法,并将MCPN模型转换成模型检测工具SPIN的输入语言——PROMELA。使用SPIN完成对系统模型的检测,以提高软件设计的可靠性。在转换过程中,考虑了对当前情态下处于激活状态的多个变迁的同时激发;并提出了一种处理Petri网公平性问题的解决方案。     

UML模型检测方法的研究

统一建模语言（UML）是设计和分析软件系统最常用的方法，如何保证UML模型满足某些特性是一个非常重要的问题，而模型检测是一种能够有效提高系统可靠性的自动化技术。研究了使用简单进程元语言解释器（SPIN）对UML模型进行检测的方法。首先对UML模型进行形式化描述，使用层次自动机来描述状态图，然后根据层次自动机的操作语义将状态图和类图的部分信息转化为SPIN的输入语言PROMELA，使用SPIN来验证模型是否满足给定的线性时序逻辑所描述的系统约束，通过LTL公式描述顺序图的方式来验证与状态图之间的一致性问题。项目组基于此方法还开发了一套模型检测工具UMLChecker。     

模型检测新技术研究

1 引言软件是否可信赖已成为一个国家的经济、国防等系统能否正常运转的关键因素之一,尤其在一些诸如核反应堆控制、航空航天以及铁路调度等安全悠关(safety-critical)领域更是如此。这类系统要求绝对安全可靠,不容半点疏漏,否则将导致灾难性后果。如1996年6月4日,欧洲航天局阿丽亚娜(Ariane)501火箭因为其控制软件的规范和设计错误而导致发射37秒后爆炸。类似的报道屡见不鲜,如何确保这些系统的可靠性成为计算机科学与控制论领域共同关注的一个焦点问题。     

基于SAT工具的限界模型检测归约方法

限界模型检测主要对路径上的属性进行检测,基于此给出一种编码方法,将LTL公式在路径上展开,从而将限界模型检测转换为命题逻辑的可满足性问题,使用SAT求解工具来完成模型检测过程。阐述归约过程的正确性与完全性,通过一个具体例子证明了该方法的有效性。     

一种基于静态词法树的程序相似性检测方法*

传统的程序相似性检测工具并不能有效地检测出一些常见的高级词法、语义理解变换的抄袭方式。首先归纳了学生常用的三类抄袭手段,然后给出了基于词法树的程序相似性检测方法。以C语言为例,总结了生成词法树的结构体,并对程序的词法树进行主数据流、结构控制流和时序流分析后得出结构体依赖图;使用形式化的图同型方法来判断代码是否相似,还给出了一个聚类方法以获得彼此相似的程序子集。通过与JPlag、BuaaSim系统针对一组典型的抄袭样本集进行评测结果对比,本方法具有更好的检测效果。     

一种多模型协同的目标提取方法

固定摄像机目标提取多以高斯混合模型为背景模型,在检测运动缓慢、间歇停滞的目标时会出现前景目标空洞的问题。为此,提出一种能够适应目标间歇停滞的多模型协同目标提取方法。采用高斯混合模型进行背景学习,通过光线检测模型和场景状态检测模型协同控制背景适时更新,利用阴影检测模型剔除阴影。实验结果表明,与KaewTraKulPong P方法相比,该方法能较完整地提取到目标轮廓,且单帧处理时间较少。     

一种软件模型检测方法及其原型系统

Microsoft Research.Zin项目

MOPS:an Infrastructure for Examining Security Properties of Software

程序分析技术 2005

基于符号模型检测方法的应对规划系统 2006

>>更多...     

应用吴方法进行高层次定界模型检验

以吴方法为理论基础,提出一种针对高层次设计验证的定界模型检验方法.通过使用多项式等式建模高层次设计和待验证性质,将定界模型检验问题转化为定理证明问题,并用吴方法有效地解决该定理证明问题.实验结果表明,与基于布尔SAT、基于LP的RTL SAT以及基于非线性求解器的性质检验方法相比,该方法在时间消耗上具有相当大的优势.     

Remove Irrelevant Atomic Formulas for Timed Automaton Model Checking

Most of the timed automata reachability analysis algorithms in the literature explore the state spaces by enumeration of symbolic states, which use time constraints to represent a set of concrete states. A time constraint is a conjunction of atomic formulas which bound the differences of clock values. In this paper, it is shown that some atomic formulas of symbolic states generated by the algorithms can be removed to improve the model checking time- and space-efficiency. Such atomic formulas are called as irrelevant atomic formulas. A method is also presented to detect irrelevant formulas based on the test-reset information about clock variables. An optimized model-checking algorithm is designed based on these techniques. The case studies show that the techniques presented in this paper significantly improve the space- and time-efficiency of reachability analysis.     

Model Checking at IBM

Over the past nine years, the Formal Methods Group at the IBM Haifa Research Laboratory has made steady progress in developing tools and techniques that make the power of model checking accessible to the community of hardware designers and verification engineers, to the point where it has become an integral part of the design cycle of many teams. We discuss our approach to the problem of integrating formal methods into an industrial design cycle, and point out those techniques which we have found to be especially effective in an industrial setting.     

并发程序的切片模型检验方法

提出了一种对并发程序进行切片以缩减模型检验状态空间的方法，首先针对并发程序中的同步与通信定义了一组依赖关系，包括并发分支与接合．非确定性，信道，共享变量等特征，对于从要验证的时态逻辑性质中提取的关于多个程序点的切片标准，文中给出算法根据相应的依赖关系通过不动点运算得到并发程序切片，可以证明得到的切片与原程序对于该性质具有相同的可满足性。     

Model Checking Programs

The majority of work carried out in the formal methods community throughout the last three decades has (for good reasons) been devoted to special languages designed to make it easier to experiment with mechanized formal methods such as theorem provers, proof checkers and model checkers. In this paper we will attempt to give convincing arguments for why we believe it is time for the formal methods community to shift some of its attention towards the analysis of programs written in modern programming languages. In keeping with this philosophy we have developed a verification and testing environment for Java, called Java PathFinder (JPF), which integrates model checking, program analysis and testing. Part of this work has consisted of building a new Java Virtual Machine that interprets Java bytecode. JPF uses state compression to handle big states, and partial order and symmetry reduction, slicing, abstraction, and runtime analysis techniques to reduce the state space. JPF has been applied to a real-time avionics operating system developed at Honeywell, illustrating an intricate error, and to a model of a spacecraft controller, illustrating the combination of abstraction, runtime analysis, and slicing with model checking.     

程序模型检查器综述

模型检查实际程序设计语言编写的程序是近年来程序验证领域的研究热点之一,出现了一批针对C,C++或Java语言的程序模型检查器原型.总结了程序模型检查中的主要问题及相关技术,以是否使用中间建模语言为标准,对现有程序模型检查器进行了分类,并具体地介绍了一些代表性工具中的模型获取及化简技术,最后展望了程序模型检查器未来的研究方向.     

Needham-Schroeder公钥协议的模型检测分析

密码协议安全性的分析是当前网络安全研究领域的一个世界性难题.提出了运用模型检测工 具SMV(symbolic model verifier)分析密码协议的方法,并对著名的Needham-Schroeder(NS )公钥协议进行了分析.分析结果表明,入侵者可以轻松地对NS公钥协议进行有效攻击,而这个 攻击是BAN逻辑分析所没有发现过的.同时,给出了经SMV分析过的一个安全的NS公钥协议 的改进版本.     

基于模型检测的系统生存性分析

提出一种采用模型检测进行系统生存性分析的形式化方法。给出系统所处环境及主要提供的服务,引入灾难和错误等因素,建立系统生存性模型。通过描述系统的可生存能力,确定其生存性需求并转换为相应的逻辑表示。以电话接入网络为例,利用PRISM对系统进行建模及验证,结果表明,该形式化方法可以规范并简化生存性分析过程。     

基于Java内存模型的并发程序模型检测

为了提高性能,Java内存模型允许编译器在优化过程中改变代码的执行顺序,同时该技术也会造成共享数据的更新顺序与本来的执行顺序不同。在多线程Java并发程序中,这些代码乱序执行会引起很多难以发现的错误。现有的Java程序模型检测技术并没有考虑这些顺序改变的问题。因此,本文提出了一种建立包含多线程交互及线程内代码乱序执行的完整模型,并利用模型检测工具进行穷举检测的算法。该算法可以发现原有技术无法发现的新问题,更好地检测高可靠性要求的Java并发程序。