跳至內容

靜態程序分析

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

靜態程序分析(英語: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). 

書目

[編輯]