中國移動(深圳)有限公司 | 鐘昌杰
軟件靜態(tài)安全檢測技術研究
中國移動(深圳)有限公司 | 鐘昌杰
軟件安全問題日益嚴重,靜態(tài)安全檢測提供了從軟件結構和代碼中尋找漏洞的方法。
安全性是軟件質量的一個重要屬性。軟件安全性是軟件在受到惡意攻擊時仍提供所需功能的能力。多數軟件的安全性問題主要源自于本身,其自身的漏洞往往被攻擊者利用,從而成為軟件安全的隱患。軟件安全檢測技術的主要作用就是檢測軟件中存在的安全問題,從而指導軟件進行安全性能的改善。
安全性相關缺陷不同于一般的軟件缺陷。一個很難發(fā)現的軟件安全漏洞可能導致大量用戶受到影響。安全性測試不同于傳統測試類型最大的區(qū)別是它強調軟件不應當做什么,而不是軟件要做什么,例如未授權用戶不能訪問數據。
軟件安全性測試可分為安全功能測試和安全漏洞測試兩個方面。
安全功能測試基于軟件的安全功能需求說明,測試軟件的安全功能實現是否與安全需求一致,包括數據機密性、完整性、可用性、不可否認性、身份認證、授權、訪問控制、審計跟蹤、委托、隱私保護、安全管理等。
安全漏洞測試從攻擊者的角度,以發(fā)現軟件的安全漏洞為目的。安全漏洞是指系統在設計、實現、操作、管理上存在的可被利用的缺陷或弱點。漏洞被利用可能造成軟件受到攻擊,使軟件進入不安全的狀態(tài),安全漏洞測試就是識別軟件的安全漏洞。
目前測評中心的安全測試工作就是要發(fā)現中國移動業(yè)務支撐系統存在的安全漏洞,對于軟件安全的檢測,通常可以按照檢測過程中是否需要執(zhí)行程序的標準分為動態(tài)測試和靜態(tài)測試兩種,本文針對軟件靜態(tài)安全檢測技術進行深入研究。
靜態(tài)代碼安全分析的第一步,是根據分析需求把程序源代碼變換成易于分析處理的程序模型,這個過程用到了編譯原理中的成熟技術。
● 詞法分析:使用正則表達式匹配將源代碼轉換為等價的符號流。
● 語法分析:使用上下文無關語法將符號流規(guī)整為語法樹,作為源代碼邏輯結構的最直接的表現。
● 抽象語法分析:通過簡化語法將語法樹轉換為包含更少節(jié)點和分支的抽象語法樹,以方便后續(xù)處理。
● 語義分析:從抽象語法樹建立符號表,為每個標識符關聯類型信息。至此,已經具備了足夠的信息來進行所謂的結構化分析。編譯器通常將抽象語法樹和符號表轉化成易于優(yōu)化的中間形式,然后送給后端生成平臺相關的目標代碼。安全分析工具可以建立更高階的中間形式,或者直接在抽象語法樹和符號表上進行后續(xù)步驟。
在分析模型建立后,就可以開始進行靜態(tài)檢測了。從早期的緩沖區(qū)溢出檢測開始,十幾年來出現了各種檢測技術,早期靜態(tài)檢測主要指靜態(tài)分析,隨著形式化驗證方法的引入,靜態(tài)檢測引入了程序抽象驗證方法。
靜態(tài)分析直接分析被測程序特征,尋找可能導致錯誤的異常。
規(guī)則檢查 程序本身的安全性可由安全規(guī)則描述。程序本身存在一些編程規(guī)則,即一些通用的安全規(guī)則,也稱之為漏洞模式,比如程序在root權限下要避免exec調用。規(guī)則檢查方法將這些規(guī)則以特定語法描述,由規(guī)則處理器接收,并將其轉換為分析器能夠接受的內部表示,然后再將程序行為進行比對、檢測。
類型推導 自動推導程序中變量和函數的類型,來判斷變量和函數的訪問是否符合類型規(guī)則。靜態(tài)漏洞檢測的類型推導由定型斷言、推導規(guī)則和檢查規(guī)則3個部分組成。定型斷言定義變量的初始類型,推導規(guī)則提供了推論系統的規(guī)則集合,檢查規(guī)則用于判定推論結果是否為“良行為”。
程序驗證方法通過使用形式化驗證技術驗證正確性的方式來檢測漏洞。
模型檢測對有限狀態(tài)的程序構造狀態(tài)機或有向圖等抽象模型,再對模型進行遍歷以驗證系統特性。一般有2種驗證方式:
● 符號化方法將抽象模型中的狀態(tài)轉換為語法樹描述的邏輯公式,然后判定公式是否可滿足。
● 模型轉換成自動機,并將需要檢查的安全時序屬性轉換為等價自動機,再將這兩個自動機取補,構成一個新的自動機,判定問題就變成檢查這個新自動機能接受的語言是否為空。
模型檢測需要列舉所有可能狀態(tài),由于軟件本身的高復雜度,對所有程序點進行建模可能會使模型規(guī)模龐大,因此一般只針對程序中某一方面屬性構造抽象模型。近期出現的一種模型檢測方法通過對內存狀態(tài)的建模,從而使原先主要檢測時序相關漏洞的模型檢測方法可對內存相關漏洞進行相關檢測。
定理證明比模型檢測的形式化方法更加嚴格,用各種判定過程來驗證程序抽象公式是否為真。判別的方法取決于公式的形式,如不等式的合取:首先由合取式構造成一個圖,合取式中每個條件對應于圖中的一個節(jié)點,然后利用給出的等式將對應的頂點合并,在頂點合并的過程中對合取式中的不等式進行檢查,如發(fā)現存在不成立,則該合取式不可滿足。
符號執(zhí)行的基本思想是將程序中變量的值邏輯轉換成抽象符號,模擬路徑敏感的程序控制流,通過約束求解的辦法,檢測是否有發(fā)生錯誤的可能。由程序執(zhí)行前的條件P出發(fā),在程序中某程序點,可推出約束條件C1∧C2∧…∧Cn ,因此在該點有P∧ Cl∧ C2∧…∧Cn->R這樣的規(guī)約式,其中R是程序結束后要滿足的條件。對該規(guī)約式的否命題求解,如有一組解滿足,說明在這個程序點上存在一組變量狀態(tài),使運行程序的結果不符。符號執(zhí)行求解工具的約束條件集合及求解能力決定了其發(fā)現錯誤的能力。理論上很多約束問題在可接受時間級內是不可解的,因此,符號執(zhí)行求解的方法只適用于某些特定問題求解上。
最終的報告并非安全缺陷的簡單總結,還應該幫助用戶判斷缺陷報告的正確性和缺陷的嚴重性,并給出適當的修復建議。從易用性考慮,缺陷報告應該支持分組、排序、屏蔽特定結果等操作。
靜態(tài)檢測技術目前的發(fā)展趨勢是將靜態(tài)檢測的各種技術進行結合,以提高性能。結合方式有以下幾種方法:
● 提供一個框架,使用不同檢測技術對程序進行檢測,獲取大量檢測結果之后進行分析。從誤報率來說,使用多種技術的檢測結果的交集來進行漏洞判斷決策,可減少誤報率。從漏報率來說,對于同一種漏洞,使用多種檢測技術的結果的并集可以減少漏報率。
● 直接在檢測技術上結合,通過技術的結合來得到新的方法,如在符號執(zhí)行的過程中加入類型推導的技術,在變量模擬執(zhí)行的過程中增加其類型特征的推導,可獲取更高的漏洞檢測率。