# 题目描述
题目给出一个二进制文件 rechall，要求输入正确的 flag 通过验证。
运行程序示例：
## **解题步骤**
## 0x01 初步分析
1.使用`file`命令检查文件类型
```bash
$ file rechall
rechall: ELF 64-bit LSB pie executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2,BuildID[sha1]=5e62deaec60953b0ae6e9e22f18f228f1d75e2f2,forGNU/Linux3.2.0,notstripped
```
2.用`strings`查找字符串
```bash
$ strings ./rechall
/lib64/ld-linux-x86-64.so.2
libc.so.6
sprintf
....
flag{%08x-%08x-%08x-%08x}
Right!
Yourflagis:%s
...
```
发现flag格式
## 0x02 静态分析
3.用IDA打开反编译程序，重命名部分变量。发现flag是由四个十六进制数字组成的
4.透过观察发现要输入的四个数字都通过checker1-4的检查才能拿到flag，并且输入的数字转换成16进制拼在一起就是flag。
5.分别进入checker1-4把代码提取出来
```c
__int64 __fastcallchecker1(inta1,inta2)
{
__int64 result;// rax
if( a1 - a2 ==0x956438B9)
result =0LL;
else
result =4294967295LL;
returnresult;
}
__int64 __fastcallchecker2(inta1)
{
__int64 result;// rax
if(3* (a1 &0x52E3F96B) - (a1 |0xAD1C0694) - a1 == -477662227)
result =0LL;
else
result =0xFFFFFFFFLL;
returnresult;
}
__int64 __fastcallchecker3(unsignedinta1)
{
if( a1 >0x10000000)
return0xFFFFFFFFLL;
if( -3* (~a1 |0xD68E3FE9)
+3* ~(a1 |0xD68E3FE9)
+4* ((~a1 &0xD68E3FE9) +2* ~(~a1 |0xD68E3FE9))
+10* (a1 &0xD68E3FE9)
- (a1 ^0xD68E3FE9) ==0x251BC4BD)
return0LL;
return0xFFFFFFFFLL;
}
__int64 __fastcallchecker4(unsignedinta1)
{
if( a1 >0x10000000)
return0xFFFFFFFFLL;
if(11* (a1 ^0xAE7C284F)
+4* (a1 &0xAE7C284F)
- (6* (a1 &0x5183D7B0)
+12* ~(a1 |0x5183D7B0))
+ -5* a1
-2* ~(a1 |0x4EDA6B7C)
- (a1 |0xB1259483)
+3* (a1 &0x4EDA6B7C)
+4* (a1 &0xB1259483)
- -2* (a1 |0xB1259483) ==0xD9E7538A)
return0LL;
return0xFFFFFFFFLL;
}
```
这里一定要让checkers返回0LL才能继续
6.使用z3库编写求解器脚本，先安装一下z3
```bash
pip install z3-solver
```
## 0x03 编写解密脚本
7.开始编写脚本
```python
fromz3import*
defsolve_checker4():
solver = Solver()
a1 = BitVec('a1',32)
solver.add(a1 <=0x10000000)
expr = (
11* (a1 ^0xAE7C284F)
+4* (a1 &0xAE7C284F)
- (6* (a1 &0x5183D7B0) +12* ~(a1 |0x5183D7B0))
+ -5* a1
-2* ~(a1 |0x4EDA6B7C)
- (a1 |0xB1259483)
+3* (a1 &0x4EDA6B7C)
+4* (a1 &0xB1259483)
- -2* (a1 |0xB1259483)
)
solver.add(expr ==0xD9E7538A)
ifsolver.check() == sat:
model = solver.model()
returnmodel[a1].as_long()
else:
returnNone
defsolve_checker3():
solver = Solver()
a1 = BitVec('a1',32)
solver.add(a1 <=0x10000000)
expr = (
-3* (~a1 |0xD68E3FE9)
+3* ~(a1 |0xD68E3FE9)
+4* ((~a1 &0xD68E3FE9) +2* ~(~a1 |0xD68E3FE9))
+10* (a1 &0xD68E3FE9)
- (a1 ^0xD68E3FE9)
)
solver.add(expr ==0x251BC4BD)
ifsolver.check() == sat:
model = solver.model()
returnmodel[a1].as_long()
else:
returnNone
defsolve_checker2():
solver = Solver()
a1 = BitVec('a1',32)
solver.add(a1 <=0x10000000)
expr = (
3* (a1 &0x52E3F96B)
- (a1 |0xAD1C0694)
- a1
)
solver.add(expr ==0xE38773ED)
ifsolver.check() == sat:
model = solver.model()
returnmodel[a1].as_long()
else:
returnNone
# 这里其实可以直接算出来checker1需要的值是多少，
# 因为伪代码里面已经往checker1里面传入了0x5294B771
defsolve_checker1():
return0x956438B9+0x5294B771
solvers = [
solve_checker1,
solve_checker2,
solve_checker3,
solve_checker4
]
times =0
foriinsolvers:
times +=1
print(f"flag{times}:{int(i())ifi()isnotNoneelse'No solution'}")
```
8.运行脚本得到十进制的flag:
```bash
$ python -u ./decryptor.py
flag1: 3891851306
flag2: 2426636161
flag3: 88939547
flag4: 232752086
```
9.把flag输入进程序:
## 0x04 Flag!
10.得到最终flag`flag{e7f8f02a-90a38781-054d1c1b-0ddf83d6}`
