程序分析
此條目需要補充更多來源。 (2018年2月1日) |
此條目翻譯自其他語言維基百科,需要相關領域的編者協助校對翻譯。 |
在計算機科學中,程序分析[1]是指自動分析一個程序的包括正確性、健壯性、安全性和活躍性等特徵的過程。 程序分析主要研究兩大領域:程序的優化和程序的正確性。前者研究如何提升程序性能並且降低程序的資源占用,後者研究如何確保程序完成預期的任務。
靜態程序分析
在程序正確性里,靜態分析可以在程序的開發階段就發現漏洞[2]。這些漏洞通常比測試階段發現的漏洞更容易修復,因為靜態分析可以直接發現漏洞的根源。
由於很多靜態分析其實無法確切地判定,因此實現靜態分析的機制不總返回正確的結果——要麼是返回了一個假陰性(返回「沒有發現問題」然而程序其實存在問題)或者是返回了一個假陽性,要麼它們不返回錯誤的結果但是有時候不會終止。儘管它們或多或少地存在種種不足,然而前者可能幫助降低漏洞的數量,而後者則在一些時候可以明確確定程序不受某類漏洞的威脅。
不正確的優化是誰都不希望的,所以在程序優化里,有兩類策略來處理無法判定的分析情況:
- 設計一個優化器時,如果認為它應該很快完成它的任務(例如編譯器里的優化器),那麼可以用一個削減過的分析算法來保證可以在一個有限的時間內完成,並且保證只做正確的優化。
- 一個第三方的優化器可能會被設計為永遠不會輸出一個錯誤的優化,但是有時候可能在找到正確的優化前永遠都不會停下來(可能永遠也找不到)。這種時候,開發者可能需要關掉這一工具並且避免它再次在要優化的代碼上運行(或者也可以修改代碼來避免觸發這個工具)。
然而,還有第三種策略有時可以用於一些規範不夠完整的語言(比如C語言)。一個做優化的編譯器在遇到未定義行為時,可以自主選擇如何生成這部分代碼。生成的代碼可以在運行時做任何事情,甚至可以崩潰。
控制流
控制流分析的目的是獲取在程序執行時一些特定位置可能調用的函數的信息。這些信息由控制流圖(英語:control flow graph,簡稱CFG)來表示,其中節點表示程序的指令,邊表示控制流。 通過識別代碼塊和循環,CFG常常被編譯器當作優化的起始點。
數據流分析
數據流分析收集程序運行到不同位置時各個值的信息和它們隨時間變化的信息。這一技巧也常被編譯器用來優化代碼。 一個有名的數據流分析的例子叫做污點檢驗,它考慮所有的可能被使用者修改的變量(也就是有「污點」、不安全的變量),並阻止這些變量在被「消毒」前被使用。這一技巧常被用來避免SQL注入攻擊。污點檢驗既可以靜態完成也可以動態完成。
抽象釋義
抽象釋義允許在不執行程序時提取出某個可能的執行的信息。 這個信息可以讓編譯器尋找某條可行的優化路徑,也可以證明一個程序不會存在某些問題。
類型系統
類型系統給程序關聯上滿足特定條件的類型。類型系統的目的是選出一個程式語言編寫的程序的一個子集,使這個子集滿足特定的性質。
- 類型檢查——驗證一個程序是否被類型系統接受
類型檢查被用來限制程序中一個對象如何被使用以及一個對象能做什麼。類型檢查是由編譯器或解釋器完成的。類型檢查也可以幫助避免如將有符號變量賦值給無符號變量所帶來的漏洞。 類型檢查可以靜態完成(在編譯期間),也可以動態完成(在運行時),或者結合二者。
靜態類型信息(可以通過類型推論,或者由代碼明確給出)也可以被用來做優化,例如把封包的數組替換為未封包的數組。
作用系統
作用系統是一類用來給出函數或方法的作用的形式化系統。一個作用(英文:effect)規定了做了什麼以及對誰做了——通常稱之為作用類型(英文:effect kind)以及作用範圍(英文:region)。
模型檢查
模型檢查指一類嚴格、形式化並且自動的檢查一個模型(在這裡指一段代碼的形式化模型,但在其他語境下也可以指一個硬體的模型)是否符合給定規範的方法。基於代碼內在狀態有限這一特點,且規範和代碼都可以被轉換為邏輯公式,我們有能力用算法來檢查一個系統是否違反規範。
動態程序分析
動態程序分析可以用程序運行時的信息來提高分析的精度並且提供運行時保護,然而它只能分析單次運行的情況,並且可能因為進行運行時檢查而降低運行性能。
測試
每個軟體都應當被測試來確保其質量,保證其按照期望穩定運行,並且確保其不會與其他軟體衝突。測試一般通過運行程序並給定一組輸入然後來評估程序給出的輸出。 即使軟體沒有指定好的安全性要求,也應當對其進行額外的安全性測試從而保證攻擊者無法隨意修改軟體並盜取數據、妨礙軟體的正常工作或者用它當作攻擊其他用戶的跳板。
監控
程序監控會記錄程序的諸多信息(例如資源占用、事件、交互等),使之可以在之後被用來尋找或定位異常行為的原因。此外,它還可以被用來做安全審查。程序的自動監控有時也被稱為運行時檢查。
程序切片
對於一個給定的程序的行為的子集,程序切片將程序削減到保持給定行為的最小形式。被削減後的程序被稱之為一個「切片」,是原程序在給定行為子集上的一個正確表示。 通常而言,找到切片是一個無法解決的問題。但是通過給定一組變量的值的行為的子集,有可能通過數據流算法來找到大約符合條件的切片。這些切片通常被開發者用來調試從而找到錯誤的原因。
參考文獻
延伸閱讀
- Agrawal, Hiralal; Horgan, Joseph R. Dynamic program slicing.
- Chunlei, Wang; Gang, Zhao; Yiqi, Dai. An Efficient Control Flow Security Analysis Approach for Binary Executables.
- Nielson, Flemming; Nielson, Hanne Riis; Hankin, Chris. Principles of Program Analysis. Springer Science+Business Media. 2005.