热门问题
时间线
聊天
视角

程式分析

来自维基百科,自由的百科全书

Remove ads

電腦科學中,程式分析[1]是指自動分析一個程式的正確性、健壯性、安全性和活躍性等特徵的過程。 程式分析主要研究兩大領域:程式的最佳化英語Program optimization程式的正確性。前者研究如何提升程式效能並且降低程式的資源占用,後者研究如何確保程式完成預期的任務或不會發生某些異常(如空指標異常)。

程式分析可以在不執行程式的情況下進行(靜態程式分析),也可在執行時進行(動態程式分析英語Dynamic program analysis),或結合二者。

靜態程式分析

對於程式正確性任務,靜態分析可以在程式的開發階段就發現漏洞[2]。這些漏洞通常比測試階段發現的漏洞更容易修復,因為靜態分析可以直接發現漏洞的根源。

由於很多靜態分析其實無法確切地判定,因此實現靜態分析的機制不總返回正確的結果——要麼是返回了一個假陰性(返回「沒有發現問題」然而程式其實存在問題)或者是返回了一個假陽性,要麼它們不返回錯誤的結果但是有時候不會終止。儘管它們或多或少地存在種種不足,然而前者可能幫助降低漏洞的數量,而後者則在一些時候可以明確確定程式不受某類漏洞的威脅。

程式最佳化的正確性至關重要。所以在程式最佳化里,有兩類策略來處理無法判定的分析情況:

  1. 設計一個最佳化器時,如果認為它應該很快完成它的任務(例如編譯器里的最佳化器),那麼可以用一個削減過的分析演算法來保證可以在一個有限的時間內完成,並且保證只做正確的最佳化。
  2. 一個第三方的最佳化器可能會被設計為永遠不會輸出一個錯誤的最佳化,但是有時候可能在找到正確的最佳化前永遠都不會停下來(可能永遠也找不到)。這種時候,開發者可能需要關掉這一工具並且避免它再次在要最佳化的代碼上執行(或者也可以修改代碼來避免觸發這個工具)。

然而,還有第三種策略有時可以用於一些規範不夠完整的語言(比如C語言)。一個做最佳化的編譯器在遇到未定義行為時,可以自主選擇如何生成這部分代碼。生成的代碼可以在執行時做任何事情,甚至可以崩潰。

Remove ads

控制流

控制流分析的目的是取得在程式執行時一些特定位置可能呼叫的函式的資訊。這些資訊由控制流圖(英語:control flow graph,簡稱CFG)來表示,其中節點表示程式的指令,邊表示控制流。 通過辨識代碼塊和迴圈,CFG常常被編譯器當作最佳化的起始點。

資料流分析

資料流分析收集程式執行到不同位置時各個值的資訊和它們隨時間變化的資訊。這一技巧也常被編譯器用來最佳化代碼。 一個有名的資料流分析的例子叫做污點檢驗,它考慮所有的可能被使用者修改的變數(也就是有「污點」、不安全的變數),並阻止這些變數在被「消毒」前被使用。這一技巧常被用來避免SQL注入攻擊。污點檢驗既可以靜態完成也可以動態完成。

抽象釋義

抽象釋義允許在不執行程式時提取出某個可能的執行的資訊。 這個資訊可以讓編譯器尋找某條可行的最佳化路徑,也可以證明一個程式不會存在某些問題。

型別系統

型別系統給程式關聯上滿足特定條件的類型。型別系統的目的是選出一個程式語言編寫的程式的一個子集,使這個子集滿足特定的性質。

  • 型別檢查——驗證一個程式是否被型別系統接受

型別檢查被用來限制程式中一個對象如何被使用以及一個對象能做什麼。型別檢查是由編譯器或直譯器完成的。型別檢查也可以幫助避免如將有符號變數賦值給無符號變數所帶來的漏洞。 型別檢查可以靜態完成(在編譯期間),也可以動態完成(在執行時),或者結合二者。

靜態型別資訊(可以通過類型推論,或者由代碼明確給出)也可以被用來做最佳化,例如把封包的陣列替換為未封包的陣列。

作用系統

作用系統英語Effect systems是一類用來給出函式或方法的作用的形式化系統。一個作用(英文:effect)規定了做了什麼以及對誰做了——通常稱之為作用類型(英文:effect kind)以及作用範圍(英文:region)。

模型檢查

模型檢查英語Model checking指一類嚴格、形式化並且自動的檢查一個模型(在這裡指一段代碼的形式化模型,但在其他語境下也可以指一個硬體的模型)是否符合給定規範的方法。基於代碼內在狀態有限這一特點,且規範和代碼都可以被轉換為邏輯公式,我們有能力用演算法來檢查一個系統是否違反規範。

動態程式分析

動態程式分析英語Dynamic program analysis可以用程式執行時的資訊來提高分析的精度並且提供執行時保護,然而它只能分析單次執行的情況,並且可能因為進行執行時檢查而降低執行效能。

測試

每個軟體都應當被測試來確保其品質,保證其按照期望穩定執行,並且確保其不會與其他軟體衝突。測試一般通過執行程式並給定一組輸入然後來評估程式給出的輸出。 即使軟體沒有指定好的安全性要求,也應當對其進行額外的安全性測試從而保證攻擊者無法隨意修改軟體並盜取資料、妨礙軟體的正常工作或者用它當作攻擊其他使用者的跳板。

監控

程式監控會記錄程式的諸多資訊(例如資源占用、事件、互動等),使之可以在之後被用來尋找或定位異常行為的原因。此外,它還可以被用來做安全審查。程式的自動監控有時也被稱為執行時檢查英語runtime verification

程式切片

對於一個給定的程式的行為的子集,程式切片英語program slicing將程式削減到保持給定行為的最小形式。被削減後的程式被稱之為一個「切片」,是原程式在給定行為子集上的一個正確表示。 通常而言,找到切片是一個無法解決的問題。但是通過給定一組變數的值的行為的子集,有可能通過資料流演算法來找到大約符合條件的切片。這些切片通常被開發者用來除錯從而找到錯誤的原因。

參考文獻

延伸閱讀

參見

外部連結

Loading related searches...

Wikiwand - on

Seamless Wikipedia browsing. On steroids.

Remove ads