简单的z3
z3-solver求解器z3-solver是由Microsoft Research(微软)开发的SMT求解器，它用于检查逻辑表达式的可满足性，可以找到一组约束中的其中一个可行解，缺点是无法找出所有的可行解 pip安装：pip install z3-solver 基本用法： 123456789import z3x.Int('x')y.Int('y')s=z3.Solver()s.add(x+y=4)if s.check() == z3.sat: print(s.model())else: raise Exception("NO SOLUTION!") 实数：y = z3.Real(name = 'y') 位向量：z = z3.BitVec(name = 'z', bv = 32) 布尔：p = z3.Bool(name = 'p') 对于布尔类型的式子而言，我们可以使用 z3 内置的 And()、Or()、Not()、Implies()...
RC4
原理RC4是一种流加密算法，密钥长度可变，可变范围是1-256字节，属于对称加密算法 生成S-boxKSA算法初始化长度为256的S盒，用种子密钥(就是我们的秘钥)循环填充另一个256字节的K表，用K表对S表进行初始置换 123456789def KSA(key): key_length = len(key) S = list(range(256)) j = 0 for i in range(256): j = (j + S[i] + key[i % key_length]) % 256 S[i], S[j] = S[j], S[i] # 交换S[i]和S[j] return S 生成密钥流PGRA算法根据S盒生成与明文长度相同的密钥流 12345678910def PRGA(S): i = 0 j = 0 while True: i = (i + 1) % 256 j = (j + S[i]) % 256 S[i], S[j] = S[j], S[i] ...
python逆向
[Litctf 2024] ezPython!!! 今天见到一道python打包成exe文件的逆向题，虽然很简单，但是安装工具遇到了一些麻烦 将.exe文件反编译为pyc文件.pyinstxtractor.py工具安装地址：https://sourceforge.net/projects/pyinstallerextractor/ 先将pyinstxtractor.py工具与我们要反编译的.exe文件放入同一个工作目录下,在终端输入python pyinstxtractor.py 文件名.py 😕因为python版本问题，imp模块无法安装，需要替换为importlibc,(pip install importlib)但是又提示importlibc没有get_magic方法，需要替换为importlib.util.MAGIC_NUMBER，又又提示module ‘importlib’ has no attribute ‘util’，于是写上from importlib.util import find_spec...
Reverse刷题笔记
[HUBUCTF 2022 新生赛]simple_RE附件是.exe文件 用ida打开F5反汇编得到： sub_401570函数对输入的flag进行变换，memcmp函数用于判断两个字符串的前n个字符是否相等 进入sub_401570： (经过chatgpt分析) 分析出这个函数的功能： 到这里我认为只要把已知字符串进行base64解码就行，发现是乱码 经过wp提示，原来是base64换表 aQvejafhmuyjbac=”qvEJAfHmUYjBac+u8Ph5n9Od17FrICL/X0gVtM4Qk6T2z3wNSsyoebilxWKGZpRD”是映射表 写脚本复原： 123456789101112131415import base64c = "5Mc58bPHLiAx7J8ocJIlaVUxaJvMcoYMaoPMaOfg15c475tscHfM"flag = ""table =...
