Baby re2 解法 题目知识点
整体分析 v17.m128i_i64[0] = mod(v7[0] * s[0], 0xFFFFFFFFFFFFFFC5LL, 0LL);
v17.m128i_i64[1] = mod(v7[1] * s[1], 0xFFFFFFFFFFFFFFC5LL, 0LL);
v18.m128i_i64[0] = mod(v7[2] * s[2], -0x3BuLL, 0LL);
v18.m128i_i64[1] = mod(v7[3] * s[3], 0xFFFFFFFFFFFFFFC5LL, 0LL);
v19.m128i_i64[0] = mod(v7[4] * s[4], 0xFFFFFFFFFFFFFFC5LL, 0LL);
v19.m128i_i64[1] = mod(v7[5] * s[5], 0xFFFFFFFFFFFFFFC5LL, 0LL);
v20.m128i_i64[0] = mod(v7[6] * s[6], 0xFFFFFFFFFFFFFFC5LL, 0LL);
v20.m128i_i64[1] = mod(v7[7] * s[7], 0xFFFFFFFFFFFFFFC5LL, 0LL);
v21.m128i_i64[0] = mod(v7[8] * v9, 0xFFFFFFFFFFFFFFC5LL, 0LL);
v21.m128i_i64[1] = mod(v7[9] * v10, 0xFFFFFFFFFFFFFFC5LL, 0LL);
v22.m128i_i64[0] = mod(v7[10] * v11, 0xFFFFFFFFFFFFFFC5LL, 0LL);
v22.m128i_i64[1] = mod(v7[11] * v12, 0xFFFFFFFFFFFFFFC5LL, 0LL);
v23.m128i_i64[0] = mod(v7[12] * v13, 0xFFFFFFFFFFFFFFC5LL, 0LL);
v23.m128i_i64[1] = mod(v7[13] * v14, 0xFFFFFFFFFFFFFFC5LL, 0LL);
v24.m128i_i64[0] = mod(v7[14] * v15, 0xFFFFFFFFFFFFFFC5LL, 0LL);
v3 = mod(v7[15] * v16, 0xFFFFFFFFFFFFFFC5LL, 0LL);
v4 = _mm_load_si128(&v17);
v24.m128i_i64[1] = v3;
v5 = _mm_or_si128(
_mm_xor_si128(_mm_load_si128(&xmmword_6020D0), v24),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(&v23), xmmword_6020C0),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(&v22), xmmword_6020B0),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(&v21), xmmword_6020A0),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(&v20), xmmword_602090),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(&v19), xmmword_602080),
_mm_or_si128(_mm_xor_si128(v4, xmmword_602060), _mm_xor_si128(_mm_load_si128(&xmmword_602070), v18))))))));
if ( *&_mm_or_si128(v5, _mm_srli_si128(v5, 8)) )
puts("Incorrect.");
else
puts("Correct. Congratulations!");
v7是输入的数据,最大126个字符
s[] 是常量,调试即可得到。
xmmword_602060 = 0x7BA58F82BD8980352B7192452905E8FB
xmmword_602070 = 0x163F756FCC221AB0A3112746582E1434
xmmword_602080 = 0xDCDD8B49EA5D7E14ECC78E6FB9CBA1FE
xmmword_602090 = 0xAAAAAAAAAA975D1CA2845FE0B3096F8E
xmmword_6020A0 = 0x55555555555559A355555555555559A3
xmmword_6020B0 = 0x55555555555559A355555555555559A3
xmmword_6020C0 = 0x55555555555559A355555555555559A3
xmmword_6020D0 = 0x55555555555559A355555555555559A3
mod 是取模函数。
大概思路是:
v7[x] * s[y] % 0xFFFFFFFFFFFFFFC5LL = v17.....v24
其中v7[x]是flag数据,s[y] 是常量,v17....v24可通过后面的运算反向求得,最后使用乘法逆元求v7,也就是flag数据。
乘法逆元a*b%c=d
a=d*b^(c-2)%c
python代码
def fastExpMod(b, e, m):
result = 1
while e != 0:
if (e&1) == 1:
# ei = 1, then mul
result = (result * b) % m
e >>= 1
# b, b^2, b^4, b^8, ... , b^(2^n)
b = (b*b) % m
return result
def r(d,b):
c = 0xFFFFFFFFFFFFFFC5
s=d*fastExpMod(b,(c-2),c) % c
return s
#flagXX = r(v17,s[y])
求解v17......v23使用z3进行符号执行后约束求解
xmmword_602060 = 0x7BA58F82BD8980352B7192452905E8FB
xmmword_602070 = 0x163F756FCC221AB0A3112746582E1434
xmmword_602080 = 0xDCDD8B49EA5D7E14ECC78E6FB9CBA1FE
xmmword_602090 = 0xAAAAAAAAAA975D1CA2845FE0B3096F8E
xmmword_6020A0 = 0x55555555555559A355555555555559A3
xmmword_6020B0 = 0x55555555555559A355555555555559A3
xmmword_6020C0 = 0x55555555555559A355555555555559A3
xmmword_6020D0 = 0x55555555555559A355555555555559A3
v17 = BitVec('v17',128)
v18 = BitVec('v18',128)
v19 = BitVec('v19',128)
v20 = BitVec('v20',128)
v21 = BitVec('v21',128)
v22 = BitVec('v22',128)
v23 = BitVec('v23',128)
v24 = BitVec('v24',128)
def _mm_or_si128(a,b):
return a|b
def _mm_xor_si128(a,b):
return a^b
def _mm_load_si128(a):
return a
v5 = _mm_or_si128(
_mm_xor_si128(_mm_load_si128(xmmword_6020D0), v24),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(v23), xmmword_6020C0),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(v22), xmmword_6020B0),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(v21), xmmword_6020A0),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(v20), xmmword_602090),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(v19), xmmword_602080),
_mm_or_si128(_mm_xor_si128(v17, xmmword_602060), _mm_xor_si128(_mm_load_si128(xmmword_602070), v18))))))))
b = v5|(v5>>8)
s = Solver()
s.add(b == 0)
s.check()
res = s.model()
完整代码from z3 import *
def fastExpMod(b, e, m):
result = 1
while e != 0:
if (e&1) == 1:
# ei = 1, then mul
result = (result * b) % m
e >>= 1
# b, b^2, b^4, b^8, ... , b^(2^n)
b = (b*b) % m
return result
def r(d,b):
c = 0xFFFFFFFFFFFFFFC5
s=d*fastExpMod(b,(c-2),c) % c
return s
print hex(r(0x55555555555559a3L,0xFFFFFFFFFFFFFFFF))
xmmword_602060 = 0x7BA58F82BD8980352B7192452905E8FB
xmmword_602070 = 0x163F756FCC221AB0A3112746582E1434
xmmword_602080 = 0xDCDD8B49EA5D7E14ECC78E6FB9CBA1FE
xmmword_602090 = 0xAAAAAAAAAA975D1CA2845FE0B3096F8E
xmmword_6020A0 = 0x55555555555559A355555555555559A3
xmmword_6020B0 = 0x55555555555559A355555555555559A3
xmmword_6020C0 = 0x55555555555559A355555555555559A3
xmmword_6020D0 = 0x55555555555559A355555555555559A3
v17 = BitVec('v17',128)
v18 = BitVec('v18',128)
v19 = BitVec('v19',128)
v20 = BitVec('v20',128)
v21 = BitVec('v21',128)
v22 = BitVec('v22',128)
v23 = BitVec('v23',128)
v24 = BitVec('v24',128)
def _mm_or_si128(a,b):
return a|b
def _mm_xor_si128(a,b):
return a^b
def _mm_load_si128(a):
return a
v5 = _mm_or_si128(
_mm_xor_si128(_mm_load_si128(xmmword_6020D0), v24),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(v23), xmmword_6020C0),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(v22), xmmword_6020B0),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(v21), xmmword_6020A0),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(v20), xmmword_602090),
_mm_or_si128(
_mm_xor_si128(_mm_load_si128(v19), xmmword_602080),
_mm_or_si128(_mm_xor_si128(v17, xmmword_602060), _mm_xor_si128(_mm_load_si128(xmmword_602070), v18))))))))
b = v5|(v5>>8)
s = Solver()
s.add(b == 0)
s.check()
res = s.model()
def ascii(x):
s = ''
for i in range(8):
s = s + chr(x & 0xff)
x = x >> 8
return s
def unp(x,i):
if i == 0:
return res[x].as_long() & 0xffffffffffffffff
else:
return res[x].as_long() >> 64
flag = ascii(r(unp(v17,0),0x20656D6F636C6557))
flag += ascii(r(unp(v17,1),0x2046544352206F74))
flag += ascii(r(unp(v18,0),0x6548202138313032))
flag += ascii(r(unp(v18,1),0x2061207369206572))
flag += ascii(r(unp(v19,0),0x6320455279626142))
flag += ascii(r(unp(v19,1),0x65676E656C6C6168))
flag += ascii(r(unp(v20,0), 0x756F7920726F6620))
flag += ascii(r(unp(v20,1), 0xFFFFFFFFFFFF002E))
flag += ascii(r(unp(v21,0), 0xFFFFFFFFFFFFFFFF))
flag += ascii(r(unp(v21,1), 0xFFFFFFFFFFFFFFFF))
flag += ascii(r(unp(v22,0), 0xFFFFFFFFFFFFFFFF))
flag += ascii(r(unp(v22,1), 0xFFFFFFFFFFFFFFFF))
flag += ascii(r(unp(v23,0), 0xFFFFFFFFFFFFFFFF))
flag += ascii(r(unp(v23,1), 0xFFFFFFFFFFFFFFFF))
flag += ascii(r(unp(v24,0), 0xFFFFFFFFFFFFFFFF))
flag += ascii(r(unp(v24,1), 0xFFFFFFFFFFFFFFFF))
print flag
[培训]内核驱动高级班,冲击BAT一流互联网大厂工作,每周日13:00-18:00直播授课
最后于 2018-5-21 23:45
被无名侠编辑
,原因:
上传的附件: