高效的静态分析-符号执行与缺陷模式课件

第十一讲高效的静态分析---符号执行与缺陷模式1第十一讲1一、符号执行 1、符号执行简介 2、代表工具：PREfix二、缺陷模式 1、缺陷模式简介 2、安全漏洞内容2一、符号执行内容2

一、符号执行1、符号执行简介2、代表工具：PREfix3一、符号执行3intx,y;1:if(x>y){2:x=x+y;3:y=x-y;4:x=x-y;5:if(x>y)foo1();6:elsefoo2();}观察下面程序：有什么问题？4intx,y;观察下面程序：有什么问题？4J.C.King于1976年提出SymbolicExecution使用符号值，而不是实际数据，作为输入将程序变量的值表示为符号表达式程序计算的输出表达为输入符号值的函数1、符号执行简介5J.C.King于1976年提出Symbolic优点分析是路径敏感的因为没有对路径、状态做近似，结果精确适合做状态检查、时序检查对并发类型的错误十分有效缺点对所有可能的状态进行穷举搜索，开销大对系统的行为进行近似，可能导致这类结果不精确对于数据密集的系统分析困难在边界处对路径、时序属性近似困难，故复合困难模型检验6优点模型检验6优点由于对路径、状态进行抽象，扩展性好可以对许多有价值的属性构造格易于组合提供了坚实的数学基础缺点适合的属性需要是简单的、“状态”“值”型的对时序性质支持弱属性格的定义不容易有时近似过强抽象解释7优点抽象解释7优点支持灵活的属性易于扩展缺点开发人员需要提供额外的信息自动化程度不高路径不敏感，对并发系统不适合演绎方法（定理证明）8优点演绎方法（定理证明）8记录执行的状态，包括：程序变量的符号值路径条件（PC:PathCondition）程序标记（后面执行什么）路径条件非常重要积累了路径的约束条件符号执行树刻画程序符号执行过程中的执行路径符号执行9记录执行的状态，包括：符号执行9最初，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(X<Y)x:X+Y,y:Y(X>Y)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)&(Y<=X)例子：10最初，x与y分别具有符号值X、Yintx,符号执行可以被看作是路径敏感分析、演绎方法及抽象解释的组合对路径条件进行近似使得抽象解释的属性区间值收缩，因此更加灵活约束近似了许多状态，降低了分析量经常被应用于测试输入的生成传统上，符号执行对有限个整数变量进行符号化，后来扩展到了处理复杂的输入数据结构和并发例如，扩展JPF工具以进行符号执行Java程序11符号执行可以被看作是路径敏感分析、演绎方法及抽象解释的组合2、典型工具：PREfix1）基本特点2）主要思路3）主要步骤122、典型工具：PREfix1）基本特点12模拟执行单个的函数！模拟过程顺序地跟踪不同的执行路径，模拟每个操作符的动作。在路径执行过程中，通过跟踪内存的状态，应用各种一致性规则，查找不一致性。在对条件选择后，通过检查内存的当前状态，分析器可以限制可达的路径。由于对路径、值的跟踪都很仔细，可以获得精确的信息。函数的行为被描述为：条件、一致性规则及表达式值的集合。行为的这种描述被称为函数的一个模型。在路径执行过程中，不论何时进入一个函数，该模型被使用，以决定应用哪个操作1）基本特点13模拟执行单个的函数！1）基本特点13在模拟过程中产生的信息足够自动地产生该函数的一个模型为在整个程序中应用这些技术，分析起始于调用图的叶节点，自底向上地向根处理。随着函数被逐层模拟，缺陷被不断发现，函数模型被高层的后续模拟所使用这种自底向上的方法使用一个函数的实现来产生函数的约束，供上层使用。这对于程序不完整时（程序还没有开发完，或者被分析的代码需要适合多个不同的程序）尤其有效14在模拟过程中产生的信息足够自动地产生该函数的一个模型142）主要思路1#include<stdlib.h>2#include<stdio.h>34char*f(intsize)5{6char*result;78if(size>0)9result=(char*)malloc(size);10if(size==1)11returnNULL;12result[0]=0;13returnresult;14}观察右边代码有什么问题？152）主要思路1#include<stdlib.h>观1#include<stdlib.h>2#include<stdio.h>34char*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,被分配的内存未被释放，也未被返回。161#include<stdlib.h>example1#include<stdlib.h>2#include<stdio.h>34char*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‘size<=0’herePathincludes3statementsonthefollowinglines:81012错误消息2：当size<=0时，函数试图解析一个未被初始化的指针（mallocinline9willnotbeexecuted).171#include<stdlib.h>example1#include<stdlib.h>2#include<stdio.h>34char*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指针时，对其赋值出现错误181#include<stdlib.h>examplewhile(therearemorepathstosimulate){initializememorystatesimulatethepath,identifyinginconsistenciesandupdatingthememorystateperformend-of-pathanalysisusingthefinalmemorystate,identifyinginconsistenciesandcreatingper-pathsummary}combineper-pathsummariesintoamodelforthefunction算法伪代码：19while(therearemorepathsto模拟单个函数需要模拟可达的路径。可达路径的集合包含所有可能的控制流路径集合。这个集合的大小往往小于明显的控制流路径。因为相同的条件往往控制多个条件模块。通常可以选择有代表性的路径来模拟。具体路径数可以由用户进行配置模拟一条路径涉及遍历函数的抽象语法树，对树上相关的语句、表达式求值。被模拟函数的内存状态随着语句的执行被不断更新。许多缺陷(例如,未初始化的内存，NULL，或者无效的指针解析)可以通过在路径模拟过程中对内存的状态应用一致性规则发现。其他(例如，内存泄漏，将指针返回给一个释放的内存)在到达路径终点时可以被发现当路径被模拟时，函数的最终内存状态被综合处理(summarized)。当所有的路径被模拟后，per-pathsummaries被组成一个函数的模型20模拟单个函数需要模拟可达的路径。可达路径的集合包含所有可能的3）主要步骤路径路径跟踪很容易发现一些问题路径中包括“功能调用、语句、结果”模拟执行是基于路径进行的为定位缺陷提供依据但不一定是唯一的路径可能是多条路径累积的结果1#include<stdlib.h>2#include<stdio.h>34char*f(intsize)5{6char*result;78if(size>0)9result=(char*)malloc(size);10if(size==1)11returnNULL;12result[0]=0;13returnresult;14}当size<=0时，函数试图解析一个未被初始化的指针（mallocinline9willnotbeexecuted).213）主要步骤路径1#include<stdlib.h内存（变量）：值与断言模拟过程中函数使用的内存需要尽可能准确地跟踪每块内存都有值：3个基本状态知道准确的值（常量）有一个初始化的值，但不知道准确的值未初始化的值断言（predicate）也可能与值关联断言可能是由1到3部分组成单个：initialized两个：x>3三个：a=b+c22内存（变量）：值与断言22内存操作：求值、测试与设置设置(setting)将一个值赋给内存，改变了内存的状态简单推理：(a>3&b>4)=>a+b>7测试(testing)在一定的上下文中对表达式求值，得到一个布尔结果。需要进行测试的三种情形：需要判定表达式，以得到一个布尔结果(例如：条件分支)语言语义要求（例如：使用前必须初始化）在模型中选择可能的输出(例子见后面关于“模型”的内容)23内存操作：求值、测试与设置23条件(condition)、假定(assumption)与选择点条件可以比路径更清晰地描述缺陷在路径模拟执行过程中，条件对应于假定当变量出现在一个表达式中、且值不确定时，可以进行假定例子中的“size”:输入参数，模拟是自底向上进行的出现两个假定，分别模拟执行，并记忆当前假定当作出一个假定时，相关内存的状态被更新这个假定可能提高其它断言的准确性对于a=b+5,当假定条件表达式a==2为真时，a对应的内存状态更新为2，b对应的内存状态可以更新为-3。此时，控制流没有由已知的值完全确定下来，被称为选择点24条件(condition)、假定(assumption)与选路径结尾分析当一条路径中的所有语句被模拟执行后，可以进行一些附加分析发现一些缺陷。例如：内存没有释放等等多路径分析一条长的路径可能因为调用而包含多条子路径需要分别分析为控制总体数目，可以设置上限路径选择是一个问题25路径结尾分析多路径分析25模型模型模拟了函数的行为模拟器遇到一个函数调用时，它通过函数的模型来模拟被调用的函数函数的模型主要是一组输出集合，这些输出代表了函数计算时对内存状态的可能改变每个输出由Guards,Constraints,Results构成约束（Constraint）是前置条件：fopen的参数必须有效结果（Result）是后置条件：fopen执行后返回值有效防卫（Guards）是测试：某个特定的输出可能依赖某个输入intknot(intj){if(j==0)return1;return0;}例子：返回值只有在“j==0”时为“1”只有在“j!=0”时为“0”26模型intknot(intj)例子：返回值只有在“j=(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}一个模型的例子：27(deref1intderef(int*p)一个模型的Warning MozillaApache GDIUsinguninitializedmemory 26.14%45%69%Dereferencinguninitializedpointer 1.73%00DereferencingNULLpointer 58.93%50%15%Dereferencinginvalidpointer 05%0Dereferencingpointertofreedmemory 1.98%00Leakingmemory 9.75%00Leakingaresource(suchasafile) 0.09%08%Returningpointertolocalstackvariable0.52%00Returningpointertofreedmemory 0.09%00Resourceininvalidstate 008%Illegalvaluepassedtofunction 0.43%00Dividebyzero 0.35%00Totalnumberofwarnings 11592013效果(1998)：Mozilla1.0,Apache1.3beta528Warning MozillaApache二、缺陷模式 1、缺陷模式简介 2、安全漏洞29二、缺陷模式 1、缺陷模式简介291、缺陷模式简介1）缺陷模式概述2）LibraryInterface（库接口）3）主要技术是什么？301、缺陷模式简介1）缺陷模式概述30显式的与隐式的独立的与嵌入式的（annotatioin）私有的与共性的模式： 设计模式 分析模式 过程模式 …… 31显式的独立的私有的模式：31分析算法从事的是举重的工作模式辨识从事的是射击的事情待查代码代码模型分析算法缺陷知识缺陷报告32分析算法从事的是举重的工作待查代码代码模型分析算法缺陷知识缺与具体应用“无关”的知识词法或者语法共性特性（死锁、空指针、内存泄露、数组越界）公共库用法（顺序、参数、接口实现，容错，安全）与具体应用“相关”的知识类型定义（操作格式，不含其它信息（信息隐藏））类型约束（调用的顺序、参数值，接口实现）需求相关（正确）定理证明符号执行模型检查模型检查抽象解释侧重点在技术（算法）方面！33与具体应用“无关”的知识定理证明符号执行模型检查模型检查抽象能侧重在知识上吗？Google翻译的启示！34能侧重在知识上吗？Google翻译的启示！341）缺陷模式概述代码必须遵守各类约束如果违反，就是缺陷对不同约束的违反，构成了不同的缺陷模式约束分类BNF：宪法共性约束（库接口）：国家法律、条例等特定软件的约束（类型）：地方法律、条例351）缺陷模式概述代码必须遵守各类约束352）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. 空集问题362）LibraryInterface（库接口）1.错误代调用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时使用“==“或者”<=“。比较String.indexOf()和0是滥用“>”和“<”。在例如if和while的逻辑表达式中误用了操作符“=”、“&”和“|”。正确的的应该是“==”、“&&”和“||”。当某个实例不属于某个类型时使用了instanceof操作：单一方法调用：37调用SimpleDateFormat的构造函数时没有传递Lo某些类中必须成对使用的方法（必须有严格的顺序）：例如I/O对象中的open和close。时序方法的约束。初始化错误。使用负数索引或者超过数组长度的索引值引发了数组溢出。更多缺陷模式，请访问：同一个类的多方法调用:38某些类中必须成对使用的方法（必须有严格的顺序）：例如I/O对使用约束栈DBMS接口约束操作系统接口约束中间件接口约束应用软件语言约束约束（BNF、基本函数）39使用约束栈DBMS接口约束操作系统接口约束中间件接口约束应用3）主要技术是什么？如何在目标代码中查找已知的模式？先做基本扫描：有相近的代码？再努力提高准确度如何描述缺陷模式？自然语言形式化：时序逻辑等半形式化/图形化403）主要技术是什么？如何在目标代码中查找已知的模式？如何描述DEFECTPATTERNINPUTExtensibilityYesNoRepresentationDescriptionfileEmbeddedcode涉及的主要技术TARGETPROGRAMINPUTJavaProgrammingLanguageRepresentationC/C++SourcecodeCompiledfilePropertyConcernedUnusedcodeCodestyleTemporalpropertyConcurrencyOtherSEMANTICANALYSISControlFlowAnalysisDataFlowAnalysisStructureAnalysisCallGraphAnalysisOUTPUTRepresentationTextreportXML/HTMLreportInteractiveGUIEvaluationforResultSoundnessCompletenessOtherPoint-toAnalysis41DEFECTPATTERNINPUTExtensibil特点缺陷定位准确查找效率较高可以针对“常见”的缺陷42特点缺陷定位准确42对比模型检查侧重状态状态是否满足性质？抽象解释侧重循环不动点是什么？符号执行侧重分支状态有冲突吗？定理证明侧重不变量破坏了不变量？模式缺陷侧重共性约束状态与共性缺陷模式匹配？结合!43对比模型检查侧重状态结合!432、安全漏洞1）SQL注入

2）脚本注入

3）跨站点攻击

4）代码分析让正确的人得到正确的服务！442、安全漏洞1）SQL注入让正确的人得到正确的服务！441）SQL注入

SQL注入的成因主要是因为向数据库提供的SQL查询语句是用字符串拼装的方式生成的最经常遭受SQL注入的页面通常是管理员/用户登陆点。不论是asp或是jsp，如果不正确的编码，都会出现这个漏洞451）SQL注入SQL注入的成因主要是因为向数据库提供的S假设我们有一个JSP页面login.jsp，它会把用户名与密码提交到指定的模块Controller调用chekAdminLogin(StringuserName,StringpassWord) 进行登陆验证如果从表中找到匹配的记录，则表示验证成功。否则返回Null表示登陆验证失败。checkAdminLogin将收集到的用户名和密码信息拼装出SQL字符串，供DAO下层使用，以从数据库中的管理员记录表中读取数据46假设我们有一个JSP页面login.jsp，它会把用户名与如果有人试图在这里进行恶意攻击：在登陆名输入框中输入123(任意值)而在密码输入框中输入’OR’1’=’1那么由于我们的SQL是靠拼出来的，所以最终提交给数据库的将是:

SELECT*FROMTD_ADMINASAWHEREA.USERNAME=’123’ANDA.PASSWORD=’’OR’1’=’1’很显然，这句SQL由于后面被加上了永真条件，登陆是一定成功的。那么不论登陆者是否是管理员，输入‘OR‘1’=’1，他都将能够登陆系统。publicAdmincheckAdminLogin(StringuserName,Stringpassword){StringstrSQL=”SELECT*FROMTD_ADMINASAWHEREA.USERNAME=’”+userName+”’ANDA.PASSWORD=’”+password+”’”;对策之一：Java中对该模式的实现有PreparedStatment或者NamingQuery一类的技术，实现了参数与逻辑的分离，可以从根本上杜绝SQL注入。47如果有人试图在这里进行恶意攻击：publicAdminc2）脚本注入这里所说的脚本，通常指的是JavaScript脚本，虽然JavaScript运行于客户端，并且有安全沙箱的保护，但是放任恶意JavaScript脚本是十分危险的一个网站，如果对输入未做合理的验证或过滤，在显示输出的时候又未做合适的格式化，那么便存在这种漏洞与SQL注入不同，脚本注入没有直接攻击服务端，实际上是攻击了客户端窃取信息！482）脚本注入这里所说的脚本，通常指的是JavaScript脚假设我们有一个新闻站点，每个新闻允许浏览者进行评论浏览者提交的评论将被存储在数据据库专门的表中，并显示在新闻的下边如果开发者除了字符长度外没有做任何输入合法验证，那么这个站点的评论输入，就存在安全漏洞。49假设我们有一个新闻站点，每个新闻允许浏览者进行评论49如果输入:好文!顶<iframesrc=”带病毒的页面”width=”0”height=”0”></iframe>那么在新闻页面上看不到任何异状但点击该信息的浏览器会悄悄下载病毒WEB2.0的流行使页面效果更加绚丽，同时也使脚本注入的攻击力提高不少对策之一：提供合理的过滤或者转换程序，在输入存放于数据库前，或者是显示在页面前对数据进行处理。尽一切可能，避免用户的输入有执行的可能。50如果输入:对策之一：503）跨站点攻击跨站攻击和脚本注入非常相似，但必须要诱使受害者点击链接才能得以执行与脚本注入的不同 用于脚本注入的恶意脚本提交后，将存储在服务器数据库中，导致每个访问问题页面的浏览者都将遭到恶意脚本的攻击而跨站攻击多数情况是将恶意脚本构造于url参数中，通过欺骗的方式去诱使受害者点击链接，使得恶意脚本执行虽然Web站点上存在安全漏洞，但是Web站点从未受到直接伤害漏洞难于查找，特别容易被忽略cross-sitescripting，简称XSS513）跨站点攻击跨站攻击和脚本注入非常相似，但必须要诱使受害者恶意攻击者（这里使用E表示）通过E-mail或HTTP将某银行的网址链接发给用户（银行用表示），该链接中附加了恶意的脚本（上图步骤1）用户访问发来的链接，进入银行网站，同时，嵌在链接中的脚本被用户的浏览器执行（上图步骤2、3）用户在银行网站的所有操作，包括用户的cookie和session信息，都被脚本收集到，并且在用户毫不知情的情况下发送给恶意攻击者（上图步骤4）恶意攻击者使用偷来的session信息，伪装成该用户，进入银行网站，进行非法活动（上图步骤5）52恶意攻击者（这里使用E表示）通过E-ma4）代码分析找出所有的系统输入位置，确定可能的攻击界面用户输入数据库配置文件网络服务命令行注册表……..

目标系统534）代码分析找出所有的系统输入位置，确定可能的攻击界面目标系对所有的输入进行验证语法检查：格式是否正确，特殊字符过滤 白名单、黑名单语义检查：输入是否恰当分析污染传播使用数据流分析判断攻击者能控制的值污染传播模式 源：read(),getenv();getpass()等接收器：Statement.executeQuery(),strcpy(); 传递：trim(); ……54对所有的输入进行验证54NationalVulnerabilityDatabase（国家漏洞数据库）55NationalVulnerabilityDatabas第十一讲高效的静态分析---符号执行与缺陷模式56第十一讲1一、符号执行 1、符号执行简介 2、代表工具：PREfix二、缺陷模式 1、缺陷模式简介 2、安全漏洞内容57一、符号执行内容2

一、符号执行1、符号执行简介2、代表工具：PREfix58一、符号执行3intx,y;1:if(x>y){2:x=x+y;3:y=x-y;4:x=x-y;5:if(x>y)foo1();6:elsefoo2();}观察下面程序：有什么问题？59intx,y;观察下面程序：有什么问题？4J.C.King于1976年提出SymbolicExecution使用符号值，而不是实际数据，作为输入将程序变量的值表示为符号表达式程序计算的输出表达为输入符号值的函数1、符号执行简介60J.C.King于1976年提出Symbolic优点分析是路径敏感的因为没有对路径、状态做近似，结果精确适合做状态检查、时序检查对并发类型的错误十分有效缺点对所有可能的状态进行穷举搜索，开销大对系统的行为进行近似，可能导致这类结果不精确对于数据密集的系统分析困难在边界处对路径、时序属性近似困难，故复合困难模型检验61优点模型检验6优点由于对路径、状态进行抽象，扩展性好可以对许多有价值的属性构造格易于组合提供了坚实的数学基础缺点适合的属性需要是简单的、“状态”“值”型的对时序性质支持弱属性格的定义不容易有时近似过强抽象解释62优点抽象解释7优点支持灵活的属性易于扩展缺点开发人员需要提供额外的信息自动化程度不高路径不敏感，对并发系统不适合演绎方法（定理证明）63优点演绎方法（定理证明）8记录执行的状态，包括：程序变量的符号值路径条件（PC:PathCondition）程序标记（后面执行什么）路径条件非常重要积累了路径的约束条件符号执行树刻画程序符号执行过程中的执行路径符号执行64记录执行的状态，包括：符号执行9最初，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(X<Y)x:X+Y,y:Y(X>Y)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)&(Y<=X)例子：65最初，x与y分别具有符号值X、Yintx,符号执行可以被看作是路径敏感分析、演绎方法及抽象解释的组合对路径条件进行近似使得抽象解释的属性区间值收缩，因此更加灵活约束近似了许多状态，降低了分析量经常被应用于测试输入的生成传统上，符号执行对有限个整数变量进行符号化，后来扩展到了处理复杂的输入数据结构和并发例如，扩展JPF工具以进行符号执行Java程序66符号执行可以被看作是路径敏感分析、演绎方法及抽象解释的组合2、典型工具：PREfix1）基本特点2）主要思路3）主要步骤672、典型工具：PREfix1）基本特点12模拟执行单个的函数！模拟过程顺序地跟踪不同的执行路径，模拟每个操作符的动作。在路径执行过程中，通过跟踪内存的状态，应用各种一致性规则，查找不一致性。在对条件选择后，通过检查内存的当前状态，分析器可以限制可达的路径。由于对路径、值的跟踪都很仔细，可以获得精确的信息。函数的行为被描述为：条件、一致性规则及表达式值的集合。行为的这种描述被称为函数的一个模型。在路径执行过程中，不论何时进入一个函数，该模型被使用，以决定应用哪个操作1）基本特点68模拟执行单个的函数！1）基本特点13在模拟过程中产生的信息足够自动地产生该函数的一个模型为在整个程序中应用这些技术，分析起始于调用图的叶节点，自底向上地向根处理。随着函数被逐层模拟，缺陷被不断发现，函数模型被高层的后续模拟所使用这种自底向上的方法使用一个函数的实现来产生函数的约束，供上层使用。这对于程序不完整时（程序还没有开发完，或者被分析的代码需要适合多个不同的程序）尤其有效69在模拟过程中产生的信息足够自动地产生该函数的一个模型142）主要思路1#include<stdlib.h>2#include<stdio.h>34char*f(intsize)5{6char*result;78if(size>0)9result=(char*)malloc(size);10if(size==1)11returnNULL;12result[0]=0;13returnresult;14}观察右边代码有什么问题？702）主要思路1#include<stdlib.h>观1#include<stdlib.h>2#include<stdio.h>34char*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,被分配的内存未被释放，也未被返回。711#include<stdlib.h>example1#include<stdlib.h>2#include<stdio.h>34char*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‘size<=0’herePathincludes3statementsonthefollowinglines:81012错误消息2：当size<=0时，函数试图解析一个未被初始化的指针（mallocinline9willnotbeexecuted).721#include<stdlib.h>example1#include<stdlib.h>2#include<stdio.h>34char*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指针时，对其赋值出现错误731#include<stdlib.h>examplewhile(therearemorepathstosimulate){initializememorystatesimulatethepath,identifyinginconsistenciesandupdatingthememorystateperformend-of-pathanalysisusingthefinalmemorystate,identifyinginconsistenciesandcreatingper-pathsummary}combineper-pathsummariesintoamodelforthefunction算法伪代码：74while(therearemorepathsto模拟单个函数需要模拟可达的路径。可达路径的集合包含所有可能的控制流路径集合。这个集合的大小往往小于明显的控制流路径。因为相同的条件往往控制多个条件模块。通常可以选择有代表性的路径来模拟。具体路径数可以由用户进行配置模拟一条路径涉及遍历函数的抽象语法树，对树上相关的语句、表达式求值。被模拟函数的内存状态随着语句的执行被不断更新。许多缺陷(例如,未初始化的内存，NULL，或者无效的指针解析)可以通过在路径模拟过程中对内存的状态应用一致性规则发现。其他(例如，内存泄漏，将指针返回给一个释放的内存)在到达路径终点时可以被发现当路径被模拟时，函数的最终内存状态被综合处理(summarized)。当所有的路径被模拟后，per-pathsummaries被组成一个函数的模型75模拟单个函数需要模拟可达的路径。可达路径的集合包含所有可能的3）主要步骤路径路径跟踪很容易发现一些问题路径中包括“功能调用、语句、结果”模拟执行是基于路径进行的为定位缺陷提供依据但不一定是唯一的路径可能是多条路径累积的结果1#include<stdlib.h>2#include<stdio.h>34char*f(intsize)5{6char*result;78if(size>0)9result=(char*)malloc(size);10if(size==1)11returnNULL;12result[0]=0;13returnresult;14}当size<=0时，函数试图解析一个未被初始化的指针（mallocinline9willnotbeexecuted).763）主要步骤路径1#include<stdlib.h内存（变量）：值与断言模拟过程中函数使用的内存需要尽可能准确地跟踪每块内存都有值：3个基本状态知道准确的值（常量）有一个初始化的值，但不知道准确的值未初始化的值断言（predicate）也可能与值关联断言可能是由1到3部分组成单个：initialized两个：x>3三个：a=b+c77内存（变量）：值与断言22内存操作：求值、测试与设置设置(setting)将一个值赋给内存，改变了内存的状态简单推理：(a>3&b>4)=>a+b>7测试(testing)在一定的上下文中对表达式求值，得到一个布尔结果。需要进行测试的三种情形：需要判定表达式，以得到一个布尔结果(例如：条件分支)语言语义要求（例如：使用前必须初始化）在模型中选择可能的输出(例子见后面关于“模型”的内容)78内存操作：求值、测试与设置23条件(condition)、假定(assumption)与选择点条件可以比路径更清晰地描述缺陷在路径模拟执行过程中，条件对应于假定当变量出现在一个表达式中、且值不确定时，可以进行假定例子中的“size”:输入参数，模拟是自底向上进行的出现两个假定，分别模拟执行，并记忆当前假定当作出一个假定时，相关内存的状态被更新这个假定可能提高其它断言的准确性对于a=b+5,当假定条件表达式a==2为真时，a对应的内存状态更新为2，b对应的内存状态可以更新为-3。此时，控制流没有由已知的值完全确定下来，被称为选择点79条件(condition)、假定(assumption)与选路径结尾分析当一条路径中的所有语句被模拟执行后，可以进行一些附加分析发现一些缺陷。例如：内存没有释放等等多路径分析一条长的路径可能因为调用而包含多条子路径需要分别分析为控制总体数目，可以设置上限路径选择是一个问题80路径结尾分析多路径分析25模型模型模拟了函数的行为模拟器遇到一个函数调用时，它通过函数的模型来模拟被调用的函数函数的模型主要是一组输出集合，这些输出代表了函数计算时对内存状态的可能改变每个输出由Guards,Constraints,Results构成约束（Constraint）是前置条件：fopen的参数必须有效结果（Result）是后置条件：fopen执行后返回值有效防卫（Guards）是测试：某个特定的输出可能依赖某个输入intknot(intj){if(j==0)return1;return0;}例子：返回值只有在“j==0”时为“1”只有在“j!=0”时为“0”81模型intknot(intj)例子：返回值只有在“j=(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}一个模型的例子：82(deref1intderef(int*p)一个模型的Warning MozillaApache GDIUsinguninitializedmemory 26.14%45%69%Dereferencinguninitializedpointer 1.73%00DereferencingNULLpointer 58.93%50%15%Dereferencinginvalidpointer 05%0Dereferencingpointertofreedmemory 1.98%00Leakingmemory 9.75%00Leakingaresource(suchasafile) 0.09%08%Returningpointertolocalstackvariable0.52%00Returningpointertofreedmemory 0.09%00Resourceininvalidstate 008%Illegalvaluepassedtofunction 0.43%00Dividebyzero 0.35%00Totalnumberofwarnings 11592013效果(1998)：Mozilla1.0,Apache1.3beta583Warning MozillaApache二、缺陷模式 1、缺陷模式简介 2、安全漏洞84二、缺陷模式 1、缺陷模式简介291、缺陷模式简介1）缺陷模式概述2）LibraryInterface（库接口）3）主要技术是什么？851、缺陷模式简介1）缺陷模式概述30显式的与隐式的独立的与嵌入式的（annotatioin）私有的与共性的模式： 设计模式 分析模式 过程模式 …… 86显式的独立的私有的模式：31分析算法从事的是举重的工作模式辨识从事的是射击的事情待查代码代码模型分析算法缺陷知识缺陷报告87分析算法从事的是举重的工作待查代码代码模型分析算法缺陷知识缺与具体应用“无关”的知识词法或者语法共性特性（死锁、空指针、内存泄露、数组越界）公共库用法（顺序、参数、接口实现，容错，安全）与具体应用“相关”的知识类型定义（操作格式，不含其它信息（信息隐藏））类型约束（调用的顺序、参数值，接口实现）需求相关（正确）定理证明符号执行模型检查模型检查抽象解释侧重点在技术（算法）方面！88与具体应用“无关”的知识定理证明符号执行模型检查模型检查抽象能侧重在知识上吗？Google翻译的启示！89能侧重在知识上吗？Google翻译的启示！341）缺陷模式概述代码必须遵守各类约束如果违反，就是缺陷对不同约束的违反，构成了不同的缺陷模式约束分类BNF：宪法共性约束（库接口）：国家法律、条例等特定软件的约束（类型）：地方法律、条例901）缺陷模式概述代码必须遵守各类约束352）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. 空集问题912）LibraryInterface（库接口）1.错误代调用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时使用“==“或者”<=“。比较String.indexOf()和0是滥用“>”和“<”。在例如if和while的逻辑表达式中误用了操作符“=”、“&”和“|”。正确的的应该是“==”、“&&”和“||”。当某个实例不属于某个类型时使用了instanceof操作：单一方法调用：92调用SimpleDateFormat的构造函数时没有传递Lo某些类中必须成对使用的方法（必须有严格的顺序）：例如I/O对象中的open和close。时序方法的约束。初始化错误。使用负数索引或者超过数组长度的索引值引发了数组溢出。更多缺陷模式，请访问：同一个类的多方法调用:93某些类中必须成对使用的方法（必须有严格的顺序）：例如I/O对使用约束栈DBMS接口约束操作系统接口约束中间件接口约束应用软件语言约束约束（BNF、基本函数）94使用约束栈DBMS接口约束操作系统接口约束中间件接口约束应用3）主要技术是什么？如何在目标代码中查找已知的模式？先做基本扫描：有相近的代码？再努力提高准确度如何描述缺陷模式？自然语言形式化：时序逻辑等半形式化/图形化953）主要技术是什么？如何在目标代码中查找已知的模式？如何描述DEFECTPATTERNINPUTExtensibilityYesNoRepresentationDescriptionfileEmbeddedcode涉及的主要技术TARGETPROGRAMINPUTJavaProgrammingLanguageRepresentationC/C++SourcecodeCompiledfilePropertyConcernedUnusedcodeCodestyleTemporalpropertyConcurrencyOtherSEMANTICANALYSISControlFlowAnalysisDataFlowAnalysisStructureAnalysisCallGraphAnalysisOUTPUTRepresentationTextreportXML/HTMLreportInteractiveGUIEvaluationforResultSoundnessCompletenessOtherPoint-toAnalysis96DEFECTPATTERNINPUTExtensibil特点缺陷定位准确查找