# Using Z3

## What is Z3?

Z3 is an **SMT Solver**, a program that can test whether a set of conditions can hold or not, and eventually find a valid solution. This is super helpful in the context of reverse engineering, where you sometimes want to find a valid input or reverse engineer a checker function.

## Installing Z3

Follow [these instructions](https://github.com/Z3Prover/z3?tab=readme-ov-file#building-z3-using-make-and-gccclang):

```bash
$ git clone https://github.com/Z3Prover/z3
$ cd z3
$ python3 scripts/mk_make.py
$ cd build
$ make
$ sudo make install
```

Wait for that to compile. Make sure you also install the [Python bindings](https://github.com/Z3Prover/z3?tab=readme-ov-file#python), which allow you to use Z3 from within Python:

```bash
$ pip install z3-solver
```

## Using Z3

Let's take the example of [Hack The Box's Hissss challenge](https://app.hackthebox.com/challenges/hissss). Once you do the whole python decompilation step, you end up with a large `if` statement for the password:

```python
if ord(password[0]) != 48 
    or password[11] != '!' 
    or ord(password[7]) != ord(password[5]) 
    or 143 - ord(password[0]) != ord(password[4]) 
    or ord(password[1]) ^ ord(password[3]) != 30 
    or ord(password[2]) * ord(password[3]) != 5610 
    or password[1] != 'p' 
    or ord(password[6]) - ord(password[8]) != -46 
    or ord(password[6]) ^ ord(password[7]) != 64 
    or ord(password[10]) + ord(password[5]) != 166 
    or ord('n') - ord(password[9]) != 1 
    or password[10] != str(3):
    
    print('Sorry, the password is incorrect.')
else:
    print(f"Well Done! HTB{{{password}}}")
```

So we have a bunch of relations. Some of them are easy - `password[0] == 48`, `password[10] == str(3)`. Some, however, would require some thinking - the different characters are **interrelated** and appear in multiple statements. Sometimes, you might have other relations - for example, `password[4] > 68`.

What we really want is to be able to plug all of this into a program that will solve the system of statements. Enter Z3!

First, set up the solver:

```python
from z3 import *

s = Solver()

password = [BitVec(f'char{i}', 8) for i in range(12)]
```

A `BitVec` is just a binary number. In this case, we are making them `8` bits long (like a character!) and also calling them `char0`, `char1`, etc. Each `charX` is the `X`th character of the flag, so `password` is really an array of characters which are represented in the form of `BitVec` so that Z3 understands them.

Now we add the conditions to the `Solver` object:

```python
s.add(password[0] == 48)
s.add(password[11] == ord('!'))
s.add(password[7] == password[5])
s.add(143 - password[0] == password[4])
s.add(password[1] ^ password[3] == 30)
s.add(password[2] * password[3] == 5610)
s.add(password[1] == ord('p'))
s.add(password[6] - password[8] == -46)
s.add(password[6] ^ password[7] == 64)
s.add(password[10] + password[5] == 166)
s.add(ord('n') - password[9] == 1)
s.add(password[10] == ord('3'))
```

We then grab the solution as well as setting an `answer` array of the correct length to populate:

```python
s.check()            # generate the model if it exists
sol = s.model()      # grab the model  
```

The values returned by `sol` are not in the simplest form possible, but we can extract the values for each index as so:

```python
flag = [sol[f].as_long() for f in password]
flag = ''.join(chr(c) for c in flag)
print(flag)
```

We get `0p3n_s3sam3!`


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://ir0nstone.gitbook.io/notes/misc/using-z3.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.