过程间流敏感的指针分析技术研究

指针分析技术是一种基础的静态程序分析技术,也是软件安全方向的研究热点之一,在软件缺陷检测、恶意代码分析、程序验证、编译器优化等应用场景中发挥着重要的作用,指针分析的精度在这些应用场景中至关重要。流敏感分析和过程间分析是提高指针分析精度最有效的两种技术。文中对现有的提高过程间流敏感指针分析精度的技术进行总结,从为提高精度所消除的信息入手,将分析方法分为两大类：一类是消除分析中的虚假信息,以避免指向信息沿虚假的返回路径或是虚假调用关系传播;另一类是消除分析中保守的指向关系,在每个程序点处根据设置的规则尽可能确定指针的唯一指向,而不是笼统地计算指针的多个可能指向。据此,详细比较了过程间流敏感指针分析技术的异同,并对指针分析技术未来的研究方向进行了展望。     

基于域敏感指针分析的细粒度数据随机化技术

针对传统的数据随机化技术静态分析精度不高的问题,提出一种基于域敏感指针分析算法的细粒度数据随机化技术。在静态分析过程中,首先对中间表示进行语法抽象,得到形式化的语言表示;然后建立非标准类型系统,描述变量之间的指向关系;最后按照类型规则进行类型推断并求解,得到域敏感的指向关系。根据指向关系对数据进行随机化加密,得到经过随机化的可执行程序。实验数据表明,基于域敏感指针分析的数据随机化技术与传统的数据随机化技术相比,分析精度显著提高;处理时间开销平均增加了2%,但运行时间开销平均减少了3%。所提技术利用域敏感的指针分析,给程序带来更少的执行开销,并能够更好地提高程序的防御能力。     

Java 指针指向分析优化

指针指向分析的主要目的是静态地获取程序在运行时刻的指针指向信息.基于Andersen算法,设计了一种有效的、上下文敏感的指针指向分析算法,支持继承、字段对象等语言特性.不同对象的字段在算法中被分别处理,同时,算法对复合类型的对象实现了基于字段的处理.为了提高算法的效率和可扩展性,引入了两种优化方式:一种是结点间的拓扑排序以降低分析过程中的迭代次数;另一种是在线的环路侦测与消除,它与拓扑排序过程同步实现,有效地提高了处理效率.实验数据表明,该算法可以用来为较大规模的Java代码生成精确的指向关系集合.     

C程序中的内存泄漏机制分析与检测方法设计

C语言作为安全关键软件的主要实现语言,其存在的内存泄漏缺陷具有很高的隐蔽性和危害性,如何保证内存泄漏检测的准确性和高效性是一大挑战。静态分析具有直接分析源码、能够较早发现软件错误,从而降低修复代价的优势。基于静态分析技术,提出了一种基于路径敏感的值流分析的内存泄漏检测方法,首先进行指针分析生成精确指向信息;然后基于指向信息构建值流约束,执行可达性分析以识别程序中的泄漏路径;最后借助指针与内存地址的有效生命周期进行验证。在典型基准C程序上的实验结果分析表明,本文方法与现有技术相比在效率和精度上都具有一定优势。     

基于SAT求解的面向对象程序类型分析

类型分析是面向对象程序分析中的重要环节,精确的类型分析能够提高其它程序分析的精度.由于传统精确分析方法固有的高复杂性,现有的类型分析大都使用粗糙的分析方法.提出了一种基于SAT求解的面向对象程序类型分析方法.该方法用命题逻辑表示类型在变量间的传递关系,将程序抽象成命题公式,并使用高效的SAT求解器求解,从而获得变量运行时的类型集合.该方法是流敏感的,并且具有良好的伸缩性,既可以进行快速但精度低的上下文不敏感分析,也可以进行较慢但精度高的上下文敏感分析.     

Android应用Activity启动环研究

Activity的循环启动构成了activity启动环(ALC),它是一种Android应用开发工程师为了完成特定功能而广泛使用的结构.由于缺乏对ALC特性的系统研究,致使当前activity跳转分析方法对启动方式不敏感,使其无法正确模拟使用特殊启动方式的Android应用的返回栈状态变化,从而产生非法路径.本文形式化的表示了以7种不同方式启动activity带来的返回栈状态变化,并提出表示activity间启动关系的activity启动图(ALG),以及启动方式敏感的activity跳转静态分析方法用于自动构建ALG.该方法首先为Android应用构造辅助主函数:为每个activity类构造一个对象的堆内存分配点,对于每个activity对象,依据控制流组织被重写的回调函数调用顺序.然后通过面向对象的字段敏感指向分析提取activity启动关系中的目标activity类和启动方式相关配置,从而构建activity对象的启动图.另外,本文设计并实现了ALC静态分析框架ALCAnalyzer,该框架能为Android应用自动生成ALG,基于ALG生成ALC集合,并能准确模拟重复执行ALC时的返回栈状态变化,预测应用在运行过程中是否会产生同类型activity实例.对1179个Android开源应用进行自动分析及人工验证的实验结果证明了启动方式敏感的activity跳转分析的准确性和分析工具的实用性,同时展现了ALC分布的广泛性和特殊启动方式被使用的广泛性.对Google Play的20个应用进行实验,结果证明相比于启动方式不敏感的activity跳转分析,ALCAnalyzer能够更准确模拟返回栈状态变化,从而防止非法路径产生,并能够为返回栈管理提供有效信息.     

使用敏感路径识别方法分析安卓应用安全性

安卓系统在手机端操作系统中长期占据主导地位,但由于安卓系统开放共享的特性和不够严谨的第三方市场审核机制,安卓平台受到众多恶意应用的侵扰.本文结合静态程序分析和机器学习方法,提出了基于敏感路径识别的安卓应用安全性分析方法.首先,针对恶意应用中存在的恶意行为以及触发条件,定义了敏感路径.其次,针对安卓应用中存在大量组件间函数调用关系,提出了一种生成应用组件间函数调用关系图的方法.再次,由于提取出的敏感路径信息无法直接作为识别特征,实现了一种基于敏感路径信息抽象的特征提取方法.最后,从GooglePlay、豌豆荚、Drebin等来源收集了493个应用APK文件作为实验数据集,本文方法的准确率为97.97%,高于基于API-Feature的检测方法（90.47%）,此外,在恶意应用和良性应用检测的精度、召回率、F度量等方面,本文方法均优于API-Feature方法.另外,实验表明APK文件大小会影响实验的结果,尤其体现在分析时间上（0-4MB大小的APK平均分析用时89秒;文件增大后,平均分析用时增长明显）.     

基于指向与数值抽象的带指针算术程序的分析方法

带指针算术的程序往往包含数组越界、缓冲区溢出等运行时错误。单纯的指针分析技术和数值分析技术都无法有效处理指针算术。为了将指针分析与数值分析相结合,首先提出一种新的指针内存模型,然后基于该模型设计了一个刻画指针指向关系和指针偏移量的抽象域。最后在抽象解释框架下,设计并实现了一个面向带指针算术C程序的静态分析工具原型PAA。实验结果表明,PAA能够有效地分析指针程序的指向关系和数值性质,并能够在效率和精度间取得合理的权衡。     

C代码API一致性检验中的等值分析

在实际中对C代码进行API一致性检验的过程中发现,API(application programming interface)规范大都涉及以数值为论域的时序性质,与在静态分析过程中所能获取的以变量符号为占位符的独立语义之间存在分析上的缺口.在仔细考察C代码变量符号间等值关系的基础上,给出基于值等价类空间的等值分析方法.这种流相关的分析方法不仅可以在API一致性检验的过程中维护变量符号域和数值域之间的对应关系,而且由于能够屏蔽等值关系以外的其他信息,还可以为后继分析的优化提供有力的支持.     

流敏感按需指针别名分析算法

为了提高交互环境下指针别名查询的响应效率,近期研究提出通过只分析与目标相关指针的按需分析策略来降低浪费在与目标无关的指针分析的额外开销。典型的代表是基于上下文无关文法的按需别名分析算法。但是,该算法的精度只局限于控制流不敏感。控制流不敏感的别名关系将约束上层分析的精度。针对该不足,提出了具有流敏感精度的按需别名分析算法。首先采用不完全静态单赋值语句形式来区分指针变量赋值实例,然后通过层次线性化编码方法来表达控制流图中的流敏感信息以构建赋值流图,最后将别名关系查询问题转换为在赋值流图上搜索目标结点间在控制流可达条件下赋值路径的可达性问题,进而实现流敏感的按需别名分析。实验表明,与流不敏感的按需别名分析相比,该方法可以在保证查询效率的前提下,有效提高按需别名分析的精度。     

基于符号约束的PLC程序正确性验证

符号约束描述了程序中的变量关系,被广泛运用于模型检测、符号执行等程序的静态分析方法中。将符号约束应用于可编程逻辑控制器(PLC)程序的正确性验证,能够发现程序中的逻辑错误。人工计算符号约束不仅冗杂枯燥,而且错误率高。针对语句表形式的PLC程序,提出一种基于符号约束的正确性验证方法,通过分析PLC源代码的控制流及数据流,构造程序的控制流图并将其转换为静态单赋值形式的三地址码,最后使用迭代计算的方法求出每个变量的符号约束。     

一种面向二进制的控制流图混合恢复方法

控制流图恢复是进行二进制文件安全性分析的基础,静态恢复分析速度快,但其精确度欠缺;动态恢复方法的优点是精确度高,但分析效率较低。将两者优点结合,提出了面向二进制程序的混合分析恢复方法,在对二进制文件进行静态分析生成控制流图的基础上,结合局部符号执行技术和反向切片技术对间接分支跳转的目的地址进行求解,之后再分析边和节点的可达性,合并不可达的边和节点。经实验验证,混合方法的分析效率与静态方法相近,远高于纯动态分析方法,其精确度较静态方法有较大提高。     

一种用于指针程序的形状分析方法

指针程序的分析一直是研究热点。本文提出一种基于形状图逻辑的形状分析方法,其中形状分析采用形状图来表达程序中指针的指向和相等关系,并用形状图逻辑来进行推理。形状图逻辑是一种把形状图看成有关指针的断言,并在此基础上对Hoare逻辑进行扩展而得到的程序逻辑。首先介绍所提出的形状图和形状图逻辑;然后在此基础之上,设计一种基于形状图逻辑的形状分析方法。     

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

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

Using dependencies to improve precision of code analysis

Development of dependency analysis methods in order to improve static code analysis precision is considered in this paper. Reasons for precision loss when detecting defects in program source code using abstract interpretation methods are explained. Need for program object dependency extraction and interpretation is justified by numerous real-world examples. Dependency classification is presented. Necessity for aggregate analysis of values and dependencies is considered. Dependency extraction from assignment statements is described. Dependency interpretation based on logic inference using logic and arithmetic rules is proposed. The methods proposed are implemented in defect detection tool Digitek Aegis, significant increase of precision is shown.     

利用主语和谓语的句法关系识别谓语中心词

谓语中心词识别对于整个句子的句法分析起着重要的作用。目前已有的谓语中心词识别方法,利用谓语中心词候选项的静态语法特征和动态语法特征来确定谓语中心词。在此基础上,本文提出一种利用句子的主语和谓语之间的句法关系来识别谓语中心词的方法。该方法除了利用谓语中心词候选项的静态语法特征和动态语法特征外,还利用主谓语之间的句法关系识别谓语中心词。实验表明,与传统方法相比,这种方法对谓语中心词的识别正确率可以提高3%左右。     

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.     

用Mathematica软件及Jacobian方法证明一、二阶热力学偏导数关系式

用Jacobian方法证明热力学函数的一、二阶偏导数关系式,其牵涉公式多而复杂,实际应用起来比较困难。利用Mathematica软件的逻辑编程及符号运算功能,再结合Jacobian方法,就使该问题证明变得概念清楚,简便易行。本文描述了其具体实施的方法。     

A Shape Graph Logic and A Shape System

Analysis and verification of pointer programs are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems in two stages. First, shape graphs at every program point are constructed using an analysis tool. Then, they are used to support the verification of other properties （e.g., orderedness）. Our prototype supports automatic verification of programs manipulating complex data structures such as splay trees, treaps, AVL trees and AA trees, etc. The proposed shape graph logic, as an extension to Hoare logic, uses shape graphs directly as assertions. It can be used in the analysis and verification of programs manipulating mutable data structures. The benefit using shape graphs as assertions is that it is convenient for acquiring the relations between pointers in the verification stage. The proposed shape system requires programmers to provide lightweight shape declarations in recursive structure type declarations. It can help rule out programs that construct shapes deviating from what programmers expect （reflected in shape declarations） in the analysis stage. As a benefit, programmers need not provide specifications （e.g., pre-/post-conditions, loop invariants） about pointers. Moreover, we present a method doing verification in the second stage using traditional Hoare logic rules directly by eliminating aliasing with the aid of shape graphs. Thus, verification conditions could be discharged by general theorem provers.     

基于LTL语义的可达性控制器合成工具

控制器合成是针对给定的获胜目标,在开放的实时系统环境中,自动地寻找获胜策略的过程.这个策略可以表述为一系列的符号化状态和动作的映射关系.在本文中,我们主要针对以线性时序逻辑（LTL）描述的可达性作为获胜目标,进行合成策略的发现.文中介绍了一种采用on-the-fly思路的合成算法,以规避状态数目太多带来的内存溢出问题.文中算法是对文献[1]的一种扩展,该算法主要用于解决基于分支时序逻辑（CTL）的控制器合成.另外,我们实现了相关的控制器合成工具CTAV/TGA（Timed Gamed Automata）,在实现的过程中,使用on-the-fly的方式,避免了穷尽状态空间,同时,通过使用zone和抽象,大大缩减了状态数目,使时空效率控制在可接受的范围内.