基于输入约束的符号执行优化

为了解决符号执行中路径爆炸、新路径发现率低等问题,提出了基于输入约束的符号执行(ICBSE)优化框架。该方法通过分析程序代码自动提取3类输入约束,随后使用这些约束引导符号执行更关注于核心功能代码。在KLEE中实现了上述优化框架,并对coreutils、binutils、grep、patch、diff这5个程序套件中的7个常用程序做了检测。ICBSE发现了7个之前未知的缺陷(KLEE只检测其中3个)。同时,ICBSE将指令行覆盖率、分支覆盖率分别提升了约20%,时间开销降低了约15%。

一种针对格式文件的符号执行优化方法

为了解决符号执行中路径爆炸、新路径发现率低等问题,提出了针对文件格式数据块约束的符号执行分析方法(FFCBSE,File Format Constraint Based Symbolic Execution)优化框架.文件格式信息的缺失会影响符号执行的效率以及测试用例生成,该方法通过分析程序代码自动分析程序读取的格式文件数据块之间的依赖关系并建立相关约束,随后使用这些约束引导符号执行更关注于核心功能代码区域.在KLEE中实现了上述优化框架,并对Tcpdump、Readelf、Elfdump、File、Zlib等7个常用文件处理程序做了检测.和KLEE以及DASE相比,FFCBSE发现了13个之前未知的缺陷,在指令覆盖率和分支覆盖率有10%~225%不同程度的提升.

基于控制流挖掘的Android系统代码漏洞分析

Android操作系统被广泛应用于智能手机、平板电脑等便携移动设备,因此Android操作系统的安全性和可靠性至关重要。本文使用控制流挖掘方法,针对Android内核代码的多种典型错误构建相关的分析脚本,进行了分析检测,并对Android系统多版本间进行横向分析对比。本文首次将控制流挖掘方法应用于Android系统,通过系统化的实验分析包含Android扩展的驱动以及Yaffs2文件系统在内的所有Android内核代码,并对Android各个内核版本进行横向对比分析,发现了代码库中一系列脆弱点。