category : reverse
points : 188
Description
I made a robot that can only communicate with “z3”. He locked himself and now he is asking me for a password !

1 file: z3_robot

Writeup We’re given a file named z3_robot.

1 2 3 $ 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

So it’s an ELF binary, 64 bit not stripped. If we run it we get the following message:

1 2 3 4 5 6 7 8 9 \_/ (* *) __)#(__ ( )...( )(_) || |_| ||// >==() | | ()/ _(___)_ [-] [-] Z3 robot says :z3 Z3Z3z3 Zz3 zz33 3Z Passz3rd? Zz3 zZ3 3Z Z3Z3z -> # WAITING FOR INPUT HERE

So I opened it with Cutter and I started analyzing `main`

:

The main read our input with fgets and then pass it as argument to `check_flag`

. If `check_flag`

function returns 1, the challenge is solved.

The graph overview of `check_flag`

is the following (not very short):

Now let’s see the decompiled of `check_flag`

(with r2ghidra-dec):

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 undefined8 check_flag (int64_t arg1) { undefined8 uVar1; uint8_t uVar2; int64_t var_8h; if (((((*(arg1 + 0x14 ) ^ 0x2b ) == *(arg1 + 7 )) && (*(arg1 + 0x15 ) - *(arg1 + 3 ) == -0x14 )) && (*(arg1 + 2 ) >> 6 == '\0' )) && ((*(arg1 + 0xd ) == 't' && ((*(arg1 + 0xb ) & 0x3fffffff U) == 0x5f )))) && ((uVar2 = (*(arg1 + 0x11 ) >> 7 ) >> 5 , *(arg1 + 7 ) >> ((*(arg1 + 0x11 ) + uVar2 & 7 ) - uVar2 & 0x1f ) == 5 && (((*(arg1 + 6 ) ^ 0x53 ) == *(arg1 + 0xe ) && (*(arg1 + 8 ) == 'z' )))))) && ((uVar2 = (*(arg1 + 9 ) >> 7 ) >> 5 , *(arg1 + 5 ) << ((*(arg1 + 9 ) + uVar2 & 7 ) - uVar2 & 0x1f ) == 0x188 && ((((*(arg1 + 0x10 ) - *(arg1 + 7 ) == 0x14 && (uVar2 = (*(arg1 + 0x17 ) >> 7 ) >> 5 , *(arg1 + 7 ) << ((*(arg1 + 0x17 ) + uVar2 & 7 ) - uVar2 & 0x1f ) == 0xbe )) && (uVar2 = (*(arg1 + 0x16 ) >> 7 ) >> 5 , *(arg1 + 7 ) << ((*(arg1 + 0x16 ) + uVar2 & 7 ) - uVar2 & 0x1f ) == 0x17c )) && (*(arg1 + 0x16 ) == ':' )) && ((*(arg1 + 0x10 ) == 's' && ((*(arg1 + 0x17 ) ^ 0x1d ) == *(arg1 + 0x12 ))))))))) )))) && (((*(arg1 + 0xe ) + *(arg1 + 0x17 ) == 0x59 && (((*(arg1 + 2 ) & *(arg1 + 5 )) == 0x30 && ((*(arg1 + 0xf ) & 0x9f U) == 0x1f )))) && ((*(arg1 + 4 ) == 's' && (((*(arg1 + 0x17 ) ^ 0x4a ) == *arg1 && ((*(arg1 + 6 ) ^ 0x3c ) == *(arg1 + 0xb ))))) { uVar1 = 1 ; } else { uVar1 = 0 ; } return uVar1; }

To solve the challenge we have to make all the constraints inside the `if`

true.

There are two possible ways to solve those constraints:

angr
z3
Angr Solution The main issues an fgets of 0x19 (25) bytes, so our input must be of that dimension.

1 2 3 4 5 proj = angr.Project("z3_robot" ,load_options={"auto_load_libs" : False }, main_opts={"base_addr" : 0 }) flag = [claripy.BVS(f"c_{i} " , 8 ) for i in range(0x19 )] flag_ast = claripy.Concat(*flag) state = proj.factory.entry_state(stdin=flag_ast)

We add the constraints that makes the flag readable:

1 2 3 for f in flag: state.solver.add(f >= 0x20 ) state.solver.add(f < 0x7f )

Then we launch the exploration to find in the stdout the string “Well done”:

1 2 3 simgr = proj.factory.simulation_manager(state) print("start exploring" ) simgr.explore(find=lambda s: b"Well" in s.posix.dumps(1 ))

And finally:

1 2 3 found = simgr.found[0 ] valid_flag = found.solver.eval(flag_ast, cast_to=bytes) print(valid_flag)

The final exploit is:

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 import angr import claripyproj = angr.Project("z3_robot" ,load_options={"auto_load_libs" : False }, main_opts={"base_addr" : 0 }) flag = [claripy.BVS(f"c_{i} " , 8 ) for i in range(0x19 )] flag_ast = claripy.Concat(*flag) state = proj.factory.entry_state(stdin=flag_ast) for f in flag: state.solver.add(f >= 0x20 ) state.solver.add(f < 0x7f ) simgr = proj.factory.simulation_manager(state) print("start exploring" ) simgr.explore(find=lambda s: b"Well" in s.posix.dumps(1 )) if len(simgr.found) > 0 : found = simgr.found[0 ] valid_flag = found.solver.eval(flag_ast, cast_to=bytes) print(valid_flag) else : print("unlucky" )

Z3 Solution Another way to solve the challenge is to use z3.

Since the ghidra’s decompiled of `check_flag`

is a bit messy we can use the IDA’s one, which is more polished:

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 return ((unsigned __int8)a1[20 ] ^ 0x2B ) == a1[7 ] && a1[21 ] - a1[3 ] == -20 && !(a1[2 ] >> 6 ) && a1[13 ] == 116 && 4 * a1[11 ] == 380 && a1[7 ] >> (a1[17 ] % 8 ) == 5 && ((unsigned __int8)a1[6 ] ^ 0x53 ) == a1[14 ] && a1[8 ] == 122 && a1[5 ] << (a1[9 ] % 8 ) == 392 && a1[16 ] - a1[7 ] == 20 && a1[7 ] << (a1[23 ] % 8 ) == 190 && a1[2 ] - a1[7 ] == -43 && a1[21 ] == 95 && ((unsigned __int8)a1[2 ] ^ 0x47 ) == a1[3 ] && *a1 == 99 && a1[13 ] == 116 && (a1[20 ] & 0x45 ) == 68 && (a1[8 ] & 0x15 ) == 16 && a1[12 ] == 95 && a1[4 ] >> 4 == 7 && a1[13 ] == 116 && *a1 >> (*a1 % 8 ) == 12 && a1[10 ] == 95 && (a1[8 ] & 0xAC ) == 40 && a1[16 ] == 115 && (a1[22 ] & 0x1D ) == 24 && a1[9 ] == 51 && a1[5 ] == 49 && 4 * a1[19 ] == 456 && a1[20 ] >> 6 == 1 && a1[7 ] >> 1 == 47 && a1[1 ] == 108 && a1[3 ] >> 4 == 7 && (a1[19 ] & 0x49 ) == 64 && a1[4 ] == 115 && ((unsigned __int8)a1[2 ] & (unsigned __int8)a1[11 ]) == 20 && *a1 == 99 && a1[4 ] + a1[5 ] == 164 && a1[15 ] << 6 == 6080 && ((unsigned __int8)a1[10 ] ^ 0x2B ) == a1[17 ] && ((unsigned __int8)a1[12 ] ^ 0x2C ) == a1[4 ] && a1[19 ] - a1[21 ] == 19 && a1[12 ] == 95 && a1[15 ] >> 1 == 47 && a1[19 ] == 114 && a1[17 ] + a1[18 ] == 168 && a1[22 ] == 58 && ((unsigned __int8)a1[23 ] & (unsigned __int8)a1[21 ]) == 9 && a1[6 ] << (a1[19 ] % 8 ) == 396 && a1[3 ] + a1[7 ] == 210 && (a1[22 ] & 0xED ) == 40 && (a1[12 ] & 0xAC ) == 12 && ((unsigned __int8)a1[18 ] ^ 0x6B ) == a1[15 ] && (a1[16 ] & 0x7A ) == 114 && (*a1 & 0x39 ) == 33 && ((unsigned __int8)a1[6 ] ^ 0x3C ) == a1[21 ] && a1[20 ] == 116 && a1[19 ] == 114 && a1[12 ] == 95 && a1[2 ] == 52 && a1[23 ] == 41 && a1[10 ] == 95 && ((unsigned __int8)a1[22 ] & (unsigned __int8)a1[9 ]) == 50 && a1[3 ] + a1[2 ] == 167 && a1[17 ] - a1[14 ] == 68 && a1[21 ] == 95 && ((unsigned __int8)a1[19 ] ^ 0x2D ) == a1[10 ] && 4 * a1[12 ] == 380 && a1[6 ] & 0x40 && ((unsigned __int8)a1[12 ] & (unsigned __int8)a1[22 ]) == 26 && a1[7 ] << (a1[19 ] % 8 ) == 380 && ((unsigned __int8)a1[20 ] ^ 0x4E ) == a1[22 ] && a1[6 ] == 99 && a1[12 ] == a1[7 ] && a1[19 ] - a1[13 ] == -2 && a1[14 ] >> 4 == 3 && (a1[12 ] & 0x38 ) == 24 && a1[8 ] << (a1[10 ] % 8 ) == 15616 && a1[20 ] == 116 && a1[6 ] >> (a1[22 ] % 8 ) == 24 && a1[22 ] - a1[5 ] == 9 && a1[7 ] << (a1[22 ] % 8 ) == 380 && a1[22 ] == 58 && a1[16 ] == 115 && ((unsigned __int8)a1[23 ] ^ 0x1D ) == a1[18 ] && a1[23 ] + a1[14 ] == 89 && ((unsigned __int8)a1[5 ] & (unsigned __int8)a1[2 ]) == 48 && (a1[15 ] & 0x9F ) == 31 && a1[4 ] == 115 && ((unsigned __int8)a1[23 ] ^ 0x4A ) == *a1 && ((unsigned __int8)a1[6 ] ^ 0x3C ) == a1[11 ];

What we need to do is:

remove the casting to (unsigned __int8).
change the pointer to the first element of the array `*a1`

to `a1[0]`

.
need to adapts the bit a bit operations a bit (:D).
Final exploit:

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 from z3 import *a1 = [BitVec(f'{i} ' , 8 ) for i in range(0x19 )] s = Solver() s.add((a1[20 ] ^ 0x2B ) == a1[7 ]) s.add(a1[21 ] - a1[3 ] == -20 ) s.add((a1[2 ] >> 6 ) == 0 ) s.add(a1[13 ] == 116 ) s.add(4 * a1[11 ] == 380 ) s.add(a1[7 ] >> (a1[17 ] % 8 ) == 5 ) s.add((a1[6 ] ^ 0x53 ) == a1[14 ]) s.add(a1[8 ] == 122 ) s.add(a1[5 ] << (a1[9 ] % 8 ) == 392 ) s.add(a1[16 ] - a1[7 ] == 20 ) s.add(a1[7 ] << (a1[23 ] % 8 ) == 190 ) s.add(a1[2 ] - a1[7 ] == -43 ) s.add(a1[21 ] == 95 ) s.add((a1[2 ] ^ 0x47 ) == a1[3 ]) s.add(a1[0 ] == 99 ) s.add(a1[13 ] == 116 ) s.add((a1[20 ] & 0x45 ) == 68 ) s.add((a1[8 ] & 0x15 ) == 16 ) s.add(a1[12 ] == 95 ) s.add(a1[4 ] >> 4 == 7 ) s.add(a1[13 ] == 116 ) s.add(a1[0 ] >> (a1[0 ] % 8 ) == 12 ) s.add(a1[10 ] == 95 ) s.add((a1[8 ] & 0xAC ) == 40 ) s.add(a1[16 ] == 115 ) s.add((a1[22 ] & 0x1D ) == 24 ) s.add(a1[9 ] == 51 ) s.add(a1[5 ] == 49 ) s.add(4 * a1[19 ] == 456 ) s.add(a1[20 ] >> 6 == 1 ) s.add(a1[7 ] >> 1 == 47 ) s.add(a1[1 ] == 108 ) s.add(a1[3 ] >> 4 == 7 ) s.add((a1[19 ] & 0x49 ) == 64 ) s.add(a1[4 ] == 115 ) s.add(a1[2 ] & a1[11 ] == 20 ) s.add(a1[0 ] == 99 ) s.add(a1[4 ] + a1[5 ] == 164 ) s.add(a1[15 ] << 6 == 6080 ) s.add(a1[10 ] ^ 0x2B == a1[17 ]) s.add(a1[12 ] ^ 0x2C == a1[4 ]) s.add(a1[19 ] - a1[21 ] == 19 ) s.add(a1[12 ] == 95 ) s.add(a1[15 ] >> 1 == 47 ) s.add(a1[19 ] == 114 ) s.add(a1[17 ] + a1[18 ] == 168 ) s.add(a1[22 ] == 58 ) s.add(a1[23 ] & a1[21 ] == 9 ) s.add(a1[6 ] << (a1[19 ] % 8 ) == 396 ) s.add(a1[3 ] + a1[7 ] == 210 ) s.add((a1[22 ] & 0xED ) == 40 ) s.add((a1[12 ] & 0xAC ) == 12 ) s.add((a1[18 ] ^ 0x6B ) == a1[15 ]) s.add((a1[16 ] & 0x7A ) == 114 ) s.add((a1[0 ] & 0x39 ) == 33 ) s.add((a1[6 ] ^ 0x3C ) == a1[21 ]) s.add(a1[20 ] == 116 ) s.add(a1[19 ] == 114 ) s.add(a1[12 ] == 95 ) s.add(a1[2 ] == 52 ) s.add(a1[23 ] == 41 ) s.add(a1[10 ] == 95 ) s.add((a1[22 ] & a1[9 ]) == 50 ) s.add(a1[3 ] + a1[2 ] == 167 ) s.add(a1[17 ] - a1[14 ] == 68 ) s.add(a1[21 ] == 95 ) s.add((a1[19 ] ^ 0x2D ) == a1[10 ]) s.add(4 * a1[12 ] == 380 ) s.add(a1[6 ] & 0x40 >= 1 ) s.add((a1[12 ] & a1[22 ]) == 26 ) s.add(a1[7 ] << (a1[19 ] % 8 ) == 380 ) s.add((a1[20 ] ^ 0x4E ) == a1[22 ]) s.add(a1[6 ] == 99 ) s.add(a1[12 ] == a1[7 ]) s.add(a1[19 ] - a1[13 ] == -2 ) s.add(a1[14 ] >> 4 == 3 ) s.add((a1[12 ] & 0x38 ) == 24 ) s.add(a1[8 ] << (a1[10 ] % 8 ) == 15616 ) s.add(a1[20 ] == 116 ) s.add(a1[6 ] >> (a1[22 ] % 8 ) == 24 ) s.add(a1[22 ] - a1[5 ] == 9 ) s.add(a1[7 ] << (a1[22 ] % 8 ) == 380 ) s.add(a1[22 ] == 58 ) s.add(a1[16 ] == 115 ) s.add((a1[23 ] ^ 0x1D ) == a1[18 ]) s.add(a1[23 ] + a1[14 ] == 89 ) s.add((a1[5 ] & a1[2 ]) == 48 ) s.add((a1[15 ] & 0x9F ) == 31 ) s.add(a1[4 ] == 115 ) s.add((a1[23 ] ^ 0x4A ) == a1[0 ]) s.add((a1[6 ] ^ 0x3C ) == a1[11 ]) print(s.check()) model = s.model() flag = '' .join([chr(int(str(model[a1[i]]))) for i in range(len(model))]) print(flag)

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 $ ./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_:)}

Flag `shkCTF{cl4ss1c_z3___t0_st4rt_:)}`