Binary type inference in Ghidra - The Trail of Bits Blog
Trail of Bits 正在发布 BTIGhidra,这是一个 Ghidra 扩展,通过从二进制文件中推断类型信息来帮助逆向工程师。该分析是过程间的,在函数之间传播和解析类型约束,同时利用用户输入来恢复额外的类型信息。这种精细的类型信息产生更地道的反编译,增强逆向工程的理解能力。下图展示了 BTIGhidra 如何在不需任何用户交互的情况下提高反编译可读性:
图 1:默认 Ghidra 反编译器输出
图 2:运行 BTIGhidra 后的 Ghidra 输出
精确的类型信息将奇怪的指针算术转换为字段访问,将 void* 转换为适当的结构类型;在适当的地方引入数组索引;并减少 void* 转换和解引用的混乱。虽然类型信息对于高质量的反编译至关重要,但恢复精确类型信息不幸地对反编译器和逆向工程师构成了重大挑战。关于变量类型的信息分散在程序中使用该变量的各处。对于逆向工程师来说,在推理局部类型时,很难在脑海中保持变量的分散使用情况。我们创建了 BTIGhidra,努力使这一挑战成为过去。
一个简单示例
让我们看看 BTIGhidra 如何改善来自名为 mooosl 的 CTF 挑战的示例二进制文件的反编译器输出(图 3)。(注意:我们的 GitHub 存储库提供了使用插件重现此演示的说明。)目标函数称为 lookup,迭代链表中的节点,直到在存储在 list_heads 中的哈希映射中找到具有匹配键的节点。¹ 该函数对查询的键进行哈希处理,然后选择存储所有具有该哈希值的键的节点的链表。接下来,它遍历链表寻找与 key 参数相等的键。
图 3:来自 mooosl 的链表查找函数
链表节点的结构(图 4)与此示例特别相关。该结构具有存储在节点中的键和值的缓冲区,以及每个缓冲区的大小。此外,每个节点都有一个 next 指针,该指针要么为 null,要么指向链表中的下一个节点。
图 4:链表节点结构定义
图 5 显示了 Ghidra 对 lookup 函数(FUN_001014fb)的初始反编译器输出。由于整个函数的类型信息较差,整体反编译质量较低。例如,源代码中的递归指针 next 导致 Ghidra 为局部变量(local_18)和返回类型发出 void** 类型。此外,key_size 函数参数(在输出中称为 param_2)的类型被视为 void* 类型,尽管并未从中加载。最后,对保存链表头节点的全局变量(称为 DAT_00104010)的访问未被视为数组索引操作。
图 5:无类型推断的 lookup 函数 Ghidra 反编译器输出。
高亮红色文本在运行类型推断后更改。
图 6 显示了运行 BTIGhidra 后与图 5 代码的差异。注意,输出现在捕获了节点结构和 next 指针的递归类型,键入为 struct_for_node_0_9* 而不是 void**。BTIGhidra 还将返回类型解析为相同类型。此外,key_size 参数(param_2)不再被视为指针。最后,全局变量的类型更新为指向链表节点指针的指针(PTR_00104040),导致 Ghidra 将加载视为数组索引操作。
图 6:有类型推断的 lookup 函数 Ghidra 反编译器输出。
高亮绿色文本由类型推断添加。
BTIGhidra 通过收集一组子类型约束然后解决这些约束来推断类型。已知函数签名的使用充当类型约束的来源。例如,图 5 中对 memcmp 的调用导致对 param_2 的约束,声明 param2 必须是 size_t 的子类型。注意,在图中,BTIGhidra 还成功识别了此函数中使用的四个字段,同时恢复了二进制文件中其他地方使用的附加字段。
此外,用户可以提供已知函数签名,为类型推断算法提供额外的类型信息,以在反编译的程序中传播。图 6 演示了来自已知函数签名(本例中为 value_dump)的新类型信息如何从调用站点流向图 5 中 lookup 函数(在反编译输出中称为 FUN_001014fb)的返回类型。红线描述了如何将用户定义的 value_dump 函数签名用于推断来自原始函数 FUN_001014fb 的返回 struct_for_node_0_9 的 field_at_8 和 field_at_24 的类型。从此调用派生的类型信息与 FUN_001014fb 的所有其他调用站点结合,以便在多态性存在时保持保守。
图 7:从 value_dump 函数签名派生的类型信息的反向传播
最终,BTIGhidra 填充了恢复结构所用字段的类型信息,如图 8 所示。这里,我们看到 field_at_8 和 field_at_24 的类型通过调用 value_dump 推断出来。然而,类型为 undefined8 的字段表明该字段未被添加的函数签名充分约束以派生字段的原子类型(即,没有使用将字段与已知类型信息关联的用法);推断算法仅确定该字段必须为八字节。
图 8:反编译链表节点的结构类型信息表
Ghidra 的反编译器确实使用其预定义类型数据库提供的已知函数签名执行一些类型传播,这些数据库覆盖了诸如 libc 之类的常见库。在反编译调用已知库函数的二进制函数时,这些类型签名用于猜测调用函数变量和参数的可能类型。这种方法有几个限制。Ghidra 不会在没有用户干预的情况下尝试合成复合类型(即结构和联合);由用户定义何时何地创建结构。此外,这种尽力而为的类型传播方法的过程间能力有限。如图 9 所示,Ghidra 的默认类型推断导致 FUN_1014fb 和 FUN_001013db 的类型冲突(void* 与 long 和 ulong),即使参数直接在两个函数之间传递。
图 9:使用 Ghidra 基本类型推断的默认反编译器输出
我们开发 BTIGhidra 的主要动机是需要在 Ghidra 中有一个类型推断算法,能够过程间地传播用户提供的类型信息。为了使这样的算法有用,它不应该猜测“错误”的类型。如果用户提交精确且正确的类型信息,那么类型推断算法不应派生冲突的类型信息,从而阻止使用用户提供的类型。例如,如果用户提供正确的类型 float 而我们推断类型 int,那么这些类型将冲突导致类型错误(形式上由底部格值表示)。因此,推断类型必须是保守的;算法不应为程序变量派生与其源代码级别类型冲突的类型。在具有子类型的类型系统中,此属性可以更精确地表述为“程序变量的推断类型应始终是程序变量实际类型的超类型”。
除了支持用户提供的类型外,BTIGhidra 还克服了 Ghidra 内置类型推断算法的许多其他缺点。即,BTIGhidra 可以操作剥离的二进制文件,合成复合类型,吸收用户提供的类型约束,派生保守的类型判断,并收集二进制文件类型的明确定义的全局视图。
将类型推断引入二进制文件
在源代码级别,类型推断算法通过收集程序文本中表达的程序项上的类型约束来工作,然后解决这些约束以产生每个项的类型。BTIGhidra 遵循类似的原则,但需要补偿编译和 C 的宽松类型引入的信息丢失。BTIGhidra 使用支持子类型、多态性和递归类型的表达性类型系统来推理 C 中常见的编程习惯用法,这些习惯用法利用语言的弱类型来模拟这些类型系统特性。此外,子类型与到达定义分析结合时,允许类型推断算法处理编译器引入的行为,例如寄存器和栈变量重用。
二进制类型推断类似地进行,但编译期间丢失的信息增加了收集类型约束的难度。为了应对这一挑战,BTIGhidra 运行各种流敏感数据流分析(例如,值集分析),这些分析由 FKIE-CAD 的 cwe_checker 提供并使用其实现,以跟踪值如何在程序变量之间流动。这些流告知哪些变量或内存对象必须是其他对象的子类型。抽象地说,如果一个值从变量 x 流入变量 y,那么我们可以保守地得出结论,x 是 y 的子类型。
使用此数据流信息,BTIGhidra 为二进制文件调用图中每个强连通组件(SCC)² 独立生成子类型约束。接下来,BTIGhidra 通过使用一组证明规则来解决 SCC 内有趣变量(即类型常量如 int 和 size_t、函数和全局变量)之间所有可派生关系来简化签名。这些签名在调用时充当函数类型效果的摘要。最后,BTIGhidra 解决每个 SCC 的类型草图,根据需要调用 SCC 的签名。
类型草图是我们对递归约束类型的表示。它们将类型表示为有向图,边由表示类型能力的字段标记,节点由边界 [lb,ub] 标记。图 10 显示了 value_dump 函数签名的类型草图示例。例如,从节点 3 到 8 的路径可以读作“ID 为 3 的类型是一个函数,其第二个输入参数是原子类型,是 size_t 的子类型和 bottom 的超类型。”这些草图在通过相当直接的图遍历降级为 C 类型时提供了方便的类型表示。类型草图还形成一个格,其 join 和 meet 操作符分别由语言交集和并集定义。这些操作在确定可以为二进制中每个函数推断的最精确多态类型时对于操纵类型很有用。Join 允许算法确定两个草图的最小超类型,meet 允许算法确定两个草图的最大子类型。
图 10:value_dump 函数签名的类型草图
多态类型推断的重要性
在 C 没有明确支持多态性的情况下,使用支持多态性的类型系统来推断 C 类型可能看起来奇怪。然而,多态性对于在存在 C 习惯用法时保持保守类型至关重要,例如通过 void 指针分派处理函数中的多种类型。也许 C 中最典型的多态函数例子是 malloc 和 free。
图 11:多态使用 free 的示例程序
在上面的示例中,我们考虑一个简单(尽管人为)的程序,将两个结构传递给 free。我们访问 foo 和 bar 的字段以向类型推断算法揭示字段信息。为了证明多态性的重要性,我修改了类型推断的约束生成阶段,为每个函数生成单个形式类型变量,而不是每个调用站点一个类型变量。此更改具有统一 free 上所有约束的效果,无论调用上下文如何。
resulting 不可靠的反编译如下:
|
|
图 12:produce 参数的不可靠推断类型
函数调用是非多态的假设导致推断出函数参数的过度精确类型(如图 12 所示),导致两个参数具有具有三个字段的相同类型。
BTIGhidra 不是统一函数的所有调用站点,而是为每个调用站点生成一个类型变量,并且仅当推断类型在细化传递后结构相等时才将实际参数类型与形式参数类型统一。这种保守假设允许 BTIGhidra 保持可靠并为图 11 中函数的参数派生两个单独的类型:
|
|
评估 BTIGhidra
二进制文件上的过程间类型推断操作于收集的目标程序的大量信息集。每个涉及的分析本身都是一个困难的计算问题。Ghidra 和我们的流敏感分析使用与控制流、ABI 信息和其他构造相关的启发式方法。这些启发式方法可能导致不正确的类型约束,当传播时可能产生广泛影响。
缓解这些问题需要强大的测试和验证策略。除了 BTIGhidra 本身,我们还发布了 BTIEval,一个用于评估具有已知真实类型的二进制文件上类型推断精度的工具。BTIEval 接受一个带有调试信息的二进制文件,并将 BTIGhidra 恢复的类型与调试信息中的类型进行比较(调试信息在类型推断期间被忽略)。评估实用程序聚合可靠性和精度指标。更广泛地使用 BTIEval 并在更多测试二进制文件上使用将帮助我们为用户提供更好的正确性保证。BTIEval 还收集计时信息,允许我们评估更改的性能影响。
尝试 BTIGhidra
预构建的 Ghidra 插件位于此处或可以从源代码构建。演练说明有助于学习如何运行分析并使用新的类型签名更新它。我们期待获得关于该工具的反馈,并欢迎任何贡献!
致谢
BTIGhidra 的基础类型推断算法受到 Noonan 等人提出的算法的启发并基于该算法。该论文中描述的方法由 GrammaTech, Inc. 持有的工艺专利 US10423397B2 专利。本博客文章中的任何观点、发现、结论或建议均为作者的观点,不一定反映 GrammaTech, Inc. 的观点。
我们还要感谢 CWE Checker 背后的 FKIE-CAD 团队。他们在 Ghidra PCode 上的静态分析平台为我们的分析提供了优秀的基础能力集。
这项研究由 Trail of Bits 进行,基于 DARPA 根据合同号 HR001121C0111 支持的工作(分发声明 A,批准公开发布:分发无限制)。本材料中表达的任何观点、发现和结论或建议均为作者的观点,不一定反映美国政府或 DARPA 的观点。
¹ 如何使用插件重现此演示的说明可在此处获得。
² 图的强连通组件是有向图中一组节点,其中存在从集合中每个节点到集合中每个其他节点的路径。概念上,函数的 SCC 将调用图分离成不相互递归调用的函数组。