使用KLEE进行密钥生成

引言

在过去几周中，我致力于逆向分析一款软件（名称保密）的序列号验证机制。用户流程十分常见：下载试用版、付款、获取序列号，并通过烦人的弹窗输入序列号激活完整功能版本。为避免对软件开发公司造成损害，本文不会提及软件名称，也不会发布密钥生成器的二进制或源代码。目标是研究真实的序列号验证案例并揭示其弱点。

本文将重点介绍逆向序列验证过程的步骤，以及使用KLEE符号化虚拟机创建密钥生成器的过程。由于无法重现所有逆向细节，我们将专注于密钥生成器本身——这是最有趣的部分。

熟悉目标

该软件是一个x86可执行文件，未采用反调试或反逆向技术。启动时显示一个弹窗，要求输入由客户号、序列号和邮箱地址组成的注册信息。这在软件中十分常见。

工具链

逆向的第一步是找到所有需要分析的关键函数。我使用了IDA Pro配合Hex-Rays反编译器，以及WinDbg调试器。最后部分在Linux下使用KLEE符号化虚拟机、gcc编译器和一些bash脚本。实际的密钥生成器是一个简单的WPF应用程序。

跳过初始部分，因为这不甚有趣。网络上有很多文章可指导使用IDA Pro进行基本逆向技术。我仅遵循一些简单规则：

重命名使用关键数据的函数，即使不清楚具体功能。例如license_validation_unknown_8比默认的sub_46fa39更好；
类似地，重命名感兴趣的数据；
确认错误时更改数据类型：对聚合数据使用结构和数组；
跟踪数据和函数的交叉引用以扩展收集范围；
可能时使用调试器验证假设。例如，若认为变量包含序列号，使用调试器中断并查看。

整体架构

收集最感兴趣的函数后，我尝试理解高级流程和简单函数。以下是验证过程中使用的主要变量和类型。为简化起见，已去除不重要的细节。

1
2
3
4
5


enum {
    ERROR,
    STANDARD,
    PRO
} license_type = ERROR;

全局变量提供许可证类型，用于启用和禁用应用程序功能。

1
2
3
4
5


enum result_t {
    INVALID,
    VALID,
    VALID_IF_LAST_VERSION
};

方便的枚举类型，用作验证结果。INVALID和VALID不言自明。VALID_IF_LAST_VERSION表示该注册仅在当前软件版本为最新时有效。这种奇怪可能性的原因稍后解释。

1
2
3
4
5


#define HEADER_SIZE 8192
struct {
    int header[HEADER_SIZE];
    int data[1000000];
} mail_digest_table;

数据结构，包含已知注册用户的邮箱地址摘要。这是一个嵌入可执行文件的大文件。启动时，资源被提取到临时文件并复制到此结构。头部向量的每个元素是指向数据向量内部的偏移量。

以下是注册检查的伪代码，使用上述数据类型和变量：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22


enum result_t check_registration(int serial, int customer_num, const char* mail) {
    // 验证序列号
    license_type = get_license_type(serial);
    if (license_type == ERROR)
        return INVALID;

    // 验证客户号
    int expected_customer = compute_customer_number(serial, mail);
    if (expected_customer != customer_num)
        return INVALID;

    // 针对已知注册验证
    int index = get_index_in_mail_table(serial);
    if (index > HEADER_SIZE)
        return VALID_IF_LAST_VERSION;
    int mail_digest = compute_mail_digest(mail);
    for (int i = 0; i < 3; ++i) {
        if (mail_digest_table[index + i] == mail_digest)
            return VALID;
    }
    return INVALID;
}

验证分为三个主要部分：

序列号自身必须有效；
序列号与邮箱地址组合必须对应实际客户号；
序列号与邮箱地址之间必须存在对应关系，存储在二进制文件的静态表中。

最后一点有些不同寻常。换句话说：每当客户购买软件时，客户表会更新其数据，并在软件的下一个版本中可用（因为数据嵌入二进制文件中，而非通过互联网下载）。这解释了VALID_IF_LAST_VERSION检查：如果您今天购买软件，当前版本不包含您的数据。您仍然可以获取“专业”版本，直到新版本发布。那时您被迫更新到新版本，以便软件可以使用更新的表验证您的注册。以下是该检查的伪代码：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23


switch (check_registration(serial, customer, mail)) {
case VALID:
    // 注册OK！激活功能
    activate_pro_functionality();
    break;
case VALID_IF_LAST_VERSION:
    {
        // 使用互联网检查当前版本是否最新
        int current_version = get_current_version();
        int last_version = get_last_version();
        if (current_version == last_version)
            // 暂时OK：新版本尚未可用
            activate_pro_functionality();
        else
            // 否则，强制用户下载新版本
            ask_download();
    }
    break;
case INVALID:
    // 注册无效
    handle_invalid_registration();
    break;
}

版本检查通过向特定页面发出HTTP请求完成，该页面返回仅包含软件最新版本号的页面。不要问我为什么保护不完全在服务器端，而是涉及静态表、版本检查等内容。我不知道！

无论如何，这是注册验证函数的整体架构，相当乏味。让我们转向有趣的部分。您可能注意到我提供了主过程的代码，但未提供辅助函数如get_license_type、compute_customer_number等的代码。这是因为我不必逆向它们。它们包含大量对注册数据的算术和逻辑操作，非常难以理解。好消息是我们不必理解它们，只需要逆向它们！

符号化执行

符号化执行是一种使用符号变量而非具体值执行程序的方法。符号变量在值可由用户输入控制时使用（可通过手动或污点分析确定），可以是文件、标准输入、网络流等。符号化执行将程序语义转换为逻辑公式。每条指令导致该公式更新。通过求解一个路径的公式，我们获得变量的具体值。如果这些值在程序中使用，执行将到达该程序点。动态符号化执行（DSE）在运行时逐步构建逻辑公式，一次跟随一个路径。当在执行过程中遇到程序分支时，引擎将条件转换为算术操作。然后选择T（真）或F（假）分支，并用此新约束（或其否定）更新公式。在路径结束时，引擎可以回溯并选择另一条路径执行。例如：

1
2
3
4
5


int v1 = SymVar_1, v2 = SymVar_2; // 符号变量
if (v1 > 0)
    v2 = 0;
if (v2 == 0 && v1 <= 0)
    error();

我们想检查error是否可达，使用符号变量SymVar_1和SymVar_2，分配给程序变量v1和v2。第2行有条件v1 > 0，因此符号化引擎为真分支添加约束SymVar_1 > 0，或为假分支添加SymVar_1 <= 0。然后它继续执行，尝试第一个约束。每当达到新的路径条件，新约束被添加到符号状态，直到该条件不再可满足。此时，引擎回溯并将一些约束替换为其否定，以到达其他代码路径。执行引擎通过求解这些约束及其否定，尝试覆盖所有代码路径。对于到达的每个代码部分，符号化引擎输出覆盖该程序部分的测试用例，提供输入变量的具体值。在给定示例中，引擎继续执行，并在第4行找到条件v2 == 0 && v1 <= 0。路径公式变为：SymVar_1 > 0 && (SymVar_2 == 0 && SymVar_1 <= 0)，这是不可满足的。符号化引擎然后提供满足先前公式（SymVar_1 > 0）的变量值。例如SymVar_1 = 1和SymVar_2的某个随机值。引擎然后回溯到前一个分支，使用约束的否定，即SymVar_1 <= 0。然后添加当前约束的否定以覆盖假分支，得到SymVar_1 <= 0 && (SymVar_2 != 0 || SymVar_1 > 0)。这可通过SymVar_1 = -1和SymVar_2 = 0满足。这结束了程序路径的分析，我们的符号化执行引擎可以输出以下测试用例：

v1 = 1；
v1 = -1, v2 = 0。

这些测试用例足以覆盖程序的所有路径。

这种方法对测试很有用，因为它有助于生成测试用例。它通常有效，且不浪费您大脑的计算能力。您知道…测试非常难以有效进行，而脑力是如此稀缺的资源！

我不想过多阐述这个话题，因为它太大，无法纳入本文。此外，我们不打算按预期方式使用符号化执行引擎进行测试。这只是因为我们不喜欢以预期方式使用事物:)

然而，我将在最后部分指出一些好的参考文献。这里我可以列出符号化执行的一些常见优缺点，仅为您提供一些背景：

优点：

当测试用例失败时，程序被证明不正确；
自动测试用例捕获手动编写测试用例中常被忽略的错误（来自KLEE论文）；
当它工作时很酷:)（来自Jérémy）；

缺点：

当没有测试失败时，我们不能确定一切正确，因为没有给出正确性证明；静态分析在有效时可以做到这一点（但通常无效！）；
覆盖所有路径不足，因为变量在一条路径中可持有不同值，仅其中一些导致错误；
对非平凡程序的完全覆盖通常不可能，由于路径爆炸或约束求解器超时；
扩展困难，引擎执行时间可能受影响；
CPU的未定义行为可能导致意外结果；
…可能还有更多备注要添加。

KLEE

KLEE是符号化执行引擎的一个优秀例子。它操作LLVM字节码，用于软件验证目的。KLEE能够自动生成实现高代码覆盖率的测试用例。KLEE还能发现内存错误，如数组越界访问和许多其他常见错误。为此，它需要程序的LLVM字节码版本、符号变量和（可选）断言。我还准备了一个Docker镜像，其中已配置并准备好使用clang和klee。因此，您没有理由不尝试！以此示例函数为例：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11


#define FALSE 0
#define TRUE 1
typedef int BOOL;

BOOL check_arg(int a) {
    if (a > 10)
        return FALSE;
    else if (a <= 10)
        return TRUE;
    return FALSE; // 不可达
}

这实际上是一个愚蠢的例子，我知道，但让我们假装用这个main函数验证它：

1
2
3
4
5
6
7
8


#include <assert.h>
#include <klee/klee.h>

int main() {
    int input;
    klee_make_symbolic(&input, sizeof(int), "input");
    return check_arg(input);
}

在main中，有一个符号变量用作要测试函数的输入。我们还可以修改它以包含断言：

1
2
3
4
5
6
7
8


BOOL check_arg(int a) {
    if (a > 10)
        return FALSE;
    else if (a <= 10)
        return TRUE;
    klee_assert(FALSE);
    return FALSE; // 不可达
}

我们现在可以使用clang将程序编译为LLVM字节码，并使用klee命令运行测试生成：

1
2


clang -emit-llvm -g -o test.ll -c test.c
klee test.ll

我们得到此输出：

1
2
3
4
5


KLEE: output directory is "/work/klee-out-0"

KLEE: done: total instructions = 26
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2

KLEE将为输入变量生成测试用例，尝试覆盖所有可能的执行路径并使提供的断言失败（如果有）。在这种情况下，我们有两条执行路径和两个生成的测试用例覆盖它们。测试用例在输出目录中（此例中为/work/klee-out-0）。为方便起见，还提供了软链接klee-last，指向最后一个输出目录。该目录内创建了一堆文件，包括两个测试用例，名为test000001.ktest和test000002.ktest。这些是二进制文件，可以使用ktest-tool实用程序检查。让我们尝试：

1
2
3
4
5
6
7


$ ktest-tool --write-ints klee-last/test000001.ktest 
ktest file : 'klee-last/test000001.ktest'
args       : ['test.ll']
num objects: 1
object    0: name: 'input'
object    0: size: 4
object    0: data: 2147483647

第二个：

1
2
3


$ ktest-tool --write-ints klee-last/test000002.ktest 
...
object    0: data: 0

在这些测试文件中，KLEE报告命令行参数、符号对象及其大小和测试提供的值。要覆盖整个程序，我们需要输入变量获得大于10的值和一个小于或等于的值。您可以看到情况如此：在第一个测试用例中使用值2147483647，覆盖第一个分支，而0用于第二个，覆盖另一个分支。

到目前为止，一切顺利。但如果我们这样更改函数呢？

1
2
3
4
5
6
7
8


BOOL check_arg(int a) {
    if (a > 10)
        return FALSE;
    else if (a < 10)    // 而不是 <=
        return TRUE;
    klee_assert(FALSE);
    return FALSE;       // 现在可达
}

我们得到此输出：

1
2
3
4
5
6
7
8


$ klee test.ll 
KLEE: output directory is "/work/klee-out-2"
KLEE: ERROR: /work/test.c:9: ASSERTION FAIL: 0
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 27
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3

这是klee-last目录内容：

1
2
3
4


$ ls klee-last/
assembly.ll   run.istats        test000002.assert.err  test000003.ktest
info          run.stats         test000002.ktest       warnings.txt
messages.txt  test000001.ktest  test000002.pc

注意test000002.assert.err文件。如果我们检查其对应的测试文件，我们有：

1
2
3
4


$ ktest-tool --write-ints klee-last/test000002.ktest 
ktest file : 'klee-last/test000002.ktest'
...
object    0: data: 10

如我们预期，当输入值为10时断言失败。因此，由于我们现在有三条执行路径，我们也有三个测试用例，整个程序被覆盖。KLEE还提供了使用真实程序重放测试的可能性，但我们现在不感兴趣。您可以在KLEE教程中看到使用示例。

KLEE发现应用程序执行路径的能力非常出色。根据OSDI 2008论文，KLEE已成功用于测试GNU COREUTILS中的所有89个独立程序及其等效的busybox端口，发现了先前未发现的错误、错误和不一致。实现的代码覆盖率每工具超过90%。非常棒！

但您可能会问：问题是，谁在乎？您稍后会看到。

使用KLEE逆向函数

由于我们有一个强大的工具来查找执行路径，我们可以使用它来查找我们感兴趣的路径。如Feliam的精彩符号化迷宫帖子所示，我们可以使用KLEE解决迷宫。想法简单但非常强大：用klee_assert(0)调用标记您感兴趣的代码部分，导致KLEE突出显示能够到达该点的测试用例。在迷宫示例中，这就像将read调用更改为klee_make_symbolic，并将prinft("You win!\n")更改为前述的klee_assert(0)。触发此断言的测试用例是解决迷宫的测试用例！

对于一个具体例子，假设我们有这个函数：

1
2
3
4
5


int magic_computation(int input) {
    for (int i = 0; i < 32; ++i)
        input ^= 1 << i;
    return input;
}

我们想知道什么输入我们得到输出253。测试这个的main可能是：

1
2
3
4
5
6
7
8
9


int main(int argc, char* argv[]) {
    int input = atoi(argv[1]);
    int output = magic_computation(input);
    if (output == 253)
        printf("You win!\n");
    else
        printf("You lose\n");
    return 0;
}

如果我们提供符号输入并实际触发断言，KLEE可以为我们解决这个问题：

1
2
3
4
5
6
7
8


int main(int argc, char* argv[]) {
    int input, result;
    klee_make_symbolic(&input, sizeof(int), "input");
    result = magic_computation(input);
    if (result == 253)
        klee_assert(0);
    return 0;
}

运行KLEE并打印结果：

1
2
3
4
5
6
7
8
9


$ clang -emit-llvm -g -o magic.ll -c magic.c
$ klee magic.ll
$ ktest-tool --write-ints klee-last/test000001.ktest
ktest file : 'klee-last/test000001.ktest'
args       : ['magic.ll']
num objects: 1
object    0: name: 'input'
object    0: size: 4
object    0: data: -254

答案是-254。让我们测试它：

1
2
3


$ gcc magic.c
$ ./a.out -254
You win!

是的！

KLEE、libc与命令行参数

并非所有函数都如此简单。至少我们可能有对C标准库的调用，如strlen、