ACTA Scientiarum Naturalium Universitatis Pekinensis
Static Analysis of Injection Security Vulnerabilities Based on Symbolic Execution
SUN Jinan1,†, PAN Kefeng1,2, CHEN Xuefeng1, ZHANG Junfu1,3
1. National Engineering and Research Center of Software Engineering, Peking University, Beijing 100871; 2. Beijing Center of Westone Information Industry Co., Ltd., Beijing 100070, 3. Beida Software Engineering Co., Ltd, Beijing 100080; † E-mail: sjn@pku.edu.cn
Abstract This research work receives symbols as input variables, simulates the execution of program, extracts the constraints binding with execution paths, such as security constraints, attack constraints and defense constraints, and constructs the SAT judgment matrix and UNSAT judgment matrix as injection vulnerabilities analysis models. According to the logical reduction results of the matrices, the states of injection vulnerabilities are decided. In the controlled experiments, the false positive and false negative ratios are greatly reduced, and the prototype system can generate correct exploits automatically. Key words injection vulnerability; symbolic execution; static analysis; web application security
注入类漏洞是Web应用代码中的一类弱点, 这种弱点当且仅当输入数据成为命令或者查询的一部分并由解释器执行时产生, 是危害程度最高的漏洞类型之一。为了降低注入类漏洞被利用的风险, Web应用中一般采取输入验证等防御对策。但是,当输入验证等防御对策存在缺陷时, 其残留的风险依然会使注入类漏洞暴露在外部威胁中。攻击者通过构造特定输入, 利用漏洞的脆弱性及其防御对策的缺陷, 产生非预期的命令, 从而造成Web应用的资产损失, 并形成一个完整的攻击路径。该攻击路径可用污染传播模型描述。
21 世纪初, Web 安全问题日益突出, 因此开发有效的 Web 安全漏洞静态分析工具受到重视。早期的分析工具实质上是专用的词法分析工具, 或称为改进后的关键字查找、匹配工具(如 ITS4[1])。这类工具将安全漏洞简化为危险函数匹配规则, 但模型过于简单, 难以成为复杂漏洞的有效检测手段。研究人员考虑描述能力更强、更复杂的建模形式,如 MOPS[2]以自动机作为安全漏洞的建模元素。但是, 基于自动机理论的模型复杂度过高、模型检查代价大的问题一直难以解决, 并且, 自动机之间的逻辑运算也是不可判定问题。代码的中间表达形式
可以表征代码若干方面的特性, 如抽象语法树(AST)、控制流图(CFG)和数据流图(DFG), 在编译理论指导下, 这些中间表达模型发展比较成熟, 在
[3–5]检测代码漏洞方面具有一定价值 。但是, 单独应用一种中间表达模型显然具有局限性, 于是研究人员开始尝试构造能够融合多种经典中间表达的、基于图的模型[6], 并发现若干重要安全漏洞[7]。
在Web安全漏洞静态分析领域, 采用符号执行技术分析安全漏洞成为当前的研究热点[8], 并出现适用于不同语言和平台的分析工具[9–11]。符号执行指不执行程序, 不对程序中的变量赋以具体值, 而用符号代表程序变量, 模拟程序执行过程, 分析程
[12]序相关语义信息的技术 通常将所分析问题转化为约束求解。约束是描述程序中变量取值或行为的一类属性, 用符号值及其运算表示, 约束的求解可转换为符号计算问题。符号执行技术的初衷是为了提高程序测试的覆盖率和效率[13–14], 具有路径敏感、分析精度较好等优点, 但由于需要记录的状态多, 分析的时空代价非常高, 受限于计算硬件条件,在早期其应用并不现实。21世纪初, 随着计算硬件能力的提高, 符号执行技术才在漏洞分析检测领域得到研究和应用[15]。研究机构及企业已陆续开发出基于符号执行的安全检测框架或工具[16]: 美国航空航天局(NASA)开发的用于Java路径测试分析的Pathfinder[17], 伊利诺伊大学香槟分校(UIUC)开发的具有混合执行能力的 CUTE 和 JCUTE2, 斯坦福大学开发的用于动态符号执行生成测试用例的KLEE[18], 加州大学伯克利分校开发的用于检测 C 语言缺陷的CREST 和二进制代码分析工具 Bitblaze[19] 。符号执行在企业界也得到重视, 部分商业产品中应用符号执行技术。微软公司开发了一系列工具, 应用于 Visual Studio 中单元测试的Pex、白盒安全模糊测试工具SAGE、混合多种约束提取技术的 YOGI以及代码缺陷查找工具 Prefix。IBM 也开发了符号执行框架Apollo。
注入类安全漏洞是危害度排名首位的 Web 应用安全漏洞。动态分析工具始终难以解决覆盖率
[20–21]低、效率低的问题 。现有的代码静态分析工具不能完全有效地检测出注入类漏洞, 主要问题在于, 不能有效地判定漏洞被利用的风险, 不能自动生成攻击向量, 因此误报率较高; 数据库对数据流影响分析不足, 也可能造成对高级注入类漏洞的 漏报。本研究针对注入类漏洞的脆弱性本质、防御对策及威胁模式, 提出一种统一建模方法, 设计对应的约束建模语言 SCL, 用于有效地描述安全约束(SC)、防御约束(DC)和攻击约束(AC)三类 Web 应用程序的属性, 支持形式化分析漏洞、对策以及威胁之间的关系。在形式化建模的基础上, 提出一种基于逻辑矩阵的注入类安全漏洞分析模型与检测方法。
本文提出在逻辑运算上可满足矩阵(SAT)以及不可满足矩阵(UNSAT)的两个检测模型, 将安全漏洞静态分析检测问题转化成 SAT 和 UNSAT 两个逻辑矩阵的可满足性求解问题, 从而提供判定注入类漏洞被利用风险是否存在的分析方法以及攻击向量自动生成方法。在符号执行技术的基础上, 重点增强字符串、正则表达式数据类型的约束求解技术, 以期实现建模语言所描述的三类约束属性及其逻辑运算的可满足性求解能力。
1 注入类漏洞的形式化描述
注入类安全漏洞的核心问题是注入的路径、注入的防御以及注入的触发 3 个方面。注入路径描述注入的污染数据的传播过程, 是分析注入是否抵达安全关键操作的依据。注入防御描述程序中沿着注入的路径, 对注入的污染数据进行防御和净化的操作, 是程序中对污染数据的防御约束。注入触发描述程序中污染数据沿着注入路径, 通过防御抵达关键操作, 符合注入漏洞攻击约束的污染数据最终会触发安全漏洞。注入路径是可达性基础, 防御约束与攻击约束是路径上的重要安全属性, 对这 3 个方面的分析构成注入类安全漏洞的形式化模型。
1.1 注入类漏洞的污染传播路径
现代 Web 服务一般采用多层结构(multi-tier),注入类安全漏洞的注入路径可能存在跨层的复杂的注入路径, 即一个注入类漏洞可能会跨越部署在不同物理节点上的 Web 应用, 其表现形式可以非常复杂。注入不仅会发生在服务端, 而且可以发生在客户端。图 1 以 SQL 注入为例, 不失一般性地给出最具有代表性的 3 种注入路径模式, 基本上涵盖目前可能存在的主要注入路径模型。图 1 中设定常见的 3 层 Web 应用架构, 即客户层、应用层和数据层。
1.1.1 服务端注入路径
服务注入路径的核心特征是注入的污染数据主
要在服务端的路径传播, 可以直接抵达服务器端数据库。服务端注入是最早出现的最常见的注入路径模式。如图 1 所示, 污染数据 D2经过客户端验证IV1后发送至服务端, 形成污染数据 D4, D4在服务端通过验证 IV2后成为净化的数据 D6, D6直接送到SQL 语句 SQL2 处, 最后送入数据库存储。
1.1.2 客户端注入路径
客户端注入路径的核心特征是注入的污染数据要在客户端进行路径传播, 利用客户端与服务端之间数据离线同步的关系, 完成注入。随着客户端数据库、HTML5 标准的发布以及无线应用的拓展,客户端注入问题已成为近年来网络安全的热点。如图1 所示, 污染数据 D1经过客户端验证 IV3后形成净化数据 D5, D5送到客户端 SQL 语句 SQL1 处, 并存储到客户端存储。随后, 客户端存储后形成的数据 D8 向服务器端数据库同步。D8 经过服务端验证IV4, 送至服务端 SQL 语句 SQL3 处, 并存储在服务器端数据库。
图 1 中, D5后出现污染数据 D8, 是客户端注入的重要特征。D5 通过客户端的输入验证 IV3, 因此D5 此时是非污染数据, 但由于用户具有客户端一切 操作的控制权, 用户完全可以绕过客户端的输入验证 IV3, 直接将污染数据送入客户端(Client Store)存储。这种情况表明, 因为控制权限问题, 所以客户端不存在真正可信的输入验证。当客户端向服务器端发送数据 D8 时, 从安全分析的角度, 该数据不应信赖, 在未通过服务器端输入验证 IV4 之前, 应该标记为污染数据。
1.1.3 二阶段注入路径
二阶段注入路径的核心特征是注入污染数据的攻击将注入与攻击分成两个独立的阶段, 即注入污染数据与攻击触发行为之间的时空相互分离。第一阶段注入污染数据D2经过客户端验证 IV1后发送至服务端, 形成污染数据D4, D4在服务端通过验证IV2后成为净化后的数据D6, D6直接送到SQL语句SQL2处, 最后送入数据库存储, 但此时在 SQL2 处并未触发注入攻击。第二阶段触发攻击, 即用户通过数据 D3 调用功能Func1, 该功能触发了SQL语句命令 SQL4, SQL4 从服务器端提取数据 D7, D7 经服务器端验证IV5送至SQL4, 参与执行。
在图 1 中, D6之后出现污染数据, 是二阶段注入的重要特征。D6通过 SQL2存入服务器端数据库
(Server Store)的过程不会发生注入攻击, 此时 D6确实是不能利用 SQL2脆弱性的未污染数据。但是,当从数据库取出 D6与 SQL4进行拼接时, 需要考虑SQL2 与 SQL4在一般情况下语义不同、D6不能利用 SQL2的脆弱性触发攻击的前提, 不能得出 D6不能利用 SQL4脆弱性触发攻击作为其必然结论, 因此对于 SQL4, 为了确保安全, 必须将进入即将拼接的 D7标记为污染数据。这也是二阶段注入攻击的特殊的隐蔽性与危害性所在。
1.2 注入类漏洞的安全约束
注入类漏洞都在危险操作处触发, 能够触发安全漏洞的必要条件是违背危险操作的安全约束。注入类漏洞的本质是使语义发生变换, 所以安全约束定义为对输入数据的约束, 该约束使语义不能发生结构或属性的变换。以下是一个 SQL 语句示例(开源项目 Utopia News Pro): $idnews = $DB->QUERY("SELECT * FROM
‘news’ WHERE newsid =".$newsid),其中, $newsid 是外部可注入的变量。
根据代码语义, 可以确定开发人员预期的 SQL语法树, 如图 2 所示。根据 SQL 语法树分析, 外部可注入的变量$newsid 受数据库表 news 中 newsid列的性质限制。通过分析整个 Web 应用的设计结构(design schema)(尤其是数据库的设计结构)可知, newsid 列的性质要求为 Int32 类型。当$newsid 输入符合 Int32 类型限制时, SQL 语法树不会发生任何结构或节点属性的变换, 代码语义也不会发生变换, 不会触发注入类漏洞。当$newsid 输入不符合Int32 类型限制时, SQL语法树就一定会发生结构或节点属性的变换, 就有可能发生注入类漏洞(并不肯定发生)。因此, newsid 列的性质就是$newsid 的 安全约束。违背安全约束是发生注入漏洞的必要条件, 所以符合安全约束是确定注入漏洞无法触发的充分条件。
可以看出, 应用代码静态分析, 确定注入变量的安全约束, 要求事先获取 Web 应用的设计结构,特别是 SQL 注入, 必须事先获取其数据库的设计结构。如果数据库结构已知, 则可以根据关键语句的 SQL 语法树, 确定注入变量的安全约束。对于注入类漏洞安全约束的确定与前提条件, 尚未有相关研究。
1.3 注入类漏洞的防御约束
一般情况下, 对安全敏感的 Web 应用程序, 至少都会采用一种或多种防御模式来约束并抵御注入类攻击。这些基本的防御主要有 3 种模式: 匹配模式、过滤模式和转义模式。
1.3.1 匹配模式
匹配模式指应用程序根据预先设定的数据特征进行匹配(如字符串的正则表达式等), 根据匹配结果和匹配规则, 决定是否接受输入的数据。例如,某应用只接受合法中国邮编为输入, 其要求匹配的字符串正则表达式为[1-9]\d{5}(?!\d), 如果输入的数据不能通过匹配, 则被拒绝。为了防止一些命令混在数据中输入, 程序可能对 SELECT 等关键字进行匹配, 如果存在, 则拒绝恶意污染的数据。匹配模式是最常见的防御对策, 又细分为黑名单与白名单模式。白名单模式最安全, 但对数据应用有较大限制; 黑名单模式存在漏洞威胁的可能性较大, 但数据应用相对灵活。
1.3.2 过滤模式
过滤模式指应用程序根据预先的规则, 将其认为有害的数据从原始输入数据中过滤删除, 达到数
据净化的目的。以下为过滤模式的典型应用: 某应用对SELECT等关键字进行过滤, 净化数据, 防止数据命令中混入关键命令。简单的过滤模式一般都有较明显的缺陷, 如一旦污染数据变成SELSELECTECT,一次过滤之后该数据变成SELECT, 如果后续不再进行过滤, 则有可能骗过验证防御机制。所以, 过滤模式一般要过滤数据至不动点, 并且要谨慎考虑数据的语义是否被改变。
1.3.3 转义模式
转义模式指应用程序根据预先规则, 将其认为有害的数据全部进行转义编码, 使转义编码后的数据不能产生破坏作用。以下为转义模式的典型应用: 对单引号进行转义(如’变成\’), 使单引号成为不具备特殊语法含义的普通符号。在Web应用中对输入数据进行URL编码和解码是常见行为, 空格等都变成URL编码形式(如%20), 防止产生歧义。转义模式是有效的注入防御对策, 能防止大量污染数据注入, 但在很多上下文环境中, 不同编码集的切换会造成编码的溢出, 转义与反转义的操作不完善配合也会造成污染数据骗过验证防御机制。 注入类安全漏洞的威胁本质是利用解释数据的语法规则, 成功地恶意修改语法分析树的结构, 进而改变代码语义, 触发注入攻击。注入类安全漏洞的攻击往往伴随对应语法树的恶意变换。语法树的变换可以是树的结构发生变化, 也可以是树中某个节点的属性发生变化。语法树的变换可以映射为注入类安全漏洞的威胁模式, 语法树结构上的变化可以作为攻击的分类标准。
2 注入类漏洞的分析研究框架
本文在分析注入类安全漏洞本质特点的基础上, 提出一种注入类安全漏洞静态分析的研究框架。如图 3 所示, 研究框架分为 3 层, 即元模型层、模型层和实现层。
1) 元模型层: 为研究框架的顶层, 通过抽象注入类安全漏洞中的主要实体, 定义全部核心的建模元素, 并描述其形式化定义及特性。
2) 模型层: 元模型层之下是模型层, 根据建模元素, 提出基于符号执行的建模语言及对应的分析
技术。核心模型是污染传播模型, 通过该模型可以直接提取安全约束和防御约束, 在具有安全漏洞威胁模式的知识支撑上, 污染传播模型可以确定攻击约束。约束提取完成后, 需要模型判定安全漏洞是否存在或攻击向量是否存在, 最后由求解模型描述求解过程并进行求解。
3) 实现层: 实现层是研究框架的最底层, 是模型层的实现部分。这一层实现符号执行框架(引擎)、注入类安全漏洞模式库、复合数据类型求解器以及多语言解析器等工具。
2.1 元模型层
元模型包含对注入类安全漏洞建模的基本元素, 这些元素根据自身性质可以分为实体、关系两大类, 实体元素具有特定的属性, 关系元素也具有特定的运算。
元模型中的实体元素是安全控制点(security control point, SCP), 指与程序安全相关的关键语句或功能块的抽象实体。对于注入类安全漏洞而言,安全控制点有 3 个子类。
1) 交互点(interactive point, IP): 程序接收外界输入数据的语句或功能块, 是程序执行流程的起始点。交互点没有前驱安全控制点, 其后继安全控制点是转向点。
2) 转向点(crossover point, CP): 程序执行路径上的关键安全语句或安全功能块, 是输入数据完成注入攻击的必经点。转向点的前驱安全控制点是交互点或其他转向点, 其后继安全控制点是触发点或其他转向点。
3) 触发点(trigger point, TP): 触发安全漏洞的关键语句或功能块, 是程序执行流程的终止点。触发点的前驱安全控制点是转向点, 没有后继安全控制点。
安全控制点具有复合数据约束属性, 对于注入类安全问题, 一般约束既有基本数据类型, 又有复杂数据类型, 这种混合多种数据类型的约束称为复合数据约束(composite data constraint)。注入的污染数据取值范围可用复合数据约束描述, 复合数据约束定义了安全连接子的连接语义。
安全连接子(security connector, SC)是元模型中的关系元素, 连接前驱安全控制点与后继安全控制点, 表示两个安全控制点之间执行路径的可达关系。关系所表达的映射决定污染值域。在一般的程 序上下文环境中, 交互点的污染值域(IPTD)语义指由威胁模式确定的攻击向量初始集。转向点的污染值域(CPTD)由前驱安全控制点(前驱控制点可以是交互点或转向点)污染值域与前驱控制点之间的连接约束合取而生成的新的污染值域。触发点的污染值域(TPTD)是攻击向量初始集经过路径中安全控制点多次连接约束后, 实际能够触发注入类安全漏洞的攻击向量集合。触发点的污染值域为空集Ø 时,表明不存在能通过各个安全控制点抵达触发点的攻击向量, 意味着程序中不存在安全漏洞。
2.2 模型层
2.2.1 安全约束模型安全约束模型不能改变代码语义, 即不能改变SQL 注入触发点语法树的性质(语法树结构的变换以及节点属性的变换都不能发生)。达到这一要求的充分条件, 就是输入的数据必须符合 Web 应用设计结构中的类型约束。表 1 列出 SQL2011 核心集的安全约束。2.2.2 防御约束模型对于匹配模式, 符合正则表达式的 Match 操作和字符串相等操作是常见约束。对于过滤模式, 字符串的替换、删除逻辑是核心操作, 因此 Substring和 Replace 操作是过滤模式的常见约束。对于转义模式, 一般需要在特殊字符前添加转义符号, 连接逻辑是转义模式的常见约束, 因此 Concat 操作是
转义模式的核心操作。此外, 一般 Web 应用中还会对字符串的长度等做限制, 这类操作也应纳入核心操作集。如长度操作 Length 和定位操作 Indexof,在防御约束中也属于常见操作, 应纳入核心操作集。对于 1.2 节的示例, 我们可以利用约束图建立防御约束模型, 如图 4 所示。2.2.3 攻击约束模型应用约束建模语言可以对主要的注入漏洞攻击模式进行建模, 并给出攻击约束图模型, 该建模语言在注入类漏洞中具有普适和扩展的能力。如适用于 1.2 节示例中的攻击约束, 图 5 为其相对应的约束图, 具体可以表达为
[Quote][delim][o|o][r|r][delim][quote](?<1>num) [Quote][=][quote]{?<1>num}。
2.3 约束判定矩阵
首先将约束之间的逻辑规范为合取范式, 即C1 ∧ C ∧ … ∧ CN的形式。原来判断蕴含式DC→ 2 SC成立, 根据形式逻辑变换规则, 可以变换为合取范式: ¬ SC∧DC = 。同样, DC → SC 不成立, 等价于
¬ SC∧DC ≠根据约束求解结果是否存在解, 以 AC, DC, SC及其否定形式构建为 SAT 约束判定矩阵和 UNSAT约束判定矩阵, 其求解结果一一对应安全漏洞的状态, 如图 6 所示。由于约束判定矩阵是对称矩阵,所以只列成三角矩阵形式即可; 并且对角线上的自反合取并不产生新的含义, 因此对角线元素也不用列出。符号 也就是UNSAT。经过考察, UNSAT 矩阵中有 3 个元素在代码分析上是有安全语义的, 下面按重要性依次列出。
1) DC∧¬ SC= 。安全语义: 安全漏洞不存在被利用的风险。
2) DC ∧ AC= 。安全语义: 现有威胁模式不可行。3) DC∧SC=。安全语义: 输入全是高风险值。类似地, 可以给出 SAT 约束判定矩阵, 如图 7所示。SAT 约束判定矩阵中符号 代表约束求解的结果不是空集, 也就是 SAT。经过考察, SAT 矩阵