Corwin de Zahr: Exploring OCaml Runtime Safety Through a CTF Challenge

I want to look at OCaml from an angle different from the one we usually use at Jane Street: under the covers, at its runtime. My day job involves making neural-network training run quickly on GPUs, and outside work I spend time on capture-the-flag competitions. This talk brings those interests together.

The setting is a challenge I wrote in 2021 called Secure OCaml Sandbox. The objective is to read a file, which is normally easy in OCaml. I have restricted the environment to make it harder; the question is how those restrictions work and how to get past them within the challenge.

In a capture-the-flag competition, participants typically try to obtain a string called the flag. Challenges can involve cryptography, web applications or reverse engineering. Here the focus is binary exploitation: understanding an application’s actual behavior and finding a bug that changes what it can do.

A challenge like this is educational rather than a realistic sandbox design. For real isolation I would use established tools such as nsjail or bubblewrap, not this construction. A somewhat artificial problem can nevertheless provide a focused way to learn how a runtime works.

The flag is in a file, but the sandbox blocks file-opening primitives as well as other functions that can undermine language soundness. Before looking for a solution, I want to explain what those restrictions are trying to protect.

By soundness I mean, roughly, that a program behaves according to what its language semantics say it can do. Some languages leave categories of behavior undefined; in C, for instance, entering undefined behavior makes reasoning about the outcome much harder. Memory safety is related because programmers depend on a memory abstraction when reasoning about code.

OCaml’s type system is central to how we reason about values and their representations. If a value is used as a type that does not match its actual representation, that reasoning can fail. Interfaces to other languages, such as the C foreign-function interface, are particularly important boundaries to examine.

The challenge uses OCaml modules and shadowing to replace selected definitions with a blocked value. A participant opens the supplied sandbox module before writing code, so the names exposed there hide the original operations. The submitted program is compiled and run under those rules.

The mindset is to look for the difference between intended behavior and real behavior. That adversarial approach is useful beyond competitions: in code review, you need to establish what a change actually does, not merely what its author expected it to do. The same skill matters when reviewing code produced by an AI system.

Four blocked examples help define the sandbox. open_in would produce an input channel for a file, while Sys.command can run a shell command. Array.unsafe_set can write outside an array’s bounds, and Obj.magic lets a value be treated as another type without the usual type-system guarantee.

Obj.magic has a type resembling a function from an arbitrary type to another arbitrary type. That ability defeats the assumptions normally made from the type: the runtime representation does not magically change just because the program treats the value as something else. The challenge therefore blocks the obvious use of it.

A sensible first question is whether I made a simpler mistake and left an easy path open. The intended behavior is to prevent file opening, but the actual behavior depends on everything the sandbox has not blocked. Checking obvious omissions can be the quickest way to solve a challenge.

I search OCaml’s interface files for functions that return an input channel and compare the results with the blocked list. There are few enough candidates to inspect. If an unblocked function directly supplied the needed channel, that would be a much simpler route.

Assuming that direct route is covered, I look for soundness problems. One lead is what I call exceptional polymorphism: a function that appears to produce a value of a type variable without having a correspondingly constrained input. Raising an exception can have a polymorphic result because normal control flow does not return from it.

A search through library interfaces turns up several suspicious candidates. Callback.register takes a name and a value of any type. On its own that may not look dangerous because it returns unit, but the value must eventually be retrieved and used somewhere; the consumer may assume a type different from the registered value’s type.

Stdlib.input_value and Parsing.peek_val also return a polymorphic value from an input channel or parser environment. The runtime does not have the type information needed to verify that the resulting value has the type a caller expects. A mismatch can make code interpret a string as an integer or vice versa.

I focus on Callback.register and trace it through the standard library. Its implementation crosses into an external runtime function, which adds a named value to a table. The next question is where the runtime retrieves and uses that registered value.

Searching the runtime for uses of the named-value lookup leads to the uncaught-exception handler. The runtime retrieves a registered handler and calls it with an exception and another argument. A participant can arrange both the registered handler and an uncaught exception, creating an opportunity for their expected types to disagree.

The first demonstration registers a handler that treats its exception argument as an integer. Raising an exception then produces a number followed by a segmentation fault. The compiler accepted the program, yet the runtime has interpreted a value with the wrong type; that shows a breach of the language-level reasoning the sandbox relied on.

But the challenge asks for the contents of a file, not merely a type-safety failure. To understand what the failure can be used for, I move on to inspect runtime values and the compiled program with tools normally used in binary analysis.

I use GDB for dynamic analysis: examining a program while it is running. PEDA adds a convenient display, and pwndbg is another useful extension. Static-analysis tools such as Ghidra, IDA Pro and Binary Ninja are also valuable when examining a program without executing it, but here I focus on the running process.

A small identity function provides an easy breakpoint. Its compiled instructions and registers show how an argument and a result move through the function. Looking at the string argument in the debugger reveals a pointer to the string’s contents, giving us a first glimpse of the runtime representation.

Next I pass several values to a function that returns a tuple: integers, variants, an exception, a record and other tuples. Disassembling the function helps identify which registers hold the successive arguments and shows data being written into successive memory locations.

The first integers do not appear in the registers as their source-level values. Zero appears as one, one as three, 256 as 513 and one million as two million and one. The observed representation follows 2x + 1; remembering that encoding matters when interpreting later results.

The debugger also shows how variant values appear. Constructors without payloads can be represented as immediate values, while constructors with payloads point to blocks. Looking just before those blocks exposes header information that helps distinguish their representation.

An exception appears as a block containing a header, information identifying the exception and its contents. A record in the example has a comparable block layout. That resemblance suggests that the type-confusion path might let one representation be interpreted as the other.

The next demonstration raises an exception carrying a unit-to-unit identity function, then has the registered callback treat the exception as a record. The record layout includes a field for the tag and a field for the body. In the program’s declared record type, the body is a fully polymorphic function.

Once the handler views that body through the record type, it can call it as if it converted between arbitrary types. In the test, a boolean and a string are printed as integers. The string result corresponds to a pointer-like representation, illustrating that the underlying bits were reinterpreted rather than converted.

This recreates the kind of power associated with Obj.magic, despite the obvious operation having been blocked. It demonstrates a failure of the challenge’s language-level restriction, but the original task still remains: obtain the file contents.

Simply reinterpreting an arbitrary value as an input channel is not enough. A working channel also depends on operating-system state, including a file descriptor and code that performs the actual read. A plausible alternative is to find file-opening code that remains in the compiled binary.

The symbol inspection shows that an open_in implementation is still present. To understand how the demonstration might reach it, I inspect closures: they include a function pointer used when the closure is called. If a closure is viewed through a mismatched representation, that pointer becomes relevant to the challenge.

A further debugger example examines simple functions as values. The code pointer leads to instructions for an addition. Since OCaml integers in this example use the 2x + 1 representation, adding two to a source-level integer corresponds to adding four to the encoded value.

The closure contains more than just a code pointer, but the first field is the one the demonstration focuses on. I outline an approach that uses the type-confusion primitive to examine a closure through a record-like view and then returns it to a function view.

The complete example first obtains the polymorphic reinterpretation through the exception callback. It then works with a closure and the difference between the addresses of its original function and the desired file-opening function. The objective is to call existing runtime code rather than fabricate the operating-system state of an input channel.

The initial attempt produces a segmentation fault instead of the flag. That is a useful debugging result: rather than assuming the idea is correct, I break in the relevant function and follow the calls to see which address is actually being invoked.

The debugger shows that the call is reaching the wrong function. I return to the binary’s symbol information, check the source and target function addresses and correct the difference used by the demonstration. The next run reads the test flag.

The integer representation explains another subtlety. The target address is even, whereas OCaml immediate integers are represented as odd values. In this particular example, working with the difference between two even addresses lets the arithmetic line up with the encoded representation. The details depend on the program and its runtime.

This is one solution to the original 2021 challenge; the archived version uses an older OCaml release. The exercise is an invitation to inspect a concrete system and understand its behavior, not evidence that the toy sandbox is a suitable production boundary.

There are other paths through the challenge. De Zahr notes that complex language implementations can have compiler soundness bugs as well as unsafe runtime interfaces. Some issues have been fixed; others he says remained outstanding at the time of the talk.

He also describes a different approach he used when writing the original challenge: arranging machine instructions inside integer literals and transferring control to them. The tagged representation and limited payload per integer make that approach more involved than the example shown here.

Other runtime or library function pointers could provide further avenues in the challenge. Another participant used an entirely different idea: cause the flag to be loaded into memory and then exploit an incorrect view of a string’s bounds to disclose memory, without needing to execute new code.

The broader lesson is to examine real behavior carefully. Runtime representations, interfaces and assumptions at language boundaries can reveal gaps that are not visible from the intended abstraction. GDB and similar tools make those details observable in a running application.