Automne's Shadow.

0CTF 2019 zer0lfsr WriteUp

lfsr z3
2019/04/11 Share

Crypto

拿到了python的加密脚本和密钥流，和常见的lfsr算法不同的是，密钥流是3个lfsr的计算结果经过combine(x1,x2,x3)函数处理后得到的。

automne

参考了p4队伍的Writeup，使用z3约束求解器进行求解。

在Kali下安装z3

python -m pip install z3-solver

下面的脚本是对单字符单lfsr的求解。

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
#encoding:utf-8

import random
import z3
import string
from Crypto.Util.number import bytes_to_long,long_to_bytes

class lfsr():
    def __init__(self, init, mask, length):
        self.init = init
        self.mask = mask
        self.lengthmask = 2**(length+1)-1

    def next(self):
        nextdata = (self.init << 1) & self.lengthmask 
        i = self.init & self.mask & self.lengthmask 
        output = 0
        while i != 0:
            output ^= (i & 1)
            i = i >> 1
        nextdata ^= output
        self.init = nextdata
        return output

def solve_lfsr(results, index1, index2, length):
    s = z3.Solver()
    x = init_recovered = z3.BitVec('x', length)
    for result in results:
        relevant_bit1 = init_recovered & (1 << index1)
        bit1_value = z3.LShR(relevant_bit1, index1)

        relevant_bit2 = init_recovered & (1 << index2)
        bit2_value = z3.LShR(relevant_bit2, index2)

        s.add(bit1_value ^ bit2_value == result)

        init_recovered = ((init_recovered << 1) & (2 ** (length + 1) - 1)) ^ result
    s.check()
    return long_to_bytes(int(str(s.model()[x])))
	
if __name__ == '__main__':
    init = random.choice(string.lowercase)
    print('target', init)
    size = len(init) * 8
    i = bytes_to_long(init)
    target = lfsr(i, 0b11000000, size)
    results = [target.next() for _ in range(size)]
    print(results)
    print('result', solve_lfsr(results, 7, 6, size))

还原效果如下图：

automne

为验证z3约束求解的效果，对2018年国赛oldstreamgame进行了测试。

首先使用题目中的脚本，生成key。

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
flag = "flag{926201d7}"
assert flag.startswith("flag{")
assert flag.endswith("}")
assert len(flag)==14

def lfsr(R,mask):
    output = (R << 1) & 0xffffffff
    i=(R&mask)&0xffffffff
    lastbit=0
    while i!=0:
        lastbit^=(i&1)
        i=i>>1
    output^=lastbit
    return (output,lastbit)

R=int(flag[5:-1],16)
mask = 0b10100100000010000000100010010100

f=open("key","w")
for i in range(100):
    tmp=0
    for j in range(8):
        (R,out)=lfsr(R,mask)
        print out
        tmp=(tmp << 1)^out
    print tmp
    f.write(chr(tmp))
f.close()

然后修改对应的solve_lfsr()函数参数

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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
#encoding:utf-8

import random
import z3
import string
from Crypto.Util.number import bytes_to_long,long_to_bytes
import libnum

'''class lfsr():
    def __init__(self, init, mask, length):
        self.init = init
        self.mask = mask
        self.lengthmask = 2**(length+1)-1

    def next(self):
        nextdata = (self.init << 1) & self.lengthmask 
        i = self.init & self.mask & self.lengthmask 
        output = 0
        while i != 0:
            output ^= (i & 1)
            i = i >> 1
        nextdata ^= output
        self.init = nextdata
        return output
'''
class lfsr():
    def __init__(self, init, mask,length):
        self.init = init
        self.mask = mask
        self.lengthmask = 2**(length+1)-1

    def next(self):
        nextdata = (self.init << 1) & self.lengthmask 
        i = self.init & self.mask & self.lengthmask 
        lastbit = 0
        while i != 0:
            lastbit ^= (i & 1)
            i = i >> 1
        nextdata ^= lastbit
        #self.init = nextdata
        return nextdata,lastbit

def solve_lfsr(results, index1, index2, index3, index4, index5, index6, index7, index8, length):
    s = z3.Solver()
    x = init_recovered = z3.BitVec('x', length)
    for result in results:
        relevant_bit1 = init_recovered & (1 << index1)
        bit1_value = z3.LShR(relevant_bit1, index1)

        relevant_bit2 = init_recovered & (1 << index2)
        bit2_value = z3.LShR(relevant_bit2, index2)

        relevant_bit3 = init_recovered & (1 << index3)
        bit3_value = z3.LShR(relevant_bit3, index3)

        relevant_bit4 = init_recovered & (1 << index4)
        bit4_value = z3.LShR(relevant_bit4, index4)

        relevant_bit5 = init_recovered & (1 << index5)
        bit5_value = z3.LShR(relevant_bit5, index5)

        relevant_bit6 = init_recovered & (1 << index6)
        bit6_value = z3.LShR(relevant_bit6, index6)

        relevant_bit7 = init_recovered & (1 << index7)
        bit7_value = z3.LShR(relevant_bit7, index7)

        relevant_bit8 = init_recovered & (1 << index8)
        bit8_value = z3.LShR(relevant_bit8, index8)

        s.add(bit1_value ^ bit2_value ^ bit3_value ^ bit4_value ^ bit5_value ^ bit6_value ^ bit7_value ^ bit8_value == result)

        init_recovered = ((init_recovered << 1) & (2 ** (length + 1) - 1)) ^ result
    s.check()
    return hex(int(str(s.model()[x])))
	
if __name__ == '__main__':

    '''init = int("926201d7",16)
    #init0 = "9201d7d5"
    #init = bytes_to_long(init0)
    tmp2 = []
    for i in range(100):
        tmp = 0
        for j in range(8):
            init,out = lfsr(init,0b10100100000010000000100010010100,32).next()
            tmp2.append((tmp << 1)^out)
    print tmp2'''

    tmp2 = []
    data = open('key').read()
    for i in range(100):
        #print data[i]
        a =  '{:08b}'.format(ord(data[i])).replace('0b','')
        for j in range(8):
            tmp2.append(a[j])
    #print tmp2
    print('result', solve_lfsr(tmp2, 2, 4, 7, 11, 19, 26, 29, 31, 32))

最终可还原key的内容

automne

可以看到，使用z3求解只需要根据mask格式修改对应参数即可。
回到问题本身。

使用如下代码：

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
import z3
import codecs
from Crypto.Util.number import bytes_to_long,long_to_bytes
import hashlib

def solve_3_lfsr(keystream, relevant_bit_indices, length, mask_length):
    len_mask = (2 ** (mask_length + 1) - 1)
    result_bits = map(long, "".join([bin(ord(c))[2:].zfill(8) for c in keystream]))
    s = z3.Solver()
    x = z3.BitVec('x', length)
    y = z3.BitVec('y', length)
    z = z3.BitVec('z', length)
    inits = [x, y, z]
    for result in result_bits:
        combs = []
        new_inits = []
        for index in range(3):
            relevant_bit1 = (inits[index] & (1 << relevant_bit_indices[index][0]))
            bit1_value = z3.LShR(relevant_bit1, relevant_bit_indices[index][0])
            relevant_bit2 = inits[index] & (1 << relevant_bit_indices[index][1])
            bit2_value = z3.LShR(relevant_bit2, relevant_bit_indices[index][1])
            single_lfsr_result = bit1_value ^ bit2_value
            combs.append(single_lfsr_result)
            new_init = ((inits[index] << 1) & len_mask) ^ single_lfsr_result
            new_inits.append(new_init)
        s.add(combine(combs[0], combs[1], combs[2]) == result)
        inits = new_inits
    s.check()
    model = s.model()
    print(model)
    x_res = int(str(model[x]))
    y_res = int(str(model[y]))
    z_res = int(str(model[z]))
    return x_res, y_res, z_res

def combine(x1,x2,x3):
    return (x1*x2)^(x2*x3)^(x1*x3)

def solve():
    with codecs.open("keystream", 'rb', 'utf8') as input_file:
        data = input_file.read()
        mask1 = (47, 22)
        mask2 = (47, 13)
        mask3 = (47, 41)
        x, y, z = solve_3_lfsr("".join(map(chr, map(ord, data)))[:48], [mask1, mask2, mask3], 48, 48)
        print(x, y, z)
        init1, init2, init3 = map(long_to_bytes, [x, y, z])
        print("flag{" + hashlib.sha256(init1 + init2 + init3).hexdigest() + "}")

if __name__ == '__main__':
    solve()

运行上面的代码，即可得到flag

automne

原文作者: Automne

原文链接: https://ce-automne.github.io/2019/04/11/0CTF-2019-zer0lfsr-WriteUp/

发表日期: April 11th 2019, 10:17:00 pm

版权声明: 本文采用知识共享署名-非商业性使用 4.0 国际许可协议进行许可

CATALOG
Total : 62
2021
2020
2019
2018
2017
lfsr z3 python reverse fat git broadcastreceiver sha-1 cbc sqli sqlite golang race condition luks hashcat photorec MAC sso oauth 2.0 padding oracle csp xss abe vdex ransomware frida ndk pwntools hashpumpy sourceleakhacker ecb socat fastjson JdbcRowsetImpl idea servlet volatility inet_aton boneh durfee lcg rabin egcd cipolla's algorithm spi snakeyaml ScriptEngineManager malware codereflect mysql yara plugin deserialization log4j rsa binary javascript prototype pollution nodejs shiro ysoserial primefac rsatool ssl AES tshark gmpy2 RsaCtfTool Hex flask ssti ecc Modular operation WebGoat8 order by tomcat nim game .iso gpg outguess sage google cloud sdk zsteg base58 fermat multi-primes prng rmi jndi Paillier Cryptosystem rsa lsb oracle SQL Injection ping delay xor CAS 单点登录 渗透测试 weblogic xxe reflect 010 editor gcd
Crypto Android Web Forensics Misc