Fighting Mutation with Mutation in Living

Hi there,

My previous blog post explored using the living library to avoid use-after-free bugs when using a Ctypes-style OCaml FFI with the garbage collector. It ended with a bit of a whimper as I discovered issues with soundness. I return with a new updated version of the library that does not appear to bear this unfortunate deficiency. This blog post will likely be of interest to those looking to interface OCaml with external resources, such as memory.

The Problem, in Short

First, let us return to the problem code in question:

let my_global_ptr_ptr : int ptr ptr = Living_core.Default.unsafe_free (get_c_ptr ())

let () =
    let my_living_int = 
        let* int_ptr = Living_ctypes.Default.allocate Living_ctypes.Default.int 5 in
        let* () = my_global_ptr_ptr <-@ int_ptr in
        let () = Gc.compact () in
        let* my_int_ptr = !@ my_global_ptr_ptr in
        let* my_int = !@ my_int_ptr in
        Living_core.Default.return my_int
    in
    let my_plain_int = Living_core.Default.unsafe_free my_living_int
    (* let () = Gc.compact () in *)
    in
    Printf.printf "%d = %d\n" my_plain_int 5

Remembering that we have defined soundness of living to be that use-after-free errors (in particular) are impossible to write, assuming you follow a couple of simple rules. Namely:

1. All functions are properly dependent — they correctly track their dependencies, and
2. All calls of unsafe_free produce a value disjoint from their dependencies — eg. not one that accidentally have pointers secretly inside them to their dependencies.

The problem arises above when you consider appending to the code the following top-level binding:

let () =
    let () = Gc.compact () in
    let my_living_int =
        let* my_int_ptr = !@ my_global_ptr_ptr in
        let* my_int = !@ my_int_ptr in
        Living_core.Default.return my_int
    in
    let my_plain_int = Living_core.Default.unsafe_free my_living_int
    in
    Printf.printf "%d = %d\n" my_plain_int 5

Here we have just repeated the dereferencing of my_global_ptr_ptr again, but since int_ptr has already been collected, this results in us accessing garbage memory. All functions were properly dependent, and all unsafe_frees I claimed to be on values disjoint from their dependencies. So what does the “fixed” code look like?

Here is the updated code.

let my_global_ptr_ptr : int ptr ptr Living_core.Default.t = get_c_ptr ()

let () =
    let my_living_int = 
        let* int_ptr = Living_ctypes.Default.allocate Living_ctypes.Default.int 5 in
        let* () = my_global_ptr_ptr <-@ int_ptr in
        let () = Gc.compact () in
        let* my_int_ptr = !@ my_global_ptr_ptr in
        let* my_int = !@ my_int_ptr in
        Living_core.Default.return my_int
    in
    let my_plain_int = Living_core.Default.unsafe_free my_living_int
    (* let () = Gc.compact () in *)
    in
    Printf.printf "%d = %d\n" my_plain_int 5

For those without eagle eyes, the only difference is that my_global_ptr_ptr at the top is not unsafe_freed anymore. In addition, (<-@) now has changed types: Originally,

val (<-@) : 'a ptr -> 'a -> unit Living_core.Default.t

but now,

val (<-@) : 'a ptr Living_core.Default.t -> 'a -> unit Living_core.Default.t

Why these changes? There are two answers: the first is that my_global_ptr_ptr was not disjoint from its dependencies. In fact, its dependencies included itself (this is true of any value constructed using bind, return, (=>) — but not map). Indeed, the Living_ctypes API is specifically designed so that obtaining a pointer wraps that pointer in a Living_core.Default.t. For a function to be properly dependent then if it returns a foreign pointer, it must depend on itself!

The other answer, friends, is mutation. Simply put, (<-@) (and all similar set-like operations) now mutate the dependencies of the value being set to. In order for such a statement to make sense, those values must be already wrapped in a Living_core.Default.t. Since get_c_ptr () is properly dependent, it indeed does this, so removing the unsafe_free is all that is required to make the code safe. Uncommenting the Gc.compact () will now disallow the collection of int_ptr, since it is safely stored in the dependencies of the globally accessible my_global_ptr_ptr.

Why Mutation?

To those that find the idea of mutation distateful, I remind you that the original Ctypes-provided operator had the following type:

val (<-@) : 'a ptr -> 'a -> unit

This function already does mutation. The only reasonable way to deal with that (that I could find) turned out to be to double-down and mutate more. Hopefully this does not turn out to be a slippery slope! But let’s dig into the details.

Lifetimes

I originally tried to solve this problem using Rust-like lifetimes, but they were somewhat intractable to work with, and couldn’t actually provide the guarantees I wanted. However, they provided one clear insight: that set functions are not like get functions, from the point of view of dependencies. Originally, here were the two definitions in Living_ctypes of (<-@) and (!@) — a set and a get function respectively:

open Ctypes

let (<-@) p x = Living_core.Default.(p <-@ x => x)
let (!@) p = Living_core.Default.(!@ p => p)

Where we recall from the previous blog post that r => d should be read as “r depends on d”, or perhaps more usefully (taking the contrapositive), “if d is no longer alive, so too r is no longer alive”. We then examine first (!@); the value obtained from dereferencing p must (as it could too be a pointer) live at least as long as p. Contrapositively, p dying means !@ p must also be dead, from the point-of-view of the garbage collector. Now (<-@): the unit makes this already a bit tricky to interpret. Let us instead pretend it had the signature of a general pure setting function that takes as an argument a continuation that proceeds with the computation after having set the value:

val set : 's -> 'a -> ('s -> 'b) -> 'b

i.e. 's is a “structure”, 'a is a “value in that structure”, and 'b is the value returned by the “rest of the program”. The function parameter, as stated above, represents a function that takes as an argument the structure after 'a has been set inside of it. Our job now is to document then the dependencies of 's, 'a, and 'b.

Thinking contrapositively, we ask for each of these values “if it’s dead, what too must be dead?“. We arrive at the following pseudo-relations.

's => 'a (* Since 'a dying would mean that the 'a inside 's must be dead, so 's must die too *)
'b => 's (* Since 'b can contain 's via the continuation, so if 's dies so too must 'b *)
(* from which if follows that: *)
'b => 'a

The first relation is the most important for our purposes: it tells us that after using a set, 's depends on 'a. If we migrate this reasoning back to the original (<-@) operator, we learn that this means that p must depend on x, after using the set, but our equation only allows the returned unit to depend on x! The only way I can see we can feasibly retain soundness is through mutation of p dependencies, because (<-@) is already an impure function.

Please let me know if you can think of another way.

The definition of (<-@) in Living_ctypes.Default instead requires a new operator add_dep : 'a Living_core.Default.t -> 'b -> unit that, as the name suggests, adds 'b as a dependency of 'a Living_core.Default.t. Here is the updated code:

open Ctypes

let (<-@) (p : 'a ptr Living_core.Default.t) (x: 'a) = 
    Living_core.Default.add_dep p x;
    Living_core.Default.map (fun p' -> p' <-@ x) p

In particular, when binding the returned value in a let*, this no longer propogates any dependencies into the body of the let*. Instead, p’s dependencies are mutated in-place. Because p now contains an x, (i.e. p is not disjoint from its dependencies) it is not (in general) safe to perform Living_core.Default.unsafe_free p.

Reasoning Ability

This change pushes a lot more responsibility on the programmer. Namely, the requirement that a value y be disjoint from its dependencies depends on not only the definition site of y, but the details of the program between then and when you want to call unsafe_free on y. However, it does recover soundness, it seems, so it may be the best we can get.

The other major revelation is that you cannot just unsafe_free an immediately allocated pointer. As stated above, this violates disjointness since that pointer’s Living_core.Default.t depends on the pointer itself! This may seem like a technicality (and kind of is, to be honest), but is important to remember when reasoning about living programs. Indeed, unless the inside a Living_core.Default.t is a scalar (and so by fast-and-loose reasoning can always be considered disjoint from its dependencies), you must use Living_core.Default.map as the last operation on a Living_core.Default.t in order to map it away from being dependent on itself. Living_core.Default.bind will not satisfy this property!

I don’t have a proof of correctness. I’m a mathematician trained, not a computer scientist, and so would only weakly know where to start with defining the semantics of these programs and all the ways they could go wrong in an attempt to prove correctness. Instead, I will likely rely on issues arising through discussion with you, my readers, and through dog-fooding this living library on Godotcaml.

Thanks for reading, and as always, let me know if you have comments, positive or negative, constructive or destructive.

Sincerely,

Matt