Corwin de Zahr：通过 CTF 挑战探索 OCaml 运行时安全

我想从一个不同于 Jane Street 日常使用方式的角度来看 OCaml：深入其运行时，看看内部机制。我的日常工作是让神经网络训练在 GPU 上运行得更快，工作之外我还参加夺旗赛。这场演讲将两种兴趣结合起来。

背景是我在 2021 年编写的 Secure OCaml Sandbox 挑战。目标是读取一个文件，这在 OCaml 中通常很容易。我限制了环境，使任务变得更难；问题是这些限制如何工作，以及如何在挑战中绕过它们。

在夺旗赛中，参赛者通常要取得一个称为 flag 的字符串。挑战可能涉及密码学、Web 应用或逆向工程。这里的重点是二进制利用：理解应用的实际行为，找到能改变其能力的缺陷。

这种挑战用于教学，并不是现实可用的沙箱设计。如果需要真正的隔离，我会使用 nsjail 或 bubblewrap 等成熟工具，而不是这个方案。不过，有些人工设计的题目可以提供一个集中的方式，帮助理解运行时的工作原理。

flag 位于一个文件中，但沙箱屏蔽了文件打开原语，以及其他可能破坏语言健全性的函数。在寻找解法之前，我想先解释这些限制试图保护什么。

我所说的健全性大致是指，程序的行为符合语言语义所允许的范围。有些语言将某些行为留作未定义；例如在 C 中，进入未定义行为会让结果更难推理。这也与内存安全有关，因为程序员推理代码时依赖内存抽象。

OCaml 类型系统是我们推理值及其表示的基础。如果把一个值当作与其实际表示不匹配的类型使用，这种推理就可能失效。与其他语言交互的接口，例如 C 外部函数接口，是尤其值得检查的边界。

挑战利用 OCaml 模块和遮蔽机制，将选定定义替换成 blocked 值。参赛者在编写代码前打开提供的沙箱模块，因此其中暴露的名称会隐藏原操作。提交的程序在这些规则下编译和运行。

思路是寻找预期行为与实际行为之间的差异。这种对抗性方法在比赛之外也有用：审查代码时，需要确认改动实际上做了什么，而不只是作者希望它做什么。审查 AI 系统生成的代码时，同样需要这种能力。

四个被屏蔽的例子有助于界定沙箱。open_in 会为文件创建输入通道，Sys.command 可以运行 shell 命令，Array.unsafe_set 可以写入数组边界之外，而 Obj.magic 允许将一个值当成另一类型使用，不受通常的类型系统保证约束。

Obj.magic 的类型类似于从任意类型到另一任意类型的函数。这种能力破坏了我们通常根据类型作出的假设：程序把值当成别的类型，并不会让运行时表示随之神奇地改变。因此，挑战屏蔽了对它的直接使用。

合理的第一个问题是：我是否犯了更简单的错误，留下了一条容易走的路？预期行为是禁止打开文件，但实际行为取决于沙箱没有屏蔽的所有操作。检查明显遗漏可能是解决挑战的最快方法。

我搜索 OCaml 的接口文件，寻找返回输入通道的函数，并将结果与屏蔽清单对照。候选项少到可以逐个检查。如果某个未屏蔽函数直接提供了所需通道，那就是简单得多的路径。

假设直接路径已被覆盖，我就寻找健全性问题。一条线索是我称为异常多态的情况：函数似乎能产生某个类型变量的值，却没有相应受约束的输入。抛出异常可以具有多态结果，因为正常控制流不会从该操作返回。

搜索库接口后发现了几个可疑候选项。Callback.register 接收名称和任意类型的值。它返回 unit，因此单看似乎不危险；但这个值最终必须在某处取出并使用，而使用者假设的类型可能不同于注册值的类型。

Stdlib.input_value 和 Parsing.peek_val 也会从输入通道或解析器环境返回多态值。运行时没有所需类型信息，无法验证所得值是否符合调用方预期。类型不匹配可能让代码把字符串解释为整数，或反过来。

我聚焦 Callback.register，并在标准库中追踪它。其实现进入外部运行时函数，将一个具名值加入表中。接下来要问的是，运行时在哪些地方取出并使用这个注册值。

搜索运行时中具名值查找的使用位置，可以找到未捕获异常处理器。运行时取出注册的处理器，传入异常和另一个参数并调用它。参赛者可以安排注册的处理器和未捕获的异常，从而使双方预期的类型出现不一致。

第一个演示注册了一个将异常参数视为整数的处理器。抛出异常后，程序输出一个数字，接着发生段错误。编译器接受了程序，但运行时用错误类型解释了值；这说明沙箱所依赖的语言层推理被打破。

不过，挑战要求取得文件内容，而不只是制造类型安全失效。为了理解这种失效能做什么，我继续使用二进制分析常用工具检查运行时值和编译后的程序。

我用 GDB 进行动态分析，也就是在程序运行时检查它。PEDA 提供便利的显示，pwndbg 是另一个有用的扩展。Ghidra、IDA Pro 和 Binary Ninja 等静态分析工具也有助于不执行程序就进行检查，但这里我聚焦运行中的进程。

一个小型恒等函数提供了方便设置的断点。它的编译指令和寄存器展示参数与结果如何经过函数。在调试器中查看字符串参数，可以看到指向字符串内容的指针，这是我们对运行时表示的第一次观察。

接下来，我向一个返回元组的函数传入多个值：整数、变体、异常、记录和其他元组。反汇编该函数有助于识别各参数所在的寄存器，也能看到数据被写入连续的内存位置。

最初的整数在寄存器中并不是源码层面的值。零显示为一，一显示为三，256 显示为 513，一百万显示为二百万零一。观察到的表示遵循 2x + 1；理解后面的结果时需要记住这个编码。

调试器也展示了变体值的表示。没有载荷的构造器可以表示为立即值，而带载荷的构造器指向内存块。检查块之前的位置可以看到头部信息，有助于区分它们的表示。

异常表现为一个内存块，其中包含头部、标识异常的信息及其内容。例子中的记录具有可比较的块布局。这种相似性暗示，类型混淆路径可能让一种表示被解释为另一种表示。

接下来的演示抛出一个携带 unit 到 unit 恒等函数的异常，然后让注册回调将异常视为记录。记录布局包含标签字段和正文字段。程序声明的记录类型中，正文是完全多态的函数。

处理器通过记录类型查看正文后，可以像它能在任意类型之间转换一样调用它。测试中，布尔值和字符串被作为整数输出。字符串结果对应一种类似指针的表示，说明底层比特只是被重新解释，而不是经过转换。

尽管显而易见的操作已经被屏蔽，这仍然重现了与 Obj.magic 相关的能力。它表明挑战的语言层限制失效，但最初的任务仍然是取得文件内容。

仅仅把任意值重新解释为输入通道是不够的。可用通道还依赖操作系统状态，包括文件描述符和执行实际读取的代码。一种可能的替代方案是寻找仍留在编译后二进制文件中的文件打开代码。

符号检查显示 open_in 的实现仍然存在。为了理解演示可能如何到达它，我检查闭包：闭包包含调用时使用的函数指针。如果通过不匹配的表示来查看闭包，这个指针就与挑战相关。

另一个调试器例子将简单函数作为值检查。代码指针指向执行加法的指令。由于这个例子的 OCaml 整数采用 2x + 1 表示，在源码层将整数加二，相当于将编码值加四。

闭包不止包含代码指针，但演示重点关注第一个字段。我概述一种方法：使用类型混淆原语通过类似记录的视图检查闭包，然后再将它恢复为函数视图。

完整例子首先通过异常回调获得多态的重新解释能力。然后它使用闭包，以及原函数地址与目标文件打开函数地址之间的差值。目标是调用已有的运行时代码，而不是为输入通道伪造操作系统状态。

最初的尝试没有得到 flag，而是发生段错误。这是有用的调试结果：我没有假设思路一定正确，而是在相关函数处设置断点，跟踪调用，查看实际调用的是哪个地址。

调试器显示调用到达了错误的函数。我回到二进制文件的符号信息，检查源函数和目标函数的地址，并修正演示使用的差值。下一次运行读出了测试 flag。

整数表示解释了另一个细节。目标地址是偶数，而 OCaml 立即整数表示为奇数。在这个特定例子中，使用两个偶数地址之差，可以让算术运算与编码表示相匹配。细节取决于具体程序及其运行时。

这是 2021 年原始挑战的一种解法；存档版本使用较旧的 OCaml 版本。这个练习邀请大家检查具体系统并理解其行为，并不能说明这个玩具沙箱适合作为生产环境的安全边界。

挑战还有其他路径。De Zahr 指出，复杂语言实现除了可能有不安全的运行时接口，也可能有编译器健全性缺陷。有些问题已经修复；他说在演讲时仍有一些尚未解决。

他还描述了编写原始挑战时采用的另一种方法：将机器指令放入整数常量，并将控制转移到这些指令。带标签表示和每个整数有限的载荷，使这种方法比这里展示的例子更复杂。

其他运行时或库的函数指针也可能为挑战提供更多路径。另一位参赛者用了完全不同的思路：先让 flag 加载到内存中，再利用对字符串边界的错误视图泄露内存，无须执行新代码。

更广泛的启示是仔细检查真实行为。运行时表示、接口和语言边界处的假设，可能揭示预期抽象中看不到的差距。GDB 等工具让这些细节在运行中的应用里变得可观察。