程序静态分析

代码分析技术程序静态分析01分析技术实践静态分析工具形式化方法使用简介目录03020405使用目的检查表用法目录0706基本信息程序静态分析（ProgramStaticAnalysis）是指在不运行代码的方式下，通过词法分析、语法分析、控制流、数据流分析等技术对程序代码进行扫描，验证代码是否满足规范性、安全性、可靠性、可维护性等指标的一种代码分析技术。静态分析技术向模拟执行的技术发展以能够发现更多传统意义上动态测试才能发现的缺陷，例如符号执行、抽象解释、值依赖分析等等并采用数学约束求解工具进行路径约减或者可达性分析以减少误报增加效率。静态分析工具，无论从科研角度还是实用性角度还有很大的提高余地，国际最好分析工具误报率在5-10%之间，能够报出的缺陷种类也仅有几百种。我国较好静态分析工具较少，一些研究所与高校正在致力于在此方面的研究和开发（成果较突出的如北京大学、中科院、清华大学等）。分析技术实践常用静态分析静态分析特点分析技术实践静态分析特点程序静态分析是与程序动态分析相对应的代码分析技术，它通过对代码的自动扫描发现隐含的程序问题，主要具有以下特点：（1）不实际执行程序。动态分析是通过在真实或模拟环境中执行程序进行分析的方法，多用于性能测试、功能测试、内存泄漏测试等方面。与之相反，静态分析不运行代码只是通过对代码的静态扫描对程序进行分析。（2）执行速度快、效率高。成熟的代码静态分析工具每秒可扫描上万行代码，相对于动态分析，具有检测速度快、效率高的特点。（3）误报率较高。代码静态分析是通过对程序扫描找到匹配某种规则模式的代码从而发现代码中存在的问题，例如可以定位strcpy（）这样可能存在漏洞的函数，这样有时会造成将一些正确代码定位为缺陷的问题，因此静态分析有时存在误报率较高的缺陷，可结合动态分析方法进行修正。常用静态分析（1）词法分析：从左至右一个字符一个字符的读入源程序，对构成源程序的字符流进行扫描，通过使用正则表达式匹配方法将源代码转换为等价的符号（Token）流，生成相关符号列表，Lex为常用词法分析工具。（2）语法分析：判断源程序结构上是否正确，通过使用上下文无关语法将相关符号整理为语法树，Yacc为常用工具。（3）抽象语法树分析：将程序组织成树形结构，树中相关节点代表了程序中的相关代码，已有javacc/Antlra等抽象语法树生成工具。（4）语义分析：对结构上正确的源程序进行上下文有关性质的审查。（5）控制流分析：生成有向控制流图，用节点表示基本代码块，节点间的有向边代表控制流路径，反向边表示可能存在的循环；还可生成函数调用关系图，表示函数间的嵌套关系。（6）数据流分析：对控制流图进行遍历，记录变量的初始化点和引用点，保存切片相关数据信息。（7）污点分析：基于数据流图判断源代码中哪些变量可能受到攻击，是验证程序输入、识别代码表达缺陷的关键。（8）无效代码分析，根据控制流图可分析孤立的节点部分为无效代码。形式化方法形式化方法程序分析中的形式化方法一般指利用纯粹严格的数学方法对软件、硬件进行分析的理论及技术。这些数学方法包括符号语义、公理语义、操作语义和抽象解释。1952年提出的Rice定理指出，任何关于程序分析的问题都是不可判定的。因此，不存在任何一种机械化的方法能够证明程序的完全正确性。然而，针对大多数的不可判定问题，仍然可以试图找到它们的一些近似解。形式化静态分析中用到的实现技术有：模型检查假设系统是有限状态的、或者可以通过抽象归结为有限状态。抽象解释将每条语句的影响模型化为一个抽象机器的状态。相比实际系统，抽象机器更简单更容易分析，但其代价是丧失了分析的完备性（并不是原始系统中的每种性质在抽象机器中都是保留的）。抽象解释当且仅当抽象机器中的每一个性质都能与原始系统中的性质正确映射时，才被称作可靠（sound）的。断言在霍恩逻辑中首次被提出。存在一些针对特定程序设计语言的工具，例如ESC/JAVA和ESC/JAVA2中分别使用的SPARK语言和JML语言。静态分析工具静态分析工具Meta-Compilation（Coverity）由Stanford大学的DawsonEngler副教授等研究开发，该静态分析工具允许用户使用一种称作metal的状态机语言编写自定义的时序规则，从而实现了静态分析工具的可扩展性。MC的实际效果非常优秀，号称在Linux内核中找出来数百个安全漏洞。MC已经商业化，属于CoverityInc.2014年被Synopsys收购。学术领域比较认可的静态分析工具，其技术处于领先地位。mygcc由一个法国人N.Volanschi开发，其思想来源于MC，试图将自定义的错误检测集成到编译时。Klocwork国内用的最为广泛的静态分析工具，由加拿大北电于1996年研发，是中国最早的能够检测语义缺陷的静态分析工具。截止到2015年其版本号为V10,也就是大家常说的K10LDRATestbed英国的编码规则类检测工具，前身为Liverpool大学开发，能够支持C/C++数千种条目的规则检测，包括MISRAC/C++,GJB5369等，是最早进入中国市场的静态分析工具，在军队、军工广泛使用，但其技术仅支持风格类检测，无法进行语义缺陷分析，导致一些常用的运行时缺陷无法发现或者较高误漏报，由此市场占有率逐步下降。使用简介使用简介在代码构建过程中使用静态分析工具有助于发现代码缺陷，并提高代码的质量。本节四个代码静态分析工具的使用：Findbugs、PMD、Checkstyle、BlueMorpho。前三个工具各有不同的特点，针对开放平台技术。如java,,C++.联合起来使用有助于减少误报错误，提高报告的准确率。第四个工具有助于理解大规模复杂业务逻辑的COBOL遗留系统.除包含词法，语法，控制流，数据流分析技术外还引入了人工智能技术，可自动推荐业务描述，生成业务文档。使用目的使用目的这三个工具检查的侧重点各有不同：本文中三个工具各自的版本分别是：FindBugs0.85、PMD2.0和CheckStyle3.3。这三个工具都可以从sourceforge下载，而且它们都为Eclipse提供了相应的plugin。用法用法关于IDE以及plugin如何使用在此不做介绍，本文主要它们如何与ant配合使用，使这些工具成为每次构建过程中的有机组成。FindBugsFindBugs的运行环境可能是这四个工具之中最苛刻的了。它工作在j2se1.4.0或以后的版本中，需要至少256MB内存。它的安装非常简单，下载之后简单的解压即可。为了与ant配合使用，它提供了对应的anttask。PMDPMD的运行环境是j2se1.3或以后版本，安装过程同样也是解压即可。对应anttask的使用：1.把lib中所有的jar复制到项目的classpath中。2.将pmd-中的rulesets解压到指定目录，这里面定义了分析所需要的规则集合。3.修改build.xml文件。在这一版本中，提供了2个anttask。一个是pmd使用规则集合进行分析；另一个是检查代码中Copy&Paste代码。检查表检查表-为每个工具建立自己的目录和classpath变量。由于这些工具大多都使用了相同的开源软件，很容易会因为使用相同软件包的不同版本而相互干扰。这种问题非常隐蔽，在这种问题上花费时间和精力是非常不值得的。通过建立不同的目录和classpath，然后在对应的anttask中引用各自的classpath，可以有效的避免它。-将这些工具纳入项目的配置