User:Liuhaots:ESP java

From Trusted Cloud Group
Jump to: navigation, search

Java版ESP介绍

ESP算法介绍:

ESP是高效的Path Sensitvie程序验证工具,它能精确又高效的分析大型程序,它的实现基于PLDI02的论文"ESP:Path-sensitive Program Verification in Polynomial Time"

传统的程序验证方法分两种:Path Sensitive和Dataflow。Path-sensitive是路径敏感,对所有的约束条件都考虑,精确的验证不同的约束条件下程序的正确性,但是考虑所有路径的状态,会消耗指数性的时间和空间,如果程序很大很复杂,时间和空间的状态爆炸会让验证工具很快崩溃,所以传统的Path Sensitive并不实用。而为了验证大型程序,通常采用Dataflow的方法(比如RacerX),Dataflow的程序分析方法,通过合并不同路径上的约束条件,减少时间和空间的消耗,不会造成状态爆炸,但是合并会丢失路径相关的状态,dataflow的分析往往有很多false positive的结果,是程序分析者困惑,没有达到分析目的,所以Dataflow的方法由于不精确,也不实用。

为了精确的验证大型程序,Property Simulation的算法被提了出来,也就是ESP所使用的算法。总的来说,Property Simulation的算法,结合了Path Sensitive和Dataflow的优点:通过状态合并,去掉与验证目标无关的状态,减少时间和空间的消耗,而通过保存与验证目标相关的状态,保证程序验证的精确性,由于验证目标的状态有限,通常只有几种,所以能保证只消耗多项式的时间。

Property指要验证的目标的性质。比如某个文件的安全性验证,该文件的状态有三种:未打开,打开,错误。如果某个文件未打开,而这时调用了close方法,会导致错误,或者那个文件已经打开,还未关闭的情况下再次调用了open方法,状态又会变为错误。再比如锁的安全性验证,某个锁的状态与文件的状态类似:未锁住,锁住,错误。连续的lock同一把锁或者解锁已经释放过的锁,都会造成错误。Property的转换可以用有限状态机(FSM)形象的表示:

关于Dataflow和PropertySimilation和Path-sensitive对比,可以用下例很好的表示:
esp


我们可以看到,PathSensitive的方法,到分析结束,记录所有路径的约束条件,正确验证了目标文件处于安全状态,但是如果被分析的程序比较复杂,要记录所有路径的状态,势必会造成状态爆炸,分析程序崩溃。而Dataflow的方法,在两条路径的合并点,总是将两条路径的状态也合并起来,所以到分析结束,只记录了一个状态,不会有状态爆炸,但是分析结果却非常粗糙,一共有3个分析结果:uninit,opened,error,其中opened和error都是false positive。

而PropertySimulation的方法,在路径的合并点,合并掉与验证目标不相关的状态,减少因为记录不相关状态的消耗,由于Property是有限的,需要记录的状态不会指数级的爆炸,达到多项式时间验证的目的。由于刻意保存了与目标状态相关的路径状态,所以也能保证程序分析的正确性。对于例子来说,第一个if分支,有两个状态:!d和d,分别对应uninit和opened两个property。第二个if分支,p和!p由于没有影响验证目标的property,所以合并以后,p和!p的信息被删除,减少了消耗。到第三个if分支,由于d与property的关系被保存下来,保证了分析结果的正确性。

ESP实现介绍:

我们的java版ESP架构,分析的是LLVM(Low Level Virtual Machine)格式的字节码。LLVM是伊利诺伊大学发起的一个开源项目,提供一个现代化的,基于SSA的编译策略能够同时支持静态和动态的任意编程语言的编译目标。利用LLVM的编译器(llvm-gcc或者Clang),可以将C/C++/Objective-C等编译成llvm格式的字节码。具体可以参见http://llvm.org/
ESP的实现分两个部分:(1)ANTLR识别llvm代码,(2)ESP算法的实现。

(1)ANTLR识别llvm代码——jllvm。
ANTLR(ANother Tool for Language Recognition),是一个可以接受含有语法描述的语言描述符并且生成程序能够识别这些语言所产生的句子。作为一个翻译程序的一部分,你可以给你的语法附上简单的操作符和行为并且告诉ANTLR如何构造AST并且如何输出它们。用ANTLR识别llvm代码后,使用自定义的java类来存储识别出的llvm代码信息(如function,instructon等)。具体的ANTLR识别llvm的文法见llvm.g。
我们自定义的java类,包含function,basicblock,各种instruction,以及各种程序中的type和value等。这一整套java类的系统我们简称为jllvm。
jllvm是llvm的前端,识别llvm代码,转换为由java类组成的llvm语言架构,然后我们在jllvm上面分析就可以了。

(2)ESP算法实现。
java实现的好处是跨平台,可扩展性高,易于维护。我们用java实现了上述的ESP算法(具体算法见PLDI02论文),用来验证程序的锁安全。在算法的实现中,大量的用了interface,利于扩展。所以如果要验证其他Property,只需要实现相应的Property的interface即可。
算法实现的重点在于状态合并,首先需要识别出某个节点是合并的节点,在该处检查两条路径的约束条件状态和Property状态,合并掉那些不影响Property的约束条件。

工具介绍:

工具的源代码可以从SVN上获取,地址是http s://192.168.1.253:8443/svn/PA/SourceCode/LockAnalysis/JLLVM

分析结果显示的是所有状态变化,初始时,某个锁的Property状态是[UNINIT],lock操作以后,状态是[LOCKED],连续两次lock操作或者对[UNINIT]的锁进行unlock操作,会导致[ERROR]状态,只有对[LOCKED]的锁进行unlock,才会变为[UNINIT]状态。状态的转换可以用有限状态机表示。与Property状态对应的是程序的执行状态,包含路径约束条件。如果一个方法包含两个锁,是分别对两个锁执行ESP的分析,然后分别输出分析结果。锁的初始状态是[UNINIT],如果分析结束以后还是[UNINIT],说明该程序的验证结果是没有错误,而[LOCKED]和[ERROR]都说明可能会有问题,而具体出问题的原因需要在执行状态中找。 下图是工具分析结果的截图: Tool.png

Personal tools
Namespaces
Variants
Actions
Navigation
Upload file
Toolbox