 |
| watch_cats |
1 - Introduction
This was a challenge for the CODE BLUE CTF Quals in 2018. The data given was a binary that would display the above, its source code (220 lines of C++) and 5 text files that looked like stage data.
The binary would present a
WATCH_DOGS-style minigame style challenges to the user, who would solve them by rotating 'joints' until they guided a signal from a source to a goal (in later stages, multiple goals at once). After solving five stages, the program would display a flag read from a file and exit. The same binary was also running remotely on the organizers' infrastructure, where it contained the same stage data and the actual competition flag.
The first two stages (pictured above) are solvable by hand. The first one requires you to just rotate one joint into place, the second requires quite a few more rotations, but is still very easy to solve in the 9 iterations that the binary allows you to perform.
 |
| A single joint rotating. |
When you get to the third stage, however, the binary stops showing you visualizations. It's time to dig deeper.
 |
| No image? oh no |
Thankfully, the source code for the challenge was provided. Reading it, we can deduce that:
- The stages are read file-by-file from the local directory.
- Each stage is a plain text file composed of the following records:
- answer, the number of steps a player can take to solve the stage
- num_cables, the number of cables that are between nodes
- num_joints, the number of joints that are connected by cables
- num_joints x (joint_type, 4x neighbor_cable), where joint_type is one of 8 possible types of joints (each with different connectivity geometry), and neighbor_cables are cable numbers [0..num_cables) into which the joint connects
- num_goals, the number of goals that the signal must reach
- num_goals x goal_number, a cable number that defines a goal cable
- H and W, the height and width (in unicode glyphs) of the stage graphic
- H x W of belong data, which defines whether a graphic:
- belongs to a cable and should be colored blue when a signal reaches that cable (belong > 0, cable number == belong), and displayed with font[i, j]
- belongs to a joint and should be colored blue when a signal rached that joint (belong < 0 joint number == -belong), and should be displayed with the joint type graphic
- belongs to neither (belong == 0) and should just be displayed with font[i, j]
Quickly auditing the code from a security point of view, I found no obvious bugs triggerable by user interaction (we're basically limited to rotating selected joints). However, it was obvious that if you solved all five stages, you would just get the flag printed to screen. Let's try that?
First, let's just write some simple Python to read a stage data into memory and allow us to further process it.
 |
| Basic Python to re-implement stage parsing and basic analysis of joints/cables. |
I also added some networkx based code to create a graph of joints/cables (where each joint, cable, source and goal is a node). This let us quickly visualize the stages, and verify that the Stage 2 visualization corresponds to the level visualization:
 |
| Stage 2, as drawn by networkx/graphviz. |
And if you look closely, it does. Now, let's draw the same style of graphs for the stages we haven't solved yet: Stages 3, 4 and 5.
 |
| Stage 3. |
 |
| Stage 4. |
 |
| Stage 5 - nope.jpg. |
By the point I looked at Stage 5, it was clear that the problem was ridiculous enough that I definitely wasn't going to solve it manually - at least not without smarter printing of the graphs so I could see joints and how their rotation changes the signal flow. Let's automate this.
2 - Solving the puzzles automatically
How do we solve a puzzle like this? It might simply be the case that I'm in the proximity of a mind-altering hammer that makes me hallucinate everything to be a nail... but I chose converting the puzzles to Verilog and using formal methods to find solutions. No, wait! Don't close this tab yet. Hear me out.
The theory is simple: let's convert every junction to be a clocked flip-flop that will take on a given cable value as it's new value if a 'joint rotation' register is in the correct position. In other words, the 'signal' propagating in the puzzle will be modeled as a 1 value propagating across joints on positive clock pulses.
 |
| Turning a stage into a Verilog module. |
This will then generate a Verilog module for every stage, looking like this:
 |
| Stage 2, as a Verilog module. |
Now in this current state, this is a decent way of representing a game puzzle in a somewhat esoteric manner. We can run this through a Verilog simulator to replicate the behaviour of the puzzle, but that's somewhat useless.
Here's where formal methods come into play. We'll be using 'yosys-smtbmc', which is a flow that involves running the Yosys synthesizer with an SMT2 backend, and then feeding those SMT2 circuit descriptions into SMT2 solvers. These circuit 'models' can be used for different modes of operation of the solver:
- BMC - bounded model check. Start from the initial Verilog module state and see if you can get it to trigger an assertion within a given amount of steps.
- K-induction. Start from an invalid state, and work backwards to see if that state can be reached from any valid state.
- Coverage. Start from the initial Verilog module state and try to reach a valid cover statement.
If you want to read more about this, Dan Gisselquist has an excellent
series of blogposts about starting with Formal Methods with yosys-smtbmc.
We'll be running in Coverage mode, with a
cover(goal[0] == 1 && ...) statement. This means that yosys-smtbmc will find how to drive the undriven rotation registers in order to get the source signal to 'reach' all the goals.
First order of business is to use
assume statements to let the solver know what sort of behaviour is valid.
We'll first create a
f_past_valid signal that will be 1 from the second cycle of the simulation. This is so that we can use any 'time-travelling' statements like
$past(signal),
$stable(signal), ... in our other formal statements. We also add our
cover statement for reaching the goals. Finally, we also add an assumption that we need to find a state where the amount of total rotations is less or equal to the amount of steps we can take in a stage.
 |
| Emitting formal assume and cover statements in Verilog module for a stage. |
Another thing we want to
assume (declare what is a valid state) is that rotation registers are stable across the execution of the proof:
 |
| Emitting formal assume statement to make joint rotation stable across proof. |
Now, we're ready to see what the solver can find for us! We re-emit the Verilog module (with formal statements) to
s2.v for Stage 2, and write a quick Symbiyosys definition of what we're trying to prove:
 |
| yosys-smtbmc solves Stage 2 of watch_cats. |
Status: PASSED! This means that the solver was able to reach the cover statement. We can now inspect the generated .vcd using GTKWave file to see the progressing state of the circuit in the solution:
 |
| Waveform of solution for Stage 2. |
I've grouped the signals so it's easy to see the progression of the 'electric signal' across cables (
c1,
c2,...
c8) and joints (
s0v,
s1v, ...). The
s0...
s5 signals on the bottom are the joint rotations in which this was possible (2,3,0,1,0,3) - our solution for Stage 2!
We can now write a bit more automation to convert the VCD dumps of the solution into 'rotate' instructions for the challenge binary, and run the same solver succesfully for stages 3 and 4. But for stage 5 (the monster one), we hit a snag:
 |
| Stage 5 impossible to solve. |
Seems like Stage 5 is unsolvable!
3 - The Fifth Stage
What do we do now? I'm going to assume that our solver is correct and in fact the fifth stage is not solvable within the confines of just a simple puzzle problem - we need to hack something!
If you look at the stage5 definition from the organizers, you see it has a very large 'answer' value (the number of steps we can take to solve the problem). While in previous stages this was an at most two-digit number, here we're given 114514 steps. So maybe there is something exploitable here?
Let's dive into the C code. Since the only thing we can interact with is the 'direction'/'rotation' of a joint, let's follow that thread of logic. After not too long, we find an interesting bug:
 |
| Challenge code showing how joints are visited by the original 'simulator'. |
Turns out the 'direction' of a joint is a char. Any time we 'rotate' it as a user, it just increments by one, without checking for overflows. The modulo operator in the
show_circuit function above will seemingly always confine the direction to [0,1,2,3]. But it only does that on joints it's visiting when propagating a 'high' signal.
So if we rotate the joint over 127 times without getting the
show_circuit visitor to visit it and sanitize it, we will overflow into -128, -127, -126, -125..., which on first visit and modulo by 4 will turn into [0, -3, -2, -1, 0, -3, ...]. Then, this negative index will be used to acess the
available array of the joint definition. This underflow will result in an access to the previous joint type's
fonts array.
Since
fonts is an array of non-zero character pointers, any check of
available that reads a
fonts member instead will result in a 'true' availability, so enabled flow for a given direction to a given neighbouring cagle. Thus, if we set the rotation to -127 (-3 after modulo), the new availability will be [1,1,1,
original_available[0]]. If we underflow-hack a joint type whose first
available array member is a 1 (and is not of type 0, so has a preceding type into which we underflow) we in result get a joint that always connects its 4 cables together (its effective availability is [1,1,1,1]).
 |
| Underflow-hack of available member into previous joint definitions' font member. |
So, the plan of action is: find the joint(s) that limit our ability to solve the challenge. Block them off from being visited by
show_circuit by rotating joints in front of it to never reach these joints. Then, underflow their direction to -127 (-3 after modulo), so that connectivity is always all-to-all (if the original joint type was [1, x, x, x]).
I played around a bit with the unsolvable generated Verilog model for Stage 5, and found that if I turn Joint 32 into an always-flowing joint, I can solve the stage with the solver. Good news: it's a joint of type 3 (which has its
availability[0] set to 1), so we can turn it into an always-flowing joint. It's also directly connected to the source via another joint, Joint 32, that we can close off easily so that the
show_circuit visitor never reaches Joint 33.
 |
| Plan of action for hacking Stage 5. |
The final 'rotate command' payload will looking something like this:
- Rotate J33 to block it off.
- Rotate J32 129 times to overflow it to -127 (-3 after modulo), turning it into an always-conducting joint
- Apply rotations from VCD solution for Stage 5, modified to have Joint 33 be always-conducting.
- Rotate J33 to re-enable it.
 |
| Solving the challenge locally. |
That's it! The remote flag was
CBCTF{Which watchdog watches the watchcats????}.
