Abstraction Recovery for Scalable Static Binary Analysis
2020-07-25 18:32:27 Author: forum.90sec.com(查看原文) 阅读量:661 收藏

Abstract

  • 静态的二进制分析相对于静态源码审计是更困难的，因为二进制处于更底层的位置，缺少了高层的抽象，例如变量，类型，函数，控制结构。

  • 提出了一种抽象恢复的静态二进制分析技术

  • 抽象恢复的前提是很多二进制程序是高层的抽象语言编写的，而且抽象的源代码更适合分析。

  • 抽象恢复的两个应用

    • c语言形式的反编译
    • rop chain的自动生成

  • 抽象恢复并不能应用到所有的二进制分析。

Overview

image-20200717090433767

  • 静态分析和动态分析对比

    • 准确性
      • 动态分析建立在程序执行的基础上，是程序真实存在的行为。
    • 覆盖率
      • 动态分析的输入可能无法覆盖所有程序路径，可能会导致一些bug的miss，但静态分析可以充分考虑这些路径。
    • 环境影响
      • 静态分析需要对外部环境建模，例如syscall,外部函数调用等等。
    • 副作用
      • 静态分析可以避免待测程序运行起来对系统的影响。当待测程序是untrust的时候这非常有必要。

  • 二进制分析的优点

    • 终端用户适用性
      • 二进制分析可以有效的适用于所有可以运行的二进制，而不需要知道源码。
    • 未定义行为
      • 在source 层面，可能有一些语法是比较模糊的，但是在二进制层面，我们可以知道它真正的执行过程，比如一些agressvie optimizers可能造成一些优化带来的安全问题。程序的最终运行还是依赖于编译器，优化程度，flags 等等。
    • 二进制特征
      • 有一些程序只能在二进制层面分析，因为关注的属性并不在source层面。比如automatic exploits generation(AEG)，需要自动化的检测漏洞并构造exploit，AEG需要了解stack frame分部和padding的信息。
    • 语言无关
      • 二进制分析可以适用于不同语言编译出来的二进制程序。从长远来看，可以避免单独给每一门语言写一个独立的analysis tool，是一种非常不同的选择。

  • 二进制分析中的挑战

    • 复杂的语义
      • 一些汇编指令是具有副作用的，比如在条件跳转时，需要flag的信息。如果完全考虑这些情况，对每个汇编指令建模时，将非常复杂。
    • 抽象的缺失
      • 基于source层面的静态分析是无法直接用到二进制的层面的，在编译过程中移除了variables,types,functions,control-flow structure的相关语法结构，而生产一些实际指令，基于实际指令的分析要难于对抽象语法的分析，例如一个局部变量，在source里面有明确的定义，在二进制层面就被放在栈上，可能难以通过栈的结构去区分这些局部变量。
      • 通过不同语言编译出来的二进制，难以在二进制层面有一个自然表示。
    • 间接调用
      • undecidable problem
      • unsound：导致不完整的CFG 或者 过于冗余的CFG

  • 现存二进制分析的方法

    • 中间语言

      • Binary Analysis Platform（BAP）
      • 可以显示的把机器语言产生的副作用flag表示出来
image-20200717202418139

  • 控制流重建

    • 尝试处理间接调用，恢复CFG

  • 抽象恢复

    • 前提：（1 二进制程序通常是从高层的抽象语言编译而来 （2 这些高层的抽象语言更适合做静态分析

    • 方法论：（C or gadget abstractions）

      • 已被编译的应用通过抽象恢复 计算出 抽象程序的行为中可观测的属性
      • 通过抽象恢复再分析要比直接分析应用更快

    • 最大的motivation： the success of static source analysis

    • 源程序 和 二进制程序最大的不同：抽象层次的不同

Source-code Abstractions

  • 反编译器应该关注的两个方面：

    1. 从实际分析出发，尽可能恢复有利于后续分析的抽象表示。
    2. 保证抽象恢复的结果是正确的。

  • 反编译器主要恢复两种抽象类型：

    1. 数据类型抽象
    2. 控制流抽象

  • Phoenix的控制流结构化算法基于structural analysis

    • semantics-preservation
    • iterative refinement

  • 背景知识：

    • 控制流分析：

      • 控制流图用 G = (\mathbb{N},\mathbb{E},n_s,n_e) 形式化的表示，其中 \mathbb{N} 表示BB集合， \mathbb{E} 表示edge集合， n_s 表示entry， n_e 表示exit
      • Domination
        • d dom n ,表示从 n_s 到 n 的每一条路径都经过了 d
        • d pdom n ,表示从 n 到 n_e 都每一条路径都经过了 d
        • immediate dominator : 这个 d 是唯一，$d$ 只是 n 的dominator。eg：f -> d -> n, f和d都是n的dominator，但是d是n的immediate dominator。关于 immediate post-dominator的定义反之亦然。
        • Loops 定义：若 edge (s,d) 是一条后向边，则 d dom s,每一条后向边都可以来定义一个头是 d 的natural loop。
        • natural loop 定义： 一个具体的naturl loop是指可以不通过 d 到达 s 的所有node的集合和 d 本身。

    • Structural Analysis：

      • 解释：Structural Analysis 是一种用来恢复高层控制结构的数据流结构结构化的算法，eg：if-then-esle，loops。
image-20200718165450251

  • SESS Analysis and Tail Regions：

    • motivation：由于Structural Analysis 是无法识别C循环结构中的break和contiune，提出了single exit single successor（SESS）来标识存在这样的退出状态的语句。

    • 方法：将exit状态转化成tail regions。eg：body;break; 将转化成一个tail regions

image-20200718170447307
  • Overview:
image-20200718171031912

  • 控制流图恢复：

    • 使用BAP，生成BIL。

  • 变量和类型恢复：

    • 使用的TIE（ TIE: Principled reverse engineering of types in binary programs），TIE使用Value Set Analysis（WYSINWYX: what you see is not what you execute）来恢复变量地址，然后对变量使用基于静态和条件约束类型推导。

  • 控制流结构化恢复：

    • 以CFG作为基础，在CFG中寻找结构化的shape，相对于在CFG中刻画了一个子图。
    • 两个特征：
      • 迭代细化
      • 语义保留

  • 语句翻译（C格式）：

    • 在CFG上通过对节点结构化的标记，需要把每一个节点所对应的BIL语法翻译成更高层的HIL，eg：比如翻译函数调用，翻译器通过callside处的栈指针，并使用类型信息来计算传参数量。
    • 优化可读性：

      • 删除冗余的死代码

      • untiling optimization （不知道是什么？）

      • tiling: 使用源语言的ast，让汇编语言尽可能的覆盖语法节点，比如$x=(y+z)/w$,首先用一个add指针来填充y+z，然后使用一个div指针来覆盖除法。

      • untiling algorithm ：输入一些statements，输出相同语义的高层次的statements，eg：$High_1[a&b]$ 表示从a&b中提取最高位的1，等价于 a <_s 0\ \&\ b <_s 0 ，（我没有理解这里的等级关系）

  • 语义保留结构分析和迭代式的控制流结构化

    • 语义保留：

      • motivation：structural analysis可以识别出与CFG可达性一致的控制流，但是无法识别于CFG语义一致的控制流。（if-true-false）eg：当x=1 和 y=2时，在源CFG上，在x=1时已经退出loop，但是在中间图上，y=2也可以退出loop，这显然是不对的。
image-20200718181839953

  • 方法：在structural analysis中很多结构化的策略都是保留语义的，但是loop这样的结构化策略，是会忽略语义的。Phoenix通过把这些会丢失语义的策略，替换成保留语义。

  • 迭代细化

    • refinement ： 在CFG上去掉边，并在对应地方加上goto语句

    • Iterative Refinement：重复执行refinement过程，直到可以结构化可以运行。

    • refinement 工作要额外小心，eg：判断b[i]会不会造成溢出，需要考虑i的取值，i是一个循环不变量。如果将while换成goto，可能就无法识别这个地方是安全的。

image-20200718183906656

  • 算法概览

    • 无环模式（当前处理的node 处于无环控制流里面）
      • acyclic schemas
      • switch region
    • 环模式 （当前处理的node 处于环控制流）
      • cyclic schemas
      • loop

  • 无环区域

    • 无环区域定义：C语言中无环控制流操作，指令序列，条件跳转，switch

      image-20200720125702597

    • 从直觉上如果仅靠shape的定义是很难区分控制流结构，例如一个switch 有两个case x=2 和x=3，其实他也是满足if-then-else结构的，但是if-then-else需要有完全相反的条件。

  • 尾部区域和虚拟边

    • motivation：可能在CFG上以某点n为子图无法匹配任何区域，提出了refine的概览，可能通过尝试去掉CFG上的某些边，可以去匹配一些控制流，这个称为refine 迭代过程，直到某次refine之后可以匹配某一个控制流结构以后，就停止refine。

    • 虚拟边：去掉CFG上一些边以后可能改变语义，虚拟边的就是用于在保留语义的情况下去掉一些边。分为两种情况的边：

      • 带条件的有向边
      • 无条件的有向边

      例如 (n_1,n_2) 是无条件的边，当去掉这条边以后，在 n_2 出标记一个标签l，再将 n_1 标识为 Goto[n_1,l] .这样结构再后面可能会被翻译成break 或者 contiune。

image-20200720202225155

  • switch 精修

    • 首先明白incomplete 和 complete switch的区别，下图从n出发所有条件 c_i 都是相对立的，即完整的switch为 \bigvee_{i \in[1,k]}c_i = true ,不完整的switch则相反。

    • switch 匹配策略：

      • 通过refined 虚拟化所有指向switch 头后面的节点。

      • 确保switch里面的node都有相同的后继节点：如果switch头节点的immediate post-dominator是所有case节点的后继，那么这个节点就是switch的 fall through后继。

      • switch的fall through的后继满足三个条件：

        • 首先是所有case节点的后继
        • 不是case节点本身
        • 这个节点有最多的来case节点的入度边。
          image-20200720231558231

      • switch candidate（候选）：通常先匹配IncSwitch，一个通常策略是switch的cases分为jump table 和default。

image-20200720233827301

  • 环区域

    • 如何在节点n处区别不同的循环结构：通过找指向n的后向边，每一条后向边 (n_b,n) 可以定义一个循环体，循环体的节点包括那些可以不通过节点n就能到达 n_b 的所有节点。（其中n为循环头）先优化处理拥有比较小的循环体的循环结构，来优先匹配更大的循环体（因为没有针对嵌套循环的策略）。

    • 三种不同类型的循环结构：（主要条件判断时机）

      image-20200721130226780

    • 特殊的SelfLoop: (可能在c语言里面的呈现形式)
      image-20200721130421151

      但是在结构匹配的时候，可以看到selfloop是没有exit边的，这是可以通过虚拟边做到的，也就是形成所谓的尾区域，来匹配一些 break，contiune，goto等语法结构。

  • 循环结构精修：

    • motivation： 如果发现了一个循环头，但是无法匹配任何循环结构，就开始进行循环结构精修。有环区域什么时候会匹配失败一个循环结构：（1 这个区域有多个入口 （2 这个区域有多个出口 （3 循环体无法被折叠。

    • step1：当有多个入口时，选择有着入度边最多的那个入口为循环头。指向其他入口的边将会被虚拟化

    • step2: 识别循环结构类型：（1 如果有一条exit边从循环体出来，则 循环结构为while （2 如果有循环结构后向边的source节点有一条出度边，则循环结构为dowhile （3 否则，只要有exit边，则循环结构为selfloop。 exit边用于确定循环结构的后继节点，反过来后继节点也可以确定循环结构保护了那些节点。

    • break /contiune：指向循环头的边 用contiune 尾区域来表示。指向循环结构后继节点的边用break 区域来表示，其他所有的虚拟边将变成goto。

    • 精修和非精修的区别：精修在于减少goto的。

      image-20200724101606866

    • step3: 去掉所有影响循环体折叠的边，eg：有一个goto指向了循环体的内部

  • 最后的排序精修

    • Motivation ：当一次迭代过程结束时，如果cfg中的没有一个节点可以被结构化，此时会尝试去掉cfg中的一些边，直到某些节点可以进行结构化。这个过程具有最小的优先级。

    • 去掉边的策略：在dominator tree上进行，优先去掉

      • A--->B ，存在从entry可以不通过A到达B的点。
      • A--->B, A点到exit只能通过B的边。

      这个策略我没太看懂，我觉得需要从大量例子来总结这样的修剪策略

Ceneral Abstractions

  • Gadget Abstractions

    • 源代码抽象的不足：
      • 源代码抽象不能表示所有二进制的语义
      • 源代码抽象不能表示一个二进制的所有行为
      • 隐藏源代码的实际行为，导致一些细节无法被发现，eg: undefined behaviors
    • 一些难以抽象的程序行为
      • get_pc_chunk 返回一个程序计数器的值
      • 代码混淆
      • 编译器优化，eg: inline function (高度优化的程序，可能运行更快但是分析越慢)
    • general abstractions： 指在所有二进制里面都可以适用的抽象。
    • gadget abstraction：gadget 指程序片段，并不需要具体的语义。

  • rop的自动构造：

    • gadget 收集
    • gadget 抽象
    • gadget 分配
Screenshot_from_2020-07-25_16-57-57

图上的Qool是面对gadget设计的一种高层次的语言，可以这样理解，c complier是为了把c语言翻译成可以运行的二进制，Qool可以类比，需要利用gadgets来实现运行我们的目标”程序“，Qool就是这样一种可以让你在高层次来进行编写自定义的程序，最后帮你翻译成gadgets的形式。在高层次编写的时候，你不需要关注gadget的类型和具体指令。c compiler可以使用所有汇编指令，但是Qool就只能使用提前收集好的gadgets。下面是Qool其中的语法：

Screenshot_from_2020-07-25_17-07-19

还需要一些关于gadget 类型的定义：

Screenshot_from_2020-07-25_17-08-15

通过Qool可以翻译成下面形式的语法树：

Screenshot_from_2020-07-25_17-13-40

文章来源: https://forum.90sec.com/t/topic/1225/1
如有侵权请联系:admin#unsafe.sh