软件静态安全检测技术研究

安全性是软件质量的一个重要属性。软件安全性是软件在受到恶意攻击时仍提供所需功能的能力。多数软件的安全性问题主要源自于本身，其自身的漏洞往往被攻击者利用，从而成为软件安全的隐患。软件安全检测技术的主要作用就是检测软件中存在的安全问题，从而指导软件进行安全性能的改善。

安全性相关缺陷不同于一般的软件缺陷。一个很难发现的软件安全漏洞可能导致大量用户受到影响。安全性测试不同于传统测试类型最大的区别是它强调软件不应当做什么，而不是软件要做什么，例如未授权用户不能访问数据。

软件安全性测试刻不容缓

软件安全性测试可分为安全功能测试和安全漏洞测试两个方面。

安全功能测试基于软件的安全功能需求说明，测试软件的安全功能实现是否与安全需求一致，包括数据机密性、完整性、可用性、不可否认性、身份认证、授权、访问控制、审计跟踪、委托、隐私保护、安全管理等。

安全漏洞测试从攻击者的角度，以发现软件的安全漏洞为目的。安全漏洞是指系统在设计、实现、操作、管理上存在的可被利用的缺陷或弱点。漏洞被利用可能造成软件受到攻击，使软件进入不安全的状态，安全漏洞测试就是识别软件的安全漏洞。

目前测评中心的安全测试工作就是要发现中国移动业务支撑系统存在的安全漏洞，对于软件安全的检测，通常可以按照检测过程中是否需要执行程序的标准分为动态测试和静态测试两种，本文针对软件静态安全检测技术进行深入研究。

静态检测从分析开始

静态代码安全分析的第一步，是根据分析需求把程序源代码变换成易于分析处理的程序模型，这个过程用到了编译原理中的成熟技术。

● 词法分析：使用正则表达式匹配将源代码转换为等价的符号流。

● 语法分析：使用上下文无关语法将符号流规整为语法树，作为源代码逻辑结构的最直接的表现。

● 抽象语法分析：通过简化语法将语法树转换为包含更少节点和分支的抽象语法树，以方便后续处理。

● 语义分析：从抽象语法树建立符号表，为每个标识符关联类型信息。至此，已经具备了足够的信息来进行所谓的结构化分析。编译器通常将抽象语法树和符号表转化成易于优化的中间形式，然后送给后端生成平台相关的目标代码。安全分析工具可以建立更高阶的中间形式，或者直接在抽象语法树和符号表上进行后续步骤。

在分析模型建立后，就可以开始进行静态检测了。从早期的缓冲区溢出检测开始，十几年来出现了各种检测技术，早期静态检测主要指静态分析，随着形式化验证方法的引入，静态检测引入了程序抽象验证方法。

静态分析直接分析被测程序特征，寻找可能导致错误的异常。

规则检查 程序本身的安全性可由安全规则描述。程序本身存在一些编程规则，即一些通用的安全规则，也称之为漏洞模式，比如程序在root权限下要避免exec调用。规则检查方法将这些规则以特定语法描述，由规则处理器接收，并将其转换为分析器能够接受的内部表示，然后再将程序行为进行比对、检测。

类型推导 自动推导程序中变量和函数的类型，来判断变量和函数的访问是否符合类型规则。静态漏洞检测的类型推导由定型断言、推导规则和检查规则3个部分组成。定型断言定义变量的初始类型，推导规则提供了推论系统的规则集合，检查规则用于判定推论结果是否为"良行为"。

程序验证方法通过使用形式化验证技术验证正确性的方式来检测漏洞。

1.模型检测

模型检测对有限状态的程序构造状态机或有向图等抽象模型，再对模型进行遍历以验证系统特性。一般有2种验证方式：

● 符号化方法将抽象模型中的状态转换为语法树描述的逻辑公式，然后判定公式是否可满足。

● 模型转换成自动机，并将需要检查的安全时序属性转换为等价自动机，再将这两个自动机取补，构成一个新的自动机，判定问题就变成检查这个新自动机能接受的语言是否为空。

模型检测需要列举所有可能状态，由于软件本身的高复杂度，对所有程序点进行建模可能会使模型规模庞大，因此一般只针对程序中某一方面属性构造抽象模型。近期出现的一种模型检测方法通过对内存状态的建模，从而使原先主要检测时序相关漏洞的模型检测方法可对内存相关漏洞进行相关检测。

2.定理证明

定理证明比模型检测的形式化方法更加严格，用各种判定过程来验证程序抽象公式是否为真。判别的方法取决于公式的形式，如不等式的合取：首先由合取式构造成一个图，合取式中每个条件对应于图中的一个节点，然后利用给出的等式将对应的顶点合并，在顶点合并的过程中对合取式中的不等式进行检查，如发现存在不成立，则该合取式不可满足。

3.符号执行

符号执行的基本思想是将程序中变量的值逻辑转换成抽象符号，模拟路径敏感的程序控制流，通过约束求解的办法，检测是否有发生错误的可能。由程序执行前的条件P出发，在程序中某程序点，可推出约束条件C1∧C2∧…∧Cn ，因此在该点有P∧ Cl∧ C2∧…∧Cn->R这样的规约式，其中R是程序结束后要满足的条件。对该规约式的否命题求解，如有一组解满足，说明在这个程序点上存在一组变量状态，使运行程序的结果不符。符号执行求解工具的约束条件集合及求解能力决定了其发现错误的能力。理论上很多约束问题在可接受时间级内是不可解的，因此，符号执行求解的方法只适用于某些特定问题求解上。

最终的报告并非安全缺陷的简单总结，还应该帮助用户判断缺陷报告的正确性和缺陷的严重性，并给出适当的修复建议。从易用性考虑，缺陷报告应该支持分组、排序、屏蔽特定结果等操作。

静态检测工具发展方向

静态检测技术目前的发展趋势是将静态检测的各种技术进行结合，以提高性能。结合方式有以下几种方法：

● 提供一个框架，使用不同检测技术对程序进行检测，获取大量检测结果之后进行分析。从误报率来说，使用多种技术的检测结果的交集来进行漏洞判断决策，可减少误报率。从漏报率来说，对于同一种漏洞，使用多种检测技术的结果的并集可以减少漏报率。

● 直接在检测技术上结合，通过技术的结合来得到新的方法，如在符号执行的过程中加入类型推导的技术，在变量模拟执行的过程中增加其类型特征的推导，可获取更高的漏洞检测率。