第十一講高效的靜態分析---符號執行與缺陷模式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特點缺陷定位準確查找