靜態程序分析
靜態程序分析（英語：）是指在不執行计算机程序的條件下，進行程序分析的方法。有些程序分析需要在程序執行時才能進行，這種程序分析稱為動態程序分析[1]。大部份的靜態程序分析的對象是針對特定版本的源代码，也有些靜態程序分析的對象是目标代码。靜態程序分析一詞多半是指配合靜態程序分析工具進行的分析，人工進行的分析一般稱為程式理解或代码审查。
靜態程序分析的複雜程度依所使用的工具而異，簡單的只考慮個別语句及声明的行為，複雜的可以分析程序的完整源代码。不同靜態程序分析技术对分析得到的資訊的用途也有所不同，簡單的可以是高亮标识可能存在的代碼錯誤（如lint），複雜的可以是形式化方法，也就是用數學的方式證明程式的某些行為符合其設計规约。
軟體度量和反向工程可以視為一種靜態程序分析的方式。在實務上，在定義所謂的軟體品質指標（software quality objectives）後，軟體度量的推導及程序分析常一起進行，在開發嵌入式系統時常會用這種方式進行。
靜態程序分析的商業用途可以用來驗證安全關鍵電腦系統中的軟體，並指出可能有计算机安全隐患的程式碼，這類的應用越來越多。[2]例如以下的產業已確定用靜態程序分析作為提昇複雜軟體品質的方法：
- 醫療軟體：美國的美国食品药品监督管理局確定在醫療設備上使用靜態程序分析[3]。
- 核能軟體：英國的健康与安全委员会建議針對堆保护系统的軟體進行靜態程序分析中[4]。
在資訊安全的領域中，靜態程序分析會稱為靜態應用程式安全檢測（Static Application Security Testing，簡稱SAST）。
形式化方法
形式化方法是一種利用純粹數學的方式分析軟體的方法，應用到的數學技巧包括指稱語義、公理語義、操作语义学及抽象释义等計算機科學中的方法。
針對任何图灵完全的程式語言，不可能存在一演算法可以找出任意程式在執行期間的所有錯誤，也沒有數學方法可以得到一程式是否會有執行期間的錯誤的結果。上述的結論是由庫爾特·哥德爾、阿隆佐·邱奇及阿蘭·圖靈在1930年代研究停機問題所得的結果。不過如同許多不可判定问题一様，在實務仍會設法找到有用的近似解。
以下是一些形式化靜態分析的實現方式：
- 模型檢查針對有有限狀態或是可以用抽象化簡化為有限狀態的系統。
- 数据流分析可以收集有關程式在不同點計算所得的可能數值。
- 抽象释义可以被看作对计算机程序的部分执行，获取关于它的语义信息（比如，控制结构、信息流）而不进行所有计算。Frama-c及Polyspace等工具主要是以抽象释义為基礎。
- 在程式碼中加入斷言，此方法最早是由霍尔逻辑提出。有些程式語言有對應的支援工具，例如SPARK（Ada程式語言的子集）、Java 建模语言（其中使用ESC/Java及ESC/Java2）及針對C語言的Frama-c WP 插件（最弱初始條件），此插件需配合延伸至ACSL（ANSI/ISO C Specification Language）的C語言。
參考資料
- 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）.
- 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 页面存档备份，存于
- FDA. . Food and Drug Administration. 2010-09-08 [2010-09-09]. （原始内容存档于2010-09-01）.
- Computer based safety systems - technical guidance for assessing software aspects of digital computer based protection systems, . [2008-07-31]. （原始内容存档于2008-07-31）.
書目
- Syllabus and readings for Alex Aiken’s Stanford University CS295 course.
- Nathaniel Ayewah, David Hovemeyer, J. David Morgenthaler, John Penix, William Pugh, “Using Static Analysis to Find Bugs 页面存档备份，存于,” IEEE Software, vol. 25, no. 5, pp. 22-29, Sep./Oct. 2008, doi:10.1109/MS.2008.130
- Brian Chess, Jacob West (Fortify Software). . Addison-Wesley. 2007. ISBN 978-0321424778.
- Flemming Nielson, Hanne R. Nielson, Chris Hankin. . Springer. 1999, corrected 2004. ISBN 978-3540654100.
- “Abstract interpretation and static analysis,” International Winter School on Semantics and Applications 2003, by David A. Schmidt