Saluki: 使用静态属性检查查找污点风格的漏洞

作者： {wh1t3p1g}@ArkTeam

原文作者： Ivan Gotovchits，Rijnard van Tonder，David Brumley

原文标题： Saluki: Finding Taint-style Vulnerabilities with Static Property Checking

原文会议： Network and Distributed Systems Security (NDSS) Symposium 2018

原文链接： http://www.ndss-symposium.org/wp-content/uploads/sites/25/2018/07/bar2018_19_Gotovchits_paper.pdf

saluki是一种用于检查二进制代码中的污点（数据依赖）安全属性的新工具。 Saluki提供了一种用于表达基于污点的策略的特定语言。Saluki在二进制程序分析中包含两个新想法。首先，Saluki使用μflux对二进制文件中数据依赖进行敏感路径，敏感上下文的恢复。其次，Saluki引入了一个合理的逻辑系统来推理数据依赖。作者在该逻辑系统上开发了一种特定的语言，用于表达安全属性。

1.saluki 运行结构

用户分两步检查安全策略。 首先，用户使用 Saluki 策略语言指定他们的安全策略。 Saluki 安全策略用于描述安全污点模式的路径属性。 策略包括两部分：（ a ）识别感兴趣的程序模式，例如，诸如 recv 和 system 之类的 API 调用，以及（ b ）在感兴趣的位置之间进行检查数据依赖关系。

如图所示，saluki的运行结构

• 载入规则
• 将二进制解析为可用于分析的中间代码
• 运行 μflux 以收集有关每个特定来源的执行的数据流。
• 在策略、程序和收集的事实的基础上运行解算器。解算器将确定这个属性是否成立。该求解器实现了一个围绕特定 DSL 构建的新型逻辑系统和算法。
• Saluki 输出结果。

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

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

2.saluki 逻辑系统和语言

作者开发了用于描述安全属性的语言，1中提到的案例就是其中一个例子。语言语法允许我们将属性指定为一系列模式和一组约束。 如果所有模式在给定约束下匹配，则属性成立。 下图为该语言语法

• 定义2——抽象程序模型

  抽象程序模型是一个三元命题函数 P = （ T ， D ， P ）。 命题 Tt 表示存在项 t （见定义2）。 命题 D （ l’ ， R’,l ， R ）表示从具有标记l的程序项中定义的变量 R 到具有标记 l’ 的程序项中使用的变量 R’ 的信息流（数据依赖性）。 命题 P （ p ， l ， R ）表示用户定义的谓词 p ，其用于在具有标号 l 的程序项中使用的变量 R.

• 定义2——程序项t

  程序项t是一个5元组 (L t , S t , C t , D t , U t )

  其中 L t 是唯一标识术语的标签， S t 是一组静态后继者， C t 是影响后继者选择的一组程序变量， D t 是由术语定义的一组程序变量 ， U t 是一组程序变量，用于术语中。

其中语法中的相关定义具体见论文，这里由于篇幅不详细叙述

Saluki 以 1675 行 OCaml 代码实现。 它建立在 BAP 平台之上，目前支持将 x86 ， x86-64 和 ARM 体系结构提升为中间表示。 BAP 为 GNU C 库执行 CFG 恢复和函数原型推理， BAP 使用 LLVM 作为反汇编后端。

项目在线地址： https://github.com/BinaryAnalysisPlatform/bap-plugins/tree/master/saluki

3.讨论

文章主要通过在二进制文件中使用安全属性提取相关敏感路径和上下文，从而进一步分析。文中提到了作者开发的安全属性语言，使用该语言用以描述我们所感兴趣的函数之间的上下文关系。这点其实有点类似属性图的实现，使用属性图的方式构造出相关代码属性库，通过类 SQL 语句，推论上下文关系，从而判断是否存在代码安全问题。文章的提取敏感路径和上下文的方式可供借鉴。