程式静态分析
程式静态分析(Program Static Analysis)是指在不运行代码的方式下,通过词法分析、语法分析、控制流、数据流分析等技术对程式代码进行扫描,验证代码是否满足规範性、安全性、可靠性、可维护性等指标的一种代码分析技术。目前静态分析技术向模拟执行的技术发展以能够发现更多传统意义上动态测试才能发现的缺陷,例如符号执行、抽象解释、值依赖分析等等并採用数学约束求解工具进行路径约减或者可达性分析以减少误报增加效率。目前的静态分析工具,无论从科研角度还是实用性角度还有很大的提高余地,国际最好分析工具误报率在5-10%之间,能够报出的缺陷种类也仅有几百种。我国较好静态分析工具较少,一些高校正在致力于在此方面的研究和开发(成果较突出的如北京大学等)。
基本介绍
- 中文名:程式静态分析
- 外文名:Program Static Analysis
- 目的:保证软体的整体质量
- 特点:不实际执行程式
分析技术及实践
程式静态分析(Program Static Analysis)可以帮助软体开发人员、质量保证人员查找代码中存在的结构性错误、安全漏洞等问题,从而保证软体的整体质量。还可以用于帮助软体开发人员快速理解文档残缺的大规模软体系统以及系统业务逻辑抽取等系统文档化等领域。 如开发20年以上的金融核心COBOL系统,动辄上千万行代码的系统规模。对于理解这样规模的系统,基于程式静态分析的辅助理解工具就能发挥积极作用。
本文首先对程式静态分析的特点、常用静态分析技术、静态分析实现方式进行描述,然后通过一个实例讲解了程式静态分析的执行过程。
静态分析特点
程式静态分析是与程式动态分析相对应的代码分析技术,它通过对代码的自动扫描发现隐含的程式问题,主要具有以下特点:
(1)不实际执行程式。动态分析是通过在真实或模拟环境中执行程式进行分析的方法,多用于性能测试、功能测试、记忆体泄漏测试等方面。与之相反,静态分析不运行代码只是通过对代码的静态扫描对程式进行分析。
(2)执行速度快、效率高。目前成熟的代码静态分析工具每秒可扫描上万行代码,相对于动态分析,具有检测速度快、效率高的特点。
(3)误报率较高。代码静态分析是通过对程式扫描找到匹配某种规则模式的代码从而发现代码中存在的问题,例如可以定位strcpy()这样可能存在漏洞的函式,这样有时会造成将一些正确代码定位为缺陷的问题,因此静态分析有时存在误报率较高的缺陷,可结合动态分析方法进行修正。
常用静态分析技术
(1)词法分析:从左至右一个字元一个字元的读入源程式,对构成源程式的字元流进行扫描,通过使用正则表达式匹配方法将原始码转换为等价的符号(Token) 流,生成相关符号列表,Lex为常用词法分析工具。
(2)语法分析:判断源程式结构上是否正确,通过使用上下文无关语法将相关符号整理为语法树, Yacc为常用工具。
(3)抽象语法树分析:将程式组织成树形结构,树中相关节点代表了程式中的相关代码,目前已有javacc/ Antlra等抽象语法树生成工具。
(4)语义分析:对结构上正确的源程式进行上下文有关性质的审查。
(5)控制流分析:生成有向控制流图,用节点表示基本代码块,节点间的有向边代表控制流路径,反向边表示可能存在的循环;还可生成函式调用关係图,表示函式间的嵌套关係。
(6)数据流分析:对控制流图进行遍历,记录变数的初始化点和引用点,保存切片相关数据信息。
(7)污点分析:基于数据流图判断原始码中哪些变数可能受到攻击,是验证程式输入、识别代码表达缺陷的关键。
(8)无效代码分析,根据控制流图可分析孤立的节点部分为无效代码。
程式静态分析是在不执行程式的情况下对其进行分析的技术,简称为静态分析。而程式动态分析则是另外一种程式分析策略,需要实际执行程式。大多数情况下,静态分析的输入都是源程式代码,只有极少数情况会使用目标代码。静态分析这一术语一般用来形容自动化工具的分析,而人工分析则往往叫做程式理解。
静态分析越来越多地被套用到程式最佳化、软体错误检测和系统理解领域。Coverity Inc.的软体质量检测产品就是利用静态分析技术进行错误检测的成功代表。国内某软体公司的闪蝶(BlueMropho)代码分析平台,是利用程式静态分析技术专注于大型机遗留系统的代码理解领域,尤其擅长分析千万行代码规模级的COBOL系统。
形式化方法
程式分析中的形式化方法一般指利用纯粹严格的数学方法对软体、硬体进行分析的理论及技术。这些数学方法包括符号语义、公理语义、操作语义和抽象解释。
1952年提出的Rice定理指出,任何关于程式分析的问题都是不可判定的。因此,不存在任何一种机械化的方法能够证明程式的完全正确性。然而,针对大多数的不可判定问题,仍然可以试图找到它们的一些近似解。
形式化静态分析中用到的实现技术有:
模型检查假设系统是有限状态的、或者可以通过抽象归结为有限状态。
抽象解释将每条语句的影响模型化为一个抽象机器的状态。相比实际系统,抽象机器更简单更容易分析,但其代价是丧失了分析的完备性(并不是原始系统中的每种性质在抽象机器中都是保留的)。抽象解释若且唯若抽象机器中的每一个性质都能与原始系统中的性质正确映射时,才被称作可靠(sound)的。
断言在霍恩逻辑中首次被提出。目前存在一些针对特定程式设计语言的工具,例如ESC/JAVA和ESC/JAVA2中分别使用的SPARK语言和JML语言。
着名的静态分析工具
Meta-Compilation(Coverity)
由Stanford大学的Dawson Engler副教授等研究开发,该静态分析工具允许用户使用一种称作metal的状态机语言编写自定义的时序规则,从而实现了静态分析工具的可扩展性。MC的实际效果非常优秀,号称在Linux核心中找出来数百个安全漏洞。MC目前已经商业化,属于Coverity Inc.2014年被Synopsys收购。目前学术领域比较认可的静态分析工具,其技术处于领先地位。
mygcc 由一个法国人N. Volanschi开发,其思想来源于MC,试图将自定义的错误检测集成到编译时。
Klocwork
国内用的最为广泛的静态分析工具,由加拿大北电于1996年研发,是中国最早的能够检测语义缺陷的静态分析工具。截止到2015年其版本号为V10,也就是大家常说的K10
LDRA Testbed
英国的编码规则类检测工具,前身为Liverpool大学开发,能够支持C/C++数千种条目的规则检测,包括MISRA C/C++, GJB5369等,是最早进入中国市场的静态分析工具,在军队、军工广泛使用,但其技术仅支持风格类检测,无法进行语义缺陷分析,导致一些常用的运行时缺陷无法发现或者较高误漏报,由此市场占有率逐步下降。截止到2015年其版本号为9.5
HP Fortify
美国HP公司的支持安全漏洞类的检测工具,能够检测C/C++/Java/PHP/ASP/JavaScript等多种语言,数千种检测项,是国内使用最为广泛的静态分析工具。但该工具整体的误报漏报率较高,虽然支持很多种安全漏洞,但需要用户做很多的二次开发工作。
Cobot(库博)
北京大学软体工程中心研发的静态分析工具,能够支持编码规则,语义缺陷的程式分析,能够支持C/C++数千条规则和缺陷的检测,是我国唯一可以称的上是静态分析产品的商业化工具。由于其自主智慧财产权,对国内的作业系统,编码标準支持的较好,检测精度也基本与上述工具持平,所以也得到了很多用户的认可。2015年通过美国CWE-Compatible 认证,是中国首个也是唯一一个通过该认证的安全检测产品。
Parasoft C++Test
美国Parasoft公司研发的支持C、C++静态分析的工具,该工具除了可以检测编码规则外,还能检测少量的语义缺陷,此外能够进行测试用例生成。
使用简介
在代码构建过程中使用静态分析工具有助于发现代码缺陷,并提高代码的质量。本节关注四个代码静态分析工具的使用:Findbugs、PMD、Checkstyle、BlueMorpho。前三个工具各有不同的特点,针对开放平台技术。如java, .net , C++. 联合起来使用有助于减少误报错误,提高报告的準确率。第四个工具有助于理解大规模複杂业务逻辑的COBOL遗留系统.除包含词法,语法,控制流,数据流分析技术外还引入了人工智慧技术,可自动推荐业务描述,生成业务文档。
使用目的
这三个工具检查的侧重点各有不同:
本文中三个工具各自的版本分别是:FindBugs 0.85、PMD 2.0和CheckStyle 3.3。这三个工具都可以从sourceforge下载,而且它们都为Eclipse提供了相应的plugin。
用法
关于IDE以及plugin如何使用在此不做介绍,本文主要关注它们如何与ant配合使用,使这些工具成为每次构建过程中的有机组成。
FindBugs
FindBugs的运行环境可能是这四个工具之中最苛刻的了。它工作在j2se1.4.0或以后的版本中,需要至少256MB记忆体。它的安装非常简单,下载之后简单的解压即可。为了与ant配合使用,它提供了对应的ant task。
PMD
PMD的运行环境是j2se1.3或以后版本,安装过程同样也是解压即可。对应ant task的使用:
1. 把lib中所有的jar複製到项目的classpath中。
2. 将pmd-2.0.jar中的rulesets解压到指定目录,这里面定义了分析所需要的规则集合。
3. 修改build.xml档案。在这一版本中,提供了2个ant task。一个是pmd使用规则集合进行分析;另一个是检查代码中Copy & Paste代码。这2个任务对应的ant task使用:
PMD任务:
<target name="pmd">
<!-- 定义任务和任务所属类所在的classpath引用 -->
<taskdef name="pmd" classname="net.sourceforge.pmd.ant.PMDTask"
classpathref="classpath"/>
<!-- 检查使用的规则档案 -->
<pmd rulesetfiles="junit_lib/rulesets/imports.xml">
<!-- 输出格式和档案名称 -->
<formatter type="html" toFile="pmd_report.html"/>
<!-- pmd所需要依赖包的classpath引用 -->
<classpath refid="classpath"/>
<!-- 要检查的项目源档案根目录 -->
<fileset dir="src">
<include name="**/*.java"/>
</fileset>
</pmd>
</target>
CPD任务:
<target name="cpd">
<!-- 定义任务和任务所属类所在的classpath -->
<taskdef name="cpd" classname="net.sourceforge.pmd.cpd.CPDTask"
classpathref="classpath"/>
<!-- 指明输出档案和判断属于copy & paste的标準 -->
<cpd minimumTokenCount="100" outputFile="cpd.txtl">
<!-- 要检查的项目源档案根目录 -->
<fileset dir="src">
<include name="**/*.java"/>
</fileset>
</cpd>
</target>
4. 运行ant pmd和ant cpd即可。
5. 参数说明:
- formatter,指明输出格式和档案。
- rulesetfiles,指明分析所需的规则档案,不同档案使用逗号分隔。
- failonerror,pmd执行出错是否中止构建过程。
- failOnRuleViolation,如果与规则冲突,是否中止构建过程。
- classpath,pmd所需的classpath。
- printToConsole,在发现问题时是否列印到ant log或控制台。
- shortFilenames,在输出报告中是否使用短档案名称。
- targetjdk13,是否把目标定为jdk13,如不能使用assert。
- failuresPropertyName,在任务结束时,插入违反规则的号码
- encoding,读源档案时所採用的编码,如utf-8。
关于规则集合的说明,以及如何自定义规则请参见pmd的文档,文档中已说得相当清楚。
CheckStyle
使用ant task:
1. 複製checkstyle-all-3.3.jar到项目的classpath中。
2. 修改build.xml档案:
<taskdef resource="checkstyletask.properties"
classpath="${weblib.dir}/checkstyle-all-3.3.jar"/>
<target name="checkstyle" depends="init">
<!-- 指明checkstyle的分析所需的规则档案 -->
<checkstyle config="checkstyle33.xml">
<!-- 要检查的档案 -->
<fileset dir="${src.code}" includes="**/*.java"/>
<!-- 指明输出格式和档案名称 -->
<formatter type="xml" toFile="report.xml"/>
</checkstyle>
<!-- 将xml档案转换成html档案 -->
<style in="report.xml" out="report.html" style="checkstyle-frames"/>
</target>
3. 运行ant checkstyle即可。
checkstyle的规则档案,即项目的代码规範,建议不要手工书写。可以使用checkstyle plug in在Eclipse配置后再导出。Checkstyle提供了预设的xslt,用来进行xml的格式转换。它们都放在contrib目录中。Checkstyle同样也提供了自定义的check,但与PMD相比,书写要複杂。详细情况请参见checkstyle的文档。
BlueMorpho(闪蝶)
BlueMorpho是独立运行的B/S程式,安装简单,无需额外配置参数档案。
- 在Windows下运行Bluemorpho windows安装包,注意有32位和64位两个版本,
- 安装完成后,在开始-程式-BlueMorpho资料夹里运行Sart bluemorho server启动分析server.
- Server启动后,在开始-程式-BlueMorpho资料夹里运行BlueMorpho即可访问闪蝶源码分析平台。
- BlueMoropho提供两种方式上传source code, 手工上传和同步从Mainframe下载COBOL源码。
- 代码上传或下载到BlueMorpho以后,即可点击任意程式进行源码分析。
检查表
- 为每个工具建立自己的目录和classpath变数。由于这些工具大多都使用了相同的开源软体,很容易会因为使用相同软体包的不同版本而相互干扰。这种问题非常隐蔽,在这种问题上花费时间和精力是非常不值得的。通过建立不同的目录和classpath,然后在对应的ant task中引用各自的classpath,可以有效的避免它。
- 将这些工具纳入项目的配置管理库中。这样可以方便而迅速的在另一台机器上重建构建环境,有效的保证了项目组中统一的构建环境。
- 重视这些输出,但是不要因为输出而困扰。它们仅仅是工具,要学会正确的对待它们。
- 三个工具都提供了自定义规则的接口,相比而言pmd书写最简单,findbugs功能最强。它们涉及AST(抽象语法树)和byte code相关的知识。