ccsc2022

Overview

These were a series of three reversing challenges that get incrementally more difficult. As the name suggests for the solution the z3 constraint solver was used for the challenges. Here I’m going to be going through challenges II and III as I didn’t manage to solve the first one by the end of the competion. For that the solution is available on the competition’s github repository.

Z3ep Xanflorp II

0. The Challenge

Crap Morty... The portal gun is still broken. You need to fix it Morty BURPPP. FIX IT!!! 
It acts weirdly. Grandpa has no time for this. Fix the circuit-board till I'm back Morty.

This challenge did not come with any files, just a tcp service to connect to.

1. Solution

Connecting to the service we can see that it gives us a random set of equations that we have to solve. This is repeated 50 times and after successfully solving all of them it prints out the flag. So for obvious reasons this couldn’t be done by hand.

via 🐍 v3.10.4 ➜  CCSC2022/reverse/z3ep_xanflorp_ii_COMPLETE nc localhost 1235
Let's see if you can fix my teleport gun Morty...
Some weird equations will appear.
Respond with floats, separated by space.
You must be quick or else the portal gun's circuit will overheat!
Are you ready [Y or N]?
Y
49*x__0 + 92*x__1 - 97*x__2 - 68*x__3 + 57*x__4 - 66*x__5 + 61*x__6 >=79
26*x__0 - 71*x__1 + 49*x__2 - 42*x__3 + 56*x__4 - 47*x__5 + 78*x__6 <=19
-37*x__0 - 58*x__1 - 22*x__2 + 94*x__3 - 11*x__4 + 48*x__5 - 95*x__6 >=41
61*x__0 + 51*x__1 + 98*x__2 + 32*x__3 + 52*x__4 + 45*x__5 + 59*x__6 >=1
27*x__0 + 58*x__1 + 39*x__2 + 87*x__3 + 54*x__4 + 15*x__5 + 64*x__6 >=69
76*x__0 - 5*x__1 + 6*x__2 + 23*x__3 - 74*x__4 - 5*x__5 - 69*x__6 <=30
-40*x__0 - 22*x__1 + 59*x__2 + 46*x__3 - 99*x__4 - 18*x__5 - 9*x__6 >=47
Answer: 

As mentioned above to solve this z3 (with python) was used in combination with pwntools for any socket communication. First, I extracted all the variable names from the equations using regular expressions and created z3 Real parameters. Then going line by line, I added all equations to the solver, found a solution and send them back to the server. The only issue I run into while writting the solver is that z3 was returning results such that the answer was at the edge of each constraint so sometimes due to rounding errors the result wouldn’t be recognized. This was solved by just removing all equal signs from the equation (‘<=’ -> ‘<’).

Honestly I’m kind of embarrased about this code since I used exec and eval which are a big no, no. Here it is:

from z3 import *
from pwn import *
import re

def convert_to_float(frac_str):
    try:
        return float(frac_str)
    except ValueError:
        num, denom = frac_str.split('/')
        try:
            leading, num = num.split(' ')
            whole = float(leading)
        except ValueError:
            whole = 0
        frac = float(num) / float(denom)
        return whole - frac if whole < 0 else whole + frac

HOST = "192.168.125.11"
PORT = 1235

io = remote(HOST, PORT)

sl = lambda x : io.sendline(x)
sla = lambda x, y : io.sendlineafter(x, y)
se = lambda x : io.send(x)
sa = lambda x, y : io.sendafter(x, y)
ru = lambda x : io.recvuntil(x)
rl = lambda : io.recvline()
cl = lambda : io.clean()

sla(b'?', b'Y')

done = False
while True:
    data = ru(b':').decode('latin1').strip()

    if "flag" in data.lower():
        io.interactive()

    parameters = sorted(set(re.findall("x__\d", data)))
    for parameter in parameters:
        exec(f"{parameter} = Real('{parameter.replace('_', '')}')")

    data = data.split('\n')[:-1]

    s = Solver()
    for equation in data:
        equation = equation.replace('=', '')
        eval(f"s.add({equation})")

    s.check()

    m = s.model()

    solution = [None] * len(parameters)
    for d in m.decls():
        value = convert_to_float(m[d].as_fraction())
        solution[int(d.name()[1])] = f"{value:.3f}"

    solution = ' '.join(solution).encode('latin1')

    sl(solution)

Z3ep Xanflorp III

0. The Challenge

We must revenge Z3ep somehow Morty! First we need to bypass his secure vault to enter the miniverse.

For the challenge we were given an ELF binary.

I solved this challenge in the non-intended way. For the inteded way using angr read the solution script by the authors.

1. Solution

After opening the binary in Ghidra the solution was apparent in my mind. I saw a massive 50 line if-statement comparing different weights. Since, at that time I have just solved the challenge above (Z3ep Xanflorp II), I already had code ready to solve a set of equations. The only problem was that this time they were in a binary file. So I copy pasted this block of text in my text editor and using a few regular expressions, I converted it into something parsable by python and z3.

I run the following expressions (vim style):

%s/[\n ]//g 				# remove new lines and spaces
%s/(uint)//g				# remove (uint) casting
%s/(byte)//g				# remove (byte) casting
%s/[()]//g					# remove parenthesis
%s/&&/\r/g					# replace AND operator with new line
%s/w\._\(\d\)_\d_/w\1/g		# change the ugly naming from ghidra
%s/\(^.*$/)/s.add(\1)		# wrap it inside s.add

      w._7_1_ == 0x72 &&
      (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((w._7_1_ == 0x72
                                                                                    && (uint)w._5_1_
                                                                                       - (uint)w.
                                                  _4_1_ == -10) &&
                                                  (uint)w._3_1_ + (uint)w._2_1_ + (uint)w._4_1_ ==
                                                  0xa2) && w._5_1_ == 0x4b) &&
                                                  (uint)w._2_1_ + (uint)(byte)w == 0x78) &&
                                                  (uint)w._7_1_ + (uint)w._2_1_ + (uint)w._3_1_ ==
                                                  0xbf) && w._3_1_ == 0x36) && w._6_1_ == 0x26) &&
                                                  w._6_1_ == 0x26) && w._7_1_ == 0x72) &&
                                                  w._7_1_ == 0x72) &&
                                                  (uint)w._4_1_ + (uint)w._5_1_ + (uint)w._3_1_ ==
                                                  0xd6) && (uint)w._4_1_ + (uint)w._6_1_ == 0x7b) &&
                                                  (uint)w._5_1_ - (uint)w._4_1_ == -10) &&
                                                  w._2_1_ == 0x17) &&
                                                  (uint)w._5_1_ + ((uint)w._6_1_ - (uint)w._4_1_) ==
                                                  0x1c) && w._6_1_ == 0x26) &&
                                                  (uint)w._3_1_ - (uint)w._5_1_ == -0x15) &&
                                                  -(uint)w._3_1_ - (uint)w._3_1_ == -0x6c) &&
                                                  w._4_1_ == 0x55) && w._2_1_ == 0x17) &&
                                                  (uint)(byte)w - (uint)w._4_1_ == 0xc) &&
                                                  w._2_1_ == 0x17) &&
                                                  (uint)w._3_1_ + (uint)w._2_1_ + (uint)w._4_1_ ==
                                                  0xa2) && -(uint)w._3_1_ - (uint)w._5_1_ == -0x81)
                                                  && (uint)w._1_1_ - (uint)w._5_1_ == 4) &&
                                                  (uint)w._5_1_ + (uint)w._2_1_ == 0x62) &&
                                                  -(uint)w._7_1_ - (uint)w._1_1_ == -0xc1) &&
                                                  (uint)w._5_1_ + (uint)w._3_1_ == 0x81) &&
                                                  ((uint)w._2_1_ - (uint)w._3_1_) - (uint)w._3_1_ ==
                                                  -0x55) && ((uint)w._3_1_ - (uint)w._2_1_) -
                                                            (uint)w._2_1_ == 8) &&
                                                  (uint)w._6_1_ + (uint)w._5_1_ + (uint)w._6_1_ ==
                                                  0x97) && (uint)w._2_1_ +
                                                           (uint)w._3_1_ + (uint)w._7_1_ == 0xbf) &&
                                                  ((uint)w._3_1_ + (uint)w._5_1_) - (uint)w._7_1_ ==
                                                  0xf) && (-(uint)w._2_1_ - (uint)w._2_1_) -
                                                          (uint)w._1_1_ == -0x7d) && w._5_1_ == 0x4b
                                                  ) && w._2_1_ == 0x17) &&
                                                (uint)(byte)w + (-(uint)w._6_1_ - (uint)w._4_1_) ==
                                                -0x1a) && (uint)w._3_1_ - (uint)w._2_1_ == 0x1f) &&
                                              (uint)w._6_1_ - (uint)w._4_1_ == -0x2f) &&
                                             w._3_1_ == 0x36) &&
                                            (uint)w._5_1_ - (uint)w._2_1_ == 0x34) &&
                                           (uint)w._4_1_ + (uint)w._4_1_ == 0xaa) && w._1_1_ == 0x4f
                                          ) && (-(uint)w._4_1_ - (uint)w._1_1_) - (uint)w._1_1_ ==
                                               -0xf3) && w._4_1_ == 0x55) &&
                                       ((uint)(byte)w - (uint)w._6_1_) + (uint)w._4_1_ == 0x90) &&
                                      w._2_1_ == 0x17) && w._1_1_ == 0x4f) && w._5_1_ == 0x4b) &&
                                   (byte)w == 0x61) && (uint)w._4_1_ - (uint)w._1_1_ == 6) &&
                                 w._6_1_ == 0x26) &&
                                (-(uint)w._3_1_ - (uint)w._5_1_) - (uint)w._5_1_ == -0xcc) &&
                               (uint)w._1_1_ - (uint)w._6_1_ == 0x29) &&
                              -(uint)w._7_1_ - (uint)w._5_1_ == -0xbd) && w._2_1_ == 0x17) &&
                            ((uint)w._4_1_ - (uint)w._2_1_) - (uint)w._5_1_ == -0xd) &&
                           w._5_1_ == 0x4b) && w._5_1_ == 0x4b) && w._6_1_ == 0x26) &&
                        w._4_1_ == 0x55) && w._4_1_ == 0x55) &&
                      (uint)w._3_1_ - (uint)w._2_1_ == 0x1f) &&
                     (uint)w._2_1_ - (uint)w._7_1_ == -0x5b) && (byte)w == 0x61) &&
                   (uint)w._3_1_ - (uint)w._5_1_ == -0x15) && w._3_1_ == 0x36) && w._2_1_ == 0x17)
                && (uint)w._4_1_ + (uint)(byte)w == 0xb6) && (byte)w == 0x61) &&
              -(uint)w._3_1_ - (uint)w._3_1_ == -0x6c) && w._5_1_ == 0x4b) && w._7_1_ == 0x72) &&
           (uint)w._3_1_ + (-(uint)w._2_1_ - (uint)w._5_1_) == -0x2c) &&
          (uint)w._1_1_ - (uint)w._6_1_ == 0x29) &&
         (uint)w._4_1_ + ((uint)w._5_1_ - (uint)w._2_1_) == 0x89) &&
        (uint)w._4_1_ + (uint)w._3_1_ == 0x8b) && w._2_1_ == 0x17) && w._5_1_ == 0x4b)

s.add(w7==0x72)
s.add(w7==0x72)
s.add(w5-w4==-10)
s.add(w3+w2+w4==0xa2)
s.add(w5==0x4b)
s.add(w2+w==0x78)
s.add(w7+w2+w3==0xbf)
s.add(w3==0x36)
s.add(w6==0x26)
s.add(w6==0x26)
s.add(w7==0x72)
s.add(w7==0x72)
s.add(w4+w5+w3==0xd6)
s.add(w4+w6==0x7b)
s.add(w5-w4==-10)
s.add(w2==0x17)
s.add(w5+w6-w4==0x1c)
s.add(w6==0x26)
s.add(w3-w5==-0x15)
s.add(-w3-w3==-0x6c)
s.add(w4==0x55)
s.add(w2==0x17)
s.add(w-w4==0xc)
s.add(w2==0x17)
s.add(w3+w2+w4==0xa2)
s.add(-w3-w5==-0x81)
s.add(w1-w5==4)
s.add(w5+w2==0x62)
s.add(-w7-w1==-0xc1)
s.add(w5+w3==0x81)
s.add(w2-w3-w3==-0x55)
s.add(w3-w2-w2==8)
s.add(w6+w5+w6==0x97)
s.add(w2+w3+w7==0xbf)
s.add(w3+w5-w7==0xf)
s.add(-w2-w2-w1==-0x7d)
s.add(w5==0x4b)
s.add(w2==0x17)
s.add(w+-w6-w4==-0x1a)
s.add(w3-w2==0x1f)
s.add(w6-w4==-0x2f)
s.add(w3==0x36)
s.add(w5-w2==0x34)
s.add(w4+w4==0xaa)
s.add(w1==0x4f)
s.add(-w4-w1-w1==-0xf3)
s.add(w4==0x55)
s.add(w-w6+w4==0x90)
s.add(w2==0x17)
s.add(w1==0x4f)
s.add(w5==0x4b)
s.add(w==0x61)
s.add(w4-w1==6)
s.add(w6==0x26)
s.add(-w3-w5-w5==-0xcc)
s.add(w1-w6==0x29)
s.add(-w7-w5==-0xbd)
s.add(w2==0x17)
s.add(w4-w2-w5==-0xd)
s.add(w5==0x4b)
s.add(w5==0x4b)
s.add(w6==0x26)
s.add(w4==0x55)
s.add(w4==0x55)
s.add(w3-w2==0x1f)
s.add(w2-w7==-0x5b)
s.add(w==0x61)
s.add(w3-w5==-0x15)
s.add(w3==0x36)
s.add(w2==0x17)
s.add(w4+w==0xb6)
s.add(w==0x61)
s.add(-w3-w3==-0x6c)
s.add(w5==0x4b)
s.add(w7==0x72)
s.add(w3+-w2-w5==-0x2c)
s.add(w1-w6==0x29)
s.add(w4+w5-w2==0x89)
s.add(w4+w3==0x8b)
s.add(w2==0x17)
s.add(w5==0x4b)

Honestly, after this point, I don’t know why I continued since I already had the weights. Apparently in my mind, I wanted the binary on my machine to tell me good job. So anything after this was useless. To make the binary congratulate me, I used gdb to modify the weights at the begining of the program and then in the middle when it tried to scramble the data. My code is below.

#!/usr/bin/python3

import z3
import time
from pwn import *
import re

context.terminal = ['tmux', 'splitw', '-v']

binary = './chall'
elf = ELF(binary)

context.binary = elf

sl = lambda x : io.sendline(x)
sla = lambda x, y : io.sendlineafter(x, y)
se = lambda x : io.send(x)
sa = lambda x, y : io.sendafter(x, y)
ru = lambda x : io.recvuntil(x)
rl = lambda : io.recvline()
cl = lambda : io.clean()
uu64 = lambda x : u64(x.ljust(8, b'\x00'))

w = z3.BitVec('w', 8)
w1 = z3.BitVec('w1', 8)
w2 = z3.BitVec('w2', 8)
w3 = z3.BitVec('w3', 8)
w4 = z3.BitVec('w4', 8)
w5 = z3.BitVec('w5', 8)
w6 = z3.BitVec('w6', 8)
w7 = z3.BitVec('w7', 8)

s = z3.Solver()

s.add(w7==0x72)
s.add(w7==0x72)
s.add(w5-w4==-10)
s.add(w3+w2+w4==0xa2)
s.add(w5==0x4b)
s.add(w2+w==0x78)
s.add(w7+w2+w3==0xbf)
s.add(w3==0x36)
s.add(w6==0x26)
s.add(w6==0x26)
s.add(w7==0x72)
s.add(w7==0x72)
s.add(w4+w5+w3==0xd6)
s.add(w4+w6==0x7b)
s.add(w5-w4==-10)
s.add(w2==0x17)
s.add(w5+w6-w4==0x1c)
s.add(w6==0x26)
s.add(w3-w5==-0x15)
s.add(-w3-w3==-0x6c)
s.add(w4==0x55)
s.add(w2==0x17)
s.add(w-w4==0xc)
s.add(w2==0x17)
s.add(w3+w2+w4==0xa2)
s.add(-w3-w5==-0x81)
s.add(w1-w5==4)
s.add(w5+w2==0x62)
s.add(-w7-w1==-0xc1)
s.add(w5+w3==0x81)
s.add(w2-w3-w3==-0x55)
s.add(w3-w2-w2==8)
s.add(w6+w5+w6==0x97)
s.add(w2+w3+w7==0xbf)
s.add(w3+w5-w7==0xf)
s.add(-w2-w2-w1==-0x7d)
s.add(w5==0x4b)
s.add(w2==0x17)
s.add(w+-w6-w4==-0x1a)
s.add(w3-w2==0x1f)
s.add(w6-w4==-0x2f)
s.add(w3==0x36)
s.add(w5-w2==0x34)
s.add(w4+w4==0xaa)
s.add(w1==0x4f)
s.add(-w4-w1-w1==-0xf3)
s.add(w4==0x55)
s.add(w-w6+w4==0x90)
s.add(w2==0x17)
s.add(w1==0x4f)
s.add(w5==0x4b)
s.add(w==0x61)
s.add(w4-w1==6)
s.add(w6==0x26)
s.add(-w3-w5-w5==-0xcc)
s.add(w1-w6==0x29)
s.add(-w7-w5==-0xbd)
s.add(w2==0x17)
s.add(w4-w2-w5==-0xd)
s.add(w5==0x4b)
s.add(w5==0x4b)
s.add(w6==0x26)
s.add(w4==0x55)
s.add(w4==0x55)
s.add(w3-w2==0x1f)
s.add(w2-w7==-0x5b)
s.add(w==0x61)
s.add(w3-w5==-0x15)
s.add(w3==0x36)
s.add(w2==0x17)
s.add(w4+w==0xb6)
s.add(w==0x61)
s.add(-w3-w3==-0x6c)
s.add(w5==0x4b)
s.add(w7==0x72)
s.add(w3+-w2-w5==-0x2c)
s.add(w1-w6==0x29)
s.add(w4+w5-w2==0x89)
s.add(w4+w3==0x8b)
s.add(w2==0x17)
s.add(w5==0x4b)

print(s.check())

m = s.model()
print(m)

solution = {}
for d in m.decls():
    value = int(m[d].as_string())
    solution[d.name()] = value

hexNum = ''
for n in sorted(solution)[::-1]:
    hexNum += hex(solution[n])[2:]

for n in sorted(solution):
    print(f"\\x{solution[n]:x}", end='')

print()

#################################################
# Everything Below here is useless
#################################################

w = int(hexNum, 16)
print(f"0x{w:x}")

gs = f'''
br _start
c
init-pwndbg

# break after yolo
br *0x0804b1b4

set *{elf.symbols.w}={w}
set *{elf.symbols.w + 4}={w >> 32}
c
set *{elf.symbols.w}={w}
set *{elf.symbols.w + 4}={w >> 32}
'''

print(gs)

# io = process(elf.path)
io = gdb.debug(elf.path, gs)

io.interactive()