靜態程序分析

维基百科,自由的百科全书
跳转至: 导航搜索

靜態程序分析英语Static program analysis)是指在不執行计算机程序的條件下,進行程序分析的方法。有些程序分析需要在程序執行時才能進行,這種程序分析稱為動態程序分析英语dynamic program analysis[1]。大部份的靜態程序分析的對象是針對特定版本的源代码,也有些靜態程序分析的對象是目标代码。靜態程序分析一詞多半是指配合靜態程序分析工具進行的分析,人工進行的分析一般稱為程式理解英语program comprehension代码审查

靜態程序分析的複雜程度依所使用的工具而異,簡單的只考慮個別敘述及宣告的行為,複雜的可以分析程序的完整源代码。不同靜態程序分析產生的資訊也有所不同,簡單的可以是標示可能的代碼錯誤(如lint),複雜的可以是形式化方法,也就是用數學的方式證明程式的某些行為符合其設計規格。

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

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

  1. 醫療軟體:美國的美国食品药品监督管理局確定在醫療設備上使用靜態程序分析[3]
  2. 核能軟體:英國的健康与安全委员会英语Health and Safety Executive建議針對堆保护系统英语Reactor Protective System的軟體進行靜態程序分析中[4]

在資訊安全的領域中,靜態程序分析會稱為靜態應用程式安全檢測Static Application Security Testing,簡稱SAST)。

形式化方法[编辑]

形式化方法是一種利用純粹數學的方式分析軟體的方法,應用到的數學技巧包括指稱語義公理語義英语axiomatic semantics操作语义学抽象释义計算機科學中的方法。

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

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

相關條目[编辑]

參考資料[编辑]

  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. http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf
  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]. 
  4. ^ Computer based safety systems - technical guidance for assessing software aspects of digital computer based protection systems, http://www.hse.gov.uk/foi/internalops/nsd/tech_asst_guides/tast046app1.htm

書目[编辑]