原文 Backward-Bounded DSE: Targeting Infeasibility Questions on Obfuscated Codes

binsec是一个开源工具，主要的应用领域：恶意软件检测、crash分析、反混淆、漏洞分析。
相当于IDA中的一个插件, 可以去除一些死代码. 实验性质的, 有兴趣的可以玩玩.

反向的意思,就是从后往前收集约束条件, 做符号执行. 与一般方式相反.

有界限的意思,就是设定一个从后往前回溯的界限.

混淆代码的逆向过程中所产生的许多问题归结为不可行问题的求解，下面的文章中提出了后向有界的动态符号执行，可以自动识别不透明谓词，并在CFG图中对其进行裁剪，新生成的CFG图非常精简。相关研究成果发表在2016 blackhat和2017 S&P上：
2016 blackhat Code Deobfuscation:Intertwining Dynamic, Static and Symbolic Approaches
2017 S&P Backward-Bounded DSE: Targeting Infeasibility Questions on Obfuscated Codes

网站 http://binsec.gforge.inria.fr/
源代码 http://binsec.gforge.inria.fr/distrib/binsec-0.1-20170301.tgz 论文发表后就没更新了

工程结构分5部分:

WP1: requirements

WP2: models and generic analysis for binary-level security

WP3: vulnerability analysis

WP4: malware analysis

WP5: experimental evaluation 

作者上传的一个反混淆的演示视频 https://www.youtube.com/watch?v=Z14ab_rzjfA

源代码主要由三部分组成

binsec 反汇编，ocaml语言编写

pinsec 跟踪生成trace，c语言编写

idasec ida插件，python语言编写

安装过程非常麻烦, 等后面有空了, 我再整理一下编译安装过程.

把文中反混淆的实验测试了一下. 如下图所示, 左边是混淆后的代码, 中间是使用BinSec标记后的代码, 右边是BinSec从中间抽取出来的有效代码

摘要

代码混淆是安全分析中的重要内容，动态符号执行提出了一个有趣的方案，比静态分析更强大，比动态分析的更完整。但是，DSE只针对某些种类的反向问题，即可行性问题。

Backward Bounded DSE是一个通用、精确、高效和强大的用来解决不可行问题的方法，我们证明了该方法对不透明谓词和调用堆栈篡改的优势。

Backward Bounded DSE不是要替代现有的DSE，而是通过以可扩展和精确的方式解决不可行性问题来补充DSE。

遵循这条线，我们提出了稀疏反汇编，反向有界DSE和静态分析的组合，能够以有保证的方式扩大动态分析，从而获得最佳的动态和静态分析。这项工作为针对严重混淆的二进制文件进行高效和精确的反汇编工具铺平了道路。

一、介绍

静态分析：IDA、objdump，但是容易被混淆：代码交叉覆盖、不透明谓词、不透明常量、调用堆栈覆盖、自修改

动态分析：仅仅覆盖少量的代码

目前，只有结合动态分析和DSE（Dynamic Symbolic Execution）才强大到足以解决严重混淆的代码。

在这篇文章中，我们感兴趣的是解决(大型)混淆程序的逆向过程中发生的不可行性问题。 预期的方法必须是精确的（低误报率），并且能够在规模（效率）和保护方面（包括自我修改（稳健性））在实际代码上进行扩展，并且足够通用于处理大型不可行性问题。 同时实现所有这些目标尤其具有挑战性.

我们结合软件形式化验证方法的一些最先进的关键功能，如推理验证，有界模型检测或DSE。特别是面向目标的、面向效率的、结合动态信息和形式推理的鲁棒性技术。

提出了Backward-Bounded DSE方法，并做了评估，主要是隐晦谓词和调用堆栈修改方面的测试，也使用了其他的程序做了测试。

最后，给出了两个应用：首先，我们描述了政府级恶意软件X-TUNNEL的深入案例研究，BB-DSE允许识别和删除所有混淆（不透明谓词）。 我们已经能够自动提取功能的去混淆版本 - 丢弃几乎50％的死亡和“虚假”指令，并提供对其保护方案的深入了解，为进一步深入调查奠定了良好的基础。 其次，我们提出了稀疏反汇编，这是一个BB-DSE，动态分析和标准静态反汇编的组合，允许以一种精确的方式扩大动态拆卸 - 获得了最好的动态和静态技术,以及令人鼓舞的初步实验。

也可以应用与其他的混淆，比如虚拟化、自修改

二、背景

混淆

这篇文章主要针对不透明谓词和调用堆栈篡改。

不透明谓词是指一个表达式，他的值在执行到某处时，对程序员而言必然是已知的，但是由于某种原因，编译器或者说静态分析器无法推断出这个值，只能在运行时确定。因此，不透明谓词可以作为控制流混淆时的条件生成器。用它构造一些必真或必假的条件，改造目标程序控制流。举个例子，在执行一些语句序列，如下面这个基本块

{

  statment1;

  statment2;

  statment3;

}

有个表达式，取值总是真或假bool op = true;

那么就可以使用op来改造上面基本块的控制流1，改造成分支结构。{

  statment1;

  if (op) {

    statment2;

    statment3;

  } else {

    statment3;

    statment2;

  }

}

由于else分支根本不可能执行，所以，运行结果和原始程序是等价的。

此文中以7y*y - 1 != x*x为例，这个表达式总是为真

调用堆栈篡改

调用堆栈修改：push X, ret

反汇编 

递归

线性扫描 objdump

动态反汇编

动态符号执行

优缺点：

三、动机

针对上面提到的反汇编中的问题，设计一个有效的方法来解决不可行性问题。

四、后向有界符号执行BACKWARD-BOUNDED DSE    BB-DSE

三个关键要素：

1. 利用推理验证来反向推理，用于精确的目标推理；

2. 与动态分析相结合的形式化方法（DSE），用于鲁棒性；

3. 利用有界模型检验来推理边界，用于可扩展性和执行可行性论证的能力。

从后往前推理，设定执行的指令条数k作为边界，收集约束条件，求解。

k太小，FN(false negative)现象，本身是不透明谓词，被判定为不是不透明谓词

k太大，由于较大的k意味着更多的空间来错过分支，它也产生更多的FP(false positive)。 因此，在一般情况下，较大的k导致较少的FN和更多的FP

实现

BINSEC/SE已开源 Pin + IDA插件

PINSEC运行，记录运行时的变量， 

IDASEC分析

BB-DSE 算法集成在其中。在解析谓词可行性时，执行反向修剪过程，以消除任何无用的变量或约束。

五、使用BB-DSE解决不可行性问题

A. 不透明谓词

3类不透明谓词：

不变量:总是为真或假

上下文关联

动态

动态执行过程中有路径，认为可行，否则调用BB-DSE看是否可行

B. 调用堆栈篡改

1. call和ret时，栈中数据是否相同

2. call和ret时，ESP值是否相同

3. 是否有多个不同的ret地址可满足

使用动态执行和BB-DSE一起，有个表没看懂

C. 其他反混淆相关的不可行性问题

不透明常量：与不透明谓词类似，不透明常量只有一个解

动态跳转闭包：比如switch，判断是否所有的jmp被找到了。判断是否没有其他输入了

虚拟机&CFG扁平化：可以证明很多分支不可达，剪除

条件自修改一撇：没太明白

六、评估：对照实验

A. 初步：与标准DSE比较

DSE不适应于不可行性问题

BB-DSE不适应于可行性问题

B. 不透明谓词评估

测试结果表示，BB-DSE在检测不透明谓词时非常精准，但是边界很重要。试验中10 < k < 30比较好

C. 调用堆栈篡改评估

BB-DSE表现很好，没有FP。该技术同时恢复真正的ret和单目标篡改后的ret。

D. 结论

这些不同的对照实验清晰地证明BB-DSE是一个解决不同种类不可行性问题的非常精确的方法。还表明在实践中找到一个合适的约束k不是一个问题。最后，这种方法似乎是可扩展的。最后一点将在第七章和第八节中得到明确证明。

这些不同的对照实验清楚地表明，BB-DSE是解决不同类型的不可行性问题的一种非常精确的方法。它们还表明，找到一个合适的界限k在实践中不是一个问题。最后，这个方法似乎是可扩展的。最后一点将在第七章和第八节中得到明确证明。

七、使用封装程序进行大规模评估

封装程序是嵌入其他程序并在运行时解压或解密它们的程序。

跟踪指令限制到10000000条。

对一个简单的程序进行加壳，使用了很多常用的加壳软件，如ACProtect/ASPack/UPX…

证明BB-DSE足够有效和健壮

八、真实的恶意程序：X-TUNNEL

APT28使用的一个加密代理组件。

移除死代码和无意义的指令，显示的CFG比原始的要精简很多。

九、应用：稀疏反汇编（SPARSE DISASSEMBLY）

1. 动态跟踪，记录trace及中间一个值

2. 静态分析，在分支处调用BB-DSE，跳过死分支

3. 使用BB-DSE找到call对应的真正的ret

最好的动静结合的反汇编方法。但依然被递归反汇编的固有弱点所限制。

十、讨论：安全分析

三个对抗方法及缓解措施：

1. 把混淆方案的计算分布在一个长的代码序列上，超过BB-DSE中的k值。对于这些“远依赖性的谓词”来说，一个很好的缓解就是依赖一个更一般的k边界的概念，例如基于def-use链长度或者一些公式复杂度标准而不是严格的指令数量。

2. 对策是引入难以解决的谓词（例如基于混合布尔算法或密码散列函数）会造成求解器超时。但是，超时可能反而暴露了重要代码。同时这样措施会使恶意软件设计大大复杂化，可能导致非典型的代码结构，容易出现相关的恶意代码指纹。

3. 一些反动态跟踪的技巧。本文中方法可以与其他技术协同工作，来缓解这个问题。

十一、相关工作

DSE和反混淆。

反向推理。反后推理在无限状态模型检查中很有名，纯粹的向后方法在二进制水平上几乎不可能实现，因为缺少计算跳跃的先验信息。而BB-DSE解决了这个问题。

反汇编。这些方法在伸缩性和健壮性方面仍然面临着重大问题。特别是，自修改很难对付，并且在这个方向中只有很少的工作存在。几项工作试图将静态分析和动态分析相结合，以便更好地反汇编。特别是，codisasm利用动态轨迹进行自动修改程序语法的静态反汇编。

混淆。不透明的谓词，为了检测它们，已经提出了多种方法，特别是抽象解释和最近与DSE的研究。堆栈篡改引起的问题以及最显着的不返回函数，提出了一种基于抽象解释的方法。以上解决方案都不能像BB-DSE那样以可扩展和可靠的方式解决问题。

十二、结论

混淆代码的逆向过程中所产生的许多问题归结为不可行的问题解决。然而，这类问题大多是标准和高级的反汇编工具的盲点。我们提出了后向有界的动态符号执行，一种精确，高效，稳健和通用的方法来解决与反混淆相关的不可行性问题。我们已经证明了这种方法对几个真实类型的混淆如不透明谓词和调用栈篡改的好处，并给出了其他保护方案的见解。后向有界的动态符号执行不取代现有的反汇编方法，而是通过解决不可行性问题来补充它们。接下来，我们展示了如何使用这些技术来解决国家资助的恶意软件（X-TUNNEL），以及如何将这一技术与标准的静态反汇编和动态分析相结合，从而以精确和有保证的方式扩大动态分析。这项工作为针对混淆二进制文件的精确高效的反汇编工具铺平了道路。

[培训]二进制漏洞攻防（第3期）；满10人开班；模糊测试与工具使用二次开发；网络协议漏洞挖掘；Linux内核漏洞挖掘与利用；AOSP漏洞挖掘与利用；代码审计。