软件工程/质量/静态分析简介

静态程序分析是指在不实际执行由该软件构建的程序的情况下对计算机软件进行的分析（对正在执行的程序进行的分析称为动态分析）。在大多数情况下，分析是在源代码的某个版本上进行的，而在其他情况下，则是在目标代码的某种形式上进行的。该术语通常应用于由自动化工具执行的分析，而人工分析被称为程序理解、程序认知或代码审查。

工具执行的分析复杂程度各不相同，从仅考虑单个语句和声明的行为，到在分析中包含程序的完整源代码。从分析中获得的信息的使用范围从突出显示可能的编码错误（例如 lint 工具）到形式化方法，这些方法在数学上证明了关于给定程序的属性（例如，其行为与规范匹配）。

可以说，软件度量和逆向工程是静态分析的形式。

静态分析在商业上的一个越来越多的应用是在验证安全关键计算机系统中使用的软件的属性，以及定位可能存在漏洞的代码。例如，医疗软件越来越复杂，美国食品药品监督管理局（FDA）已将使用静态代码分析作为提高软件质量的一种手段。

形式化方法

形式化方法是应用于软件（和硬件）分析的术语，其结果完全通过使用严格的数学方法获得。使用的数学技术包括指称语义、公理语义、操作语义和抽象解释。

已证明，除了程序状态空间是有限的假设之外，查找所有可能的运行时错误，或者更一般地说，任何形式的违反程序最终结果规范的现象，都是不可判定的：不存在可以始终如一地正确回答给定程序是否可能或不可能出现运行时错误的机械方法。这一结果可以追溯到 1930 年代丘奇、库尔特·哥德尔和图灵的工作（见停机问题和 Rice 定理）。与大多数不可判定问题一样，人们仍然可以尝试给出有用的近似解。

形式化静态分析的一些实现技术包括

• 模型检验考虑具有有限状态或可以通过抽象简化为有限状态的系统；
• 数据流分析是一种基于格子的技术，用于收集有关可能值的集合的信息；
• 抽象解释模拟每个语句对抽象机器状态的影响（即它基于每个语句和声明的数学属性来“执行”软件）。这种抽象机器过拟合了系统的行为：因此，抽象系统变得更易于分析，但以不完整性为代价（并非原始系统的所有属性都对抽象系统成立）。但是，如果执行得当，抽象解释是可靠的（抽象系统的每个属性都可以映射到原始系统的真实属性）。Frama-c 框架和 Polyspace 很大程度上依赖于抽象解释。
• 正如 Hoare 逻辑首先建议的那样，在程序代码中使用断言。有些编程语言有工具支持（例如，SPARK 编程语言（Ada 的一个子集）和 Java 建模语言 - JML - 使用 ESC/Java 和 ESC/Java2，以及 C 语言的 ANSI/ISO C 规范语言）。

参考书目

• 课程大纲和读物，来自 Alex Aiken 的斯坦福 CS295 课程。
• Nathaniel Ayewah、David Hovemeyer、J. David Morgenthaler、John Penix、William Pugh，“使用静态分析查找错误” IEEE 软件，第 25 卷，第 5 期，第 22-29 页，2008 年 9/10 月，doi:10.1109/MS.2008.130
• Brian Chess、Jacob West（Fortify Software）（2007）。使用静态分析进行安全编程. Addison-Wesley. ISBN 978-0321424778.
• Adam Kolawa（Parasoft），静态分析最佳实践 白皮书
• 通过精确的静态和运行时分析改进软件安全，Benjamin Livshits，第 7.3 节“用于安全性的静态技术”，斯坦福博士论文，2006 年。
• Flemming Nielson、Hanne R. Nielson、Chris Hankin（1999 年，2004 年修正）。程序分析原理. 施普林格. ISBN 978-3540654100. {{cite book}}: 检查日期值：|year= (帮助)CS1 maint: multiple names: authors list (link)
• “抽象解释和静态分析，” 2003 年语义学与应用国际冬季研讨会，由 David A. Schmidt 主持

外部链接

• SAMATE 项目，自动化静态分析工具资源
• 将静态分析集成到软件开发流程中
• 代码质量改进 - 编码标准一致性检查（DDJ）
• 第 59 期：静态代码分析 采访（播客）来自软件工程广播
• 为编码标准实施自动化治理 解释了为什么以及如何将静态代码分析集成到构建流程中