原文 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为例，这个表达式总是为真

[招生]科锐逆向工程师培训(2024年11月15日实地，远程教学同时开班, 第51期)