HACKvent 2015: Day 15

15 Dec 2015
CTF: Hackvent 2015
Link to challenge:
Date Completed: 15 December 2015



Straight away this looks like a logic solver problem. I intend to use Z3 theorem solver (link) as I am most familiar with it out of all the available solvers out there.

First step is to understand the problem. Each letter corresponds to a single digit 0-9. The q  digit cannot be 0. Each digit is represented by exactly 2 letters. In the grid of equations, a series of letters like bytwycju means 8 digits. Ie if b  was 2 and y  was 8, it would be a number starting with 28XXXXXX. The operations used in the equations are   & ^ | + - ==. C-like operator precedence is also used but this will match up nicely with python operator precedence.

Looking at the secret message, is it 38 pairs of letters. If each letter is a single digit then each pair must correspond to a ASCII  capital letters/numbers/spaces…etc. So I am going to assume the secret message is a 38 character length string.

Every letter from the alphabet is present in the challenge description and equations except for: aekmpr
This works out nicely as excluding those 6 letters leaves 20 letters total which leaves exactly 2 letters per digit, perfect!

So I start writing a new python script and add in all the rules I need. I use a BitVec of 32 bits because some operations become large. I could use a BitVec of 4 bits but then certain bitwise operations would overflow which is not what I want.

For each equation I need to generate a list of long constraints to add to the Z3 solver object. To do this I use a short python script written by OS-Freeze from Germany (thanks!) which was slightly modified by myself:

The above script would produce:

I simply change the equation for each equation in the challenge description until I have all of the constraints I need.

Now I can construct my actual solver script:

This is really a simple script. I use a dictionary called ZV to keep track of all my letters. I add in every letter as 32 bit BitVec’s. Next I add the constraint that ensures each letter is in [0,9]. I add the q != 0 contraint which eliminates the trivial all zero solution. Finally I add all the rules I generated above and run the script!

The following solution is found after 20 seconds or so:

I write a short script to decode the original message using the above solution (or key).
I end up with:

I run the script and the following message is printed:


I enter this into the ball-0-matic, get the daily QR code and the daily flag!

Day 15 Solution Ball

Flag:  HV15-U3bA-BKhc-gNqN-Hit6-C1fK

No Comments

Posted in Hackvent 2015


Leave a Reply