基于抽象-验证-细化范例的软件模型检测

如何保证软件系统的正确性和可靠性是当前软件开发面临的主要问题之一。模型检测作为一种重要的自动化验证技术在软件的分析与验证中正取得越来越多的成功。本文以微软的SLAM和加州大学伯克利分校的BLAST为例综述性地介绍了基于抽象-验证-细化范例的软件模型检测。     

软件模型检测中的抽象

软件模型检测对保证软件的正确性和可靠性具有十分重要的意义，而抽象是减轻模型检测中状态爆炸问题最重要的技术之一。本文综述当前广泛应用于软件模型检测中的抽象技术，介绍了该领域的进展及研究方向。     

程序重构预处理在提高软件模型检测效率中的应用

针对软件模型检测目前很难处理大型程序的问题,提出用程序重构技术对待检的源代码进行预处理,以提高模型检测算法的效率.程序重构将大型程序分解成语义一致的小型过程的集合,由于模型检测算法中过程总结边可单独计算,而且在程序中对某过程的调用可能有多次,这种预处理可以避免状态空间的重复搜索,从而降低模型检测算法在空间和时间上的开销.根据表达程序性质的线性时序逻辑LTL公式的构成,给出了程序重构预处理前后程序语义相等的充分条件;并给定程序和性质公式,用blast作为程序模型检测实验工具,比较程序重构预处理前后blast的运行结果.理论分析和部分程序上的实验表明：程序重构预处理能降低大型程序的模型检测开销,并满足软件模型检测的安全性要求.     

面向源代码的软件漏洞静态检测综述

软件静态漏洞检测依据分析对象主要分为二进制漏洞检测和源代码漏洞检测。由于源代码含有更为丰富的语义信息而备受代码审查人员的青睐。针对现有的源代码漏洞检测研究工作，从基于代码相似性的漏洞检测、基于符号执行的漏洞检测、基于规则的漏洞检测以及基于机器学习的漏洞检测4个方面进行了总结，并以基于源代码相似性的漏洞检测系统和面向源代码的软件漏洞智能检测系统两个具体方案为例详细介绍了漏洞检测过程。     

谓词抽象技术中循环反例的解决方法研究

为了解决谓词抽象技术面临的程序中循环体的每次迭代都至少需要一个谓词来实现的难题,提出了一个两阶段的不完全判定过程,用来对一个包含循环的反例进行可行性模拟.通过给出的循环探测算法来从抽象模型中提取出包含循环的反例,并用循环迭代的数量作为参数来确定模拟实例.实验结果表明,该方法在典型的缓冲溢出实例中的表现优于传统的抽象求精方法.     

软件源代码中的代码克隆现象及其检测方法

如果软件源程序中的一个代码段和同一程序中的另一个代码段在结构或语义上类似,这些代码段就成了代码克隆.概述代码克隆存在的各种形式,分析代码克隆产生的原因,并在概括了代码克隆检测的一般过程以后进一步阐述两类代码克隆检测方法:基于语义抽象树的检测方法和基于Token序列的检测方法.     

软件模型检测新技术研究

软件模型检测以其潜在的商业价值一直为学术界和工业界关注．本文通过剖析模型检测工具SLAM，探讨软件模型检测的机理、方法及若干核心技术，并总结出软件模型检测的一些新策略．     

并行软件模型检测

并行化是提高模型检测效率的重要手段。该文研究了基于标号迁移系统的C程序模型检测,提出一种软件模型检测并行化的方法。该方法利用软件模型检测工具模块化验证(MAGIC)的模块化特性对C程序进行组件分解,将各组件均衡地分发到若干计算节点,由节点调用MAGIC完成验证。由于保证节点间只有少量的通信与同步,该方法能达到较好的并行加速比,具有良好的可扩展性。实验结果显示,该方法大幅压缩了检测时间,有利于大规模软件的形式化验证。     

谓词抽象技术研究

随着软、硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,成为验证大规模系统的瓶颈.谓词抽象是解决状态空间爆炸的最有效方法之一,近年来得到迅速发展.介绍了谓词抽象的基本算法并比较了不同的求解支持工具;重点分析了反例指导的抽象求精和基于插值的抽象求精原理;分析了产生新谓词的各种方法的优、缺点;最后指出了谓词抽象技术进一步发展所面临的挑战和发展方向.     

面向随机模型检验的模型抽象技术

随机模型检验是经典模型检验理论的延伸和推广,由于其结合了经典模型检验算法和线性方程组求解或线性规划算法等,并且运算处理的是关于状态的概率向量而非经典模型检验中的位向量,所以状态爆炸问题在随机模型检验中更为严重.抽象作为缓解状态空间爆炸问题的重要技术之一,已经开始被应用到随机模型检验领域并取得了一定的进展.以面向随机模型检验的模型抽象技术为研究对象,首先给出了模型抽象技术的问题描述,然后按抽象模型构造技术分类归纳了其研究方向及目前的研究进展,最后对比了目前的模型抽象技术及其关系,总结出其还未能给出模型抽象问题的满意答案,并指出了有效解决模型抽象问题未来的研究方向.     

变量极小不可满足在模型检测中的应用

提出一个结合变量抽象和有界模型检测(BMC)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(VMU)的数学概念来驱动抽象精化的验证过程.一个VMU公式F的变量集合是保证其不可满足性的一个极小集合.严格证明了VMU驱动的精化满足抽象精化框架中的两个理想性质:有效性和极小性.虽然VMU的判定问题和极小不可满足(MU)一样难,即DP完全的,该案例研究表明,在变量抽象精化过程中,VMU比MU更为有效.     

模型检验中抽象技术研究综述

在模型检验中,抽象技术是解决状态空间爆炸问题的有效方法之一。论文描述了模型检验对抽象模型的基本要求,给出了抽象模型的定义及其评价指标,对抽象技术和自动化的抽象精化技术的主要方法及其研究进展作了比较深入、全面的综述,并讨论了抽象技术今后的发展方向。     

模型检验软件体系结构研究与进展

软件体系结构经过10多年的发展,在体系结构的基础理论、体系结构风格、体系结构描述语言和体系结构建模等方面的研究取得了一系列可喜的成就。目前,就软件体系结构的分析、评价、测试和验证的研究也在如火如荼地进行中。模型检验是一种基于自动机理论的形式验证方法,采用穷举状态空间的方式来证明系统的模型是否满足要验证的属性。同传统的测试和验证的手段相比,模型检验有其自身的优势。为此,越来越多的研究人员正在将模型检验技术应用到软件体系结构的分析和验证中。本文调查了模型检验技术在软件体系结构中的应用现状,剖析了影响软件体系结构模型检验的因素,给出了软件体系结构模型检验的未来主题。     

Parallel Assignments in Software Model Checking

In this paper we investigate how formal software verification systems can be improved by utilising parallel assignment in weakest precondition computations.We begin with an introduction to modern software verification systems. Specifically, we review the method in which software abstractions are built using counterexample-guided abstraction refinement (CEGAR). The classical NP-complete parallel assignment problem is first posed, and then an additional restriction is added to create a special case in which the problem is tractable with an O(n²) algorithm. The parallel assignment problem is then discussed in the context of weakest precondition computations. In this special situation where statements can be assumed to execute truly concurrently, we show that any sequence of simple assignment statements without function calls can be transformed into an equivalent parallel assignment block.Results of compressing assignment statements into a parallel form with this algorithm are presented for a wide variety of software applications. The proposed algorithms were implemented in the ComFoRT reasoning framework [J. Ivers and N. Sharygina. Overview of ComFoRT: A model checking reasoning framework. Technical Report CMU/SEI-2004-TN-018, Carnegie Mellon Software Engineering Institute, 2004] and used to measure the improvement in the verification of real software systems. This improvement in time proved to be significant for many classes of software.     

Software Model Checking: The VeriSoft Approach

Verification by state-space exploration, also often referred to as model checking, is an effective method for analyzing the correctness of concurrent reactive systems (for instance, communication protocols). Unfortunately, traditional model checking is restricted to the verification of properties of models, i.e., abstractions, of concurrent systems.We discuss in this paper how model checking can be extended to analyze arbitrary software, such as implementations of communication protocols written in programming languages like C or C++. We then introduce a search technique that is suitable for exploring the state spaces of such systems. This algorithm has been implemented in VeriSoft, a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary code.During the past five years, VeriSoft has been applied successfully for analyzing several software products developed in Lucent Technologies, and has also been licensed to hundreds of users in industry and academia. We discuss applications, strengths and limitations of VeriSoft, and compare it to other approaches to software model checking, analysis and testing.     

基于CEGAR的C程序空指针解引用检测

随着计算机软件规模和复杂度的日益增长,软件系统的可靠性和安全性倍受关注.空指针解引用是程序中常见的一类错误.提出了一种基于反例制导抽象精化CEGAR的C程序空指针解引用检测方法.该方法首先使用线性时序逻辑描述空指针解引用问题,然后通过抽象精化的方法检测待测程序中是否含有空指针解引用错误.为了达到完全自动验证的目标,同时针对空指针解引用问题,研究了该类性质的时序逻辑表达方法,并自动从程序中针对所有的指针变量,形成相应的时序逻辑公式.实验结果表明,所提出的方法在大规模C程序的空指针解引用检测方面有着重要的实际应用价值.