Shattered Tablet
Table of Contents
Introduction
I had no intention of writing today, I just logged to get some practice in, on the basics, since I was tired to go into much theory, but this one was solved in less than 15-20 minutes. I thought why not: Let’s try to get some writing practice as well.
Deep in an ancient tomb, you’ve discovered a stone tablet with secret information on the locations of other relics. However, while dodging a poison dart, it slipped from your hands and shattered into hundreds of pieces. Can you reassemble it and read the clues?
Static analysis:
We are given just a single binary tablet, and the flag lies inside it,
since there is no remote machine to launch.
Decompiling
Immediately upon seeing the decompiled main, I thought of a similar challenge I recently completed: It must have been spooky license but I am not 100% sure of it.
if (((((uStack_28._2_1_ == '4') && (uStack_38._4_1_ == '3')) && (uStack_28._4_1_ == 'r')) && ((((uStack_48._1_1_ == 'T' && (uStack_38._5_1_ == 'v')) && ((uStack_48._6_1_ == '0' && ((uStack_28._7_1_ == '}' && (uStack_28._6_1_ == 'd')))))) && (uStack_30._7_1_ == 'r')))) && ((((((uStack_30._5_1_ == '3' && (uStack_40 == '3')) && (uStack_38._6_1_ == 'e')) && ((uStack_28._3_1_ == '1' && (uStack_48._5_1_ == 'r')))) && ((uStack_48 == 'H' && ((uStack_28 == '3' && (uStack_38._2_1_ == '.')))))) && (((((uStack_40._5_1_ == '4' && (((((uStack_48._3_1_ == '{' && (uStack_40._2_1_ == '_')) && (uStack_38 == '.')) && ((uStack_48._4_1_ == 'b' && (uStack_48._7_1_ == 'k')))) && (uStack_40._7_1_ == 't')))) && (((uStack_40._6_1_ == 'r' && (uStack_38._3_1_ == 'n')) && ((uStack_30._1_1_ == 't' && (((uStack_38._1_1_ == '.' && (uStack_40._1_1_ == 'n')) && (uStack_30._6_1_ == '_')))))))) && (((uStack_30._2_1_ == '0' && (uStack_30 == '_')) && (uStack_40._4_1_ == 'p')))) && ((((uStack_38._7_1_ == 'r' && (uStack_30._4_1_ == 'b')) && ((uStack_28._1_1_ == 'p' && (((uStack_48._2_1_ == 'B' && (uStack_30._3_1_ == '_')) && (uStack_40._3_1_ == '4')))))) && (uStack_28._5_1_ == '3')))))))) {
We are given a set of constraints we need the flag to meet. To do that we can use the z3-solver library, though it feels even easier than that. In fact I can do it by myself probably:
- Write the checks above in a separate sample file
- Break it down to its essentials (see shell command)
Some
vimquick formatting tricks and … We’re good to go:
cat test.txt | sed -E 's/&&|\)+|\(+/\n/g' | grep uStack | uniq | sort
Ustack_48: HTB{br0k
Ustack_40: 3n_4p4rt
Ustack_38: ...n3ver
Ustack_30: _t0_b3_r
Ustack_28: 3p41r3d}
Update: z3 solution
I wanted to test my z3 skills, since it took me a long time in the previous challenge. This one was more tedious, but here is the source:
import z3 # To find the length I simply piped the shell command to wc letters = [z3.Int(f's_{i}') for i in range(40) ] solver = z3.Solver() # Actually unnecessary, since we have the letters in == # for l in letters: # solver.add(z3.And( l >= 33, l <= 127)) solver.add(letters[33] == ord('p')) solver.add(letters[34] == ord('4')) solver.add(letters[32] == ord('3')) solver.add(letters[35] == ord('1')) solver.add(letters[36] == ord('r')) solver.add(letters[37] == ord('3')) solver.add(letters[38] == ord('d')) solver.add(letters[39] == ord('}')) solver.add(letters[24] == ord('_')) solver.add(letters[25] == ord('t')) solver.add(letters[26] == ord('0')) solver.add(letters[27] == ord('_')) solver.add(letters[28] == ord('b')) solver.add(letters[29] == ord('3')) solver.add(letters[30] == ord('_')) solver.add(letters[31] == ord('r')) solver.add(letters[16] == ord('.')) solver.add(letters[17] == ord('.')) solver.add(letters[18] == ord('.')) solver.add(letters[19] == ord('n')) solver.add(letters[20] == ord('3')) solver.add(letters[21] == ord('v')) solver.add(letters[22] == ord('e')) solver.add(letters[23] == ord('r')) solver.add(letters[9] == ord('n')) solver.add(letters[10] == ord('_')) solver.add(letters[8] == ord('3')) solver.add(letters[11] == ord('4')) solver.add(letters[12] == ord('p')) solver.add(letters[13] == ord('4')) solver.add(letters[14] == ord('r')) solver.add(letters[15] == ord('t')) solver.add(letters[1] == ord('T')) solver.add(letters[2] == ord('B')) solver.add(letters[3] == ord('{')) solver.add(letters[4] == ord('b')) solver.add(letters[5] == ord('r')) solver.add(letters[6] == ord('0')) solver.add(letters[7] == ord('k')) solver.add(letters[0] == ord('H')) if solver.check() == z3.sat: m = solver.model() answ = '' for i in letters: # as_string does not work -> the integer is transformed into a string. answ += (f'{chr(m.evaluate(i).as_long())}') print(answ)