We are provided with a file containing LLVM IR language. It is an intermediate representation used by the LLVM framework to easily handle the backend of the compiler. This means we can compile the checker.ll file into a real binary to then reverse it using a decompiler.
To compile the file, we used these commands
llvm-as checker.ll -o checker.bc
llc checker.bc -o checker.s
gcc checker.s -o checker
We now have a 64 bits x86_64 ELF executable:
file checker
checker: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /nix/store/p9kdj55g5l39nbrxpjyz5wc1m0s7rzsx-glibc-2.40-66/lib/ld-linux-x86-64.so.2, for GNU/Linux 3.10.0, not stripped
Using Ghidra, we can use the decompiler and figure out what is happening in the code in a more readable manner. We clearly see that it takes input and checks it using the checker_i_hardly_know_her function. We see that it simply checks some rules on the input buffer.
bool checker_i_hardly_know_her(char *param_1)
{
int iVar1;
bool bVar2;
bVar2 = false;
if ((((((param_1[4] == param_1[0xe]) && (bVar2 = false, param_1[0xe] == param_1[0x11])) &&
(bVar2 = false, param_1[0x11] == param_1[0x17])) &&
(((bVar2 = false, param_1[0x17] == param_1[0x19] &&
(bVar2 = false, param_1[9] == param_1[0x14])) &&
((bVar2 = false, param_1[10] == param_1[0x12] &&
((bVar2 = false, param_1[0xb] == param_1[0xf] &&
(bVar2 = false, param_1[0xf] == param_1[0x18])))))))) &&
(bVar2 = false, param_1[0x18] == param_1[0x1f])) &&
((((((bVar2 = false, param_1[0x1f] == param_1[0x1b] &&
(bVar2 = false, param_1[0xd] == param_1[0x1a])) &&
(bVar2 = false, param_1[0x10] == param_1[0x1d])) &&
((bVar2 = false, param_1[0x13] == param_1[0x1c] &&
(bVar2 = false, param_1[0x1c] == param_1[0x20])))) && (bVar2 = false, param_1[0x24] == '}')
) && ((bVar2 = false, param_1[6] == '{' &&
(bVar2 = false, (int)param_1[8] == param_1[7] + -0x20)))))) {
iVar1 = strncmp(param_1,"byuctf",6);
bVar2 = false;
if ((((iVar1 == 0) &&
(((bVar2 = false, (int)param_1[9] + (int)param_1[0x14] == param_1[0x1f] + 3 &&
(bVar2 = false, param_1[0x1f] + 3 == (int)*param_1)) &&
(bVar2 = false, (int)param_1[10] == param_1[7] + 6)))) &&
(((bVar2 = false, (int)param_1[8] == param_1[9] + 0x1b &&
(bVar2 = false, (int)param_1[0xc] == param_1[0xd] + -1)) &&
(bVar2 = false, (int)param_1[0xd] == param_1[10] + -3)))) &&
((((bVar2 = false, (int)param_1[10] == param_1[0x10] + -1 &&
(bVar2 = false, (int)param_1[0x10] == param_1[0xe] + -1)) &&
((bVar2 = false, (int)param_1[0x23] == param_1[5] + -2 &&
(((bVar2 = false, (int)param_1[5] == param_1[0x15] + -1 &&
(bVar2 = false, (int)param_1[0x15] == param_1[0x16] + -1)) &&
(bVar2 = false, (int)param_1[0x16] == param_1[0x1c] * 2)))))) &&
((bVar2 = false, (int)param_1[0x21] == param_1[0x20] + 1 &&
(bVar2 = false, param_1[0x20] + 1 == param_1[0x22] + -3)))))) {
bVar2 = (int)param_1[0x1e] == param_1[7] + 1;
}
}
return bVar2;
}
To easily figure out the flag, we can use a SAT solver like Z3. We have to use the checked rules and it will found a solution to the constraints.
from z3 import *
# Create an array of 37 symbolic bytes (since param_1[0x24] = 36 is accessed)
param_1 = [BitVec(f'param_1_{i}', 8) for i in range(37)]
s = Solver()
# Restrict all characters to printable ASCII for sanity
for ch in param_1:
s.add(ch >= 0x20, ch <= 0x7e)
# Conditions from the function
s.add(param_1[4] == param_1[0xe])
s.add(param_1[0xe] == param_1[0x11])
s.add(param_1[0x11] == param_1[0x17])
s.add(param_1[0x17] == param_1[0x19])
s.add(param_1[9] == param_1[0x14])
s.add(param_1[10] == param_1[0x12])
s.add(param_1[0xb] == param_1[0xf])
s.add(param_1[0xf] == param_1[0x18])
s.add(param_1[0x18] == param_1[0x1f])
s.add(param_1[0x1f] == param_1[0x1b])
s.add(param_1[0xd] == param_1[0x1a])
s.add(param_1[0x10] == param_1[0x1d])
s.add(param_1[0x13] == param_1[0x1c])
s.add(param_1[0x1c] == param_1[0x20])
s.add(param_1[0x24] == ord('}'))
s.add(param_1[6] == ord('{'))
s.add(param_1[8] == param_1[7] - 0x20)
# strncmp(param_1, "byuctf", 6) == 0
for i, c in enumerate("byuctf"):
s.add(param_1[i] == ord(c))
# More logic constraints
s.add(param_1[9] + param_1[0x14] == param_1[0x1f] + 3)
s.add(param_1[0x1f] + 3 == param_1[0]) # *param_1 == param_1[0]
s.add(param_1[10] == param_1[7] + 6)
s.add(param_1[8] == param_1[9] + 0x1b)
s.add(param_1[0xc] == param_1[0xd] - 1)
s.add(param_1[0xd] == param_1[10] - 3)
s.add(param_1[10] == param_1[0x10] - 1)
s.add(param_1[0x10] == param_1[0xe] - 1)
s.add(param_1[0x23] == param_1[5] - 2)
s.add(param_1[5] == param_1[0x15] - 1)
s.add(param_1[0x15] == param_1[0x16] - 1)
s.add(param_1[0x16] == param_1[0x1c] * 2)
s.add(param_1[0x21] == param_1[0x20] + 1)
s.add(param_1[0x20] + 1 == param_1[0x22] - 3)
s.add(param_1[0x1e] == param_1[7] + 1)
# Check satisfiability
if s.check() == sat:
m = s.model()
result = ''.join([chr(m[ch].as_long()) for ch in param_1])
print("Found input that satisfies the checker:")
print(result)
else:
print("No solution found.")
Running the program using Python will result to :
python3 decode.py
Found input that satisfies the checker:
byuctf{lL1r_not_str41ght_to_4sm_458d}