静态程序分析
在计算机科学中,与动态程序分析相反,在计算机科学中,静态程序分析(或静态分析)是对执行的计算机程序进行的分析,与动态程序分析相比,该程序在执行过程中执行。
该术语通常应用于由自动化工具执行的分析,其中人类分析通常称为“程序理解”,程序理解或代码审查。在最后的最后,还使用了软件检查和软件演练。在大多数情况下,该分析是对程序源代码的某些版本进行的,在其他情况下,对其对象代码进行了分析。
理由
工具执行的分析的复杂性因仅考虑单个陈述和声明的行为的分析而异,而这些分析是在其分析中包含程序的完整源代码的分析。从分析获得的信息的使用范围从突出可能的编码错误(例如,棉绒工具)到数学上证明有关给定程序属性的正式方法(例如,其行为与其规范相匹配)。
软件指标和逆向工程可以描述为静态分析的形式。通过定义所谓的软件质量目标,可以越来越多地部署软件指标和静态分析,尤其是在创建嵌入式系统的过程中。
静态分析的商业用途越来越多,是对安全 - 关键计算机系统中使用的软件的属性验证并找到潜在的脆弱代码。例如,以下行业已经确定了使用静态代码分析作为提高日益复杂且复杂软件质量的一种手段:
- 医疗软件:美国食品药品监督管理局(FDA)已确定使用静态分析对医疗设备的使用。
- 核软件:在英国,核监管办公室(ONR)建议在反应堆保护系统上使用静态分析。
- 航空软件(结合动态分析)。
- 汽车和机器(功能安全功能构成了每个汽车产品开发阶段的组成部分, ISO 26262 ,第8节)。
VDC Research在2012年的一项研究报告说,接受调查的嵌入式软件工程师中有28.7%使用静态分析工具,有39.7%的人希望在2年内使用它们。 2010年的一项研究发现,欧洲研究项目中有60%的采访开发人员至少使用了其基本IDE内置静态分析仪。但是,只有大约10%的人使用了其他其他(也许更高级)的分析工具。
在应用程序安全行业中,还使用了名称静态应用程序安全测试(SAST)。 SAST是安全开发生命周期(SDL)的重要组成部分,例如Microsoft定义的SDL和软件公司中的常见实践。
工具类型
OMG(对像管理小组)发表了一项有关软件质量测量和评估所需的软件分析类型的研究。该文档有关“如何根据CISQ建议提供弹性,安全,高效,易于更改IT系统”的文档描述了三个级别的软件分析。
- 单位水平
- 在特定程序或子例程中进行的分析,而无需连接到该程序的上下文。
- 技术水平
- 分析考虑了单位程序之间的交互,以获得整体程序的更全面和语义观点,以便发现问题并避免明显的误报。
- 系统级别
- 分析考虑了单位程序之间的交互,但不限于一种特定的技术或编程语言。
可以定义进一步的软件分析。
- 任务/业务层面
- 分析考虑了在软件系统内实施的业务/任务层条款,规则和流程作为企业或计划/任务层活动的一部分。这些元素是在不限于一种特定技术或编程语言的情况下实施的,在许多情况下,它们分布在多种语言上,但在静态提取和分析以进行任务保证的系统理解。
正式方法
形式方法是应用于软件(和计算机硬件)的分析的术语,其结果纯粹是通过使用严格的数学方法来获得的。所使用的数学技术包括表示语义,公理语义,操作语义和抽象解释。
通过简单地减少停止问题,可以证明(对于任何图灵完整的语言),在任意程序中找到所有可能的运行时错误(或更一般而言,任何形式的违反规范的最终结果违反了规格一个程序)是不可决定的:没有机械方法可以始终如实回答任意程序是否可能表现出运行时错误。这一结果可以追溯到1930年代教堂,哥德尔和图灵的作品(请参阅:停止问题和赖斯的定理)。与许多不确定的问题一样,人们仍然可以尝试提供有用的近似解决方案。
正式静态分析的一些实施技术包括:
- 抽象解释,以建模每个语句对抽像机器状态的影响(即,它基于每个语句和声明的数学属性“执行”软件)。这款抽象的机器过度评估了系统的行为:因此,使抽象系统更简单地以牺牲不完整为代价(并非原始系统的每个属性对抽象系统都是正确的)。但是,如果正确完成,抽象的解释是正确的(抽象系统的每个属性都可以映射到原始系统的真实属性)。
- 数据流分析,一种基于晶格的技术,用于收集有关可能值集的信息;
- Hoare Logic ,一种正式系统,具有一组逻辑规则,以严格地推理计算机程序的正确性。有一些编程语言的工具支持(例如, Spark编程语言( ADA的子集)和Java建模语言-JML - 使用ESC/Java和ESC/Java2 ,Frama-C WP(最弱的先决条件)插件语言使用ACSL( ANSI/ISO C规范语言)扩展。
- 模型检查,考虑具有有限状态或可以通过抽象将其降低到有限状态的系统;
- 符号执行,用于得出代表代码特定点突变变量值的数学表达式。
数据驱动的静态分析
数据驱动的静态分析使用大量代码来推断编码规则。例如,可以在Github上使用所有Java开源软件包来学习良好的分析策略。规则推理可以使用机器学习技术。也可以从大量过去的修复和警告中学习。
修复
静态分析仪会发出警告。对于某些类型的警告,可以设计和实施自动补救技术。例如,Logozzo和Ball提出了C# CCCHECK的自动补救措施。