这里主要记录打CTF比赛过程中学到的东西，WriteUp放在Github仓库，这里可能主要写一些常用方法

WriteUp地址

https://github.com/2aurora2/CTF-WriteUp

工具/方法篇

求解多元线性方程组

这个是在学校新生赛碰到的一道逆向题需要求解多个未知数的线性方程组，有挺多方法的，看到wp才发现python有一个z3库可以用来求解。

这个库不仅可以用来求解线性方程组，还可以用来求解一些约束条件下的可行解，不过这里主要介绍求解线性方程组。

z3-solver库就自行安装，注意名字是z3-solver不是z3

首先对需要求解的变量需要声明类型，主要有整型(Int)，实型(Real)和向量(BitVec)，以那道逆向题为例需要求解23个未知量的线性方程组，其中未知量均为整数，则声明如下: 

1
2
3
4
from z3 import *

#  Int创建一个整型变量，Ints创建多个整型变量；其中参数为变量名字的字符串；实型和向量同理
x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23 = Ints('x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23')

然后创建一个求解器并添加约束条件：

1
2
3
4
5
6
7
8
9
solver = Solver()

solver.add(
    212 * x22 + 819 * x21 + 421 * x20 + 814 * x19 + 781 * x18 + 184 * x17 + 709 * x16 + 401 * x15 + 351 * x14 + 993 * x13 + 814 * x12 + 553 * x11 + 495 * x10 + 646 * x9 + 565 * x8 + 271 * x7 + 520 * x6 + 770 * x5 + 335 * x4 + 680 * x3 + 625 * x2 + 215 * x1 + 250 * x0 + 525 * x23 == 1173434)

solver.add(
    909 * x22 + 819 * x21 + 404 * x20 + 323 * x19 + 961 * x18 + 625 * x17 + 630 * x16 + 760 * x15 + 781 * x14 + 353 * x13 + 207 * x12 + 363 * x11 + 126 * x10 + 569 * x9 + 279 * x8 + 988 * x7 + 115 * x6 + 815 * x5 + 598 * x4 + 186 * x3 + 795 * x2 + 744 * x1 + 371 * x0 + 354 * x23 == 1290416)

…………

最后检查是否存在解以及输出解的结果：

1
2
print(solver.check())      # 解存在返回sate/sat；反之返回 unsate/unsat
print(solver.model())     # 先执行check再执行model可得到解的结果