redpwnCTF 2020 - SMarT-solver

Description:

Find the correct flag. :) NOTE: All letters in the flag are lowercase

Files:

As we can guess by the name, this challenge will probably have something to do with “Satisfiability modulo theories”, or SMT for short. Running the program:

> file
SMarT-solver: ELF 64-bit LSB pie executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, for GNU/Linux 3.2.0, BuildID[sha1]=27bf1ae8e39bad973a605ab44e3b36a64e2134c6, not stripped

> ./SMarT-solver
Welcome to SMarT solver!
The #1 solution for your flag checking needs.

Enter a flag: not a flag

Sorry, that is not the correct input.

Too big to open in Ghidra or Binja, so objdump ftw. We can see these repeating blocks in the main function.

movzx 	edx, BYTE PTR [rbp-x]
movzx 	eax, BYTE PTR [rbp-y]
cmp 	dl,al
jbe	somewhere

These are basically doing comparisons against the two values, x and y, and depending on their values, doing a jump to the end of the program or continuing to the next block. Following the jbe to its destination shows us that is just nop’ing and jumping to the same place:

nop
jmp    22f20 <main+0x226c6>

Since main is at 0x85a, it is jumping to the line 0x22f20. These lines at the end just calls puts, which is just the “Sorry, that is not the correct input” after we input the wrong flag.

To solve this, we have to pass all the compares. We can write a parser that will convert the ugly assembly into lines for our z3 script.

So after removing some of the garbage data with some vim-fu and parsing it with the parse.py script, we run the model and get our answer… well not really. We are left with numbers that fit the model, but don’t exactly help us.

input_0xe3 = -5,
input_0xea = 14,
input_0x11f = 6,
input_0x119 = -1,
input_0x115 = -3,
input_0x110 = 17,
input_0xff = -1,
input_0xf0 = 8,
input_0xe2 = 14,
input_0x11b = 14,
...

There was hint that all the numbers were lowercase, so we can assume the numbers correlate to the ascii table, so we add a constraint that each input has to be above 97, the decimal value of ‘a’. We can easily do that modifying our little parse script.

Now running the script gives us:

input_0xe3 = 97,
input_0xea = 116,
input_0x11f = 108,
input_0x119 = 101,
input_0x115 = 99,
input_0x110 = 119,
input_0xff = 101,
input_0xf0 = 110,
input_0xe2 = 116,
input_0x11b = 116,
...

This seems better. Unfortunately, the inputs aren’t sorted in order, but with some vim-fu again, we can fix that. Running a simple python script to grab that character value we get:

flag{thequickbrownfoxjumpedoverthelazydogandlearnedhowtoautomateanalysis|

The last character should be ‘}’ but whatever, close enough :)