0x01 基本用法求解器在使用 z3 进行约束求解之前我们首先需要获得一个 求解器 类实例，本质上其实就是一组约束的集合：
1>>> s = z3.Solver()
变量再创建用于解方程的变量
12345import z3;x = z3.Int(name = 'x') #x是整形变量y = z3.Real(name = 'y') #y是实数z = z3.BitVec(name= 'z', bv = 32) #z是长度为32位的向量（向量长度需初始化）p = z3.Bool(name = 'p') #p是bool型
整型与实数类型变量之间可以互相进行转换：
12z3.ToReal(x)z3.ToInt(y)
还能创建常量
1z3.IntVal(val = 114514) #int类型常量
添加约束用add()方法为指定求解器添加约束，条件为初始化中变量组成的式子；
12s.add(x + 5 == 111)s.add(y + 3 == x)
bool类型还可逻...
hachimi0x01 去trycatch反调试ida打开发现很明显代码不完整，看到trylevel这个函数，搜索知是用于修改trycatch异常处理等级的函数，程序很可能是通过trycatch进行混淆；
看汇编，真正程序应该在except块里，
正常逻辑如下进入4e1357
其中注意到dir ecx，ecx是0，这里抛出除零异常进入expect块；
流程如下：ida默认了jmp从而忽略了expect的反编译；
// ida不能识别异常，函数只有通过jge再到jmp一条路可走，认为上面_except这一块永远不会执行；
既然jmp_145e不会执行，那就把jmp_145e nop掉,后面还有个except过滤器也nop了；
代码就正常了；
// 这样让expect一定会顺序执行，因为他本来就一定会执行，所以正好是对的
0x02 去花
加密代码不完整，继续看汇编；
下面的call_+5和jz很明显是花，直接force jump,得到完整加密；
先tea后异或，解密如下：
1234567891011121314151617181...
fisher0x01 解密ida打开文件，main函数：
将输入加密为str1与密文比较，加密逻辑为换表base64；
fake flag;
尝试动调也错，感觉strcmp不能正常执行；
动调进入strcmp，发现系统指令被修改为一个jmp，进入后出现真正的加密函数
输入每八位执行一个tea加密（sub_7ff)，v5是密文，v9是key（后八位是0）；
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106#include<iostream>#include<string>#include<algorithm>#include<vector>#include<...
flower0x00 动调elf文件,idawsl动调无法正常运行,提示Don’t trace me:(,猜测有反调试.
0x01 去花ida发现标红，无法f5,track到有很明显的花,4048e5处jz和jnz必有一个执行,所以call永不执行
直接nop掉call,然后选中标红段按c强转为code,找到函数头按u再按p重定义,即可正常f5
0x02 去反调试对主函数按x向上追溯,发现这里第24行的cin没有执行,下第10行的断点后调试,发现在check中会跳出
进入发现ptrace反调试函数,if(调试)就进入下面的块
直接让他不进入即可,将jz改为jmp
然后就可以正常调试了,solve加密函数也能正常显示
0x03 解密encode函数就是将输入自增,异或和与enc中比较
解密代码:
12345678910111213141516171819202122#include<iostream>#include<string>#include<algorithm>#include<vector>using...