RE WP November 29, 2019

2019 nctf wp

Words count 1.7k Reading time 2 mins. Read count 1000000

DEBUG

动态调试即可,发现函数最后要和s比较,s经过多次加密。

上图cmp dl,al就是比较过程.
动态调试看寄存中的值就可以得到flag。
本道题有一个值得学习的算法在rc4上

https://odoiys.github.io/2019/11/29/rc4%E5%AD%A6%E4%B9%A0/

签到题

使用z3求解器

from z3 import *
a = [12, 83, 78, 39, 23, 27, 4, 53, 85, 53, 78, 6, 85, 6, 6, 12, 24, 52, 14, 92, 3, 34, 73, 36, 9, 74, 42, 67, 58, 27, 86, 62, 48, 48, 0, 36, 96, 25, 37, 12, 15, 26, 1, 52, 46, 84, 83, 72, 68]
b = [18564,37316,
32053,
33278,
23993,
33151,
15248,
13719,
34137,
27391,
28639,
18453,
28465,
12384,
20780,
45085,
35827,
37243,
26037,
39409,
17583,
20825,
44474,
35138,
36914,
25918,
38915,
17672,
21219,
43935,
37072,
39359,
27793,
41447,
18098,
21335,
46164,
38698,
39084,
29205,
40913,
19117,
21786,
46573,
38322,
41017,
29298,
43409,
19655]
s = Solver()
key = [BitVec('u%d'%i,8) for i in range(49)]
for i in range(7):
    for j in range(7):
        s.add(b[i*7+j] == key[i*7]*a[j]+key[i*7+1]*a[7*1+j]+key[i*7+2]*a[7*2+j]+key[i*7+3]*a[7*3+j]+key[i*7+4]*a[7*4+j]+key[i*7+5]*a[7*5+j]+key[i*7+6]*a[7*6+j])
flag = ''
if s.check() == sat:
    result = s.model()
    for i in range(49):
        flag += chr(result[key[i]].as_long().real)
    print flag

z3有问题可以看这个链接
https://ericpony.github.io/z3py-tutorial/guide-examples.htm

0%