看雪CTF2017-秋季赛2题
###心路历程
这道题做下来还是觉得自己的经验太少练习不够，虽然已经找到413131处的乱码，但是当时认为是混淆，没有想到会是溢出。这学期多抽点时间看看PWN好了。
###题目思路
一开始要你解两个方程
这两个方程无解。有铁脑壳要是执意解方程就走远了。
###溢出
实际上。第13-15个字符是溢出覆盖了下一个要跳转的地址，如果字符串个数多于15个程序就崩溃了。
那么413131处的乱码也可以解释了。
所以13-15的字符应该是11A（这里是小端读入）
###
过去发现其实就是解三个方程，下面附上z3代码解方程（只用关注x,y,z，其他是模板）1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51#!/usr/bin/env python
from z3 import *
def get_models(s):
# from 0vercl0k's z3tools.py
while s.check() == sat:
m = s.model()
yield m
s.add(Or([sym() != m[sym] for sym in m.decls()]))
s = Solver()
a, b, c, d, e, f, g, h, i, j, k, l = BitVecs('a b c d e f g h i j k l', 8)
x,y,z=BitVecs('x y z',64)
s.add(And(0x20 < c, c < 0x7f))
s.add(And(0x20 < d, d < 0x7f))
s.add(And(0x20 < e, e < 0x7f))
s.add(And(0x20 < f, f < 0x7f))
s.add(And(0x20 < g, g < 0x7f))
s.add(And(0x20 < h, h < 0x7f))
s.add(And(0x20 < i, i < 0x7f))
s.add(And(0x20 < j, j < 0x7f))
# from PIN trace
s.add(((x-y)<<2)+x+z==0xeaf917e2)
s.add(((x-y)<<1)+(x-y)+x+z==0xe8f508c8)
s.add(((x-y)<<1)+(x-y)+x-z==0xc0a3c68)
s.add(a==0x31)
s.add(b==0x31)
s.add(c == 0x31)
s.add(d == 0x31)
s.add(e == 0x31)
s.add(f == 0x31)
s.add(g == 0x31)
s.add(h == 0x31)
s.add(i == 0x31)
s.add(j == 0x31)
s.add(k == 0x31)
s.add(l== 0x3l)
for m in get_models(s):
serial = [m[a].as_long(), m[b].as_long(), m[c].as_long(), m[d].as_long(),
m[e].as_long(), m[f].as_long(), m[g].as_long(), m[h].as_long(),
m[i].as_long(), m[j].as_long(), m[k].as_long(), m[l].as_long(), m[x].as_long(), m[y].as_long(),m[z].as_long()]
key = ''
for _ in serial: print _
结果如下
显而易见，第一组解就是我们的答案
对应字符是Just0for0fun。
###答案