跳转到内容

静态程序分析

本页使用了标题或全文手工转换
维基百科,自由的百科全书

静态程序分析(英语: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). 

书目

[编辑]