Ghost in the Shellcode 2015 — Blocky’s Revenge
This past weekend was host to Ghost in the Shellcode 2015, an incredible CTF run by the excellent people in Men in Black Hats and Marauders. The team I play for, Samurai, ended up placing 2nd.
Of special note this year was Pwnadventure — an MMORPG which served as the foundation for 6 of the year’s challenges.
One of the challenges was Blocky’s Revenge, a reverse engineering problem I solved with my brilliant teammate Fugi. You started the challenge by finding “Fort Blox” hidden in one of the game’s many mountain ranges. At the entrance of the fort, was a room, pictured below, with a switch, two wires, a gate, and a locked door. It quickly became clear that the gate was a NOT gate, and that the door could be opened by simply flipping the switch off:
The next room contained an AND gate:
The following two rooms introduced us to OR gates and XOR gates. These rooms weren’t meant to pose a challenge, and instead simply served to introduce us to the rules behind the circuits. The fifth room was where things got difficult:
With a locked door at the far end of the room, and 32 switches at the entrance, it was clear that we were essentially looking at a combination lock, and had to find the arrangement of switches that would unlock the door.
Fugi and myself set to work on transcribing the circuit to paper, so that we could more easily have a feel for what we were looking at. We split the circuit in half, and set to work on migrating it to a Google Docs spreadsheet. After a few hours, we were done.
The circuit contained 40 rows, each with anywhere between 2 and 42 gates.
The spreadsheet gave us a great medium for experimenting with the circuit, while also seeing all of the intermediate state. Try copying the spreadsheet into your own document and modifying the values in the “switch” column to see what we mean.
With 2^32 possibilities, we weren’t prepared to try them all. Instead, realizing that the circuit encoded a boolean formula, and that we were being asked to produce a model that satisfies the formula, we turned to Z3, a theorem prover developed by Microsoft Research.
We used our spreadsheet to define a formula within Z3, then used Z3 to prove satisfiability and produce a model.
Running Z3 — try it yourself online — gives the following model:
Which encodes the solution: 01101001100011111010101111111010
By returning to the game and flipping the switches to their respective positions, the door opens, and the challenge is completed.
