跳转到内容

靜態程序分析

本页使用了标题或全文手工转换
维基百科,自由的百科全书
(重定向自靜態程式分析

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

書目