静态程序分析
静态程序分析（英语：Static program analysis）是指在不运行程序的条件下，进行程序分析的方法。和要在程序运行时才能进行的动态程序分析是不同的[1]。大部分的静态程序分析的对象是针对特定版本的源代码，也有些静态程序分析的对象是目标代码。静态程序分析一词多半是指配合静态程序分析工具进行的分析，人工进行的分析一般称为程序理解或代码审查。
静态程序分析的复杂程度依所使用的工具而异，简单的只考虑个别语句及声明的行为，复杂的可以分析程序的完整源代码。不同静态程序分析技术对分析得到的信息的用途也有所不同，简单的可以是高亮标识可能存在的代码错误（如lint），复杂的可以是形式化方法，也就是用数学的方式证明程序的某些行为符合其设计规约。
软件度量和反向工程可以视为一种静态程序分析的方式。在实务上，在定义所谓的软件质量指针（software quality objectives）后，软件度量的推导及程序分析常一起进行，在开发嵌入式系统时常会用这种方式进行。
静态程序分析的商业用途可以用来验证安全关键计算机系统中的软件，并指出可能有计算机安全隐患的代码，这类的应用越来越多。[2]例如以下的产业已确定用静态程序分析作为提升复杂软件质量的方法：
- 医疗软件：美国的美国食品药品监督管理局确定在医疗设备上使用静态程序分析[3]。
- 核能软件：英国的健康与安全委员会建议针对堆保护系统的软件进行静态程序分析中[4]。
在信息安全的领域中，静态程序分析会称为静态应用程序安全检测，简称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. Infusion Pump Software Safety Research at 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). Secure Programming with Static Analysis. Addison-Wesley. 2007. ISBN 978-0321424778.
- Flemming Nielson, Hanne R. Nielson, Chris Hankin. Principles of Program Analysis. Springer. 1999, corrected 2004. ISBN 978-3540654100.
- “Abstract interpretation and static analysis,” （页面存档备份，存于互联网档案馆） International Winter School on Semantics and Applications 2003, by David A. Schmidt （页面存档备份，存于互联网档案馆）