An evaluation of the effectiveness of symbolic testing

The effectiveness in discovering errors of symbolic evaluation and of testing sad static program analysis are studied. The three techniques are applied to a diverse collection of programs and the results compared. Symbolic evaluation is used to carry out symbolic testing and to generate symbolic systems of path predicates. The use of the predicates for automated test data selection is analysed. Several conventional types of program testing strategies are evaluated. The strategies include branch testing, structured testing and testing on input values having special properties. The static source analysis techniques that are studied include anomaly analysis and interface analysis. Examples are included which describe typical situations in which one technique is reliable but another unreliable. The effectiveness of symbolic testing is compared with testing on actual data and with the use of an integrated methodology that includes both testing and static source analysis. Situations in which symbolic testing is difficult to apply or not effective are discussed. Different ways in which symbolic evaluation can be used for generating test data are described. Those ways for which it is most effective are isolated. The paper concludes with a discussion of the most effective uses to which symbolic evaluation can he put in an integrated system which contains all three of the validation techniques that are studied.     

程序状态条件合并中变量隐式关联分析方法

程序分析的主要目标是对程序的性质进行研究,符号执行作为目前主流的分析方法在生成高效的测试用例集或提高路径覆盖率等方面发挥着重要的作用,其中路径条件表达式的提取以及约束求解是路径分析过程中的关键步骤.现有的路径分析方法普遍存在约束求解效率不高而导致的路径覆盖率较低的问题.由于符号执行引擎所采用的搜索策略不尽相同,在符号执行分析过程中存在状态合并的过程,该抽象过程可能导致产生不正确的测试用例.以提高路径分析效率为目标,提出一种高效的程序分析方法：首先对传统的符号执行树的表示方法进行改进,提取不同路径共享的符号表达式和路径约束条件以提高符号执行过程中状态合并的效率,然后采用隐式关联分析方法,产生逆向分析中的依赖条件集合,并给出基于依赖条件重构的算法以提高路径覆盖率.实验结果表明：相对于传统的状态合并以及符号执行方法,该方法有更为高效的状态合并效率以及更高的路径约束条件分析精度.     

函数调用路径测试用例自动生成的方法研究

测试用例自动生成是软件测试自动化中最为关键的组成部分之一,符号执行作为一种程序分析方法,以其可提供高覆盖率测试用例的优势被广泛应用其中,但路径爆炸和约束求解问题很大程度制约了符号执行技术在现实程序分析中的应用。将研究粒度由语句提升至函数,利用抽象语法树和字节码序列提取到的函数关键信息和控制信息得到函数调用关系模型,设计算法生成函数调用路径（函数调用路径表示程序从开始到结束之间函数的调用或执行序列）。该方法不仅减少了测试路径数目缓解了路径爆炸问题,还有效解决了控制条件中存在函数导致符号表达式难求解的问题。实验结果表明该方法可优化测试路径集,在不降低覆盖率的前提下减少测试用例数量。     

Symbolic execution of floating‐point computations

Symbolic execution is a classical program testing technique which evaluates a selected control flow path with symbolic input data. A constraint solver can be used to enforce the satisfiability of the extracted path conditions as well as to derive test data. Whenever path conditions contain floating‐point computations, a common strategy consists of using a constraint solver over the rationals or the reals. Unfortunately, even in a fully IEEE‐754‐compliant environment, this leads not only to approximations but also can compromise correctness: a path can be labelled as infeasible although there exists floating‐point input data that satisfy it. In this paper, the peculiarities of symbolic execution of programs with floating‐point numbers are addressed. Issues in the symbolic execution of this kind of program are carefully examined and a constraint solver is described that supports constraints over floating‐point numbers. Preliminary experimental results demonstrate the value of the approach proposed. Copyright © 2005 John Wiley & Sons, Ltd.     

Symbolic Evaluation and the Analysis of Programs

Symbolic evaluation is a form of static program analysis in which symbolic expressions are used to denote the values of program variables and computations. It does not require the user to specify which path at a conditional branch to follow nor how many cycles of a loop to consider. Instead, a symbolic evaluator uses conditional expressions to represent the uncertainty that arises from branching and develops and attempts to solve recurrence relations that describe the behavior of loop variables.     

基于目标制导符号执行的静态缓冲区溢出警报自动确认技术

缓冲区溢出漏洞是一类严重的安全性缺陷。目前存在动态测试和静态分析技术来检测缓冲区溢出缺陷:动态测试技术的有效性取决于测试用例的设计,而且往往会引入执行开销;静态分析技术及自动化工具已经被广泛运用于缓冲区溢出缺陷检测中,然而静态分析由于采取了保守的策略,其结果往往包含数量巨大的误报,需要通过进一步人工确认来甄别误报,但人工确认静态分析的结果耗时且容易出错,严重限制了静态分析技术的实用性。符号执行技术使用符号代替实际输入,能系统地探索程序的状态空间并生成高覆盖度的测试用例。本文提出一种基于目标制导符号执行的静态缓冲区溢出警报确认方法,使用静态分析工具的输出结果作为目标,制导符号执行确认警报。我们的方法分为3步:首先在过程间控制流图中检测静态分析警报路径片段的可达性,并将可达的警报路径片段集合映射为用于确认的完整确认路径集合;其次在符号执行中通过修剪与溢出缺陷疑似语句无关的路径,指导符号执行沿特定确认路径执行;最后在溢出缺陷疑似语句收集路径约束并加入溢出条件,通过约束求解的结果,对静态分析的警报进行分类。基于上述方法我们实现了原型工具BOVTool,实验结果表明在实际开源程序上BOVTool能够代替人工减少检查59.9%的缓冲区溢出误报。     

分布式符号执行平台

在软件工程学中,符号执行技术是一门高效的程序缺陷检测技术.符号执行使用符号值作为程序的输入,将程序的执行转变为相应符号表达式的操作,通过系统地遍历程序的路径空间,实现对程序行为的精确分析.然而,因受路径爆炸问题与约束求解问题的制约,符号执行技术也面临着可扩展性差的问题.为了在一定程度上缓解该问题,本文实现了一个分布式符号执行平台,该平台在调度算法的调度下将任务从主节点分发给多个工作节点,进而实现了任务的并行执行,降低了符号执行的时间开销.     

精确的程序静态分析

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

SYMCON—A Hybrid Symbolic/Connectionist System for Word Sense Disambiguation

Connectionist methods and knowledge-based techniques are two largely complementary approaches to natural language processing (NLP). However, they both have some potential problems which preclude their being a general purpose processing method. Research reveals that a hybrid processing approach that combines connectionist with symbolic techniques may be able to use the strengths of one processing paradigm to address the weakness of the other one. Hence, a system that effectively combines the two different approaches can be superior to either one in isolation. This paper describes a hybrid system—SYMCON (SYMbolic and CONnectionist) which integrates symbolic and connectionist techniques in an attempt to solve the problem of word sense disambiguation (WSD), which is arguably one of the most fundamental and difficult issues in NLP. It consists of three sub-systems: first, a distributed simple recurrent network (SRN) is trained by using the standard back-propagation algorithm to learn the semantic relationships among concepts, thereby generating categorical constraints that are supplied to the other two sub-systems as the initial results of pre-processing. The second sub-system of SYMCON is a knowledge-based symbolic component consisting of a knowledge base containing general inferencing rules in a certain application domain. Third, a localist network is used to select the best interpretation among multiple alternatives and potentially ambiguous inference paths by spreading activation throughout the network. The structure, initial states, and connection weights of the network are determined by the processing outcome in the other two sub-systems. This localist network can be viewed as a medium between the distributed network and the symbolic sub-system. Such a hybrid symbolic/connectionist system combines information from all three sources to select the most plausible interpretation for ambiguous words.     

遗传算法辅助的动态符号执行测试方法

动态符号执行是一种有效的软件测试方法,但由于受到约束求解器求解能力的限制,在面对较为复杂的程序和路径条件时,动态符号执行的路径覆盖率还有待提升。针对上述问题,提出了一种遗传算法辅助的动态符号执行测试方法,并基于此方法实现了原型工具JDart-Ga。该方法结合遗传算法的优势,生成约束求解器无法求解的约束条件对应测试输入,从而提升动态符号执行的路径覆盖率。实验结果表明,在测试存在动态符号执行无法覆盖路径的3个实验对象时,所提出方法的路径覆盖率与JDart相比分别提升了16%至23%。     

A unified symbolic evaluation framework for parallelizing compilers

The quality of many optimizations and analyses of parallelizing compilers depends significantly on the ability to evaluate symbolic expressions and on the amount of information available about program variables at arbitrary program points. In this paper, we describe an effective and unified symbolic evaluation framework that statically determines the values of variables and symbolic expressions, assumptions about and constraints between variable values, and the condition under which control flow reaches a program statement. We introduce the program context, a novel representation for comprehensive and compact control and data flow analysis information. Program contexts are described as first order logic formulas, which allows us to use public domain software for standard symbolic manipulation. Computations are represented as algebraic expressions defined over a program's problem size. Our symbolic evaluation techniques comprise accurate modeling of assignment and input/output statements, branches, loops, recurrences, arrays, and procedures. All of our techniques target both linear, as well as nonlinear, expressions and constraints. Efficiency of symbolic evaluation is highly improved by aggressive simplification techniques. A variety of examples, including program verification, dependence analysis, array privatization, communication vectorization, and elimination of redundant communication, are used to illustrate the effectiveness of our approach. We present results from a preliminary implementation of our framework, which is used as part of a parallelizing compiler that demonstrates the potential performance gains achievable by employing symbolic evaluation to support program parallelization.     

基于混合输入的环境交互问题研究

针对软件安全测试中静态符号执行技术难以处理环境交互的问题, 提出了一种基于混合输入的符号执行方法。首先, 定义了程序执行的一致性模型, 系统化地分析了符号执行与实际执行的逼近问题; 接着, 提出了符号执行与具体执行的转换方法及维护一致性的启发式策略; 最后, 通过区分可求解约束和复杂约束条件, 提出了具体值和符号值混合代入法化简复杂约束的路径求解算法。实验结果表明该方法在处理环境交互问题上的可行性和有效性, 扩展了静态符号执行的能力。     

基于条件值的C/C++预处理测试算法

传统C/C++代码的预处理分析利用符号执行推断预处理中自由变量条件表达式的值,但是该算法的时间复杂度是指数型的.为降低时间复杂度,提出一种快速符号执行算法.源代码通过词法分析器得到顶处理变量和路径条件,为预处理变量建立节点,把路径条件转化为条件表达式,通过符号执行算法将两者整合为条件值c-value的形式,最终显示预处...     

Evaluating deadlock detection methods for concurrent software

Static analysis of concurrent programs has been hindered by the well-known state explosion problem. Although many different techniques have been proposed to combat this state explosion, there is little empirical data comparing the performance of the methods. This information is essential for assessing the practical value of a technique and for choosing the best method for a particular problem. In this paper, we carry out an evaluation of three techniques for combating the state explosion problem in deadlock detection: reachability searching with a partial-order state-space reduction, symbolic model checking and inequality-necessary conditions. We justify the method used for the comparison, and carefully analyze several sources of potential bias. The results of our evaluation provide valuable data on the kinds of programs to which each technique might best be applied. Furthermore, we believe that the methodological issues we discuss are of general significance in comparison of analysis techniques     

Applying static analysis for automated extraction of database interactions in web applications

Database interactions are among the most essential functional features in web applications. Therefore, for the testing and maintenance of a web application, it is important that the web engineer could identify all the database interactions in the web application. However, the highly dynamic nature of web applications makes it challenging to extract all the possible database interactions from source code.In this paper, we propose an automated approach to extract database interactions from source code by using symbolic execution and inference rules. Our approach automatically identifies all the possible database interaction points. After that, all the program paths, which pass through each interaction point, are also computed. Each of these paths is then symbolically executed following our proposed symbolic evaluation rules. We also develop inference rules to deduce the interaction types from the set of symbolic expressions derived during the symbolic execution. Experiments have been conducted to evaluate the performance and usefulness of the proposed approach. The results indicate that even with some limitations in handling function calls, pointers and polymorphism, our approach still gives an average precision of 79.2%, which is 45.4% more than that of the conservative approach.     

Static Analysis for State-Space Reductions Preserving Temporal Logics

In this paper we present two methods that use static analysis of parallel programs to create reduced models for them. Our algorithms examine the control-flow graph of a program (the syntax) and create a smaller transition system than would have been created otherwise. The smaller transition system is equivalent to the original transition system of the program with respect to temporal logic specifications.The two methods are orthogonal in their approach. The first, called path reduction, reduces the state-space by compressing computation paths. This method reduces the number of steps each computation takes. The second method, called dead variable reduction, reduces according to the variable domains. It identifies classes of equivalent states which differ only on variable values (and not the program counter) and uses a representative for each class. We also consider a refinement of the dead variable reduction, based on partially dead variables, which may result in a greater reduction.Our algorithms are based on syntactic manipulation of expressions, thus enabling us to handle programs with variables over finite as well as infinite domains. Both methods can easily be combined with either explicit state or symbolic methods (and with each other).We used the Murphi verifier to test the amount of reduction achieved by both methods. We let Murphi perform a DFS search and compared the sizes of the original and reduced transition systems, for several examples and according to both reductions. The results show that path reduction and the reduction based on partially dead variables give significant reductions, while the effect of fully dead variables is less impressive. We discuss the differences between the approaches, and the reasons for these results.     

基于聚类分析的搜索引擎自动性能评价

传统的搜索引擎性能评价方法需要人工标注标准答案集,需花费大量的人力物力,并且评价结果依赖于人工标注的准确性,效率较低。该文基于聚类分析的思路,提出了一种搜索引擎性能评价指标和自动进行搜索引擎性能评价的方法,此方法能自动计算信息类查询的覆盖范围,并根据其覆盖范围对检索结果进行聚类,通过类间距和类内距等指标实现检索性能的自动评价。实验结果表明,基于聚类指标的评价方法与人工标注的评价方法的评价结果是相一致的。     

一种基于程序功能标签切片的制导符号执行分析方法

提出了一种基于程序功能标签切片的制导符号执行分析方法OPT-SSE.该方法从程序功能文档提取功能标签,利用程序控制流分析,建立各功能标签和程序基本块的映射关系,并根据功能标签在程序执行中的顺序关系生成功能标签执行流.针对给定的代码目标点,提取与之相关的功能执行流切片,根据预定义好的功能标签流制导规则进行符号执行分析,在路径分析过程中,及时裁剪无关的功能分支路径以提升制导效率.通过对不同的功能标签流进行分离制导符号执行分析,可避免一直执行某复杂循环体的情形,从而提高对目标程序的整体分支覆盖率和指令覆盖率.实验结果表明,通过对binutils、gzip、coreutils等10个不同软件中的20个应用工具上的分析,OPT-SSE与KLEE提供的主流搜索策略相比,代码目标制导速度平均提升到4.238倍,代码目标制导成功率平均提升了31%,程序指令覆盖率平均提升了8.95%,程序分支覆盖率平均提升了8.28%.     

Solving geometric constraints in a parallel network

The paper describes a network implementation of the SUP-INF method for solving sets of inequalities, giving several advantages over previous implementations. The cost of symbolic manipulation is transferred to compile time allowing an increase in speed at run time due to parallel evaluation. Further, allowing iteration in the network improves the competence of the method when working with nonlinear expressions. The network is used to implement a geometric reasoner for a computer vision program and this is shown to meet the general requirements for such a system.