# ezbolt

## Bypassing Decryption

I really did not feel like reversing the decryption that was laid out in the ezbolt extension.

Therefore instead I added in GDB into the Docker container, built the container, then when running the container, I used GDB to break on the point at which the decrypted text was being passed to execute by PHP. This was how I dumped out the following string:

```

```

Which realistically is a lot of bs to look through. However, if you take it apart, it is a bunch of comparisons that occur and are &&'d together. This is their "one liner" way of deciding if the input is correct against their **constraints**.

Oo constraints. Fancy. Lets use Z3.

## The Script

The following script was used to solve the challenge. Let's break it down.

### compare_to_constraint

I am using this function to convert `$f[9]*$f[17]-$f[35]+$f[33]==4646` into `flag[9]*flag[17]-flag[35]+flag[33]==4646` which we can then use to add constraints into Z3. For those who do not know, z3 is a nice constraint solver which could let you solve multivariate problems given a well constrained problem. You may find something similar in your linear algebra class where you had to solve a system of equations using constraints set forth by the other equations. This is a similar problem; each comparison will give a constraint and at the end, the flag must adhere to all of them. So if I can convert all of these into a comparison that the Z3 solver will understand, I can compaile one big comparison chain then just ask z3 to solve it for me.

### BitVec?

This is a bitvector. All that is going on here is we are creating an array of bit vectors, think of these like arrays of singular bits. You may think of a string as one array of characters. Now think of a string as an array of characters which are each an array of 8 bits. Now you are coming to what is this array of bitvectors. This object is what z3 uses to allow us to add in constraints and it to represent its solve in. We then convert this later into an actual character by doing `chr(s.model()[c].as_long())`.

```
#!/usr/bin/env python3

import z3
import re

def compare_to_constraint(comp, flag, solver):
res = int(comp.split(b"==")[1])

args = [m.start() for m in re.finditer(b"\$f", comp)]
ops = []
indexes = []
for idx in args:
stop = comp[idx:].find(b']') + 1
ops.append(
comp[idx + stop: idx + stop + 1].decode().strip()
)
indexes.append(
int(comp[idx + 3: idx + stop - 1])
)
ops = ops[:-1]

chall = ''
ops.reverse()
indexes.reverse()
try:
while True:
chall += f'flag[{indexes.pop()}]'
chall += f'{ops.pop()}'
except:
pass
chall += f'=={res}'

resp = eval(chall)
solver.add(resp)

s = z3.Solver()

php = open('./fuscated.php', 'rb').read().split(b"&&")[2:-1]
flag = []
for c in range(39):
flag.append(z3.BitVec(f"flag_{c}", 8))

for comp in php:
con = compare_to_constraint(comp, flag, s)

if s.check() == z3.sat:
print(
''.join(chr(s.model()[c].as_long()) for c in flag)
)
else:
print("Failed..")
```

## End

All and all. Quite simple, but a fun and good intro example for making use of z3.