C/C++程序静态内存泄漏警报自动确认方法

内存泄漏是C/C++程序的一种常见的、难以发现的缺陷,一直困扰着软件开发者,尤其是针对长时间运行的程序或者系统软件,内存泄漏的后果十分严重.针对内存泄漏的检测,目前主要有静态分析和动态测试两种方法.动态测试实际运行程序,具有较大开销,同时依赖测试用例的质量;静态分析技术及自动化工具已经被学术界和工业界广泛运用于内存泄漏缺陷检测中,然而由于静态分析采取了保守的策略,其结果往往包含数量巨大的误报,需要通过进一步人工确认来甄别误报,但人工确认静态分析的结果耗时且容易出错,严重限制了静态分析技术的实用性.本文提出了一种基于混合执行测试的静态内存泄漏警报的自动化确认方法.首先,针对静态分析报告的目标程序中内存泄漏的静态警报,对目标程序进行控制流分析,并计算警报的可达性,形成制导信息;其次,基于警报制导信息对目标程序进行混合执行测试;最后,在混合执行测试过程中,监控追踪内存对象的状态,判定内存泄漏是否发生,对静态警报进行动态确认并分类.实验结果表明该方法可以对静态内存泄漏警报进行有效的分类,显著降低了人工确认的工作量.实验详情参见：http://ssthappy.github.io/memleak/.     

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

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

一种C程序内存访问缺陷自动化检测方法研究

符号执行是目前较为行之有效的软件缺陷自动化检测方法,计算代价昂贵与程序执行路径爆炸是两个影响其性能的关键问题.提出了一种针对C语言程序内存访问缺陷的符号执行检测方法,该方法可通过自动化构造的测试用例发现程序内部的内存访问缺陷,如缓冲区溢出、跨界访问和指针异常等.使用符号跟踪缓冲区长度的方法,一方面减少了符号变量的数量,另一方面由此精确抽象C语言库中字符串操作函数的行为,解决了符号执行过程间函数调用的步进问题;使用动态切片的方法,裁减路径探索过程中的冗余路径,从而解决在程序内部路径搜索时发生的路径爆炸问题.实验表明,提供的检测方法不但可行,而且验证代价较小,具有较强的实用性.     

基于符号执行的缓冲区溢出漏洞自动化利用

软件规模与数量的快速增长给软件安全研究带来了严峻的挑战,以人工方式分析漏洞已难以完成漏洞危害性的评估。分析缓冲区溢出漏洞的形成原理,提出一种缓冲区溢出漏洞自动化利用方法。该方法采用符号执行检测漏洞,为缓解符号执行中状态爆炸问题,使用危险函数切片减少状态数量。对于检测到的漏洞,通过构建约束表达式和约束求解自动生成exploit。针对进程中不存在空间足够的可控内存块的情况,以shellcode分段存放的方式利用漏洞。实验结果表明,该方法可有效缓解符号执行路径爆炸问题,自动检测漏洞并生成适用性较好的exploit。     

静态缺陷检测中的误报消除技术研究

误报率是衡量静态缺陷检测工具的重要指标.在对比分析了各种误报消除技术的基础上,提出了一种前向数据流分析结合逆向约束搜索技术的误报消除方法:前向数据流分析的保守数据流解可以用于缺陷状态迭代,并得到初始的缺陷检测结果;根据缺陷发生处的数据流特征,逆向搜索可能导致缺陷发生的约束条件,该约束条件可以作为通用约束求解器的输入判断缺陷的可满足性,从而对初始的缺陷检测结果进行精化.同时,在数据流分析过程中引入符号执行技术,不仅提高了数据流分析的精度,且便于约束表示及转化,提高了约束搜索的效率.对SPECCPU2000中11个工程的对比实验表明,前向数据流分析与逆向约束搜索相结合的误报消除方法在增加了有限开销的同时有效地消除了部分误报,且与同类工具相比具有更好的可扩展性.     

一种需求驱动的缓冲区溢出检测算法

本文提出一种流敏感的静态检测算法。通过需求驱动的控制流分析和数据流分析,建立内存访问语句和函数调用语句发生溢出的线性约束,从而将缓冲区溢出的检测问题转换为线性约束求解问题。我们实现了该算法的原型,实验表明,该原型可以准确而高效地发现实际程序中的缓冲区溢出漏洞。     

C程序内存泄漏智能化检测方法

内存泄漏在采用显式内存管理机制的C语言中是一种常见的代码缺陷,内存泄漏的检测方法目前主要是静态分析与动态检测.动态检测开销大,且高度依赖测试用例;静态分析目前被学术界和工业界广泛应用,但是存在大量误报,需要人工对检测结果进行确认.内存泄漏静态分析的误报通常是由于对指针、分支语句和全局变量分析的不准确性导致的.提出了一种内存泄漏的智能化检测方法,通过使用机器学习算法学习程序特征与内存泄漏之间的相关性,构建机器学习分类器,并应用机器学习分类器进一步提高内存泄漏静态分析的准确性.首先构建机器学习分类器,然后通过静态分析方法构建从内存分配点开始的Sparse Value Flow Graph（SVFG）,并从中提取内存泄漏相关特征,再使用规则和机器学习分类器进行内存泄漏的检测.实验结果显示,该方法在分析指针、分支语句和全局变量时是有效的,能够提高内存泄漏检测的准确性,降低内存泄漏检测结果的误报.最后,对未来研究的可行性以及面临的挑战进行了展望.     

基于GCC的符号执行工具

静态分析和符号执行是发现源代码缺陷和提高源代码质量的两种有效方式。然而,这两种技术都面临各自的问题,静态分析误报率较高和符号执行一直面临着路径爆炸难题。为了减少静态分析和符号执行的这些限制,本文构建了一个称为ABARZER-SE的工具,它是第一个基于GCC结合符号执行和静态分析的源代码检测工具。ABAZER-SE由两个阶段组成,第一阶段是通过符号执行获取可行性路径,第二阶段应用静态分析技术对可行性路径分析找到源代码中缺陷。实验结果表明该工具具有可行性、有效性和可扩展性。     

基于可执行文件的缓冲区溢出检测模型

给出缓冲区溢出的基本原理和现有检测技术,针对二进制可执行文件中存在的缓冲区溢出漏洞,提出一种缓冲区溢出检测模型,该模型采用静态检测和动态检测相结合的方法。对检测结果采取污点跟踪法进行人工分析,采用插件技术给出缓冲区溢出检测模型的具体设计。实验结果证明该模型的设计是有效的。     

基于符号执行与混合约束求解的测试用例生成研究

由于现有基于符号执行的测试用例生成方法无法对关于字符串的测试用例生成提供有效支持,因此提出并实现了基于符号执行与混合约束求解测试用例自动化生成方法。该方法利用模型检测软件对被测软件源代码进行符号执行,生成关于字符串与数值的混合约束集,利用字符串-数值约束求解器对约束集进行求解,最终根据求解结果生成软件测试用例与不可达路径。实验结果表明,该方法较好地支持了关于字符串测试用例生成,且具有良好的效率与准确性。     

Automatic Buffer Overflow Warning Validation

Static buffer overflow detection techniques tend to report too many false positives fundamentally due to the lack of software execution information. It is very time consuming to manually inspect all the static warnings. In this paper, we propose BovInspector, a framework for automatically validating static buffer overflow warnings and providing suggestions for automatic repair of true buffer overflow warnings for C programs. Given the program source code and the static buffer overflow warnings, BovInspector first performs warning reachability analysis. Then, BovInspector executes the source code symbolically under the guidance of reachable warnings. Each reachable warning is validated and classified by checking whether all the path conditions and the buffer overflow constraints can be satisfied simultaneously. For each validated true warning, BovInspector provides suggestions to automatically repair it with 11 repair strategies. BovInspector is complementary to prior static buffer overflow discovery schemes. Experimental results on real open source programs show that BovInspector can automatically validate on average 60% of total warnings reported by static tools.

     

Using static symbolic execution to detect buffer overflows

Buffer overrun remains one of the main sources of errors and vulnerabilities in the C/C++ source code. To detect such kind of defects, static analysis is widely used. In this paper, we propose a path-sensitive static analysis based on symbolic execution with state merging. For buffers with compile-time-known sizes, we present an interprocedural path- and context-sensitive overrun detection algorithm that finds program points satisfying a proposed error definition. The described approach was implemented in the Svace static analyzer without significant loss of performance. On Android 5.0.2, these detectors generated 351 warnings, 64% of which were true positives. In addition, we describe a prototype of an intraprocedural heap buffer overflow detector and present an example of a defect found by this detector.     

SymFuzz:一种复杂路径条件下的漏洞检测技术

当前漏洞检测技术可以实现对小规模程序的快速检测,但对大型或路径条件复杂的程序进行检测时其效率低下。为实现复杂路径条件下的漏洞快速检测,文中提出了一种复杂路径条件下的漏洞检测技术SymFuzz。SymFuzz将导向式模糊测试技术与选择符号执行技术相结合,通过导向式模糊测试技术对程序路径进行过滤,利用选择符号执行技术对可能触发漏洞的路径进行求解。该技术首先通过静态分析获取程序漏洞信息;然后使用导向式模糊测试技术,快速生成可以覆盖漏洞函数的测试用例;最后对漏洞函数内可以触发漏洞的路径进行符号执行,生成触发程序漏洞的测试用例。文中基于AFL与S2E等开源项目实现了SymFuzz的原型系统。实验结果表明,SymFuzz与现有的模糊测试技术相比,在复杂路径条件下的漏洞检测效果提高显著。     

智能合约安全漏洞挖掘技术研究

近年来，以智能合约为代表的第二代区块链平台及应用出现了爆发性的增长，但频发的智能合约漏洞事件严重威胁着区块链生态安全。针对当前主要依靠基于专家经验的代码审计效率低下的问题，提出开发通用的自动化工具来挖掘智能合约漏洞的重要性。首先，调研并分析了智能合约面临的安全威胁问题，总结了代码重入、访问控制、整数溢出等10种出现频率最高的智能合约漏洞类型和攻击方式；其次，讨论了主流的智能合约漏洞的检测手段，并梳理了智能合约漏洞检测的研究现状；然后，通过实验验证了3种现有符号执行工具的检测效果。对于单一漏洞类型，漏报率最高达0.48，误报率最高达0.38。实验结果表明，现有研究涵盖的漏洞类型不完整，误报及漏报多，并且依赖人工复核；最后，针对这些不足展望了未来研究方向，并提出一种符号执行辅助的模糊测试框架，能够缓解模糊测试代码覆盖率不足和符号执行路径爆炸问题，从而提高大中型规模智能合约的漏洞挖掘效率。     

Goal-oriented dynamic test generation

ContextMemory safety errors such as buffer overflow vulnerabilities are one of the most serious classes of security threats. Detecting and removing such security errors are important tasks of software testing for improving the quality and reliability of software in practice.ObjectiveThis paper presents a goal-oriented testing approach for effectively and efficiently exploring security vulnerability errors. A goal is a potential safety violation and the testing approach is to automatically generate test inputs to uncover the violation.MethodWe use type inference analysis to diagnose potential safety violations and dynamic symbolic execution to perform test input generation. A major challenge facing dynamic symbolic execution in such application is the combinatorial explosion of the path space. To address this fundamental scalability issue, we employ data dependence analysis to identify a root cause leading to the execution of the goal and propose a path exploration algorithm to guide dynamic symbolic execution for effectively discovering the goal.ResultsTo evaluate the effectiveness of our proposed approach, we conducted experiments against 23 buffer overflow vulnerabilities. We observed a significant improvement of our proposed algorithm over two widely adopted search algorithms. Specifically, our algorithm discovered security vulnerability errors within a matter of a few seconds, whereas the two baseline algorithms failed even after 30 min of testing on a number of test subjects.ConclusionThe experimental results highlight the potential of utilizing data dependence analysis to address the combinatorial path space explosion issue faced by dynamic symbolic execution for effective security testing.     

Filtering false alarms of buffer overflow analysis using SMT solvers

Buffer overflow detection using static analysis can provide a powerful tool for software programmers to find difficult bugs in C programs. Sound static analysis based on abstract interpretation, however, often suffers from false alarm problem. Although more precise abstraction can reduce the number of the false alarms in general, the cost to perform such analysis is often too high to be practical for large software. On the other hand, less precise abstraction is likely to be scalable in exchange for the increased false alarms. In order to attain both precision and scalability, we present a method that first applies less precise abstraction to find buffer overflow alarms fast, and selectively applies a more precise analysis only to the limited areas of code around the potential false alarms. In an attempt to develop the precise analysis of alarm filtering for large C programs, we perform a symbolic execution over the potential alarms found in the previous analysis, which is based on the abstract interpretation. Taking advantage of a state-of-art SMT solver, our precise analysis efficiently filters out a substantial number of false alarms. Our experiment with the test cases from three open source programs shows that our filtering method can reduce about 68% of false alarms on average.     

An analysis on secure coding using symbolic execution engine

Business’ dependency on a software or computer program is getting higher. In such an environment, eliminating security vulnerabilities have become increasingly important and difficult as programs are more complicated and have greater impacts on businesses. We analyzed the security vulnerabilities of code using a symbolic execution engine that tracks data which would kill or might make the program vulnerable. We also present smart fuzzing using the data from the symbolic execution engine, an effective software vulnerability-finding testing that automatically generates inputs that crash or penetrate the program. By using symbolic execution engine, we can produce the automatically-generated data that are strong against vulnerability issues. In the case when program verification tools fail to verify a program, either the program is buggy or the report is a false alarm. In this case, the burden is put on users in manually classifying the report, which is a time-consuming, error-prone task and it does not utilize facts already proven by the analysis. We present a new technique for assisting users in classifying error reports. Our technique computes small, relevant queries presented to a user, which capture exact information that the analysis misses to either discharge or validate the error. In this paper, a methodology proper to detecting the security vulnerability is suggested by engrafting the symbol-based engine into the secure coding. Also, its effect was verified through the security vulnerability inspection test using the suggested symbolic execution engine. A notion of symbolically executing the program has been presented, which is closely related to the normal notion of program execution. It offers the advantage that one symbolic execution may represent a large, usually infinite, class of normal executions. This can be used for great advantages in the program inspecting and debugging.