PlaidCTF 2021: Plaid Party Planning IV
This year’s edition of the Plaid Party Planning saga explores a type confusion in OCaml. The bug results from two OCaml performance optimizations interacting poorly.
Optimization #1: Float unboxing. When it can, the OCaml compiler will
convert floats from their default representation as heap-allocated
values into 64-bit values in
xmm registers or on the stack.
This optimization is fairly standard and saves a lot of indirections when
working with floats.
Optimiziation #2: Zero-alloc option.
Core_kernel.Uopt module provides a zero-alloc version of
'a option that claims that
'a Uopt.t = 'a. This lie
enables the compiler to elide expensive
Uopt on immediate (as opposed to heap-allocated) values.
Uopt uses a string constant to represent the value
Because string constants are statically allocated, they
never move in memory and never need to be garbage collected,
so there’s no need to
If you combine these two optimizations by using a
you can probably expect some fireworks. The compiler sees
Uopt.none : float Uopt.t as
Uopt.none : float because
of the lying type equality and decides to apply float unboxing
Uopt.none is actually a string.
Instead of unboxing a boxed float, we’re reinterpreting the first
8 characters of
Uopt.none as a 64-bit float.
This unboxed “float” is no longer physically equal to
so any operations checking for none will fail.
Let’s take a look at how this all comes together in Plaid Party Planning IV (PPPIV). Your task in PPPIV is to divide the Plaid party participants up into several breakout rooms and provide them entertainment for the remote afterparty. Each participant has a list of game preferences and each game had a list of attributes. Based on these preferences and attributes, the PPPIV web planner evaluates the assignment to give you a score. Naturally, you’d like to make the score as high as possible.
If you manage to make the score higher than
1e20 the server
will send you the flag.
A back-of-the-envelope calculation indicates that the
evaluation function can only produce scores
of at most
1e7, far short of the needed bound.
Instead, we can look to some
float Uopt.t refs hanging around.
let evaluate_room ~num_people (room : Room.Full.t) = match Float.O.(num_people <= 0.) with | true -> 0. | false -> let result = ref Uopt.none in (match Map.data room.games with |  -> (* talking is worth ... less *) result := Uopt.some 1. | [ g1 ] -> update_if_useful result (evaluate_game ~num_people g1 room.people) ...
result is a
float Uopt.t ref. The documentation
Uopt notes that
It should also not be used in a record that contains only
float Uopt.ts, because the compiler would treat that as a float-only record and would unbox the record fields.
This description is similar but isn’t quite what’s happening here.
In this case, we hit the optimization where refs are stack allocated. The compiler
then sees a stack-allocated float and unboxes it.
Even though a
float ref is a record
with a single float field, without the stack allocation,
the polymorphism in the
'a ref would
prevent the float from being unboxed.
To exploit this bug, we need to somehow keep that unboxed none in the result after processing
all the games.
update_if_useful provides us a way
let[@inline] update_if_useful result value = if not Float.O.(value < 1.337) then result := Uopt.some value ;;
If we produce a game so bad that
evaluate_game lands under 1.337 then
we will keep the unboxed none.
The final evaluation removes any score outliers before returning, so
we need to trigger the bug in 3 out of the 4 rooms.
Now, we need to figure out a way to produce a horrible game. If we fix the number of people in the room, the score on a game is a monotonic function of the sum of the scores of the individual people. It suffices to greedily add people in order of increasing score to find the worst possible people for that game and room size.
Because the total problem size is small, we can iterate over all the games and all the room sizes and compute all the worst possible games.
Writing a little solver gives us 3 mutually-acceptable games that satisfying the requirements:
- luke, b2xiao, and kylar playing War
- zaratec playing Person do Thing by herself
- ubuntor playing Among Us by himself