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

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

Response time analysis of EQL real-time rule-based systems

Real-time rule-based expert systems are embedded decision systems that must respond to changes in the environments within stringent timing constraints. Given a program p, the response time analysis problem is to determine the response time of p. This problem consists of: determining whether or not the execution of p always terminates in bounded time; and computing the maximal execution time of p. The Equational Logic (EQL) language is a simple language designed for real-time applications. It has been proved by A.K. Mok (1989) that the response time analysis problem is undecidable if the program variables have infinite domains, and is PSPACE-hard in the case where all of the variables have finite domains. However, we have observed that the use of a simple syntactic and semantic check on programs coupled with other techniques such as state space graph checks can dramatically reduce the time needed in the analysis. There are sets of syntactic and semantic constraint assertions such that if the set S of rules satisfies any of them, then the execution of S always terminates in bounded time. Each of these sets of syntactic and semantic constraint assertions is called a Special Form. The focus of the paper is on proving the existence of two Special Forms and determining tight response time upper bounds of EQL rule-based programs. For each known Special Form, an algorithm used to calculate the maximal response time of programs satisfying this Special Form is presented. Additionally, to enhance the applicability of the proposed algorithms, we show how the General Analysis Algorithm can be used with these algorithms     

基于LCC的测试程序控制流路径子集生成算法

针对路径覆盖测试技术中如何计算被测试程序的有效控制流路径子集的关键性问题,提出一种利用LCC编译器的前端结果来生成基于一次循环策略的测试程序控制流路径子集的算法。该算法通过引入邻接矩阵并借助自定义的堆栈数据结构来完成控制流路径子集的生成。通过实验程序对算法进行检验,结果表明,该方法能高效准确地计算出待测源程序片的控制流路径子集。     

The impact of incorrectly speculated memory operations in a multithreaded architecture

The speculated execution of threads in a multithreaded architecture, plus the branch prediction used in each thread execution unit, allows many instructions to be executed speculatively, that is, before it is known whether they actually needed by the program. In this study, we examine how the load instructions executed on what turn out to be incorrectly executed program paths impact the memory system performance. We find that incorrect speculation (wrong execution) on the instruction and thread-level provides an indirect prefetching effect for the later correct execution paths and threads. By continuing to execute the mispredicted load instructions even after the instruction or thread-level control speculation is known to be incorrect, the cache misses observed on the correctly executed paths can be reduced by 16 to 73 percent, with an average reduction of 45 percent. However, we also find that these extra loads can increase the amount of memory traffic and can pollute the cache. We introduce the small, fully associative wrong execution cache (WEC) to eliminate the potential pollution that can be caused by the execution of the mispredicted load instructions. Our simulation results show that the WEC can improve the performance of a concurrent multithreaded architecture up to 18.5 percent on the benchmark programs tested, with an average improvement of 9.7 percent, due to the reductions in the number of cache misses.     

一种快速程序最坏执行时间分析方法研究

给出一种带有路径冲突检测的程序最坏情况执行时间估计方法,这种方法首先检测程序中存在的分支约束,然后将程序中存在的分支约束信息转化为程序流程控制图（CFG图）中结点之间的语义冲突,并按照结点对的形式保存在相应的冲突数组里,在接下来的WCET计算阶段通过边搜索程序执行路径边检测冲突数组里保存的已有的冲突关系以便在搜索路径的同时排除非可行执行路径,最终在可行执行路径集中选择具有最大执行时间的执行路径。与以往的方法相比,在保持估计精度的前提下,本文的方法避免了穷举所有执行路径带来的复杂度,提高了搜索的效率。实验结果表明本文方法对于语句间语义依赖关系比较强的实时程序能够快速且有效地给出估计结果。     

Formal timing analysis for distributed real-time programs

A static analysis method for verifying timing properties of real-time distributed programs is presented. The goal is to calculate the worst-case response time of concurrent tasks which run mainly independently but share, and may have to wait for, logical or physical devices. For such tasks, the determination of the worst-case waiting time is a crucial problem because of the unpredictable order of synchronization events. We investigate the class of distributed Client-Server programs in which independent, time-critical tasks (clients) are synchronized only through additional server tasks, playing the role of monitors or resource managers. This model follows well-known real-time design guidelines for distributed ADA programs proposed to enhance schedulability and synchronization analysis. Our formal analysis approach is flow graph oriented. It leads to generating reduced program paths each of which represents a sequence of ordered local and global operations, thus transforming and reducing the original problem of computing the worst-case waiting time of a concurrent task into a graph-theoretic problem of calculating the maximal blocking time for one of its corresponding program paths. While local operations are completely independent global operations require mutually exclusive access to shared resources. We prove that computing the worst-case blocking time for a program path is NP-complete. Even for a reduced problem solution—which would yield a good upper bound for the worst-case blocking time—there was a conjecture maintained over many years that this problem was NP-complete. A major result of this paper is to show that this is wrong. Instead, we construct a polynomial solution algorithm, and we prove its correctness. The effectiveness and complexity of our method are discussed, with particular emphasis on distributed real-time debugging.     

RTL和门级结合的处理器时延测试产生方法

针对处理器的数据通路中的通路时延故障,提出一种基于指令集的处理器时延测试产生方法．对于每条指令提取出状态矩阵,并基于状态矩阵将通路分为功能不可测（FUPs）和潜在功能可测的（PFTPs）．对PFTPs记录潜在测试指令（序列）组合,提取控制和数据约束,在门级进行有约束的非强健时延测试产生．最后的测试指令由控制指令（序列）＋潜在测试指令（序列）＋观测指令（序列）构成．     

SymPas: Symbolic Program Slicing

Program slicing is a technique for simplifying programs by focusing on selected aspects of their behavior.Current mainstream static slicing methods operate on dependence graph PDG (program dependence graph) or SDG (system dependence graph),but these friendly graph representations may be a bit expensive for some users.In this paper we attempt to study a light-weight approach of static program slicing,called Symbolic Program Slicing (SymPas),which works as a dataflow analysis on LLVM (low-level virtual machine).In our SymPas approach,slices are stored in symbolic forms,not in procedures being re-analyzed (cf.procedure summaries).Instead of re-analyzing a procedure multiple times to find its slices for each callling context,we calculate a single symbolic slice which can be instantiated at call sites avoiding re-analysis;SymPas is implemented with LLVM to perform slicing on LLVM intermediate representation (IR).For comparison,we systematically adapt IFDS (interprocedural finite distributive subset) analysis and the SDG-based slicing method (SDG-IFDS) to statically slice IR programs.Evaluated on open-source and benchmark programs,our backward SymPas shows a factor-of-6 reduction in time cost and a factor-of-4 reduction in space cost,compared with backward SDG-IFDS,thus being more efficient.In addition,the result shows that after studying slices from 66 programs,ranging up to 336800 IR instructions in size,SymPas is highly size-scalable.     

求不相交QoS路由的一种整数线性规划方法

提出求解不相交QoS路由问题的一种整数线性规划方法.首先,利用一个0-1变量集合来表示不相交路由和路由的QoS需求;然后,通过拉格朗日乘子将集合中的复杂约束引入所导出的整数线性规划问题的目标函数中.因为约束系数矩阵是全幺模矩阵,所以这类整数线性规划问题能用单纯形法容易地求解,从而可在求解线性规划问题的迭代过程中求出不相交QoS路由.数值实验结果表明了所提出方法的有效性.     

Using symbolic execution and data flow criteria to aid test data selection

The utilization is described of a data flow path selection criterion in a symbolic execution system. The system automatically generates a subset of program paths according to a certain control flow criterion. This subset is called the ZOT-subset, since it requires paths that traverse loops zero, one and two times. Experience indicates that traversing this subset of program paths is enough to cover most control flow and data flow components of the program. The problem with the ZOT-subset is that it might contain, for large programs, a large number of paths. The number of paths in this subset can be reduced by concentrating on executable paths that cover vital components of programs such as data flow components. This object is achieved by employing a data flow path selection criterion in the system. The system symbolically executes the paths of the ZOT-subset, and creates a system of branch conditions for each one. The user determines infeasible paths by checking the consistency of each system of conditions. The system selects feasible paths from the ZOT-subset that cover the data flow criterion. Solving the systems of conditions of the selected paths provides the user with test data to fulfil the given data flow criterion.     

An intelligent subtitle detection model for locating television commercials.

A strategy for locating television (TV) commercials in TV programs is proposed. Based on the observation that most TV commercials do not have subtitles, the first stage exploits six subtitle constraints and an adaptive neurofuzzy inference system model to determine whether a frame contains a subtitle or not. The second stage involves locating the mark-in/mark-out points using a genetic algorithm. An interactive user interface allows users to efficiently identify and fine-tune the exact boundaries separating the commercials from the program content. Furthermore, erroneous boundaries are manually corrected. Experimental results show that the precision rate and recall rates exceed 90%.     

Disjunctive LP+integrity constraints= stable model semantics

We show that stable models of logic programs may be viewed as minimal models of programs that satisfy certain additional constraints. To do so, we transform the normal programs into disjunctive logic programs and sets of integrity constraints. We show that the stable models of the normal program coincide with the minimal models of the disjunctive program thatsatisfy the integrity constraints. As a consequence, the stable model semantics can be characterized using theextended generalized closed world assumption for disjunctive logic programs. Using this result, we develop a bottomup algorithm for function-free logic programs to find all stable models of a normal program by computing the perfect models of a disjunctive stratified logic program and checking them for consistency with the integrity constraints. The integrity constraints provide a rationale as to why some normal logic programs have no stable models.     

Generating test data for both paths coverage and faults detection using genetic algorithms: multi-path case

Generating test data that can expose the faults of the program is an important issue in software testing. Although previous methods of covering path can generate test data to traverse target path, the test data generated by these methods are difficult in detecting some low-probabilistic faults that lie on the covered paths. We present a method of generating test data for covering multiple paths to detect faults in this study. First, we transform the problem of covering multiple paths and detecting faults into a multi-objective optimization problem with constraint, and construct a mathematical model for it. Then, we give a strategy of solving the model based on a weighted genetic algorithm. Finally, we apply our method to several real-world programs, and compare it with several methods. The experimental results confirm that the proposed method can more efficiently generate test data that not only traverse the target paths but also detect faults lying in them than other methods.     

Automated constraint-based addition of nonmasking and stabilizing fault-tolerance

We focus on the constraint-based automated addition of nonmasking and stabilizing fault-tolerance to hierarchical programs. We specify legitimate states of the program in terms of constraints that should be satisfied in those states. To deal with faults that may violate these constraints, we add recovery actions while ensuring interference freedom among the recovery actions added for satisfying different constraints. Since the constraint-based manual design of fault-tolerance is well known, we expect our approach to have a significant benefit in automating the addition of fault-tolerance. We illustrate our algorithm with four case studies: stabilizing mutual exclusion, stabilizing diffusing computation, a data dissemination problem in sensor networks, and tree maintenance. With experimental results, we show that the complexity of our algorithm is reasonable and that it can be reduced using the structure of the hierarchical systems.We also reduced the time complexity of the synthesis using parallelism. We consider two approaches to speedup the synthesis algorithm: first, the use of the multiple constraints that have to be satisfied during synthesis; second, the use of the distributed nature of the programs being synthesized. We show that our approaches provide significant reduction in the synthesis time.To our knowledge, this is the first instance where automated synthesis has been successfully used in synthesizing programs that are correct under fairness assumptions. Moreover, in three of the case studies considered in this paper, the structure of the recovery paths is too complex to permit existing heuristic-based approaches for adding recovery.     

Finding a minimal set of base paths of a program

An approach to finding a minimal set of base paths of a program is described. The program digraph is reduced to a weighted loopfree graph (WLFG) in which a node represents a subgraph of the program digraph that contains at most one outermost loop of the program. An algorithm for finding a maximal cutset of the WLFG is given such that (1) a maximal cutset does not contain two arcs that lie on a single path of the WLFG, and (2) its capacity is equal to the cardinality of a minimal set of base paths of the program. The algorithm repeatedly finds an eliminable arc and removes it from the WLFG until either the WLFG contains three nodes or no more eliminable arc can be found. An illustration is given for finding a maximal cutset and subsequently a minimal set of base paths.     

多路径测试数据自动生成方法及应用

以程序结构测试自动生成为研究背景,提出了一种重叠路径结构用以描述程序路径,并以此为基础设计了一种多路径测试数据生成适应值算法,实现了一次搜索完成多条路径的测试数据生成。算法通过目标路径间共享遗传算法产生的中间个体减少单一路径搜索始于随机产生的无序个体的初期迭代,从而加快搜索收敛的速度。应用于常用的基准程序和取自实际项目的程序,该算法与典型的分支谓词距离算法相比平均消耗时间缩短了70.6%。     

Worst Case Execution Time Analysis for a Processor with Branch Prediction

The fundamental requirement for hard real-time systems is that task deadlines be never missed. As a consequence, knowing tasks worst case execution times (WCET) is crucial for such systems. Taking into account modern architectural features makes it possible to determine tighter WCET bounds than with program analysis that ignores such features. While effects of caches and pipelines on WCET analysis have been extensively studied, to our knowledge the effect of the branch prediction on WCET evaluation has not been studied yet. This paper describes a method for statically bounding the number of timing penalties due to erroneous branch predictions. The proposed method is based on static program analysis and branch target buffer modelling. It consists in collecting information on branch target buffer evolution by considering all possible execution paths of a program. Collected information can then be used to classify control transfer instructions so that their worst case branching cost can be estimated and incorporated into the program WCET. A method is also given to tightly predict the WCET of loops whose number of iterations depend on counter variables of outer loops. Experimental results show that the timing penalty due to wrong branch predictions estimated by the proposed technique is close to the real one, which demonstrates the practical applicability of our method.     

面向高层次综合的自定义指令自动识别方法

针对在高层次综合（HLS）过程中性能提升、功耗降低困难等问题,提出了一种面向高层次综合的自定义指令自动识别方法。在高层次综合过程之前实现对自定义指令的枚举和选择,从而为高层次综合提供通用的自定义指令识别方法。首先,将高层次源代码转换为控制数据流图（CDFG）,实现了对源代码的预处理;其次,基于控制数据流图内的数据流图（DFG）,采用子图枚举算法以自底而上的方式枚举出所有连通凸子图,有效提高了用户可灵活修改约束条件的能力;然后,分别从面积、性能和代码量三个角度考虑,利用子图选择算法选择部分最佳子图作为最终的自定义指令;最后,用所选的自定义指令重新生成新代码作为高层次综合工具的输入。与传统高层次综合相比,采用基于出现频率的模式选择可平均减少19.1%的面积,采用基于关键路径的子图选择可平均减少22.3%的时延。此外,与TD算法相比,所提算法的枚举效率平均提升70.8%。实验结果表明,自定义指令自动识别方法使高层次综合在电路设计中能够显著地提升性能,减少面积和代码量。     

基于实时自动机的连续时段演算的验证

时段演算是描述和推导嵌入式实时系统和混成系统性质的一种区间时态逻辑.扩展线性时段不变式是时段演算的重要子集.针对实时自动机,提出一种连续时间语义下扩展线性时段不变式的有界模型检验方法.该方法将扩展线性时段不变式的有界模型检验问题转化为量词线性算术公式的正确性问题,从而可以采用量词消去技术进行求解.首先,运用符号化的思想,在实时自动机上利用深度优先搜索找到所有满足观测时长约束的符号化路径片段;然后,将每条符号化路径片段转化为一个量词线性算术公式;最后,利用量词消去工具求解.与已有工作相比,基于实时自动机设计了验证算法.另外,降低了验证复杂度,并且加速了验证过程的实际速度.     

基于关键点路径的快速测试用例自动生成方法

测试数据的自动生成,是提高软件测试效率的重要手段.从软件测试工程实践的角度提出快速生成测试数据的完整模型,更有利于提高测试数据生成效率.为此:(1)提出关键点路径表示法,以得出待测程序的理论路径数,并快速确定已覆盖路径的邻近路径;(2)用随机生成的数据运行简化后的插装程序,得到部分测试数据;(3)将理论路径分成易覆盖路径、难覆盖路径和不可行路径;(4)根据已覆盖路径及其测试数据提供的信息,使用遗传算法生成难覆盖路径的测试数据.仿真实验结果表明了所提方法的有效性.