形状分析符号执行引擎中的状态合并

符号执行技术以其良好的精确度控制和代码覆盖率被广泛应用于静态程序分析和高覆盖率测试用例自动生成。 符号执行 在分析程序时,以模拟真实的程序执行过程的方式分析程序的数据流和控制流信息,并检查程序可能出现的所有状态,得到程序的分析结果。高精确度和高覆盖率要求对程序状态描述具体而完备,这会导致符号执行过程中常见的状态爆炸问题。首先提出在不同的执行路径上对具体内存状态进行合并的算法,然后对内存模型进行适度的抽象,扩大状态合并算法的适用范围,最后讨论状态合并所带来的实际效果,并提出了状态合并的优化解决方案。所提出的算法在符号执行引擎ShapeChecker上实现,并取得了良好的实验结果。     

An empirical investigation into open source web applications’ implementation vulnerabilities

Current web applications have many inherent vulnerabilities; in fact, in 2008, over 63% of all documented vulnerabilities are for web applications. While many approaches have been proposed to address various web application vulnerability issues, there has not been a study to investigate whether these vulnerabilities share any common properties. In this paper, we use an approach similar to the Goal-Question-Metric approach to empirically investigate four questions regarding open source web applications vulnerabilities: What proportion of security vulnerabilities in web applications can be considered as implementation vulnerabilities? Are these vulnerabilities the result of interactions between web applications and external systems? What is the proportion of vulnerable lines of code within a web application? Are implementation vulnerabilities caused by implicit or explicit data flows? The results from the investigation show that implementation vulnerabilities dominate. They are caused through interactions between web applications and external systems. Furthermore, these vulnerabilities only contain explicit data flows, and are limited to relatively small sections of the source code.     

Dynamic verification of C++ generic algorithms

Dynamic verification is a new approach to formal verification, applicable to generic algorithms such as those found in the Standard Template Library (STL, part of the Draft ANSI/ISO C++ Standard Library). Using behavioral abstraction and symbolic execution techniques, verifications are carried out at an abstract level such that the results can be used in a variety of instances of the generic algorithms without repeating the proofs. This is achieved by substituting for type parameters of generic algorithms special data types that model generic concepts by accepting symbolic inputs and deducing outputs using inference methods. By itself, this symbolic execution technique supports testing of programs with symbolic values at an abstract level. For formal verification one also needs to generate multiple program execution paths and use assertions (to handle while loops, for example), but the authors show how this can be achieved via directives to a conventional debugger program and an analysis database. The assertions must still be supplied, but they can be packaged separately and evaluated as needed by appropriate transfers of control orchestrated via the debugger. Unlike all previous verification methods, the dynamic verification method thus works without having to transform source code or process it with special interpreters. They include an example of the formal verification of an STL generic algorithm     

Tuning parallel symbolic execution engine for better performance

Symbolic execution is widely used in many code analysis, testing, and verification tools. As symbolic execution exhaustively explores all feasible paths, it is quite time consuming. To handle the problem, researchers have paralleled existing symbolic execution tools (e.g., KLEE). In particular, Cloud9 is a widely used paralleled symbolic execution tool, and researchers have used the tool to analyze real code. However, researchers criticize that tools such as Cloud9 still cannot analyze large scale code. In this paper, we conduct a field study on Cloud9, in which we use KLEE and Cloud9 to analyze benchmarks in C. Our results confirm the criticism. Based on the results, we identify three bottlenecks that hinder the performance of Cloud9: the communication time gap, the job transfer policy, and the cache management of the solved constraints. To handle these problems, we tune the communication time gap with better parameters, modify the job transfer policy, and implement an approach for cache management of solved constraints. We conduct two evaluations on our benchmarks and a real application to understand our improvements. Our results show that our tuned Cloud9 reduces the execution time significantly, both on our benchmarks and the real application. Furthermore, our evaluation results show that our tuning techniques improve the effectiveness on all the devices, and the improvement can be achieved upto five times, depending upon a tuning value of our approach and the behaviour of program under test.     

A survey of new trends in symbolic execution for software testing and analysis

Symbolic execution is a well-known program analysis technique which represents program inputs with symbolic values instead of concrete, initialized, data and executes the program by manipulating program expressions involving the symbolic values. Symbolic execution has been proposed over three decades ago but recently it has found renewed interest in the research community, due in part to the progress in decision procedures, availability of powerful computers and new algorithmic developments. We provide here a survey of some of the new research trends in symbolic execution, with particular emphasis on applications to test generation and program analysis. We first describe an approach that handles complex programming constructs such as input recursive data structures, arrays, as well as multithreading. Furthermore, we describe recent hybrid techniques that combine concrete and symbolic execution to overcome some of the inherent limitations of symbolic execution, such as handling native code or availability of decision procedures for the application domain. We follow with a discussion of techniques that can be used to limit the (possibly infinite) number of symbolic configurations that need to be analyzed for the symbolic execution of looping programs. Finally, we give a short survey of interesting new applications, such as predictive testing, invariant inference, program repair, analysis of parallel numerical programs and differential symbolic execution.     

基于符号化执行的Fuzzing测试方法

设计并实现一种基于符号化执行的Fuzzing测试方法。通过代码插装,在程序执行过程中收集路径约束条件,依据一定的路径遍历算法生成新路径约束条件并进行求解,构造可以引导程序向新路径执行的输入测试数据。提出一种改进的污点分析机制,对路径约束条件进行简化,提高了代码覆盖率和漏洞检测的效率。     

Extending symbolic execution for automated testing of stored procedures

Stored procedures in database management systems are often used to implement complex business logic. Correctness of these procedures is critical for flawless working of the system. However, testing them remains difficult due to many possible database states and constraints on data. This leads to mostly manual testing. Newer tools offer automated execution for unit testing of stored procedures but the test cases are still written manually. We propose an approach of using dynamic symbolic execution for generating automated test cases and corresponding database states for stored procedures. We model the constraints on data imposed by the schema and the SQL statements, treating values in database tables as symbolic. We use SMT solver to find values that will drive the stored procedure on a particular execution path. We instrument the internal execution plans generated by PostgreSQL to extract constraints. We use Z3 to generate test cases consisting of table data and procedure inputs. Our evaluation using stored procedures from a large business application and various GitHub repositories quantifies the evidence of effectiveness of our technique by generating test cases that lead to schema constraint violations and user-defined exceptions.     

基于符号执行的Android原生代码控制流图提取方法

提出了一种基于符号执行的控制流图提取方法,该方法为原生库中的函数提供了符号执行环境,对JNI 函数调用进行模拟,用约束求解器对符号进行求解。实现了控制流图提取原型系统 CFGNative。实验结果表明,CFGNative可准确识别样例中所有的JNI函数调用和原生方法,并能够在可接受的时间内达到较高的代码覆盖率。     

基于符号执行和N-scope复杂度的代码混淆度量方法

代码混淆可有效对抗逆向工程等各类MATE攻击威胁,作为攻击缓和性质的内生安全技术发展较为成熟,对代码混淆效果的合理度量具有重要价值。代码混淆度量研究相对较少,针对代码混淆弹性的度量方法与泛化性、实用性度量方法相对缺乏。符号执行技术广泛应用于反混淆攻击,其生成遍历程序完整路径输入测试集的难度可为混淆弹性度量提供参考,然而基于程序嵌套结构的对抗技术可显著降低符号执行效率,增加其混淆弹性参考误差。针对上述问题,提出结合符号执行技术和N-scope复杂度的代码混淆度量方法,该方法首先基于程序符号执行时间定义程序混淆弹性;其次提出适配符号执行的N-scope复杂度,定义程序混淆强度同时增强符号执行对多层嵌套结构程序的混淆弹性度量鲁棒性;进而提出结合动态分析与静态分析的混淆效果关联性分析,通过对程序进行符号执行与控制流图提取量化混淆效果。面向C程序构建了该度量方法的一种实现框架并验证,实验对3个公开程序集及其混淆后程序集约4 000个程序进行混淆效果度量,度量结果表明,提出的度量方法在较好地刻画混淆效果的同时拥有一定的泛化能力与实用价值;模拟真实混淆应用场景给出了该度量方法的使用样例,为混淆技术使...     

Using symbolic execution to guide test generation

Although a number of weaknesses of symbolic execution, when used for software testing, have been highlighted in the literature, the recent resurgence of strongly‐typed languages has created opportunities for re‐examining symbolic execution to determine whether these shortfalls can be overcome. This paper discusses symbolic execution in general and makes two contributions: (a) overcoming one of the key problems, analysing programs with indexed arrays; and (b) describing the incorporation of a symbolic execution module for test case generation into an integrated testing tool. For methods which index arrays, a new approach determines all the possible values of each array index, allowing the generation of equivalence classes for every possible combination of array element aliases. An incremental simplification approach, which converts path expressions to canonical forms in order to identify infeasible paths at the earliest opportunity and thus reduce the analysis time, is also described. Symbolic execution is most effective when included in an integrated test and analysis environment: a component test bench was built with a symbolic execution module integrated into it, providing a toolbox of software component test and code analysis methods aimed at programmers at all levels. Copyright © 2000 John Wiley & Sons, Ltd.     

动态web应用中的缺陷定位研究

在动态web应用中,动态生成的HTML页面产生的缺陷难以定位并且会严重影响web应用程序的可用性和稳定性。针对以上问题,本文提出了一种基于符号约束集的web缺陷定位方法,通过对web服务端程序的动态符号执行生成一个带有符号约束的树模型,并给出了一个高效的缺陷映射定位算法。为验证该方法的有效性,本文对几个基于PHP的开源web程序进行实验,结果表明该方法在web应用的HTML缺陷检测定位覆盖率和准确率方面都有所改进。     

Model-driven development of composite context-aware web applications

Context-awareness constitutes an essential aspect of services, especially when interaction with end-users is involved. In this paper a solution for the context-aware development of web applications consisting of web services is presented. The methodology proposes a model based approach and advocates in favour of a complete separation of the web application functionality from the context adaptation at all development phases (analysis, design, implementation). In essence, context adaptation takes place on top of and is transparent to the web application business functionality. Starting from UML diagrams of independent web services and respective UML context models, our approach can produce a functional composite context-aware application. At execution level this independence is maintained through an adaptation framework based on message interception.     

Hunter:一种指令集体系结构无关的二进制级动态测试用例生成技术

动态测试用例生成技术是一类新兴的软件测试技术。由于使用该类技术无需任何人工干预,也无需验证人员具备任何专业知识,同时该类技术能够无误地发现程序错误,越来越多的研究者采用该技术查找预发布的二进制级软件错误。然而,已有的该类技术及其实现系统不具有可重定向性,只能处理面向某种特定指令集体系结构(ISA)的二进制代码,进行测试用例的生成与查错。本文提出了一种全新的指令集体系结构无关的二进制级动态测试用例生成技术,以及实现该技术的系统Hunter。与已有的动态测试用例生成技术不同,Hunter具有极强的可重定向性,可对任何指令集体系结构的二进制代码进行查错,定向地为其生成指向不同执行路径的测试用例。Hunter定义了一套元指令集体系结构(MetaISA),将在二进制代码执行过程中收集到的所有执行信息映射为MetaISA,并对生成的MetaISA序列进行符号化执行、约束收集、约束求解以及测试用例生成,从而使整个过程与ISA无关。我们实现了Hunter,将其重定向至32位x86、PowerPC和Sparc ISA,并使用该系统为6个含有已知错误的测试程序查错。实验结果表明,由于MetaISA的引入,只需很小的开销,Hunter系统即可容易且有效地重定向至不同的ISA,并且Hunter能够有效地发现面向32位x86、PowerPC和Sparc ISA编写的二进制应用中隐藏极深的错误。     

面向数据库模式变更的代码演化推荐方法

许多软件依赖数据库来存储信息。数据库模式的变更可能导致程序代码中与数据库相关的SQL语句代码不能正常执行,因而找出一种能够直接定位到需要修改的SQL语句代码并推荐出这些代码可能的修改方案的方法是十分必要的。提出的面向数据库模式变更的代码演化推荐方法首先自动检测出软件系统数据库模式发生的变更,随后采用程序切片技术得出与数据库操作相关的程序切片;确定受到数据库模式变更影响的程序切片后,利用源程序转换流程图算法将程序切片转化为程序流程图;根据程序流程图的分支条件得出SQL语句所有可能的特定执行路径;最后采用图映射的方法对每条路径的SQL语句进行变更语句推荐,推荐出新数据库模式下可执行的SQL语句。为了验证该方法的可行性,实现了一个用于自动检测数据库模式变更并能推荐出SQL语句演化后代码的插件工具。     

Managing Conflicts between Rules

Rules are used as a programming paradigm in several application domains, including active databases, planning, expert systems, and billing. For example, active databases have rules that execute upon the occurrence of particular events if specified condition predicates are satisfied. It is often the case that multiple rules are fireable when a particular event occurs. We propose a declarative mechanism to control the interaction and execution of multiple rules. The mechanism is based upon logical meta-rules that can express various types of relationships between rules. The meta-rules allow us to reason statically about the rule behavior. We can determine, in polynomial time, whether a rule will never execute, whether two rules can ever be executed together, and whether a rule system is guaranteed to have a unique execution set for all possible rules that become fireable. In this paper, we illustrate our techniques using rules in an active database. A system based upon the meta-rules and the static analysis presented here has been found to be of value in a billing application at AT & T to control interactions between discount plans.     

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

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

结合静态分析与动态符号执行的软件漏洞检测方法

动态符号执行是近年来新兴的一种软件漏洞检测方法,它可以为目标程序的不同执行路径自动生成测试用例,从而获得较高的测试代码覆盖率。然而,程序的执行路径很多,且大部分路径都是漏洞无关的,通常那些包含危险函数调用的路径更有可能通向漏洞。提出一种基于静态分析的有导动态符号执行方法,并实现了一个工具原型SAGDSE。该方法通过静态分析识别目标程序中调用危险函数的指令地址,在动态符号执行过程中遇到这些指令地址时收集危险路径约束,再通过约束求解生成走危险路径的测试用例,这些测试用例将更可能触发程序漏洞。实验结果表明了该方法的有效性。     

Simple linear string constraints

Modern web applications often suffer from command injection attacks. Even when equipped with sanitization code, many systems can be penetrated due to software bugs. It is desirable to automatically discover such vulnerabilities, given the bytecode of a web application. One approach would be symbolically executing the target system and constructing constraints for matching path conditions and attack patterns. Solving these constraints yields an attack signature, based on which, the attack process can be replayed. Constraint solving is the key to symbolic execution. For web applications, string constraints receive most of the attention because web applications are essentially text processing programs. We present simple linear string equation (SISE), a decidable fragment of the general string constraint system. SISE models a collection of regular replacement operations (such as the greedy, reluctant, declarative, and finite replacement), which are frequently used by text processing programs. Various automata techniques are proposed for simulating procedural semantics such as left-most matching. By composing atomic transducers of a SISE, we show that a recursive algorithm can be used to compute the solution pool, which contains the value range of each variable in concrete solutions. Then a concrete variable solution can be synthesized from a solution pool. To accelerate solver performance, a symbolic representation of finite state transducer is developed. This allows the constraint solver to support a 16-bit Unicode alphabet in practice. The algorithm is implemented in a Java constraint solver called SUSHI. We compare the applicability and performance of SUSHI with Kaluza, a bounded string solver.     

基于符号执行和人机交互的自动向量化方法

自动向量化技术是一种针对单指令多数据(SIMD)向量化计算单元的并行编译优化技术,它能够自动将源程序中多个相同标量操作合并为一个向量操作,从而提升系统吞吐量。随着SIMD向量化计算单元的广泛应用,自动向量化技术已经成为学术界和商业界的研究热点。针对现有自动向量化技术可向量化模块识别难、向量化优化方案选择难、可移植性差等问题,提出了一种基于符号执行和人机交互的自动向量化方法。首先借助于符号执行技术,获得较好的可移植性和较高的可向量化模块识别率;然后利用人机交互技术选择出理想的向量化方案。应用示例及实验结果表明,该方法具有较好的可操作性,能够有效提升自动向量化技术的优化效果和可移植性。