Z3 robot
The given file is a 64bit elf not stripped.
Find the binary here: z3_robot
file z3_robot
z3_robot: 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]=bce2975b632a64a4c4af2009a81f41f43619dad1, not stripped
Let’s run it to see what it is about.
./z3_robot
\_/
(* *)
__)#(__
( )...( )(_)
|| |_| ||//
>==() | | ()/
_(___)_
[-] [-] Z3 robot says :z3 Z3Z3z3 Zz3 zz33 3Z Passz3rd? Zz3 zZ3 3Z Z3Z3z
->
So it’s looks like the binary waits a password.
I decompiled it with IDA to have the pseudo code, as it will make the reversing part fast enough. Below is the pseudo code of the check password function.
undefined8 check_flag(byte *param_1)
{
undefined8 uVar1;
byte bVar2;
if (((((((((((param_1[0x14] ^ 0x2b) == param_1[7]) &&
((int)(char)param_1[0x15] - (int)(char)param_1[3] == -0x14)) &&
((char)param_1[2] >> 6 == '\0')) &&
((param_1[0xd] == 0x74 && (((int)(char)param_1[0xb] & 0x3fffffffU) == 0x5f)))) &&
((bVar2 = (byte)((char)param_1[0x11] >> 7) >> 5,
(int)(char)param_1[7] >> ((param_1[0x11] + bVar2 & 7) - bVar2 & 0x1f) == 5 &&
(((param_1[6] ^ 0x53) == param_1[0xe] && (param_1[8] == 0x7a)))))) &&
((bVar2 = (byte)((char)param_1[9] >> 7) >> 5,
(int)(char)param_1[5] << ((param_1[9] + bVar2 & 7) - bVar2 & 0x1f) == 0x188 &&
(((((int)(char)param_1[0x10] - (int)(char)param_1[7] == 0x14 &&
(bVar2 = (byte)((char)param_1[0x17] >> 7) >> 5,
(int)(char)param_1[7] << ((param_1[0x17] + bVar2 & 7) - bVar2 & 0x1f) == 0xbe)) &&
((int)(char)param_1[2] - (int)(char)param_1[7] == -0x2b)) &&
(((param_1[0x15] == 0x5f && ((param_1[2] ^ 0x47) == param_1[3])) &&
((*param_1 == 99 && ((param_1[0xd] == 0x74 && ((param_1[0x14] & 0x45) == 0x44)))))))))))
) && ((param_1[8] & 0x15) == 0x10)) &&
(((param_1[0xc] == 0x5f && ((char)param_1[4] >> 4 == '\a')) && (param_1[0xd] == 0x74)))) &&
(((((bVar2 = (byte)((char)*param_1 >> 7) >> 5,
(int)(char)*param_1 >> ((*param_1 + bVar2 & 7) - bVar2 & 0x1f) == 0xc &&
(param_1[10] == 0x5f)) &&
((((int)(char)param_1[8] & 0xacU) == 0x28 &&
((param_1[0x10] == 0x73 && ((param_1[0x16] & 0x1d) == 0x18)))))) &&
((param_1[9] == 0x33 &&
((((param_1[5] == 0x31 && (((int)(char)param_1[0x13] & 0x3fffffffU) == 0x72)) &&
((char)param_1[0x14] >> 6 == '\x01')) &&
(((char)param_1[7] >> 1 == '/' && (param_1[1] == 0x6c)))))))) &&
(((((((char)param_1[3] >> 4 == '\a' &&
(((param_1[0x13] & 0x49) == 0x40 && (param_1[4] == 0x73)))) &&
((param_1[0xb] & param_1[2]) == 0x14)) &&
(((((*param_1 == 99 && ((int)(char)param_1[5] + (int)(char)param_1[4] == 0xa4)) &&
(((int)(char)param_1[0xf] & 0x3ffffffU) == 0x5f)) &&
((((param_1[10] ^ 0x2b) == param_1[0x11] && ((param_1[0xc] ^ 0x2c) == param_1[4])) &&
(((int)(char)param_1[0x13] - (int)(char)param_1[0x15] == 0x13 &&
((param_1[0xc] == 0x5f && (param_1[0xc] == 0x5f)))))))) &&
((char)param_1[0xf] >> 1 == '/')))) &&
(((param_1[0x13] == 0x72 && ((int)(char)param_1[0x12] + (int)(char)param_1[0x11] == 0xa8))
&& (param_1[0x16] == 0x3a)))) &&
(((param_1[0x15] & param_1[0x17]) == 9 &&
(bVar2 = (byte)((char)param_1[0x13] >> 7) >> 5,
(int)(char)param_1[6] << ((param_1[0x13] + bVar2 & 7) - bVar2 & 0x1f) == 0x18c)))))))) &&
(((((((int)(char)param_1[7] + (int)(char)param_1[3] == 0xd2 &&
((((int)(char)param_1[0x16] & 0xedU) == 0x28 && (((int)(char)param_1[0xc] & 0xacU) == 0xc)
))) && ((param_1[0x12] ^ 0x6b) == param_1[0xf])) &&
((((((((param_1[0x10] & 0x7a) == 0x72 && ((*param_1 & 0x39) == 0x21)) &&
((param_1[6] ^ 0x3c) == param_1[0x15])) &&
((param_1[0x14] == 0x74 && (param_1[0x13] == 0x72)))) && (param_1[0xc] == 0x5f)) &&
(((param_1[2] == 0x34 && (param_1[0x17] == 0x29)) &&
((param_1[10] == 0x5f &&
((((param_1[9] & param_1[0x16]) == 0x32 &&
((int)(char)param_1[2] + (int)(char)param_1[3] == 0xa7)) &&
((int)(char)param_1[0x11] - (int)(char)param_1[0xe] == 0x44)))))))) &&
(((param_1[0x15] == 0x5f && ((param_1[0x13] ^ 0x2d) == param_1[10])) &&
((((int)(char)param_1[0xc] & 0x3fffffffU) == 0x5f &&
(((((param_1[6] & 0x40) != 0 && ((param_1[0x16] & param_1[0xc]) == 0x1a)) &&
((bVar2 = (byte)((char)param_1[0x13] >> 7) >> 5,
(int)(char)param_1[7] << ((param_1[0x13] + bVar2 & 7) - bVar2 & 0x1f) == 0x17c &&
((((param_1[0x14] ^ 0x4e) == param_1[0x16] && (param_1[6] == 99)) &&
(param_1[0xc] == param_1[7])))))) &&
(((int)(char)param_1[0x13] - (int)(char)param_1[0xd] == -2 &&
((char)param_1[0xe] >> 4 == '\x03')))))))))))) &&
(((param_1[0xc] & 0x38) == 0x18 &&
(((bVar2 = (byte)((char)param_1[10] >> 7) >> 5,
(int)(char)param_1[8] << ((param_1[10] + bVar2 & 7) - bVar2 & 0x1f) == 0x3d00 &&
(param_1[0x14] == 0x74)) &&
((bVar2 = (byte)((char)param_1[0x16] >> 7) >> 5,
(int)(char)param_1[6] >> ((param_1[0x16] + bVar2 & 7) - bVar2 & 0x1f) == 0x18 &&
(((((int)(char)param_1[0x16] - (int)(char)param_1[5] == 9 &&
(bVar2 = (byte)((char)param_1[0x16] >> 7) >> 5,
(int)(char)param_1[7] << ((param_1[0x16] + bVar2 & 7) - bVar2 & 0x1f) == 0x17c)) &&
(param_1[0x16] == 0x3a)) &&
((param_1[0x10] == 0x73 && ((param_1[0x17] ^ 0x1d) == param_1[0x12])))))))))))) &&
((((int)(char)param_1[0xe] + (int)(char)param_1[0x17] == 0x59 &&
(((param_1[2] & param_1[5]) == 0x30 && (((int)(char)param_1[0xf] & 0x9fU) == 0x1f)))) &&
((param_1[4] == 0x73 &&
(((param_1[0x17] ^ 0x4a) == *param_1 && ((param_1[6] ^ 0x3c) == param_1[0xb])))))))))) {
uVar1 = 1;
}
else {
uVar1 = 0;
}
return uVar1;
}
As we can see there are a lot of tests to check each character of the password. As mentioned by the challenge title, we can use the Z3 solver.
To do so, I extracted few tests to give them to the Z3 solver.
#! /bin/env python
from z3 import *
keyLenght = 25
solver = Solver()
# bit vector with password lenght
param_1 = [BitVec('pw{}'.format(i), 8) for i in range(0,24)]
solver.add(param_1[0] == 99)
solver.add(param_1[1] == 0x6c)
solver.add(param_1[2] == 0x34)
solver.add(param_1[3] == 115)
solver.add(param_1[4] == 0x73)
solver.add(param_1[5] == 0x31)
solver.add(param_1[6] == 99)
solver.add(param_1[7] + 115 == 0xd2)
solver.add(param_1[8] == 0x7a)
solver.add(param_1[9] == 0x33)
solver.add(param_1[10] == 0x5f)
solver.add(param_1[0xb] == 0x3c ^ 99)
solver.add(param_1[0xc] == 0x5f)
solver.add(param_1[0xd] == 0x74)
solver.add(param_1[0xe] == 0x53 ^ 99)
solver.add(param_1[0xf] == param_1[0x12] ^ 0x6b)
solver.add(param_1[0x10] == 0x73)
solver.add(param_1[0x11] - param_1[0xe] == 0x44)
solver.add(param_1[0x12] + param_1[0x11] == 0xa8)
solver.add(param_1[0x13] == 0x72)
solver.add(param_1[0x14] == 0x74)
solver.add(param_1[0x15] == 0x5f)
solver.add(param_1[0x16] == 0x3a)
solver.add(param_1[0x17] == 0x29)
if solver.check() == sat:
model = solver.model()
flag = ""
print(model)
# print ascii
for i in param_1:
flag += chr(model[i].as_long())
print(flag)
else:
print("Unsat")
After few seconds of trial, the following password will be given: cl4ss1c_z3___t0_st4rt_:) and can be used to validate the challenge.
./z3_robot
\_/
(* *)
__)#(__
( )...( )(_)
|| |_| ||//
>==() | | ()/
_(___)_
[-] [-] Z3 robot says :z3 Z3Z3z3 Zz3 zz33 3Z Passz3rd? Zz3 zZ3 3Z Z3Z3z
-> cl4ss1c_z3___t0_st4rt_:)
\_/
(* *)
__)#(__
( )...( )(_)
|| |_| ||//
>==() | | ()/
_(___)_
[-] [-] Z3 robot says :
Well done, valdiate with shkCTF{cl4ss1c_z3___t0_st4rt_:)}