Saluki: Finding Taint-style Vulnerabilities with Static Property Checking

出处:NDSS

作者:Ivan Gotovchits,Rijnard van Tonder,David Brumley

1.摘要

我们介绍了Saluki,一种新的工具,用于检查二进制代码中的污染型(数据依赖)安全属性。 Saluki提供了一种特定领域的语言来表达基于污点的政策。 Saluki可以在一些CWE类型的实际程序中找到漏洞,包括命令注入、弱PRNG种子和缺少消毒检查,如SQL转义例程或缓冲区长度检查。 Saluki在二进制程序分析中包含了两个新思想。 首先,Saluki使用µflux,一种新的静态分析技术,用于路径敏感、上下文敏感地恢复二进制文件中的数据依赖事实。 第二,Saluki引入了一个健全的逻辑系统来推理数据依赖事实。 我们在逻辑系统之上开发了一种特定于域的语言,将安全属性表示为形式规范。 Saluki包括一个可判定的求解程序,以(基于底层逻辑)证明一组数据依赖事实是否满足安全属性。 我们的评估表明,Saluki能够在COTSx86、x86-64和ARM软件中发现漏洞。

2.方法

2.1 Saluki操作

用户分两步检查安全策略。 首先,用户使用Saluki策略语言指定其安全策略。 Saluki安全策略描述了安全污染类型的路径属性。 策略有两个部分:(A)确定感兴趣的程序模式,例如recv和系统等API调用,以及(B)检查感兴趣位置之间的数据依赖关系。 我们的设计有三个目标:

  1. 提取具有高保真度、低误报和多路径的数据依赖项。

    Saluki通过“执行”代码片段提取所有数据依赖流(直到到达指定的执行深度),并沿执行代码片段提取所有依赖项。 因此,它是对许多路径进行路径和上下文敏感分析的一种类型,并且与动态分析具有相似的保真度,因为每个执行都是数据依赖的见证。

  2. 关于所有提取的数据依赖流的安全策略的理由。 特别是,我们不希望对每个路径分别进行推理的爆炸,因为许多路径共享类似的依赖关系。 在Saluki中,我们使用自定义逻辑以合理的方式对所有提取的数据依赖项进行推理。

  3. Saluki使用了一种轻量级的策略语言,带有一种用于模式匹配和从策略本身抽象出低级细节的工具。 策略抽象低级细节,例如read是否将结果放在堆栈(x86)或寄存器(如ARM)上。

saluki_architecture

  1. 在规范中加载。
  2. 将二进制解析为适合分析的中间表示IR(intermediate representation)。
  3. 运行µflux从每个指定的源收集有关执行的数据流事实。
  4. 运行一个解决方案的政策,程序,并收集事实。 求解器确定属性是否成立。 求解器实现了一个新的逻辑系统和算法建立在规范DSL的周围。
  5. Saluki输出属性不成立的示例路径。 实际输出不是完整的路径,而是被污染指令和流ID的浓缩形式。

以下面的样例安全属性为例

sample

通常不希望从recv函数中获取到数据直接流入到system函数,所以定义两个感兴趣的API函数(recv,system),其中recv函数可以接受4个参数,但是只对buf感兴趣,这里可以用_来表示不感兴趣的参数。其中cmd/buf,用来限制数据流,从buf进入到cmd。

下面具体说下流程:

  • 二进制处理 (binary processing)

    saluki将规范以及二进制作为输入。首先使用BAP来将指令解析为中间语言IR。

  • 污点种子(taint seeding)

    saluki解析规范以获取约束变量,每个变量都会被链接到程序的相应位置并在后续的过程中被标识为污点种子。在上例中,cmd是recv函数中使用的约束变量。saluki会为每个种子使用一个特殊的id来标志该种子。

  • uflux

    后续saluki会使用uflux来收集数据依赖关系,uflux会寻寻找种子并遵循一定的种子生成策略,默认情况下,使用的是随机种子生成策略。并根据解释器的执行状态来决定遇到分支时是否都执行或只选择其中一条。执行过程中解释器根据定义的规则去传播污点,并生成D(l′, R′, l, R)传播形式(表示中间语言地址l’处的变量R’由地址l处的R决定)。uflux为每条路径保持着一个执行状态并进行分析当遇到下列条件时会停止执行:

    • 达到与定义的最大执行指令数量。
    • 遇到一个没有模型化的函数调用。
    • 遇到一个间接跳转。
  • saluki 求解器

    saluki输入程序IR,程序执行流以及安全策略,试图满足安全策略中的代码。

2.2 漏洞规范

CWE-78漏洞是一类典型的漏洞包括:

  • CWE-89 SQL注入漏洞。
  • CWE-337/676伪随机数漏洞。

CWE-252未检查返回值。如keys = calloc(1, sizeof(int) * sc->files->size);没有检查keys的返回值而size是用户可控的,导致漏洞。语法规范是

1
2
prop calloc_maybe_checked ::=
p := calloc(_) |- when c jmp _ s.t. c/p

局限:无法描述内存冲突漏洞,特别是使用计数器拷贝溢出的,虽然无法检测输入的长度,但是可以检测不安全api造成的漏洞,如strcpy:

1
2
3
 prop if_strcpy_dst_depends ::=
recv(_,*p,_,_),strcpy(_,*q) |- never
s.t. q/p

µflux在这个空间中击中了不同的设计点。 一,µflux模拟具体的动态行为。 这使得我们可以在静态分析(例如别名)和二进制分析(例如变量恢复、面向对象代码标识)中避开昂贵的符号推理技术。 第二,执行行为是由多个策略可参数化的。 这克服了动态技术的局限性,如模糊和具体化执行,其中(A)只能在运行时检测由执行路径触发的bug,(B)必须始终从程序入口点开始。

2.3 动机

函数间以及上下文数据流分析是不可预测的,任何寻求处理该方式的方法都只能使用类似的方法。

一个可行的方法是静态的枚举路径。第二种方法是考虑现实路径,通过使用fuzzing或符号执行来枚举输入。

uflux与上面的设计不同。uflux首先模拟具体的动态行为;其次执行行为可以通过策略实现参数化。这两种方式弥补了动态技术如fuzzing以及符号执行的不足:只能在运行时检测bug以及必须从程序入口点开始执行程序。

2.4 设计

  • 分支策略(Branching Policy):决定与非决定性分支(前者是评估具体走哪条分支后者是走所有的分支)。当使用决定性策略时,会去推断该执行哪条分支以此来避免路径爆炸;而使用非决定性分支时,会忽略分支谓词直接执行所有的分支生成相应的路径。

  • 从任意地方开始执行(Execute Anywhere):uflux可以从中间语言的任意指令处开始执行。允许我们使用相应的策略规范从感兴趣的地方开始执行。

  • 数据依赖(Data Dependence):初始的寄存器以及内存状态可以使用种子策略来生成。我们感兴趣的是数据流而不是数据本身的值。我们对程序术语(值的传递)上的数据流语义感兴趣,以查找漏洞,而不是值本身。

  • 精确度与权衡:为了实现数据依赖关系的高覆盖率、低误报率以及覆盖更多的路径。uflux必须寻找到数据依赖关系并忽略分支的条件。

3. saluki逻辑系统以及语言

Saluki逻辑系统以及语言使得可以推理显示的数据依赖事实,引入了安全策略语言(security policy language)用于表达漏洞模式。

3.1 语法及语义

我们使用特定于域的语言来定义属性,语法允许我们将属性定义为模式序列和一组约束。如果所有模式在给定的约束下匹配成功,那么属性就成立。

语法示例如下图所示:

我们将语义定义为一组公理,如下图所示:

  • 定义1: 函数模型p由三个命题函数组成PP = (T , D, P)。命题T表示存在术语t;命题D(l′, R′, l, R)表示数据流l标签处的r变量传递到了l’处的变量r’;命题P(p, l, R)表示用户定义的谓词p用于表示l标签处的变量R。

  • 定义2: 术语t(program term t)是一个有序的5元组(Lt, St, Ct, Dt, Ut)

    • Lt是唯一标识术语的标签。
    • St是一组静态后继者。
    • Ct是一组影响后继者选择的程序变量。
    • Dt是一组程序变量,由一个术语定义。
    • Ut是术语中使用的一组程序变量。

现从上至下的给出saluki语言的定义:

  • 属性(Property): 公理(prop)指出,如果属性p⊢p’s.t.c成立,则约束c下的模式p的匹配必须意味着在相同约束下匹配串联p,p’。
  • 模式(Patterns):用户定义模式,模式包含逻辑变量,逻辑变量会被绑定到程序的变量,这个过程称之为:模式评估。并用 [p]v =t R表示,其意义为模式p的逻辑变量v模式评估到术语t中的r变量。
  • 约束(Constraints):模式在一些约束下匹配。模式p如果与每个约束都匹配的情况下,在约束列表下匹配。

4. 评估

5.思考

  • 本文中分片段执行代码逻辑的想法很有借鉴意义
  • 在二进制文件中使用安全属性提取相关敏感路径和上下文可供借鉴

参考链接

Paper Note:Saluki: Finding Taint-style Vulnerabilities with Static Property Checking

感谢观看,如有不足或错误,恳请大佬指正 (^_^)#