Ghidra中的二进制类型推断 - Trail of Bits博客
Trail of Bits发布了BTIGhidra,这是一个Ghidra扩展,通过从二进制文件中推断类型信息来帮助逆向工程师。该分析是过程间的,在函数之间传播和解析类型约束,同时利用用户输入来恢复额外的类型信息。这种精细的类型信息产生更地道的反编译结果,增强了逆向工程的理解。下图展示了BTIGhidra如何无需用户交互即可提高反编译可读性:
图1:默认Ghidra反编译器输出
图2:运行BTIGhidra后的Ghidra输出
精确的类型信息将奇怪的指针算术转换为字段访问,将void转换为适当的结构类型;在适当的地方引入数组索引;并减少了void转换和间接引用的混乱。虽然类型信息对于高质量的反编译至关重要,但恢复精确的类型信息不幸地对反编译器和逆向工程师构成了重大挑战。关于变量类型的信息分散在程序中使用该变量的任何地方。对于逆向工程师来说,在推理局部类型时,很难在脑海中保持变量的分散使用。我们创建了BTIGhidra,努力使这一挑战成为过去。
一个简单的例子
让我们看看BTIGhidra如何改进来自CTF挑战mooosl的示例二进制文件的反编译输出(图3)。(注意:我们的GitHub存储库提供了使用插件重现此演示的说明。)目标函数称为lookup,迭代链表中的节点,直到在存储在list_heads中的哈希映射中找到匹配键的节点。¹ 该函数对查询的键进行哈希处理,然后选择存储所有具有该哈希值的键的节点的链表。接下来,它遍历链表寻找与键参数相等的键。
图3:来自mooosl的链表查找函数
链表节点的结构(图4)与此示例特别相关。该结构具有存储在节点中的键和值的缓冲区,以及每个缓冲区的大小。此外,每个节点都有一个next指针,该指针要么为null,要么指向链表中的下一个节点。
图4:链表节点结构定义
图5显示了Ghidra对lookup函数(FUN_001014fb)的初始反编译器输出。由于整个函数的类型信息较差,整体反编译质量较低。例如,源代码中的递归指针next导致Ghidra为局部变量(local_18)和返回类型发出void**类型。此外,键大小函数参数(在输出中称为param_2)的类型被视为void*类型,尽管没有从中加载。最后,对保存链表头节点的全局变量(称为DAT_00104010)的访问不被视为数组索引操作。
图5:无类型推断的lookup函数Ghidra反编译器输出。
突出显示的红色文本在运行类型推断后更改。
图6显示了运行BTIGhidra后与图5代码的差异。注意,输出现在捕获了节点结构和next指针的递归类型,键入为struct_for_node_0_9*而不是void**。BTIGhidra还将返回类型解析为相同类型。此外,键大小参数(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的类型是一个函数,其第二个in参数是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 unsound反编译如下:
|
|
图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的观点。
¹如何使用插件重现此演示的说明可在此处获得。
²图的强连通组件是