使用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();

我们想通过使用符号变量SymVar_1和SymVar_2（分配给程序变量v1和v2）检查error是否可达。在第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.

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

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

我不想在这个话题上阐述太多，因为它太大，无法融入本文。此外，我们不打算以测试目的使用符号执行引擎。这只是因为我们不喜欢以它们 intended 的方式使用事物 :)

然而，我将在最后部分向你指出一些好的参考资料。这里我可以列出符号执行的一些常见优点和缺点，只是为了给你一点背景：

优点：

当测试用例失败时，程序被证明是不正确的；
自动测试用例捕获了手动编写测试用例中经常被忽视的错误（这来自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并将printf("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!

是的！