Pwn进你的心
0%

angr的使用与符号执行

Posted on In 3.2k 3 mins.

Angr 介绍

angr 是一个二进制代码分析工具（基于 python），能够自动化完成二进制文件的分析，并找出漏洞

  • 它将以前多种分析技术集成进来，­­­能够进行动态的符号执行分析（类似于 KLEE 和 Mayhem），也能够进行多种静态分析
  • PS：使用符号执行分析一个程序时，该程序会使用符号值作为输入（并非使用具体值），在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值

传统符号执行

传统符号执行是一种静态分析技术

  • 通过使用抽象的符号（静态或者全局变量的名称）代替具体值来模拟程序的执行
  • 当遇到分支语句时，它会探索每一个分支，将分支条件加入到相应的路径约束中
  • 若约束可解，则说明该路径是可达的

接下来就通过以下的伪代码案例来推演这个过程：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
int twice(int v){
    return 2*v;
}

void testme(int x,int y){
    z = twice(y);
    if(z == x){
        if(x>y+10){
            ERROR;
        }
    }
}

int main(){
    x = sym_input();
    y = sym_input();
    testme(x,y);
    return 0;
}
  • 程序不会直接输入具体值，而是输入一个符号值
  • 接着尽可能探索每一个分支，把程序的所有执行路径表示成一棵执行树

符号执行维护了：

  • 符号状态 σ (symbolic state)：变量到符号表达式的映射
  • 符号路径约束 PC (path constraint)：表示当前路径的约束条件

在对程序的某一路径分支进行符号执行的终点，把 PC 输入约束求解器 (constraint solver) 以获得求解，生成实际的输入值

  • PS：如果程序把生成的具体值作为输入执行，它将会和符号执行运行在同一路径，即此时 PC 的公式所表示的路径，并且以同一种方式结束

经典的符号执行有一个关键的缺点，若符合执行路径的符号路径约束无法使用约束求解器进行有效的求解，则无法生成输入

动态符号执行

混合“实际执行”和“符号执行” (concolic execution)，是真正意义上的动态符号执行

  • 经典的符号执行，过度的依赖了符号执行的约束求解能力，限制了传统符号执行的能力发挥
  • 如果能加入具体值进行分析，将大大简化分析过程，降低分析的难度和提升效率
  • 但分析过程中，仍不可避免的还是需要将各种条件表达式，进行符号化抽象后变成约束条件参与执行

将程序语句转换为符号约束的精度，对符号执行所达到的覆盖率以及约束求解的可伸缩性会产生重大影响，所以如何做好 “混合具体(Concrete)执行” 和 “符号(Symbolic)执行” 的能力的平衡，就成为现代符号执行的关键点

选择性符号执行

受路径爆炸和约束求解问题的制约，符号执行不适用于程序规模较大或逻辑复杂的情况，并且对于与外部执行环境交互较多的程序尚无很好的解决方法

选择性符号执行有助于解决这类问题，也是具体执行和符号执行混合的一种分析技术，依据特定的分析，决定符号执行和具体执行的切换使用

  • 用户可以指定一个完整系统中的任意部分进行符号执行分析（可以是应用程序、库文件、系统内核和设备驱动程序等）
  • 选择性符号执行在符号执行和具体执行间转换，并透明地转换符号状态和具体状态
  • 选择性符号执行极大地提高了符号执行在实际应用中对大型软件分析测试的可用性，且不再需要对这些环境进行模拟建模

选择性符号执行在指定区域内的符号化搜索，就是完全的符号执行，在该区域之外均使用具体执行完成，选择性符号执行的主要任务就是在分析前将大程序区分为 “具体执行区域” 和 “符号执行区域”

参考：符号执行（symbolic executio）技术综述

Angr 安装

为了不与 pwntools 库引起冲突，可以采用拉取 docker 镜像的方式进行使用（当然也可以直接 pip install angr 也可以）

1
docker pull angr/angr

以下脚本可以方便我们运行 docker angr：

1
2
3
4
#! /bin/zsh
pwd=`pwd`
script=$1
docker run -it -u angr --rm -v $pwd:/mnt -w /mnt angr/angr "/home/angr/.virtualenvs/angr/bin/python" "/mnt/$script" $2 $3

使用该脚本：

1
./angr script.py

Angr 使用

Github 上有一个针对 angr 的练习集：

这里先通过 00_angr_find 来了解 angr 的基础用法

IDA 分析出来的代码如下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
int __cdecl main(int argc, const char **argv, const char **envp)
{
  int i; // [esp+1Ch] [ebp-1Ch]
  char s1[9]; // [esp+23h] [ebp-15h] BYREF
  unsigned int v6; // [esp+2Ch] [ebp-Ch]

  v6 = __readgsdword(0x14u);
  printf("Enter the password: ");
  __isoc99_scanf("%8s", s1);
  for ( i = 0; i <= 7; ++i )
    s1[i] = complex_function(s1[i], i);
  if ( !strcmp(s1, "JACEJGCS") )
    puts("Good Job.");
  else
    puts("Try again.");
  return 0;
}
  • 其中的 complex_function 是一个加密的过程
1
2
3
4
5
6
7
8
9
int __cdecl complex_function(int a1, int a2)
{
  if ( a1 <= 64 || a1 > 90 )
  {
    puts("Try again.");
    exit(1);
  }
  return (3 * a2 + a1 - 65) % 26 + 65;
}

如果采用常规的解题思维，那就要对 complex_function 进行逆向，分析出输入值，但 angr 采用了不同的做法

先新建一个 angr 工程：

1
p = angr.Project("./00_angr_find")

告诉 angr 一个初始化状态：（Unicorn 框架允许执行任意一段二进制代码）

1
init_state = p.factory.entry_state() # 程序入口点

生成一个 SimulationManagers 对象，用于管理“模拟执行”：

1
sm = p.factory.simulation_manager(init_state)

告诉 SimulationManagers 对象需要查找的路径地址，并开始“模拟执行”：

1
sm.explore(find=0x08048678)
  • angr 会把输入值 s1 转化为一个符号向量（用于决定“模拟执行”的路径）
1
__isoc99_scanf("%8s", s1);
  • 然后遍历所有的程序路径，找到进入各个路径的约束条件：
  • 最后把目标路径的约束输入约束求解器 (constraint solver) 以获得求解，生成实际的输入值

最终的结果存放在 found 中，我们可以打印出来：

1
2
3
found_state = sm.found[0]
print(found_state.posix.dumps(1))
print(found_state.posix.dumps(0))
1
2
b'Enter the password: '
b'JXWVXRKX'