基于条件执行切片谱的多错误定位

基于程序谱的错误定位技术由于其较高的定位效率已成为当前软件调试领域研究热点之一.这种技术通常根据测试覆盖信息计算程序语句发生错误的可疑度来进行错误定位.然而,这种技术会随着程序中错误数目的增多效率不断下降.鉴于此,提出了一种基于条件执行切片谱的多错误定位技术(conditioned execution slicing spectrum-based multiple fault localization, CESS-MFL),以提高多错误定位的效率.CESS-MFL技术首先根据输入变量的谓词条件构建错误相关条件执行切片的谱矩阵,然后依次计算错误相关条件执行切片中的元素(语句或语句块)的可疑度,并生成可疑度报告.实验验证了CESS-MFL技术比当前流行的基于程序谱的Tarantula技术、基于程序切片的Intersection技术、Union技术有更高的多错误定位效率,并且可在有效的时间和空间复杂度内完成.     

一种支持多线程程序的符号执行技术

符号执行是一种实用的验证程序中是否包含某类错误的技术,具有0误报率的优点,但是主流的执行工具并不支持分析多线程程序。本文对已有的多线程程序的符号执行工具进行分析,发现存在的问题有：1）有些工具性能好,但是不支持外部库,实用性很差;2）有些工具支持外部库函数,但是版本老,难以更新和维护,无法检查减法溢出、乘法溢出、移位溢出等基本类型的bug。本文基于最主流的符号执行工具KLEE设计并实现支持多线程程序的符号执行工具——MTSE（Multi-Thread Symbolic Execution）。MTSE支持libc和libc++库,并且相对于已有的同类工作Cloud9,MTSE可以多查找出约50%的程序缺陷,并且指令覆盖率和分支覆盖率上均有约30%的提升。     

一种基于逆向程序流的程序切片算法*

传统的程序切片方法一般基于程序依赖图(PDG)和系统依赖图(SDG)的可达性算法,但是在建立PDG和SDG的过程中会计算一些与切片无关的数据依赖,造成时空资源的浪费及切片效率的降低。提出了一种基于程序逆向流的切片算法,它事先建立逆向程序流,再从切片点开始沿逆向程序流扫描程序以获得程序切片,只计算与切片相关的数据依赖,从而提高了切片计算的时空效率。通过实验发现该算法具有一定的可行性和实用性。本算法适用于包括Fortran、C等编程语言在内的命令式程序的切片生成。     

一种面向二进制的控制流图混合恢复方法

控制流图恢复是进行二进制文件安全性分析的基础,静态恢复分析速度快,但其精确度欠缺;动态恢复方法的优点是精确度高,但分析效率较低。将两者优点结合,提出了面向二进制程序的混合分析恢复方法,在对二进制文件进行静态分析生成控制流图的基础上,结合局部符号执行技术和反向切片技术对间接分支跳转的目的地址进行求解,之后再分析边和节点的可达性,合并不可达的边和节点。经实验验证,混合方法的分析效率与静态方法相近,远高于纯动态分析方法,其精确度较静态方法有较大提高。     

Automated bug isolation via program chipping

This paper introduces program chipping, a simple yet effective technique to isolate bugs. This technique automatically removes or chips away parts of a program so that the part that contributes to some symptomatic output becomes more apparent to the user. Program chipping is similar in spirit to traditional program slicing and debugging techniques, but chipping uses very simple techniques based on the syntactic structure of the program. We have developed a chipping tool for Java programs, called ChipperJ, and have run it on a variety of small to large programs, including a Java compiler, looking for various symptoms. The results are promising. The reduced program is generally about 20–35% of the size of the original. ChipperJ takes less than an hour on large programs to perform this reduction; even if it took overnight, that would be reasonable if it saves the developer time. Copyright © 2006 John Wiley & Sons, Ltd.     

基于SMT求解器的路径敏感程序验证

随着软件规模的不断扩大以及复杂度的不断增长,人们越来越关注软件的可信性问题.验证程序是否满足断言所描述的性质,是保证软件可信性的一种常见方法.路径敏感的程序验证由于不可能遍历所有的路径,需要合并路径信息,因此造成精度上的损失.提出一种基于SMT求解器的路径敏感程序验证方法,在保证精确度的前提下,有效减少路径搜索空间.其基本思想是,利用最大强连通分量压缩循环路径,然后根据目标断言对控制流图进行切片.使用一种布尔表达式方法对路径空间进行抽象,结合抽象解释和符号执行技术对路径进行验证.结合F-Soft平台和Z3工具对该方法进行了实验验证,结果表明,该方法在验证的精确度和效率上都有较好的效果.     

一种用于测试数据生成的动态程序切片算法

介绍了程序切片技术的基本概念，提出了一种基于前向分析的动态程序切片算法，探讨了程序切片在软件测试数据生成中的应用，结果表明可以有效地提高基于路径的测试数据生成效率。     

精确的程序静态分析

程序的静态分析是程序语言和编译领域的一个重要研究方向,已经被研究了很多年.近年来,它也引起形式方法和软件工程领域的重视,被用于程序测试和正确性验证.文中从程序的语法特征、所关心的数据类型和程序性质等方面比较了一些静态分析技术.着重描述基于路径的分析方法,特别是符号执行技术,讨论了程序路径可行性分析问题及其分类、复杂度.针对程序分析精度的一种量化指标,说明了其计算方法.     

相关路径静态分析中协同式逆向推理方法

相关路径生成,是程序动态分析中的一种重要方法.通过对目标执行路径的获取和分析来生成与其相关的近邻执行路径,在程序行为特征分析、编译优化和调试等研究方向有重要的作用.现有的方法主要通过改变路径节点序列来生成近邻的路径集合,由于缺乏关键节点的路径引导信息,导致生成大量冗余或者无效的路径集合.提出采用协同式逆向分析的近邻路径生成方法,针对目标路径的后置条件,采用逆向符号分析方法产生程序各个基本块的前置条件作为执行路径的引导信息.同时,通过调整距离因子k的取值,可以有针对性地生成与目标路径的编辑距离不超过k的近邻路径集合.实验结果表明:与现有方法相比,该方法在准确性和效率方面有明显的优势.     

Automatic extraction of executable program subsets by simultaneous dynamic program slicing

Developers of software product families and maintainers of legacy software can benefit from the ability to automatically extract a correctly functioning subset of the code of a system that performs a desired subset of its behaviors. This article introduces a technique for automatic subsetting based on computing asimultaneous dynamic program slice of the code for a set of representative inputs. I show first why the naive approach (unioning traditional dynamic slices) fails, then give an abstract algorithm that succeeds in any slicing framework satisfying certain (mild) assumptions. Experiments using an implementation within the ISAT environment indicate that the algorithm consistently produces significantly smaller subsets than three competing approaches. I also discuss how to characterize the subset's correctness on inputs of interest outside the set used to compute the slice.     

A formal relationship between program slicing and partial evaluation

A formal relationship between program slicing and partial evaluation is established. It is proved that for terminating programs, a residual program produced by partial evaluation is semantically equivalent to a conditioned slice. Received May 2002 Revised Octber 2004 and July 2005 Accepted August 2005 by D. J. Cooke     

基于语义的恶意软件判定器框架

目前代码迷惑技术已经成为构造恶意软件变体的主要方式,大量出现的病毒变体使得传统基于程序文本特征的病毒排查工具的防护作用大大降低.本文提出一种新的基于语义的恶意软件变体判定框架,为了确定一个程序是否是某种恶意软件的变体:首先基于符号执行收集程序语义状态,然后通过证明语义之间是否满足变体关系来确定该程序是否是恶意软件的变体.本框架能够识别经代码迷惑变换后得到的程序是属于变换前程序的变体,从而可以减少对病毒数据库的更新.最后,通过一个实现了该框架的原型系统来说明基于语义的恶意软件判定器框架的可行性.     

Slicing, Chopping, and Path Conditions with Barriers

One of the critiques on program slicing is that slices presented to the user are hard to understand. This is mainly related to the problem that slicing dumps the results onto the user without any explanation. This work will present an approach that can be used to filter slices. This approach basically introduces barriers which are not allowed to be passed during slice computation. An earlier filtering approach is chopping which is also extended to obey such a barrier. The barrier variants of slicing and chopping provide filtering possibilities for smaller slices and better comprehensibility. The concept of barriers is then applied to path conditions, which provide necessary conditions under which an influence between the source and target criterion exists. Barriers make those conditions more precise.     

基于抽象符号表的内存模型

符号执行技术在软件测试和程序验证中发挥着重要作用。如何抽象和处理程序中各种数据类型和语法成分是符号执行必须解决的问题。本文提出抽象符号表的概念,以及基于抽象符号表建模内存的方法。抽象符号表记录可寻址对象的名称、类型、抽象地址和符号值,是一种简单、精确的内存抽象机制。内存模型是所有使用符号执行的技术的前提,本文系统给出了一个面向符号执行的内存模型。基于抽象符号表的内存模型能够统一处理各种数据类型和语法成分,包括函数和类,能够直接处理指针别名问题,不需要额外的别名分析算法。经过一些性能优化处理,基于抽象符号表的内存模型具有较好的性能。     

JUTA: 一个Java自动化单元测试工具

描述了一个Java自动化的单元测试工具JUTA.JUTA首先调用工具Soot解析单个Java方法的源码,并将源码解析成一个控制流图.在此基础上,采用符号执行的方法分析控制流图上的路径.工具能够自动地产生满足覆盖率标准的程序的测试用例.这种方法产生的所有测试用例都是可执行的,并且一般来说具有较小的测试用例数.如果用户能够合理地给出描述程序错误的断言,框架JUTA能够自动地检查源码中部分特定类型的错误.实验结果表明工具对Java单元代码的动态测试和静态测试均能在可接受的时间内给出有效的结果.     

一种精简二进制代码的程序理解方法

精简二进制代码形式的软件是软件分析和程序理解需要处理的一类具有代表性的对象,基于高级语言源代码和调试符号信息的传统分析方法在处理此类软件时受到了极大限制。提出一种精简二进制形式软件的理解方法,首先将分析对象转变为运行期进程,引入实际运行中的进程信息;然后引入程序的行为特征,以程序表现出的外在行为和对外接口作为辅助信息,将此类外部特征映射到程序代码;最后基于切片思想和调试技术,获得程序切片并分析。这种方法为分析理解过程扩展了信息量,降低了复杂度,解决了分析此类软件时信息缺失和难以建立理解模型的问题。     

基于符号执行的自动利用生成系统

在本文中,我们提出BAEG,一个自动寻找二进制程序漏洞利用的系统.BAEG为发现的每一个漏洞产生一个控制流劫持的利用,因此保证了它所发现的漏洞都是安全相关并且可利用的.BAEG针对输入造成程序崩溃的情况进行分析,面临的挑战主要有两点：1）如何重现崩溃路径,获取崩溃状态;2）如何自动生成控制流劫持利用.对于第一点,本论文提出路径导向算法,将崩溃输入作为符号值,重现崩溃路径.对于第二点,我们总结多种控制流劫持的利用原理,建立对应的利用产生模型.此外,对于非法符号读、写操作,BAEG还可以让程序从崩溃点继续执行,探索程序深层次代码,检测崩溃路径逻辑深处是否还有利用点.     

一种C程序断言的全自动静态验证方法

在软件程序中插入断言是保证软件质量的一个简单但有效的方法，人们常使用测试的方法检验程序中的断言是否满足，但测试很难保证验证的完备性。本文提出了一种可以保证完备性的全自动静态断言验证方法，其基本思想是基于程序切片符号执行程序的所有执行路径，并证明路径上的所有断言都满足。为了尽量减少符号执行的语句的数量，使用了基于反例的抽象精化方法，从一个粗略的切片标准开始迭代地符号执行一爷路径，根据验证的反例自动生成下一次迭代过程中使用的精化的切片标准。包含循环的程序可能具有无穷多条程序执行路径，提出的基于符号执行上下文不变式证明的方法可以证明由于循环导致的无穷多条路径中断言都满足，从而使得验证过程可以终止。实验表明，提出的全自动静态断言验证方法不仅可行，而且验证代价较小，具有较强的实用性。     

Unit Test Data Generation for C Using Rule-Directed Symbolic Execution

Unit testing is widely used in software development. One important activity in unit testing is automatic test data generation. Constraint-based test data generation is a technique for automatic generation of test data, which uses symbolic execution to generate constraints. Unit testing only tests functions instead of the whole program, where individual functions typically have preconditions imposed on their inputs. Conventional symbolic execution cannot detect these preconditions, let alone converting these preconditions into constraints. To overcome these limitations, we propose a novel unit test data generation approach using rule-directed symbolic execution for dealing with functions with missing input preconditions. Rule-directed symbolic execution uses predefined rules to detect preconditions in the individual function, and generates constraints for inputs based on preconditions. We introduce implicit constraints to represent preconditions, and unify implicit constraints and program constraints into integrated constraints. Test data generated based on integrated constraints can explore previously unreachable code and help developers find more functional faults and logical faults. We have implemented our approach in a tool called CTS-IC, and applied it to real-world projects. The experimental results show that rule-directed symbolic execution can find preconditions (implicit constraints) automatically from an individual function. Moreover, the unit test data generated by our approach achieves higher coverage than similar tools and efficiently mitigates missing input preconditions problems in unit testing for individual functions.

     

基于条件分类可执行切片谱的软件缺陷定位

基于条件执行切片谱的多错误定位（Multiple Fault Localization based on Conditioned Execution Slicing Spectrum，CESS-MFL）考虑了程序的依赖性，可以一定程度降低程序随着缺陷数的增多而效率降低的问题，但该技术仍受与缺陷无关语句的影响比较大。因此，提出了一种基于条件分类可执行切片的软件缺陷定位方法（Conditioned Classification Execution Slicing Spectrum-based Software Fault Localization，CCESS-SFL），该技术对CESS-MFL技术中的谓词条件进行了改进并分类。根据谓词条件与缺陷相关执行切片确定条件特征集，根据条件特征集进行分类得到条件分类执行切片谱，计算元素的可疑度，最后生成可疑度报告。CCESS-SFL技术在西门子7个套件中得到了有效的验证，它优于当前流行的Tarantula、Jaccard、Ochiai以及CESS-MFL技术，可以进一步降低与缺陷无关语句的影响。