首页
社区
课程
招聘
[原创]rctf2018 - baby re2
发表于: 2018-5-21 23:45 4871

[原创]rctf2018 - baby re2

2018-5-21 23:45
4871

Baby re2 解法

题目知识点

  • SSE 指令集
  • 乘法逆元

整体分析

  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

[注意]传递专业知识、拓宽行业人脉——看雪讲师团队等你加入!

最后于 2018-5-21 23:45 被无名侠编辑 ,原因:
上传的附件:
收藏
免费 0
支持
分享
最新回复 (3)
雪    币: 190
活跃值: (194)
能力值: ( LV3,RANK:31 )
在线值:
发帖
回帖
粉丝
2
请教一下,对于这个程序,在IDA做了什么修改呢,是创建了数组吗?
2018-5-29 15:47
0
雪    币: 6911
活跃值: (9069)
能力值: ( LV17,RANK:797 )
在线值:
发帖
回帖
粉丝
3
ZakiGui 请教一下,对于这个程序,在IDA做了什么修改呢,是创建了数组吗?
对的。。部分变量的类型手动改一改就很容易阅读了。
2018-5-30 20:06
0
雪    币: 5676
活跃值: (1303)
能力值: ( LV17,RANK:1185 )
在线值:
发帖
回帖
粉丝
4
SSE反编译效果还真的不如直接看汇编
2018-5-31 05:09
0
游客
登录 | 注册 方可回帖
返回
//