angrでシンボリック実行をやってみる

Reversing

シンボリック実行とは、プログラム上の変数をシンボルとして扱い、シンボルに対する一連の操作を分析することで条件を満たす入力値を特定するプログラム解析手法である。 ここでは、CTFチームShellphishが開発しているバイナリ解析ツールangrを使い、簡単なプログラムに対してシンボリック実行を適用してみる。

環境

Ubuntu 14.04.4 LTS 64bit版

$ uname -a
Linux vm-ubuntu64 3.19.0-25-generic #26~14.04.1-Ubuntu SMP Fri Jul 24 21:16:20 UTC 2015 x86_64 x86_64 x86_64 GNU/Linux

$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 14.04.4 LTS
Release:        14.04
Codename:       trusty

$ gcc --version
gcc (Ubuntu 4.8.4-2ubuntu1~14.04.1) 4.8.4

angrのインストール

まず、GithubリポジトリのREADMEを参考に、必要なパッケージをインストールする。

$ sudo apt-get install build-essential python-dev libffi-dev python-virtualenv

ディレクトリを作成し、virtualenv環境のもとでangrをインストールする。

$ mkdir angr
$ cd angr/
$ virtualenv ENV
$ . ENV/bin/activate
(ENV)$ pip install angr

簡単なプログラムを解析してみる

ここでは、次のような簡単な認証を行うプログラムについて考える。

/* test.c */
#include <stdio.h>
#include <string.h>

void succeeded()
{
    puts("auth succeeded!");
}

void failed()
{
    puts("auth failed.");
}

int main(int argc, char *argv[])
{
    char username[256];
    char password[256];
    printf("Enter username: ");
    scanf("%s", username);
    printf("Enter password: ");
    scanf("%s", password);
    if (strcmp(username, "admin") == 0 && strcmp(password, "letmein") == 0) {
        succeeded();
    } else {
        failed();
    }
    return 0;
}

ドキュメントを参考に、angrを使って上のプログラムの解析を行うスクリプトを書くと次のようになる。

# solve.py
import angr

p = angr.Project('./test', load_options={'auto_load_libs': False})

addr_main = p.loader.main_bin.get_symbol('main').addr
addr_succeeded = p.loader.main_bin.get_symbol('succeeded').addr
addr_failed = p.loader.main_bin.get_symbol('failed').addr
print "main = %x" % addr_main
print "succeeded = %x" % addr_succeeded
print "failed = %x" % addr_failed

initial_state = p.factory.blank_state(addr=addr_main)
initial_path = p.factory.path(initial_state)
pg = p.factory.path_group(initial_path)
e = pg.explore(find=(addr_succeeded,), avoid=(addr_failed,))

if len(e.found) > 0:
    print 'Dump stdin at succeeded():'
    s = e.found[0].state
    print "%r" % s.posix.dumps(0)

上のスクリプトでは、main関数のアドレスを初期状態とし、succeeded関数に到達するパスを探索した後、その時点での標準入力をダンプする。 このとき、failed関数に到達したパスについてはそれ以上の探索を打ち切る。

プログラムコードをコンパイルし、スクリプトを実行してみる。

(ENV)$ gcc test.c -o test

(ENV)$ python solve.py
main = 4006a8
succeeded = 400686
failed = 400697
Dump stdin at succeeded():
'admin\x00\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x00\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x00\x01\x01\x01\x00letmein\x00\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01'

上の結果から、関数の一覧とsucceeded関数に到達する標準入力のダンプが出力されていることがわかる。 さらに、標準入力のダンプにおいて、認証を通過する入力であるadmin\x00およびletmein\x00が含まれていることが確認できる。

(ENV)$ ./test
Enter username: admin
Enter password: letmein
auth succeeded!

関連リンク