使用事件自动机规约的C语言有界模型检测

提出使用事件自动机对 C 程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法。事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性。事件自动机将属性规约与C程序本身隔离,不会改变程序的结构。在事件自动机的基础上,提出了自动机可达树的概念。结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法。最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法。实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约。     

有效的C 内存泄露检测方法

提出了一个有效的C 内存泄漏检测方法.方法在分析内存泄漏的基础上,通过重新实现动态内存分配和释放函数,记录内存分配的确切位置并跟踪动态内存的使用情况.在程序结束时,方法利用跟踪结果检测和定位内存泄漏.最后,通过在Windows和Linux平台上的实验验证了本文方法的有效性.     

基于Yices对时间自动机的有界模型检测

为了避免在有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,给出一个利用SMT(satisfiability modulo theories)工具进行的对时间自动机进行有界模型检测的方法.该方法将时间自动机模型直接转换成SMT工具可识别的逻辑公式,利用SMT工具可求解包含有整数型和实数型变量逻辑公式的能力来进行模型检测.实验结果表明,对于某些可达性性质的验证,该方法的效率有一定的优势.     

基于Linux的动态内存检测工具的设计与实现

内存的动态内存使用问题是C/C＋＋程序员永远面临的问题。针对内存管理和使用的各类错误,设计并实现一个基于Linux的动态内存检测模块,可以对源码程序检测出内存泄漏、内存写溢出、“野指针”操作和内存管理函数的不匹配等问题。实验结果表明,系统具有效率高、易用性好的特点。     

利用双向推导检测Java程序中的内存泄漏

Java应用程序中大量使用动态内存。Java程序运行过程中会自动对不可达的动态内存进行回收,但不能及时地对应用程序中可达但不活跃的动态内存进行回收,从而造成内存泄漏。为有效地检测内存泄漏,提出了采用双向推导进行内存泄漏检测的方法,在推导的过程中利用分离逻辑理论对应用程序中的动态内存进行分析,确定到达程序中每条语句的可达的动态内存和活跃的动态内存,辅助完成动态内存泄漏的检测。     

Spark环境下基于SMT的分布式限界模型检测

在基于可满足性模理论(SMT)的限界模型检测中,限界深度对于程序验证结果的可信性和程序验证效率具有重要影响。传统串行检测方法由于单机处理性能和内存的限制,不能在限界较深的条件下进行验证。针对该问题,在Spark环境下提出一种分布式限界模型检测方法。将源程序的LLVM中间表示(LLVM-IR)构造为Spark内置的数据结构Pair RDD,利用MapReduce算法将Pair RDD转化为表示验证条件的弹性分布式数据集(VCs RDD),VCs RDD转化为SMT-LIB并输入SMT求解器进行验证。实验结果表明,与传统串行检测方法相比,该方法提高了验证过程中的限界深度和验证结果的正确率,并且对于复杂度较高的程序在限界相同的情况下其验证速度也有所提升。     

一个动态内存管理模块的实现

介绍一个动态内存管理模块,可以有效地检测C程序中内存泄漏和写内存越界等错误,适用于具有标准C语言开发环境的各种平台.     

Linux平台下基于源代码插装的动态内存检测

在C／C＋＋语言程序中．指针的使用使代码灵活、简便．但所带来的类似内存泄漏、内存写溢出等的内存使用的错误却很难分析和消除．针对这些容易出现的内存使用错误．提出了Linux平台下一种基于源文件信息提取和源代码插装的动态内存检测方法，设计实现了一个动态内存检测模块DDMEM．可以检测源代码的内存泄漏、内存写溢出、释放野指针和内存管理函数的不匹配等问题．给出了写溢出错误的一个实例检测，以验证方法的有效性．     

动态内存错误的静态检测

内存泄漏、空指针引用等动态内存错误在C,C 等支持动态内存操作的程序中普遍存在．在程序中,动态内存管理错误是导致动态内存错误的根本原因．动态内存错误的静态检测方法是在对程序进行静态分析的基础上,应用路径别名分析方法,确定动态内存变量之间存在的过程内和过程间的路径别名关系,在此基础上对程序中违反动态内存管理模式的动态内存操作进行分析,以确定程序中存在的动态内存错误．     

一个动态内存管理模块的实现

介绍一个动态内存管理模块，可以有效地检测C程序中内存泄漏和写内存越界等错误，适用于具有标准C语言开发环境的各种平台。     

Bounded Model Checking of CTL^*

Bounded Model Checking has been recently introduced as an efficient verification method for reactive systems. This technique reduces model checking of linear temporal logic to propositional satisfiability. In this paper we first present how quantified Boolean decision procedures can replace BDDs. We introduce a bounded model checking procedure for temporal logic CTL＊ which reduces model checking to the satisfiability of quantified Boolean formulas. Our new technique avoids the space blow up of BDDs, and extends the concept of bounded model checking.     

一种混合式内存泄漏静态检测方法

内存泄漏是导致系统性能降低的重要问题.提出一种基于模型检测算法的内存泄漏静态检查方法TMC.该方法依据程序的控制流图构建对应于程序执行的有限状态自动机,进而在此基础上应用模型检测算法分析程序中可能存在的内存泄漏.论文利用几个典型的程序实例详细说明了TMC的工作原理,并通过基于内存操作密集的测试程序集PtrDist的实验对TMC进行了验证.实验结果表明,TMC能够显著提升内存泄漏分析的精度.     

C/C++程序静态内存泄漏警报自动确认方法

内存泄漏是C/C++程序的一种常见的、难以发现的缺陷,一直困扰着软件开发者,尤其是针对长时间运行的程序或者系统软件,内存泄漏的后果十分严重.针对内存泄漏的检测,目前主要有静态分析和动态测试两种方法.动态测试实际运行程序,具有较大开销,同时依赖测试用例的质量;静态分析技术及自动化工具已经被学术界和工业界广泛运用于内存泄漏缺陷检测中,然而由于静态分析采取了保守的策略,其结果往往包含数量巨大的误报,需要通过进一步人工确认来甄别误报,但人工确认静态分析的结果耗时且容易出错,严重限制了静态分析技术的实用性.本文提出了一种基于混合执行测试的静态内存泄漏警报的自动化确认方法.首先,针对静态分析报告的目标程序中内存泄漏的静态警报,对目标程序进行控制流分析,并计算警报的可达性,形成制导信息;其次,基于警报制导信息对目标程序进行混合执行测试;最后,在混合执行测试过程中,监控追踪内存对象的状态,判定内存泄漏是否发生,对静态警报进行动态确认并分类.实验结果表明该方法可以对静态内存泄漏警报进行有效的分类,显著降低了人工确认的工作量.实验详情参见：http://ssthappy.github.io/memleak/.     

Melton: a practical and precise memory leak detection tool for C programs

Memory leaks are a common type of defect that is hard to detect manually. Existing memory leak detection tools suffer from lack of precise interprocedural analysis and path-sensitivity. To address this problem, we present a static interprocedural analysis algorithm, that performs fully pathsensitive analysis and captures precise function behaviors, to detect memory leak in C programs. The proposed algorithm uses path-sensitive symbolic execution to track memory actions in different program paths guarded by path conditions. A novel analysis model called memory state transition graph (MSTG) is proposed to describe the tracking process and its results. In order to do interprocedural analysis, the proposed algorithm generates a summary for each procedure from MSTG and applies the summary at the procedure’s call sites. A prototype tool called Melton is implemented for this procedure. Melton was applied to five open source C programs and 41 leaks were found. More than 90% of these leaks were subsequently confirmed and fixed by their maintainers. For comparison with other tools, Melton was also applied to some programs in standard performance evaluation corporation (SPEC) CPU 2000 benchmark suite and detected more leaks than the state of the art approaches.     

基于SAT的软件验证

线性时态逻辑SE-LTL是具有高表达力和基于状态、事件推理能力的并发系统规约语言.目前,SE-LTL的模型检测算法依然是显式的,状态空间爆炸是检测的主要困难.对SE-LTL引入一种有界模型检测技术,该技术将SE-LTL模型检测归约为命题公式的可满足性问题,避免了基于二叉图方法中状态空间的快速增长,加速了验证过程.对SE-LTL-X进一步在该技术中集成stuttering等价技术.实验结果表明该集成有效地降低了验证时间.     

基于开放编译器的内存泄漏检测机制

内存泄漏是程序设计中经常出现的问题，会降低系统性能，甚至耗尽内存空间导致系统崩溃。文章采用反射和开放编译技术，对开放编译器OpenC 进行了扩展与改进，设计并实现了一个CC 动态内存泄漏检测工具，以帮助开发和测试人员查找内存泄漏。     

Model checking driven static analysis for the real world: designing and tuning large scale bug detection

Model checking and static analysis are traditionally seen as two separate approaches to software analysis and verification. In this work we define a model, checking approach for the static analysis of large C/C++ source code bases to detect potential run-time issues such as program crashes, security vulnerabilities and memory leaks. Working on the intersection of software model checking and automated static bug detection for real-life systems, we address a number of issues: how to scale for real-life systems of 1,000,000 LoC or more, how to quickly write new checks, and most importantly how to distinguish between relevant and irrelevant bugs and fine tune the analysis accordingly. We define our model checking-based static analysis approach implemented in our tool Goanna, illustrate a number of design and implementation decisions to obtain practical outcomes and relevant results, and present our findings by empirical data obtained from regularly analyzing large industrial and open source code bases such as the Firefox Web browser.     

Verification of consensus algorithms using satisfiability solving

Consensus is at the heart of fault-tolerant distributed computing systems. Much research has been devoted to developing algorithms for this particular problem. This paper presents a semi-automatic verification approach for asynchronous consensus algorithms, aiming at facilitating their development. Our approach uses model checking, a widely practiced verification method based on state traversal. The challenge here is that the state space of these algorithms is huge, often infinite, thus making model checking infeasible. The proposed approach addresses this difficulty by reducing the verification problem to small model checking problems that involve only single phases of algorithm execution. Because a phase consists of a small, finite number of rounds, bounded model checking, a technique using satisfiability solving, can be effectively used to solve these problems. The proposed approach allows us to model check several consensus algorithms up to around 10 processes.     

C程序内存泄漏智能化检测方法

内存泄漏在采用显式内存管理机制的C语言中是一种常见的代码缺陷,内存泄漏的检测方法目前主要是静态分析与动态检测.动态检测开销大,且高度依赖测试用例;静态分析目前被学术界和工业界广泛应用,但是存在大量误报,需要人工对检测结果进行确认.内存泄漏静态分析的误报通常是由于对指针、分支语句和全局变量分析的不准确性导致的.提出了一种内存泄漏的智能化检测方法,通过使用机器学习算法学习程序特征与内存泄漏之间的相关性,构建机器学习分类器,并应用机器学习分类器进一步提高内存泄漏静态分析的准确性.首先构建机器学习分类器,然后通过静态分析方法构建从内存分配点开始的Sparse Value Flow Graph（SVFG）,并从中提取内存泄漏相关特征,再使用规则和机器学习分类器进行内存泄漏的检测.实验结果显示,该方法在分析指针、分支语句和全局变量时是有效的,能够提高内存泄漏检测的准确性,降低内存泄漏检测结果的误报.最后,对未来研究的可行性以及面临的挑战进行了展望.