Shattered Tablet

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 vim quick 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)

Introduction

Static analysis:

Decompiling

Update: z3 solution

Update: `z3` solution