第十一讲高效的静态分析---符号执行

与缺陷模式一、符号执行1、符号执行简介2、代表工具:PREfix二、缺陷模式1、缺陷模式简介2、安全漏洞内容一、符号执行1、符号执行简介2、代表工具:PREfixintx,y;1:if(x>y){2:x=x+y;3:y=x-y;4:x=x-y;5:if(x>y)foo1();6:elsefoo2();}观察下面程序:有什么问题J.
C.
King于1976年提出SymbolicExecution使用符号值,而不是实际数据,作为输入将程序变量的值表示为符号表达式程序计算的输出表达为输入符号值的函数1、符号执行简介优点分析是路径敏感的因为没有对路径、状态做近似,结果精确适合做状态检查、时序检查对并发类型的错误十分有效缺点对所有可能的状态进行穷举搜索,开销大对系统的行为进行近似,可能导致这类结果不精确对于数据密集的系统分析困难在边界处对路径、时序属性近似困难,故复合困难模型检验优点由于对路径、状态进行抽象,扩展性好可以对许多有价值的属性构造格易于组合提供了坚实的数学基础缺点适合的属性需要是简单的、"状态""值"型的对时序性质支持弱属性格的定义不容易有时近似过强抽象解释优点支持灵活的属性易于扩展缺点开发人员需要提供额外的信息自动化程度不高路径不敏感,对并发系统不适合演绎方法(定理证明)记录执行的状态,包括:程序变量的符号值路径条件(PC:PathCondition)程序标记(后面执行什么)路径条件非常重要积累了路径的约束条件符号执行树刻画程序符号执行过程中的执行路径符号执行最初,x与y分别具有符号值X、Y在每个分支点,PC根据输入的假定确定不同的值如果PC不成立,该路径不可达可以大大减少路径组合intx,y;1:if(x>y){2:x=x+y;3:y=x-y;4:x=x-y;5:if(x>y)foo1();6:elsefoo2(x:X,y:Y(x>y)x:X,y:Y(X>Y)x:X,y:Y(XY)x:X+Y,y:X(X>Y)x:Y,y:X(X>Y)x:Y,y:X(X>Y)&(Y>X)x:Y,y:X(X>Y)&(Y2#include34char*f(intsize)5{6char*result;78if(size>0)9result=(char*)malloc(size);10if(size==1)11returnNULL;12result[0]=0;13returnresult;14}观察右边代码有什么问题1#include2#include34char*f(intsize)5{6char*result;78if(size>0)9result=(char*)malloc(size);10if(size==1)11returnNULL;12result[0]=0;13returnresult;14}example1.
c(11):warning14:leakingmemoryproblemoccursinfunction'f'Thecallstackwhenmemoryisallocatedis:example1.
c(9):fProblemoccurswhenthefollowingconditionsaretrue:example1.
c(8):when'size>0'hereexample1.
c(10):when'size==1'herePathincludes4statementsonthefollowinglines:891011example1.
c(9):usedsystemmodel'malloc'forfunctioncall:'malloc(size)'functionreturnsanewmemoryblockmemoryallocated错误消息1:当size=1时,直接返回NULL,被分配的内存未被释放,也未被返回.
1#include2#include34char*f(intsize)5{6char*result;78if(size>0)9result=(char*)malloc(size);10if(size==1)11returnNULL;12result[0]=0;13returnresult;14}example1.
c(12):warning10:dereferencinguninitializedpointer'result'problemoccursinfunction'f'example1.
c(6):variabledeclaredhereProblemoccurswhenthefollowingconditionsaretrue:example1.
c(8):when'size2#include34char*f(intsize)5{6char*result;78if(size>0)9result=(char*)malloc(size);10if(size==1)11returnNULL;12result[0]=0;13returnresult;14}example1.
c(12):warning11:dereferencingNULLpointer'result'problemoccursinfunction'f'example1.
c(9):valuecomesfromreturnvalueof'malloc'hereProblemoccurswhenthefollowingconditionsaretrue:example1.
c(8):when'size>0'hereexample1.
c(10):when'size!
=1'hereproblemoccurswhen'memoryexhausted'Pathincludes4statementsonthefollowinglines:891012example1.
c(9):usedsystemmodel'malloc'forfunctioncall:'malloc(size)'functionreturns0memoryexhausted错误消息3:当size>0,但malloc失败,result返回NULL指针时,对其赋值出现错误while(therearemorepathstosimulate)initializememorystatesimulatethepath,identifyinginconsistenciesandupdatingthememorystateperformend-of-pathanalysisusingthefinalmemorystate,identifyinginconsistenciesandcreatingper-pathsummary}combineper-pathsummariesintoamodelforthefunction算法伪代码:模拟单个函数需要模拟可达的路径.
可达路径的集合包含所有可能的控制流路径集合.
这个集合的大小往往小于明显的控制流路径.
因为相同的条件往往控制多个条件模块.
通常可以选择有代表性的路径来模拟.
具体路径数可以由用户进行配置模拟一条路径涉及遍历函数的抽象语法树,对树上相关的语句、表达式求值.
被模拟函数的内存状态随着语句的执行被不断更新.
许多缺陷(例如,未初始化的内存,NULL,或者无效的指针解析)可以通过在路径模拟过程中对内存的状态应用一致性规则发现.
其他(例如,内存泄漏,将指针返回给一个释放的内存)在到达路径终点时可以被发现当路径被模拟时,函数的最终内存状态被综合处理(summarized).
当所有的路径被模拟后,per-pathsummaries被组成一个函数的模型3)主要步骤路径路径跟踪很容易发现一些问题路径中包括"功能调用、语句、结果"模拟执行是基于路径进行的为定位缺陷提供依据但不一定是唯一的路径可能是多条路径累积的结果1#include2#include34char*f(intsize)5{6char*result;78if(size>0)9result=(char*)malloc(size);10if(size==1)11returnNULL;12result[0]=0;13returnresult;14}当size3三个:a=b+c内存操作:求值、测试与设置设置(setting)将一个值赋给内存,改变了内存的状态简单推理:(a>3&b>4)=>a+b>7测试(testing)在一定的上下文中对表达式求值,得到一个布尔结果.
需要进行测试的三种情形:需要判定表达式,以得到一个布尔结果(例如:条件分支)语言语义要求(例如:使用前必须初始化)在模型中选择可能的输出(例子见后面关于"模型"的内容)条件(condition)、假定(assumption)与选择点条件可以比路径更清晰地描述缺陷在路径模拟执行过程中,条件对应于假定当变量出现在一个表达式中、且值不确定时,可以进行假定例子中的"size":输入参数,模拟是自底向上进行的出现两个假定,分别模拟执行,并记忆当前假定当作出一个假定时,相关内存的状态被更新这个假定可能提高其它断言的准确性对于a=b+5,当假定条件表达式a==2为真时,a对应的内存状态更新为2,b对应的内存状态可以更新为-3.
此时,控制流没有由已知的值完全确定下来,被称为选择点路径结尾分析当一条路径中的所有语句被模拟执行后,可以进行一些附加分析发现一些缺陷.
例如:内存没有释放等等多路径分析一条长的路径可能因为调用而包含多条子路径需要分别分析为控制总体数目,可以设置上限路径选择是一个问题模型模型模拟了函数的行为模拟器遇到一个函数调用时,它通过函数的模型来模拟被调用的函数函数的模型主要是一组输出集合,这些输出代表了函数计算时对内存状态的可能改变每个输出由Guards,Constraints,Results构成约束(Constraint)是前置条件:fopen的参数必须有效结果(Result)是后置条件:fopen执行后返回值有效防卫(Guards)是测试:某个特定的输出可能依赖某个输入intknot(intj){if(j==0)return1;return0;}例子:返回值只有在"j==0"时为"1"只有在"j!
=0"时为"0"(deref(paramp)(alternatereturn_0(guardpeqpNULL)(constraintmemory_initializedp)(resultpeqreturnNULL)alternatereturn_X(guardpnepNULL)(constraintmemory_initializedp)(constraintmemory_valid_pointerp)(constraintmemory_initialized*p)(resultpeqreturn*p)))1intderef(int*p)2{3if(p==NULL)4returnNULL;5return*p;6}一个模型的例子:WarningMozillaApacheGDIUsinguninitializedmemory26.
14%45%69%Dereferencinguninitializedpointer1.
73%00DereferencingNULLpointer58.
93%50%15%Dereferencinginvalidpointer05%0Dereferencingpointertofreedmemory1.
98%00Leakingmemory9.
75%00Leakingaresource(suchasafile)0.
09%08%Returningpointertolocalstackvariable0.
52%00Returningpointertofreedmemory0.
09%00Resourceininvalidstate008%Illegalvaluepassedtofunction0.
43%00Dividebyzero0.
35%00Totalnumberofwarnings11592013效果(1998):Mozilla1.
0,Apache1.
3beta5二、缺陷模式1、缺陷模式简介2、安全漏洞1、缺陷模式简介1)缺陷模式概述2)LibraryInterface(库接口)3)主要技术是什么显式的与隐式的独立的与嵌入式的(annotatioin)私有的与共性的模式:设计模式分析模式过程模式……分析算法从事的是举重的工作模式辨识从事的是射击的事情待查代码代码模型分析算法缺陷知识缺陷报告与具体应用"无关"的知识词法或者语法共性特性(死锁、空指针、内存泄露、数组越界)公共库用法(顺序、参数、接口实现,容错,安全)与具体应用"相关"的知识类型定义(操作格式,不含其它信息(信息隐藏))类型约束(调用的顺序、参数值,接口实现)需求相关(正确)定理证明符号执行模型检查模型检查抽象解释侧重点在技术(算法)方面!
能侧重在知识上吗Google翻译的启示!
1)缺陷模式概述代码必须遵守各类约束如果违反,就是缺陷对不同约束的违反,构成了不同的缺陷模式约束分类BNF:宪法共性约束(库接口):国家法律、条例等特定软件的约束(类型):地方法律、条例2)LibraryInterface(库接口)1.
错误代码1.
1.
操作1.
2.
方法调用1.
2.
1.
单一方法调用1.
2.
2.
同一个类的多方法调用1.
2.
3.
不同类的多方法调用1.
3.

类定义1.
3.
1.
单一接口关联1.
3.
2.
单继承关联1.
3.
3.
其它1.
4.
线程1.
5.
引用2.
不安全代码3.
脆弱代码3.
1.
需求检查3.
2.
异常相关3.
3.
线程3.
4.
其他4.
低效率代码4.
1.
线程4.
2.
String和StringBuffer4.
3.
Number和Wrapper4.
4.
其它5.
冗余代码5.
1.
无用代码5.
2.
不必要代码5.
2.
1.
不必要的Null检查5.
2.
2.
不必要的代码5.
3.
复制代码5.
4.
空集问题调用SimpleDateFormat的构造函数时没有传递Local参数.
调用Calendar.
set方法设置月份时使用了超出0到11的参数.
调用BigDecimal的构造函数时使用decimal数值.
调用substring时使用0作为参数.
调用ObjectOutPut.
writeObject时使用不可序列化的对象.
调用Double.
longBitsToDouble时使用整型参数.
调用PreparedStatement的setXXX时使用0作为参数索引值.
调用ResultSet的setXXX/updateXXX方法时使用0作为参数索引值.
调用Pattern的compile时使用了无效句法的正则表达式.
调用System.
runFinalizersOnExit或者Runtime.
runFinalizersOnExit显示的调用finalize.
在比较数组和非数组、不相关的类和接口、不同类型以及不同接口时调用equals"/"或者"/="跟随着0(除数为0)在比较两个实体时使用了"=="或者"!
=",例如字符串、引用、浮点型以及双精度型.
在比较Doube和Double.
NAN以及Integer和Integer.
MAX_VALUE时使用"=="或者""和"alert("这里存在脚本注入漏洞.
");那么,这句话将被存储在数据库评论表中.
以后,每一个浏览者打开这个新闻页面是,都将会弹出这样一个消息框.
上面的攻击者很仁慈,没有做过多的破坏.
但是如果输入:window.
location.
href="www.
baidu.
com";那么打开这个新闻页面,该页面将被从定向到baidu的页面上.
如果目标页面一个有恶意代码的页面,那么每个浏览者的机器都可能中毒.

如果输入:好文!
顶那么在新闻页面上看不到任何异状但点击该信息的浏览器会悄悄下载病毒WEB2.
0的流行使页面效果更加绚丽,同时也使脚本注入的攻击力提高不少对策之一:提供合理的过滤或者转换程序,在输入存放于数据库前,或者是显示在页面前对数据进行处理.
尽一切可能,避免用户的输入有执行的可能.