路径模糊:一种有效抵抗符号执行的二进制混淆技术

符号执行能够对软件的路径分支信息进行收集和形式化表示,然后通过路径可达性推理得到软件行为同用户输入、网络输入等外部执行环境间的依赖关系.这些依赖关系已被广泛地应用到漏洞发掘、代码复用、协议分析等领域.该逆向分析技术也可被黑客用于软件破解、篡改和盗版等,对软件知识产权的保护带来了新的威胁.提出了一种新的基于路径模糊的软件保护方法以抵抗基于符号执行的逆向分析:利用条件异常代码替换条件跳转指令来隐藏程序的路径分支信息,使用不透明谓词技术引入伪造的路径分支来弥补程序在统计属性上的差异,并对路径模糊技术的强度、弹性和开销进行了分析.实验结果表明路径模糊技术能保护各类路径分支条件,有效减少路径分支信息的泄露,抵抗基于符号执行的逆向分析.     

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

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

基于符号执行和数据挖掘的路径可达性检测研究

要把静态分析技术真正应用于软件工程的实践中,程序中的不可到达路径依旧是一个巨大的障碍。在缺乏不可到达路径信息的情况下,数据流信息只能以一种非常保守的方式被利用,因而使进一步的工作,例如测试数据生成或者软件缺陷检测变得更加困难和低效。本文提出一种融合符号执行以及数据挖掘的混合型方法来检测程序中的不可到达路径,充分利用符号执行的精确性以及数据挖掘的高效性,这种方法被证明是有效并且实用的。     

面向动态加载的Android恶意行为动静态检测方法

动态加载是Android提出的一种新的执行体分类的运行时加载机制,能够有效提高动态行为配置能力。但由于动态加载部分的程序不包含在APK中,因此静态分析技术无法对动态加载点的恶意行为形成有效检测,而动态分析技术则难以覆盖到所有执行路径,也无法形成充分的检测。针对该问题,提出一种动静态结合的检测方法。先对宿主APK进行静态分析提取Call-Graph,以获得动态加载点的执行路径,再通过路径制导的动态执行获取动态加载的程序,从而形成完整的分析。通过实例研究验证了该方法的有效性。     

二进制代码安全分析综述

近几十年来,计算机硬件性能和软件规模技术已不同以往,其承载了人类社会生活生产的方方面面.计算机技术的飞速发展,也带来了人们对程序安全问题的关注.由于市面上存在着较多的遗留软件,这些软件无人维护且缺乏源代码支持,其安全性令人担忧,而二进制分析技术被用来解决该类软件问题.二进制分析技术根据其检测方式不同可分为:基于静态的二进制代码分析技术、基于动态的二进制代码分析技术和动静态混合的二进制代码分析技术.本文调研了近年来的二进制代码安全分析领域上相关研究,分别详细阐述了这3类技术中的主要方法,并对其关键技术进行详细介绍.     

基于程序切片的测试用例生成系统研究与实现

介绍了一种基于程序行为切片的测试用例生成系统的实现方案,系统在不扫描全部程序路径的情况下,生成可以覆盖全部程序行为的测试用例集。系统分为静态分析、动态符号执行以及测试用例生成3个模块。在静态分析模块中根据输入的程序代码分析程序的控制流和信息流,提取程序的控制依赖和数据依赖,并计算程序的潜在依赖;动态符号执行模块求解约束条件、生成测试用例和分析代码执行过程;测试用例生成模块根据执行路径和依赖关系计算被路径覆盖的程序行为切片和未被覆盖的程序行为切片,然后根据未被覆盖的程序行为切片,引导符号执行生成能覆盖新的程序行为切片的测试用例。实验证明,本系统生成的测试用例集可以保证覆盖所有的程序行为,同时能显著减少生成的测试用例数量。     

一种动静结合的代码反汇编框架

反汇编技术是二进制代码分析的基础,传统的静态反汇编方法存在着数据代码混编和间接跳转指令等带来的反汇编困难.为此,本文提出了一种动静结合的代码反汇编框架DTBC.在DTBC中,静态反汇编引擎根据传统反汇编算法实现代码的静态反汇编,通过代码分析技术标记程序中的敏感指令;符号执行引擎利用混合符号执行技术和约束求解器生成可达敏感指令的程序输入;动态仿真引擎模拟不同输入条件下的程序执行过程,通过监控代码的执行路径达到反汇编求精的目的.实验模拟的结果表明,DTBC能够有效提高代码反汇编的准确性和覆盖率.     

《软件分析》专辑前言

软件分析(Software Analysis)是以软件为对象通过静态或动态的方法进行人工或自动分析,以验证、确认、监控或发现软件性质(或者规约、约束)的过程或活动.软件分析是计算机科学与技术领域的经典和核心内容,源于人们试图认识程序行为和性质的努力.早期的软件分析主要还是程序分析,是高级语言编译过程的第一步工作,长期以来,在编译理论和技术的发展中得到了较深入的研究.     

精准执行可达性分析:理论与应用

精准执行可达性分析探究计算机程序状态之间的可达性关系,通过分析软件的文档、源代码或二进制程序并进行必要测试验证,以求出在既定限制下从初始状态到特定代码位置的目标状态的准确触发输入和执行路径.精准执行可达性分析在定向测试、静态分析结果核验、错误复现和漏洞POC构造等领域均有广泛应用.本文对近年来国内外学者在该研究领域取得的相关研究成果进行了系统的分析、提炼和总结.首先,指出了精准执行可达性分析对应的约束求解问题,以双向符号分析和程序归纳为主线介绍了其主要研究方法,讨论了相关技术难点.其次,对目前已经存在的精准执行可达性应用进行了分类分析.进而,指出精准执行可达性分析应用中程序分析、归纳和约束求解等方面存在的挑战.最后,对可能的解决办法以及未来发展方向进行了展望.     

支持形状分析的符号执行引擎的设计与实现

目前提高软件可靠性的方法有3种:动态测试、静态分析和程序验证。动态测试的结果依赖于测试集的设计,误报率低,漏报率高,分析结果不稳定。程序验证可以对程序的各种性质进行完备的验证。但目前程序验证通常都需要手动证明,分析成本最高。而程序静态分析可以更早、更全面、较高效和低成本地检测到程序中的缺陷。其中符号执行技术是一种比较有应用前景的静态分析技术,可以很好地控制 精确度。针对符号执行可伸缩性差和容易产生路径爆炸的问题,在符号执行过程中利用形状分析技术实现自动推导循环不变式和构建函数行为规范,实现了一个较为实用的C程序分析工具。     

基于格的数据流分析框架研究

数据流分析是编译系统中的一个重要的内容,也是程序静态分析的一个方面。论文按程序执行路径对数据流分析问题进行分类,这有利于建立数据流分析的统一的描述模型,并以此为基础论述了数据流分析框架与数据流分析的内在联系,这为并发程序的数据流分析奠定了良好的基础。     

软件执行路径的高层次可视化表示

软件的主要特征信息，如功能性信息，常常隐藏在它的结构里面，仅仅分析软件系统的结构不足以揭示它们，只能在对软件的各条执行路径的确认过程中获得，对软件执地路长的分析是软件理解过程是一个必可少的辅助手段，程序执行路径（ＥｘｅｃｕｔｉｏｎＰａｈｔ，ＥＰ）概念和它在程序测试，排障（纠错）和理解等方面的用途是大家所知晓的并已有记录，本文给出了一种系统性的方法，可根据从程序设计语言的说明规程产生的结构模型，自动     

全路径剖析方法

路径剖析是动态分析的一项重要技术,通过获取和分析程序中各条路径的执行次数,在编译优化、软件调试和测试等诸多方面发挥重要作用.针对现有技术剖析能力不足的情况(即只能或者剖析非循环路径,或者首先界定循环体执行次数的上限、然后对于执行循环体不多于该次数的路径进行剖析),对使用单个探针变量剖析过程内路径的方法进行了改进,提出了全路径剖析PAP方法,利用探针插装和回溯过程获取路径的执行次数,可以剖析过程内包含任意有限长度的路径;进一步地,针对PAP方法所需探针数目多于EPP方法的问题,通过对控制流图中包含的可规约无环子图实施EPP方法,可以减少PAP方法所需探针的数目.另外,作为PAP方法的一个典型应用,还讨论了如何通过在方法调用图中添加返回边,再利用PAP方法获取方法层次的执行序列的基本思想,满足了某些方法级动态影响分析技术的需要.实验和实例分析表明,PAP在处理循环路径剖析的问题上是有效的,并有很好的效率.     

Profiling selected paths with loops

Path profiling records the frequency of each path in an executed program.To accomplish profiling,probes are instrumented in the program and executed as the program runs.So,the number of probes has a significant impact on the efficiency of a profiling technique.By profiling only the interesting paths,existing techniques try to improve the profiling efficiency by reducing the number of probes and optimize path encodings for efficient storage.However,they lack accuracy,waste time on running uninteresting paths,and can mainly deal with acyclic paths.In this article,a novel technique called Profiling Selected Paths(PSP)is introduced to profile selected paths,which enables custom selection for both acyclic and cyclic paths and increases the execution efficiency by early termination on uninteresting paths.Theoretical analysis and experimental evaluation indicate that PSP performs better than existing techniques.     

高精度的大规模程序数据竞争检测方法

随着技术的不断发展,软件系统的非确定性（Uncertainty）不断增强,数据竞争是并发系统这一类典型的非确定性软件系统中常见的缺陷.尽管数据竞争静态检测近年来取得了巨大进展,但其面临的重要问题仍然存在.先前的静态技术要么以分析精度为代价达到高扩展性,要么由于高精度分析而导致可扩展性问题.本文提出一种解决上述矛盾的分段分析方法——GUARD.它首先基于程序值流进行轻量级上下文敏感的数据访问分析,以识别出候选的数据竞争子路径而非完整的程序路径.接下来,进行可能并行执行（May-Happen-in-Parallel,即MHP）分析来确定程序中的两个数据访问操作是否可能会同时执行.MHP分析基于线程流图（TFG）将线程信息进行编码以便于高效地查询各个子路径之间的并发关系.最后,对于每条存在MHP数据访问的子路径,进行重量级路径敏感分析以确定数据竞争路径的可行性.针对12个开源项目的实验评估显示GUARD能够在1870秒内完成对130万行代码的工业规模项目的检测,且平均误报率为16.0%.此外GUARD的分析速度更快,比现有的前沿技术平均快了6.08倍并且显著降低误报率.除此之外,GUARD在其中还发现了12个数据竞争漏洞.我们将它们全部报告给了开发者,其中8个已得到了确认.     

A Systematic Review of Search Strategies in Dynamic Symbolic Execution

One of the major concerns of dynamic symbolic execution (DSE) based automated test case generation is its huge search space which restricts its usage for industrial-size program testing. In fact, DSE performs test case generation by exploring paths of the program, and the number of program paths is exponential in the number of branch conditions encountered during execution. Thus, by increasing the number of branches, the search space will be extremely large and without applying an effective and efficient technique to explore the search space, DSE would fail to achieve the predesignated goals in the given budget. To this end, different search strategies have been proposed to prioritize program paths and to select the most promising ones with respect to the testing goal. In this paper, we conduct a comprehensive systematic review of search strategies in DSE. We collect different techniques and methods concerning the topic, classify and summarize them, highlight their advantages and drawbacks, and provide a complete comparison of the methods in each category. The classification is carried out according to the type of search and also the information source exploited by the strategies to direct DSE. We also analyze the evaluation methodologies of experiments reported on this subject, give a general overview of them, perform a set of experiments and provide a set of guidelines for conducting future experiments in this area of research.     

USING DISTRIBUTION-FREE LEARNING THEORY TO ANALYZE SOLUTION-PATH CACHING MECHANISMS

Much research in machine learning has been focused on the problem of symbol-level learning (SLL), or learning to improve the performance of a program given examples of its behavior on typical inputs. A common approach to symbol-level learning is to use some sort of mechanism for saving and later reusing the solution paths used to solve previous search problems. Examples of such mechanisms are macro-operator learning, explanation-based learning, and chunking. However, experimental evidence that these mechanisms actually improve performance is inconclusive. This paper presents a formal framework for analysis of symbol-level learning programs, and then uses this framework to investigate a series of solution-path caching mechanisms which provably improve performance. The analysis of these mechanisms is illuminating in many respects; in particular, in order to obtain positive results, it is necessary to use a novel representation for a set of solution paths, and also to apply certain unusual optimizations to a set of solution paths. Several of the predictions made by the model have been confirmed by recently published experiments.     

Automatic generation of path covers based on the control flowanalysis of computer programs

Branch testing a program involves generating a set of paths that will cover every arc in the program flowgraph, called a path cover, and finding a set of program inputs that will execute every path in the path cover. This paper presents a generalized algorithm that finds a path cover for a given program flowgraph. The analysis is conducted on a reduced flowgraph, called a ddgraph, and uses graph theoretic principles differently than previous approaches. In particular, the relations of dominance and implication which form two trees of the arcs of the ddgraph are exploited. These relations make it possible to identify a subset of ddgraph arcs, called unconstrained arcs, having the property that a set of paths exercising all the unconstrained arcs also cover all the arcs in the ddgraph. In fact, the algorithm has been designed to cover all the unconstrained arcs of a given ddgraph: the paths are derived one at a time, each path covering at least one as yet uncovered unconstrained arc. The greatest merits of the algorithm are its simplicity and its flexibility. It consists in just visiting recursively in combination the dominator and the implied trees, and is flexible in the sense that it can derive a path cover to satisfy different requirements, according to the strategy adopted for the selection of the unconstrained arc to be covered at each recursive iteration. This feature of the algorithm can be employed to address the problem of infeasible paths, by adopting the most suitable selection strategy for the problem at hand. Embedding of the algorithm into a software analysis and testing tool is recommended     

Time and cost risk analysis

The Project Management Group at UMIST has been involved with the development of project management software since the early 1970s, and has developed a construction project risk analysis program named CASPAR. Recently, the program has been further developed to include time-only probability analysis which reports the most frequently observed critical paths, the probability of achieving milestone dates, and the most likely completion data for the project. The original CASPAR program has also been extended to illustrate the effect of risks on both the cost and duration of a project. The results are presented in terms of ‘probability contours’ which quantify the probability of achieving values of both the cost and duration.     

Path testing of computer programs with loops using a tool for simple loop patterns

The purpose of this paper is to present a method for testing computer programs with iteration loops. Given such programs, we have shown that for classes of program paths, identified as sequences of simple loop paths, there is a characterizing function called a simple loop pattern. The key idea of simple loop patterns is that these special functions form a base set which can represent any path computation in the given program. A software tool called SILOP has been developed to automatically generate these simple loop patterns, and each corresponding sequence of simple loop paths can be considered as a test case. The tester uses each test case, and with knowledge of the application program, can generate corresponding test data. This paper also presents a method for selecting the specific paths and test data to determine the simple loop pattern reliably. The tester can use this selection method to predict the number of tests required. In order to apply this selection method, the given program must be a linear computer program. The SILOP tool and this test selection method have been applied to commercial software; in this paper, this computational experience is reported and several examples are given to demonstrate the approach.