Hacking OCaml

Context and Objective

• The presentation focuses on "binary exploitation" techniques applied to the OCaml programming language, specifically within the context of a Capture The Flag (CTF) challenge named "Secure OCaml Sandbox" (created in 2021).
• The core challenge involves escaping a sandbox where standard file reading primitives (open_in), system command execution (Sys.command), and unsound functions (Array.unsafeSet, obj.magic) are blocked.
• The speaker argues that real-world sandboxing (e.g., using nsjail or bwrap) differs from CTF challenges, which are designed for educational purposes to expose internal runtime behaviors and semantics.
• The primary goal of the exploit is to break the soundness of OCaml—specifically its type system—to execute arbitrary operations, ultimately reading a blocked file to retrieve the "flag."

Mechanisms of Soundness Violation

• Exceptional Polymorphism: The speaker identifies "exceptional polymorphism" as a key vulnerability where free type variables (e.g., 'a, 'b) appear in return types without runtime constraints, particularly when exceptions are raised.
• Suspect Functions: Three specific standard library functions were identified as sources of unsoundness because they return a generic 'a type without encoding the actual runtime type:
  • callback.register: Takes a value and registers it, but the retrieval mechanism lacks type constraints on the stored value.
  • Stdlib.input_value: Reads binary data from an input channel and returns a generic 'a, relying entirely on the caller's expectation of the type.
  • Parsing.to_peek: Similar to input_value, returns a generic 'a based on parser input rather than runtime verification.
• Foreign Function Interface (FFI): The boundary between OCaml and C is highlighted as a critical area where type safety is inherently compromised, allowing obj.magic (which has type 'a -> 'b) to directly bypass the type system.

Exploitation Strategy and Runtime Analysis

• Dynamic Analysis Tools: The speaker utilizes GDB extended with PEDA and PwnDBG to perform dynamic analysis, inspecting memory, registers, and the call stack while the OCaml runtime executes.
• Data Representation Discovery:
  • Integers: OCaml integers are stored as 2x + 1 (tagged pointers), meaning they always end in an odd bit (0x1) to distinguish them from pointers.
  • Exceptions and Records: The runtime representation of an exception and a record is identical, consisting of a header word, a tag, and the body data.
  • Closures: Closures are represented as a code pointer followed by an environment; manipulating the closure's memory layout allows the attacker to redirect the function pointer.
• The callback.register Attack Vector: The exploit leverages callback.register to inject an identity function (unit -> unit) into the "uncaught exception handler" (handle_uncaught_exception).
  • When an exception is raised, the handler retrieves the registered value.
  • By raising an exception and registering the identity function, the attacker tricks the runtime into treating the exception body as a function of arbitrary type.
  • This effectively constructs a custom obj.magic function capable of casting any type to any other type.

Execution of the File Read

• Closure Manipulation: The constructed obj.magic is used to reinterpret the memory representation of a closure.
• Function Pointer Redirection: The attacker modifies the internal function pointer of the closure to point to the address of the blocked open_in function within the OCaml runtime binary.
  • Address Calculation: Due to the 2x + 1 integer representation, addresses must be calculated as (target_addr - current_addr) rather than setting the address directly, as target addresses are even (ending in 0) while tagged integers must be odd.
• Successful Execution: The modified closure is invoked as a string-to-channel function, successfully calling open_in, reading the blocked file, and returning the flag.

Alternative Exploitation Vectors Mentioned

• Compiler Soundness Bugs: Independent of runtime manipulation, the speaker notes that historical bugs in the OCaml compiler itself (type system inconsistencies) can be exploited to break soundness without modifying standard library functions.
• Shellcode Injection: A previous method involved packing custom assembly shellcode into integer literals, though this is constrained by the 63-bit integer limit and the odd-number tagging requirement.
• GLIBC Hook Overwriting: Attackers could potentially overwrite global function pointers like malloc or free hooks accessible via the runtime to gain control.
• Heap Leaking via MD5 API: A non-execution attack involves using the MD5 API to load the file content into memory repeatedly, then manipulating the heap structure to leak the flag's memory address and contents without needing to call open_in directly.

Forward-Looking and Educational Implications

• Adversarial Mindset: The talk emphasizes the necessity of an adversarial mindset in code review, particularly with AI-generated code, to identify the gap between "intended behavior" and "actual behavior" in complex systems.
• Runtime Deep Dive: The presentation concludes that understanding low-level runtime behavior is essential for security analysis, even in high-level languages like OCaml that claim strict memory and type safety.