-
-
[原创]看雪ctf秋季赛 第二题 利用z3解方程
-
发表于: 2017-10-29 10:55
-
hello
输入后的两个call 并没有什么用 干扰视线
在text段有一段shellcode，构造9876543210ab11A的输入可以跳转到该shellcode上，这是一段很花很花的东西
跳转不看，我们将有用的汇编取出来
00413150 | 33 C0 | xor eax,eax | 00413184 | A3 34 B0 41 00 | mov dword ptr ds:[41B034],eax | 004131BA | 58 | pop eax | x ecx 004131EB | 8B C8 | mov ecx,eax | x 0041321F | 58 | pop eax | y ebx 00413254 | 8B D8 | mov ebx,eax | y 00413289 | 58 | pop eax | z edx 004132B5 | 8B D0 | mov edx,eax | z 004132AD | 8B D0 | mov edx,eax | 004132E2 | 8B C1 | mov eax,ecx | eax = ecx = x 00413316 | 2B C3 | sub eax,ebx | eax = eax-ecx = x-y 00413349 | C1 E0 02 | shl eax,2 | eax = (x-y)<<2 00413380 | 03 C1 | add eax,ecx | eax = ((x-y)<<2)+ x 004133B5 | 03 C2 | add eax,edx | eax = ((x-y)<<2)+ x+z 004133E9 | 2D E2 17 F9 EA | sub eax,EAF917E2 | eax = ((x-y)<<2)+ x+z-0xEAF917E2 00413455 03C1 ADD EAX,ECX 00413489 2BC3 SUB EAX,EBX ; EAX=EAX-EBX=x-y 004134BF 8BD8 MOV EBX,EAX ; EBX=x-y 004134F3 D1E0 SHL EAX,1 ; EAX= (x-y)<<1 00413525 03C3 ADD EAX,EBX ; EAX=EAX+EBX= ((x-y)<<1)+(x-y) 00413559 03C1 ADD EAX,ECX ; EAX= ((x-y)<<1)+(x-y)+x 0041358F 8BC8 MOV ECX,EAX ; ECX=EAX 004135C3 03C2 ADD EAX,EDX ; EAX= ((x-y)<<1)+(x-y)+x+z 004135F7 2D C808F5E8 SUB EAX,0xE8F508C8 ; EAX= ((x-y)<<1)+(x-y)-0xE8F508C8 00413665 8BC1 MOV EAX,ECX ; EAX= ((x-y)<<1)+(x-y)+x 0041365D 8BC1 MOV EAX,ECX ; 004136A7 2BC2 SUB EAX,EDX ; EAX= EAX-EDX=((x-y)<<1)+(x-y)+x-z
然后可以获取三个算式
我们使用z3求解
$ cat solve.py
#!/usr/bin/env python
# coding=utf-8
from z3 import *
x, y ,z = BitVecs('x y z', 64)
#x = Real('x')
#y = Real('y')
#z = Real('z')
solve(((x - y) << 2) + x + z == 0xEAF917E2,((x - y) << 1) + (x - y) + x + z == 0xE8F508C8,((x - y) << 1) + (x - y) + x - z == 0x0C0A3C68)
# swing @ swingdeMacBook-Pro in /private/tmp [21:32:21]
$ python solve.py
[z = 1853187632, y = 1919903280, x = 1953723722]
[招生]科锐逆向工程师培训(2024年11月15日实地，远程教学同时开班, 第51期)
