This weekend, I participated in the TUCTF competition. I am glad to see a familiar CTF pop up from last year – and while I did not make as much progress as I had hoped, it’s always a good thing to have someone keep my ego in check, and to have an indication of where I need to improve my skills.
In this post, I will present two writeups, which I used the Z3 Prover to solve.
This challenge was presented as a Linux binary, and accompanying source code, both of which you can download here.
I first attempted to review the source code, which appeared to perform two primary functions:
- Perform a transposition of a 25-character input string into a 5×5 matrix
- Perform a series of linear equations, which created a string – each byte would be constructed from parts of the matrix (and thus, parts of the input).
This second part is represented in the source code as follows:
The result of this operation (the “auth” string) is then compared against a preset string – if the two are equal, the flag is valid. I initially attempted to use angr to solve the problem by plugging it into a template “find this, give me stdin” script, but I took the opportunity to familiarize myself with the Z3 Prover framework.
With the Z3 framework, we will take the following approach:
- We create a set of variables in the globals() namespace, corresponding to entries in the “mat” array.
- We create a set of constraints, based on the known values (e.g. “mat_1_1 + mat_4_1 == auth_17”, “auth_17 == <known value>”)
- We use the solver to automatically generate a solution for this series of equations, then extract the solution into string form.
Note that there are two shortcomings: firstly, there may be more than one solution (and in this model, we just filter down the inputs until we get one that works), and secondly, using this approach without source code is far trickier than templated angr solves. Still, this gets us close enough that we can manually tweak the characters to get the rest of the flag:
You can download the final Python script here.
In a similar vein to the above, the Grammar Lesson problem was presented as part of the “LuciferVM” challenge, gated behind some easier challenges. This challenge was presented as a text file, which described a set of rules for a grammar, the crucial parts of which are below:
The challenge was to generate a valid “key”, and send it to a remote server.
At a glance, this describes the grammar for a tree-structure, as follows:
Again, with z3, this is rather easy – we simply create a model including each “digit”, limit the characters to between 0 and 9 and let the script do the solving.
This generated random keys, which I then passed to a target server – but on passing one key in, the server would ask for another. I banked on the fact that if I switched the order of the digits around in a pair without changing anything else, I could create a new key which satisfied one of these conditions:
You can download the script used here.
I will stop this post here for cleaner categorization – I will post two more writeups in another post.