Abstraction Recovery for Scalable Static Binary Analysis

paper

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
  • 背景知识:

    • 控制流分析:

      • 控制流图用 形式化的表示,其中 表示BB集合, 表示edge集合, 表示entry, 表示exit
      • Domination
        • dom ,表示从 的每一条路径都经过了
        • pdom ,表示从 都每一条路径都经过了
        • immediate dominator : 这个 是唯一, 只是 的dominator。eg:f -> d -> n, f和d都是n的dominator,但是d是n的immediate dominator。关于 immediate post-dominator的定义反之亦然。
        • Loops 定义:若 edge 是一条后向边,则 dom ,每一条后向边都可以来定义一个头是 的natural loop。
        • natural loop 定义: 一个具体的naturl loop是指可以不通过 到达 的所有node的集合和 本身。
    • 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 regionsimage-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,让汇编语言尽可能的覆盖语法节点,比如,首先用一个add指针来填充y+z,然后使用一个div指针来覆盖除法。

        • untiling algorithm :输入一些statements,输出相同语义的高层次的statements,eg: 表示从a&b中提取最高位的1,等价于 ,(我没有理解这里的等级关系)

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

    • 语义保留:

      • 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上一些边以后可能改变语义,虚拟边的就是用于在保留语义的情况下去掉一些边。分为两种情况的边:

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

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

        image-20200720202225155
    • switch 精修

      • 首先明白incomplete 和 complete switch的区别,下图从n出发所有条件 都是相对立的,即完整的switch为 ,不完整的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就能到达 的所有节点。(其中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