跳至內容

靜態程式分析

本頁使用了標題或全文手工轉換
維基百科,自由的百科全書

靜態程式分析(英語:Static program analysis)是指在不執行程式的條件下,進行程式分析的方法。和要在程式執行時才能進行的動態程式分析英語dynamic program analysis是不同的[1]。大部份的靜態程式分析的對象是針對特定版本的原始碼,也有些靜態程式分析的對象是目標碼。靜態程式分析一詞多半是指配合靜態程式分析工具進行的分析,人工進行的分析一般稱為程式理解代碼審查

靜態程式分析的複雜程度依所使用的工具而異,簡單的只考慮個別陳述式及聲明的行為,複雜的可以分析程式的完整原始碼。不同靜態程式分析技術對分析得到的資訊的用途也有所不同,簡單的可以是突顯標識可能存在的代碼錯誤(如lint),複雜的可以是形式化方法,也就是用數學的方式證明程式的某些行為符合其設計規約。

軟件度量反向工程可以視為一種靜態程式分析的方式。在實務上,在定義所謂的軟件質素指標(software quality objectives)後,軟件度量的推導及程式分析常一起進行,在開發嵌入式系統時常會用這種方式進行。

靜態程式分析的商業用途可以用來驗證安全關鍵電腦系統中的軟件,並指出可能有電腦安全隱患的程式碼,這類的應用越來越多。[2]例如以下的產業已確定用靜態程式分析作為提昇複雜軟件質素的方法:

  1. 醫療軟件:美國的美國食品藥品監督管理局確定在醫療裝置上使用靜態程式分析[3]
  2. 核能軟件:英國的健康與安全委員會英語Health and Safety Executive建議針對堆保護系統英語Reactor Protective System的軟件進行靜態程式分析中[4]

在資訊保安的領域中,靜態程式分析會稱為靜態應用程式安全檢測,簡稱SAST。

形式化方法

形式化方法是一種利用純粹數學的方式分析軟件的方法,應用到的數學技巧包括指稱語義公理語義操作語意學抽象釋義電腦科學中的方法。

針對任何圖靈完全的程式語言,不可能存在一演算法可以找出任意程式在執行期間的所有錯誤,也沒有數學方法可以得到一程式是否會有執行期間的錯誤的結果。上述的結論是由庫爾特·哥德爾阿隆佐·邱奇阿蘭·圖靈在1930年代研究停機問題所得的結果。不過如同許多不可判定問題一様,在實務仍會設法找到有用的近似解。

以下是一些形式化靜態分析的實現方式:

相關條目

參考資料

  1. ^ Industrial Perspective on Static Analysis. Software Engineering Journal Mar. 1995: 69-75Wichmann, B. A., A. A. Canning, D. L. Clutterbuck, L. A. Winsbarrow, N. J. Ward, and D. W. R. Marsh. 存档副本 (PDF). [2011-02-28]. (原始內容 (PDF)存檔於2011-09-27). 
  2. ^ Improving Software Security with Precise Static and Runtime Analysis, Benjamin Livshits, section 7.3 「Static Techniques for Security,」 Stanford doctoral thesis, 2006. http://research.microsoft.com/en-us/um/people/livshits/papers/pdf/thesis.pdf頁面存檔備份,存於互聯網檔案館
  3. ^ FDA. Infusion Pump Software Safety Research at FDA. Food and Drug Administration. 2010-09-08 [2010-09-09]. (原始內容存檔於2010-09-01). 
  4. ^ Computer based safety systems - technical guidance for assessing software aspects of digital computer based protection systems, 存档副本. [2008-07-31]. (原始內容存檔於2008-07-31). 

書目