# Ví dụ z3 sử dụng trong CTF

Mô tả tìm các giá trị trong list khi có mối liên hệ giữa các phần tử (yêu cầu):

```python
from z3 import *
 
s = Solver()
 
n = [Int(f'n[{i}]') for i in range(60)] # khai báo list n gồm 60 pt Int
 
for i in range(60): #add điều kiện các pt đều lớn hơn 0
  s.add(n[i] >0)
 
# dưới là add các ràng buộc các pt
s.add(n[9]+n[32]+n[26]== 337)
s.add(n[47]+n[14]+n[58]== 329)
s.add(n[56]+n[32]+n[19]== 316)
s.add(n[32]+n[6]+n[51]== 304)
s.add(n[43]+n[14]+n[44]== 318)
s.add(n[55]+n[2]+n[50]== 313)
s.add(n[36]+n[50]+n[35]== 311)
s.add(n[52]+n[42]+n[55]== 311)
s.add(n[44]+n[9]+n[22]== 335)
s.add(n[57]+n[27]+n[32]== 344)
s.add(n[8]+n[33]+n[16]== 322)
s.add(n[38]+n[6]+n[26]== 273)
s.add(n[53]+n[27]+n[2]== 327)
s.add(n[15]+n[35]+n[32]== 328)
s.add(n[17]+n[15]+n[21]== 308)
s.add(n[28]+n[52]+n[22]== 326)
s.add(n[12]+n[53]+n[48]== 317)
s.add(n[34]+n[50]+n[6]== 279)
s.add(n[22]+n[32]+n[47]== 347)
s.add(n[30]+n[32]+n[38]== 333)
s.add(n[48]+n[7]+n[59]== 359)
s.add(n[40]+n[15]+n[31]== 299)
s.add(n[20]+n[30]+n[15]== 304)
s.add(n[19]+n[7]+n[13]== 321)
s.add(n[54]+n[36]+n[56]== 306)
s.add(n[37]+n[10]+n[5]== 284)
s.add(n[0]+n[4]+n[6]== 239)
s.add(n[41]+n[52]+n[11]== 315)
s.add(n[18]+n[42]+n[10]== 315)
s.add(n[3]+n[55]+n[34]== 333)
s.add(n[27]+n[45]+n[43]== 338)
s.add(n[25]+n[51]+n[39]== 321)
s.add(n[16]+n[35]+n[4]== 290)
s.add(n[4]+n[28]+n[59]== 306)
s.add(n[5]+n[44]+n[31]== 295)
s.add(n[6]+n[56]+n[58]== 276)
s.add(n[14]+n[22]+n[25]== 300)
s.add(n[51]+n[4]+n[36]== 284)
s.add(n[2]+n[38]+n[5]== 296)
s.add(n[11]+n[40]+n[49]== 336)
s.add(n[35]+n[38]+n[31]== 317)
s.add(n[23]+n[34]+n[5]== 295)
s.add(n[1]+n[5]+n[52]== 307)
s.add(n[46]+n[26]+n[33]== 298)
s.add(n[13]+n[1]+n[23]== 311)
s.add(n[49]+n[36]+n[50]== 313)
s.add(n[39]+n[25]+n[16]== 313)
s.add(n[58]+n[36]+n[18]== 322)
s.add(n[31]+n[7]+n[28]== 338)
s.add(n[21]+n[35]+n[45]== 333)
s.add(n[24]+n[46]+n[33]== 299)
s.add(n[29]+n[15]+n[0]== 292)
s.add(n[26]+n[5]+n[23]== 283)
s.add(n[10]+n[52]+n[39]== 319)
s.add(n[7]+n[12]+n[44]== 334)
s.add(n[50]+n[27]+n[29]== 301)
s.add(n[33]+n[22]+n[43]== 320)
s.add(n[45]+n[49]+n[10]== 338)
s.add(n[42]+n[58]+n[57]== 326)
s.add(n[59]+n[10]+n[12]== 331)
s.add(n[18] == 110)
 
s.check()
sol = [] #tạo list kq
 
for i in range(60):
    sol.append(s.model().eval(n[i]).as_long())
print(''.join([chr(int(c)) for c in sol])) #in ra kq
```

{% hint style="success" %}
`as_long()` - Return a Z3 integer numeral as a Python long (bignum) numeral.

`as_string()` - Return a Z3 integer numeral as a Python string.

`as_binary_string()` - Return a Z3 integer numeral as a Python binary string.
{% endhint %}

{% hint style="success" %}
`eval()` - để đánh giá động các biểu thức từ đầu vào dựa trên chuỗi hoặc dựa trên mã được biên dịch. Nếu bạn chuyển 1 chuỗi vào thì hàm sẽ phân tích chuỗi đó, biên dịch nó thành mã byte và đánh giá nó dưới dạng một biểu thức Python. ([Tìm hiểu thêm](/home/education/install-tools/1.-install-flare-vm.md))

```python
eval(expression[, globals[, locals]])
```

* Hàm nhận 1 đối số đầu tiên - được gọi là biểu thức, chứa biểu thức mà bạn cần đánh giá và nó cũng có 2 đối số tùy chọn.
* Ví dụ:

```python
>>> eval("2 ** 8")
256
>>> eval("1024 + 1024")
2048
>>> eval("sum([8, 16, 32])")
56
>>> x = 100
>>> eval("x * 2")
200
```

* Lưu ý hàm chỉ chấp nhận biểu thức, nên không chấp nhận các hàm như if, for, while, import...
  {% endhint %}

{% hint style="info" %}

* <mark style="color:red;">`simplify()`</mark> - hàm này được dử dụng để rút gọn biểu thức

```python
>>> simplify(x + 1 + y + x + 1)
2 + 2*x + y
```

* <mark style="color:red;">`Distinct()`</mark> - hàm tạo một biểu thức riêng biệt đối với các đối số với nhau:

```python
>>> x = Int('x')
>>> y = Int('y')
>>> Distinct(x, y)
x != y #là số x và y khác nhau
>>> z = Int('z')
>>> Distinct(x, y, z)
Distinct(x, y, z)
>>> simplify(Distinct(x, y, z))
Distinct(x, y, z)
>>> simplify(Distinct(x, y, z), blast_distinct=True)
And(Not(x == y), Not(x == z), Not(y == z))
```

{% endhint %}

Class registers in z3: ([Tìm hiểu thêm](https://github.com/FSecureLABS/z3_and_angr_binary_analysis_workshop/tree/master/z3/x86))

```python
from z3 import *

class Registers:

	def __init__(self):
		self.eax = BitVec('eax', 32)
		self.ebx = BitVec('ebx', 32)
		self.ecx = BitVec('ecx', 32)
		self.edx = BitVec('edx', 32)
		self.edi = BitVec('edi', 32)
		self.esi = BitVec('esi', 32)
		self.ebp = BitVec('ebp', 32)
		self.esp = BitVec('esp', 32)

		self.eip = BitVec('eip', 32)

		self.cf = Bool('cf')
		self.zf = Bool('zf')
		self.sf = Bool('sf')
		self.of = Bool('of')
```


---

# 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://viettaliii.gitbook.io/home/ctf/cheatsheet/python/z3py/vi-du-z3-su-dung-trong-ctf.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.