FXTi's blog
0%

ciscn2020

Posted on Edited on

2020国赛预赛WP

智能合约看看这里

z3

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
from z3 import *

v5 = [BitVec('inp'+str(i), 8) for i in range(42)]
v4 = [None for _ in range(42)]

v4[0] = 34 * v5[3] + 12 * v5[0] + 53 * v5[1] + 6 * v5[2] + 58 * v5[4] + 36 * v5[5] + v5[6];
v4[1] = 27 * v5[4] + 73 * v5[3] + 12 * v5[2] + 83 * v5[0] + 85 * v5[1] + 96 * v5[5] + 52 * v5[6];
v4[2] = 24 * v5[2] + 78 * v5[0] + 53 * v5[1] + 36 * v5[3] + 86 * v5[4] + 25 * v5[5] + 46 * v5[6];
v4[3] = 78 * v5[1] + 39 * v5[0] + 52 * v5[2] + 9 * v5[3] + 62 * v5[4] + 37 * v5[5] + 84 * v5[6];
v4[4] = 48 * v5[4] + 14 * v5[2] + 23 * v5[0] + 6 * v5[1] + 74 * v5[3] + 12 * v5[5] + 83 * v5[6];
v4[5] = 15 * v5[5] + 48 * v5[4] + 92 * v5[2] + 85 * v5[1] + 27 * v5[0] + 42 * v5[3] + 72 * v5[6];
v4[6] = 26 * v5[5] + 67 * v5[3] + 6 * v5[1] + 4 * v5[0] + 3 * v5[2] + 68 * v5[6];
v4[7] = 34 * v5[10] + 12 * v5[7] + 53 * v5[8] + 6 * v5[9] + 58 * v5[11] + 36 * v5[12] + v5[13];
v4[8] = 27 * v5[11] + 73 * v5[10] + 12 * v5[9] + 83 * v5[7] + 85 * v5[8] + 96 * v5[12] + 52 * v5[13];
v4[9] = 24 * v5[9] + 78 * v5[7] + 53 * v5[8] + 36 * v5[10] + 86 * v5[11] + 25 * v5[12] + 46 * v5[13];
v4[10] = 78 * v5[8] + 39 * v5[7] + 52 * v5[9] + 9 * v5[10] + 62 * v5[11] + 37 * v5[12] + 84 * v5[13];
v4[11] = 48 * v5[11] + 14 * v5[9] + 23 * v5[7] + 6 * v5[8] + 74 * v5[10] + 12 * v5[12] + 83 * v5[13];
v4[12] = 15 * v5[12] + 48 * v5[11] + 92 * v5[9] + 85 * v5[8] + 27 * v5[7] + 42 * v5[10] + 72 * v5[13];
v4[13] = 26 * v5[12] + 67 * v5[10] + 6 * v5[8] + 4 * v5[7] + 3 * v5[9] + 68 * v5[13];
v4[14] = 34 * v5[17] + 12 * v5[14] + 53 * v5[15] + 6 * v5[16] + 58 * v5[18] + 36 * v5[19] + v5[20];
v4[15] = 27 * v5[18] + 73 * v5[17] + 12 * v5[16] + 83 * v5[14] + 85 * v5[15] + 96 * v5[19] + 52 * v5[20];
v4[16] = 24 * v5[16] + 78 * v5[14] + 53 * v5[15] + 36 * v5[17] + 86 * v5[18] + 25 * v5[19] + 46 * v5[20];
v4[17] = 78 * v5[15] + 39 * v5[14] + 52 * v5[16] + 9 * v5[17] + 62 * v5[18] + 37 * v5[19] + 84 * v5[20];
v4[18] = 48 * v5[18] + 14 * v5[16] + 23 * v5[14] + 6 * v5[15] + 74 * v5[17] + 12 * v5[19] + 83 * v5[20];
v4[19] = 15 * v5[19] + 48 * v5[18] + 92 * v5[16] + 85 * v5[15] + 27 * v5[14] + 42 * v5[17] + 72 * v5[20];
v4[20] = 26 * v5[19] + 67 * v5[17] + 6 * v5[15] + 4 * v5[14] + 3 * v5[16] + 68 * v5[20];
v4[21] = 34 * v5[24] + 12 * v5[21] + 53 * v5[22] + 6 * v5[23] + 58 * v5[25] + 36 * v5[26] + v5[27];
v4[22] = 27 * v5[25] + 73 * v5[24] + 12 * v5[23] + 83 * v5[21] + 85 * v5[22] + 96 * v5[26] + 52 * v5[27];
v4[23] = 24 * v5[23] + 78 * v5[21] + 53 * v5[22] + 36 * v5[24] + 86 * v5[25] + 25 * v5[26] + 46 * v5[27];
v4[24] = 78 * v5[22] + 39 * v5[21] + 52 * v5[23] + 9 * v5[24] + 62 * v5[25] + 37 * v5[26] + 84 * v5[27];
v4[25] = 48 * v5[25] + 14 * v5[23] + 23 * v5[21] + 6 * v5[22] + 74 * v5[24] + 12 * v5[26] + 83 * v5[27];
v4[26] = 15 * v5[26] + 48 * v5[25] + 92 * v5[23] + 85 * v5[22] + 27 * v5[21] + 42 * v5[24] + 72 * v5[27];
v4[27] = 26 * v5[26] + 67 * v5[24] + 6 * v5[22] + 4 * v5[21] + 3 * v5[23] + 68 * v5[27];
v4[28] = 34 * v5[31] + 12 * v5[28] + 53 * v5[29] + 6 * v5[30] + 58 * v5[32] + 36 * v5[33] + v5[34];
v4[29] = 27 * v5[32] + 73 * v5[31] + 12 * v5[30] + 83 * v5[28] + 85 * v5[29] + 96 * v5[33] + 52 * v5[34];
v4[30] = 24 * v5[30] + 78 * v5[28] + 53 * v5[29] + 36 * v5[31] + 86 * v5[32] + 25 * v5[33] + 46 * v5[34];
v4[31] = 78 * v5[29] + 39 * v5[28] + 52 * v5[30] + 9 * v5[31] + 62 * v5[32] + 37 * v5[33] + 84 * v5[34];
v4[32] = 48 * v5[32] + 14 * v5[30] + 23 * v5[28] + 6 * v5[29] + 74 * v5[31] + 12 * v5[33] + 83 * v5[34];
v4[33] = 15 * v5[33] + 48 * v5[32] + 92 * v5[30] + 85 * v5[29] + 27 * v5[28] + 42 * v5[31] + 72 * v5[34];
v4[34] = 26 * v5[33] + 67 * v5[31] + 6 * v5[29] + 4 * v5[28] + 3 * v5[30] + 68 * v5[34];
v4[35] = 34 * v5[38] + 12 * v5[35] + 53 * v5[36] + 6 * v5[37] + 58 * v5[39] + 36 * v5[40] + v5[41];
v4[36] = 27 * v5[39] + 73 * v5[38] + 12 * v5[37] + 83 * v5[35] + 85 * v5[36] + 96 * v5[40] + 52 * v5[41];
v4[37] = 24 * v5[37] + 78 * v5[35] + 53 * v5[36] + 36 * v5[38] + 86 * v5[39] + 25 * v5[40] + 46 * v5[41];
v4[38] = 78 * v5[36] + 39 * v5[35] + 52 * v5[37] + 9 * v5[38] + 62 * v5[39] + 37 * v5[40] + 84 * v5[41];
v4[39] = 48 * v5[39] + 14 * v5[37] + 23 * v5[35] + 6 * v5[36] + 74 * v5[38] + 12 * v5[40] + 83 * v5[41];
v4[40] = 15 * v5[40] + 48 * v5[39] + 92 * v5[37] + 85 * v5[36] + 27 * v5[35] + 42 * v5[38] + 72 * v5[41];
v4[41] = 26 * v5[40] + 67 * v5[38] + 6 * v5[36] + 4 * v5[35] + 3 * v5[37] + 68 * v5[41];

v6 = [20247, 40182, 36315, 36518, 26921, 39185, 16546, 12094, 25270, 19330, 18540, 16386, 21207, 11759, 10460, 25613, 21135, 24891, 18305, 27415, 12855, 10899, 24927, 20670, 22926, 18006, 23345, 12602, 12304, 26622, 19807, 22747, 14233, 24736, 10064, 14169, 35155, 28962, 33273, 21796, 35185, 14877]

s = Solver()

for i in range(42):
    s.add(v4[i] == v6[i])

print(s.check())
print(s.model())

print("".join(map(lambda x: chr(s.model()[x].as_long()), v5)))

hyperthreading

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
from z3 import *

target = [221, 91, 158, 29, 32, 158, 144, 145, 144, 144, 145, 146, 222, 139, 17, 209, 30, 158, 139, 81, 17, 80, 81, 139, 158, 93, 93, 17, 139, 144, 18, 145, 80, 18, 210, 145, 146, 30, 158, 144, 210, 159]

inp = [BitVec('inp'+str(i), 8) for i in range(42)]

s = Solver()
for i in range(42):
    tmp = inp[i] << 6 ^ inp[i] >> 2
    tmp ^= 0x23
    tmp += 35
    s.add(target[i] == tmp)

print(s.check())
print(s.model())
print("".join(map(lambda x: chr(s.model()[x].as_long()), inp)))

oplog

别的都没什么好说的，主要是这个合约部署和后面的Galios Field上面的Sage写法。

如果出题人给的是合约的ABI和字节码，如何部署？

用Remix的控制台，把部署语句压缩成一行直接部署：

1
(new web3.eth.Contract(JSON.parse('[ { "inputs": [ { "internalType": "uint256", "name": "choose", "type": "uint256" }, { "internalType": "uint256", "name": "arg1", "type": "uint256" }, { "internalType": "uint256", "name": "arg2", "type": "uint256" }, { "internalType": "uint256", "name": "arg3", "type": "uint256" } ], "name": "calcx", "outputs": [], "stateMutability": "nonpayable", "type": "function" }, { "inputs": [ { "internalType": "uint256", "name": "key1", "type": "uint256" }, { "internalType": "uint256", "name": "key2", "type": "uint256" }, { "internalType": "uint256", "name": "key3", "type": "uint256" } ], "name": "feistel", "outputs": [], "stateMutability": "nonpayable", "type": "function" }, { "inputs": [ { "internalType": "uint256", "name": "_flag", "type": "uint256" } ], "name": "setflag", "outputs": [], "stateMutability": "nonpayable", "type": "function" }, { "inputs": [ { "internalType": "uint256", "name": "p", "type": "uint256" } ], "name": "setr1", "outputs": [], "stateMutability": "nonpayable", "type": "function" }, { "inputs": [ { "internalType": "uint256", "name": "p", "type": "uint256" } ], "name": "setr2", "outputs": [], "stateMutability": "nonpayable", "type": "function" }, { "inputs": [ { "internalType": "uint256", "name": "p", "type": "uint256" } ], "name": "setr3", "outputs": [], "stateMutability": "nonpayable", "type": "function" }, { "inputs": [], "name": "flag", "outputs": [ { "internalType": "uint256", "name": "", "type": "uint256" } ], "stateMutability": "view", "type": "function" }, { "inputs": [], "name": "r1", "outputs": [ { "internalType": "uint256", "name": "", "type": "uint256" } ], "stateMutability": "view", "type": "function" }, { "inputs": [], "name": "r2", "outputs": [ { "internalType": "uint256", "name": "", "type": "uint256" } ], "stateMutability": "view", "type": "function" }, { "inputs": [], "name": "r3", "outputs": [ { "internalType": "uint256", "name": "", "type": "uint256" } ], "stateMutability": "view", "type": "function" }, { "inputs": [], "name": "x1", "outputs": [ { "internalType": "uint256", "name": "", "type": "uint256" } ], "stateMutability": "view", "type": "function" }, { "inputs": [], "name": "x2", "outputs": [ { "internalType": "uint256", "name": "", "type": "uint256" } ], "stateMutability": "view", "type": "function" }, { "inputs": [], "name": "x3", "outputs": [ { "internalType": "uint256", "name": "", "type": "uint256" } ], "stateMutability": "view", "type": "function" } ]'), {data: '0x' + '608060405234801561001057600080fd5b506104f5806100206000396000f3fe608060405234801561001057600080fd5b50600436106100cf5760003560e01c80636ca5b5b01161008c5780638bf6e410116100665780638bf6e41014610236578063a3b7887314610254578063a7ba732e14610272578063c4ee5c77146102a0576100cf565b80636ca5b5b0146101cc5780637059c7e0146101ea578063890eba6814610218576100cf565b80630bcbbd21146100d4578063343943bd146100f25780634ff135711461011057806356b15fe31461012e5780635e031f4a146101705780636c3ce6761461019e575b600080fd5b6100dc6102ec565b6040518082815260200191505060405180910390f35b6100fa6102f2565b6040518082815260200191505060405180910390f35b6101186102f8565b6040518082815260200191505060405180910390f35b61016e6004803603606081101561014457600080fd5b810190808035906020019092919080359060200190929190803590602001909291905050506102fe565b005b61019c6004803603602081101561018657600080fd5b81019080803590602001909291905050506103f5565b005b6101ca600480360360208110156101b457600080fd5b810190808035906020019092919050505061040a565b005b6101d461041f565b6040518082815260200191505060405180910390f35b6102166004803603602081101561020057600080fd5b8101908080359060200190929190505050610425565b005b61022061043a565b6040518082815260200191505060405180910390f35b61023e610440565b6040518082815260200191505060405180910390f35b61025c610446565b6040518082815260200191505060405180910390f35b61029e6004803603602081101561028857600080fd5b810190808035906020019092919050505061044c565b005b6102ea600480360360808110156102b657600080fd5b8101908080359060200190929190803590602001909291908035906020019092919080359060200190929190505050610456565b005b60025481565b60045481565b60055481565b60007155555555555555555555555555555555555590506000712aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa905060008060008460045416925083600454169150829050819250878183181891508290508192508681831818915082905081925085818318189150818318600481905550846005541692508360055416915082905081925087818318189150829050819250868183181891508290508192508581831818915081831860058190555084600654169250836006541691508290508192508781831818915082905081925086818318189150829050819250858183181891508183186006819055505050505050505050565b806000548161040057fe5b0660028190555050565b806000548161041557fe5b0660038190555050565b60015481565b806000548161043057fe5b0660018190555050565b60005481565b60035481565b60065481565b8060008190555050565b600184141561047b5780600354028260025402846001540201016004819055506104b9565b60028414156104a05780600354028260025402846001540201016005819055506104b8565b80600354028260025402846001540201016006819055505b5b5050505056fea264697066735822122035d843a487b40ebb72b85fe1e1239e8fa66574935048ffc5425538b76ad05ac964736f6c63430006010033'})).deploy().send({ from: '0x2f442DA9db20809d245a7D40DE452cd361B2dc90', gas: 1500000, gasPrice: '30000000000000' }, function(error, transactionHash){ }) .on('receipt', function(receipt){ console.log(receipt.contractAddress); }) .then(function(newContractInstance){ console.log(newContractInstance.options.address); })

而且相关文档是真的烂的可怕，Infra的API只接受Raw的transaction，非常麻烦。

关于EVM反编译，

https://ethervm.io/decompile 的结果不如 https://ropsten.etherscan.io/bytecode-decompiler

还有就是Z3并不擅长涉及求余之类的数论相关运算，要尽量避免。这次就是通过舍去两个变量让r1,r2,r3得到求解之后利用中国剩余定理的到flag再过滤.

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
from z3 import *
from functools import reduce
def chinese_remainder(n, a):
    sum = 0
    prod = reduce(lambda a, b: a*b, n)
    for n_i, a_i in zip(n, a):
        p = prod // n_i
        sum += a_i * mul_inv(p, n_i) * p
    return sum % prod



def mul_inv(a, b):
    b0 = b
    x0, x1 = 0, 1
    if b == 1: return 1
    while a > 1:
        q = a // b
        a, b = b, a%b
        x0, x1 = x1 - q * x0, x0
    if x1 < 0: x1 += b0
    return x1

#flag = BitVec('flag', 256)

s = Solver()
s.add(1 == 1)
SAT = s.check()
s = Solver()
'''
r1 = flag % 0x88c218df8c5c25674af5808d963bfee9
r2 = flag % 0xfa8cca1bced017e0ab064d4844c3020b
r3 = flag % 0xe0ac283049469716cebd61a5b97b8bef
'''
r1 = BitVec('r1', 256)
r2 = BitVec('r2', 256)
r3 = BitVec('r3', 256)

x1 = 0xd062 * r1 + 0x37b9 * r2 + 0xcc13 * r3
x2 = 0xa4fb * r1 + 0xa0a5 * r2 + 0x2fca * r3
x3 = 0x8f9b * r1 + 0x9805 * r2 + 0xa6a0 * r3
s.add(x1 == 14678491206170330851881690558556870568208252)

key1 = BitVec('key1', 256)
#key2 = BitVec('key2', 256)
#key3 = BitVec('key3', 256)

'''
temp2 = x1 & 0x2aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa
temp4 = temp2 ^ (x1 & 0x555555555555555555555555555555555555) ^ key1
temp6 = temp4 ^ temp2 ^ key2;
x1 = temp6 ^ temp6 ^ temp4 ^ key3;

temp8 = x2 & 0x2aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa;
temp9 = temp8 ^ (x2 & 0x555555555555555555555555555555555555) ^ key1;
temp10 = temp9 ^ temp8 ^ key2;
x2 = temp10 ^ temp10 ^ temp9 ^ key3;

temp11 = x3 & 0x2aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa;
temp12 = temp11 ^ (x3 & 0x555555555555555555555555555555555555) ^ key1;
temp13 = temp12 ^ temp11 ^ key2;
x3 = temp13 ^ temp13 ^ temp12 ^ key3;
'''

x1 = (x1 & 0x2aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa) ^ (x1 & 0x555555555555555555555555555555555555) ^ key1# ^ key3
x2 = (x2 & 0x2aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa) ^ (x2 & 0x555555555555555555555555555555555555) ^ key1# ^ key3
x3 = (x3 & 0x2aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa) ^ (x3 & 0x555555555555555555555555555555555555) ^ key1# ^ key3

s.add(x1 == 2357997788534811140333166336809177915724020)
s.add(x2 == 94024083436562980853861433269689272115769)
s.add(x3 == 7686765725723381031146546660250331403246417)

while s.check() == SAT:
    print(s.model())

    r11 = s.model()[r1].as_long()
    r22 = s.model()[r2].as_long()
    r33 = s.model()[r3].as_long()

    m = [0x88c218df8c5c25674af5808d963bfee9, 0xfa8cca1bced017e0ab064d4844c3020b, 0xe0ac283049469716cebd61a5b97b8bef]
    x = [r11, r22, r33]
    ff = chinese_remainder(m, x)
    LCM = 18079899862495296260944292753688576132233298796008754698177042981570096503703413266619648780022095131173540040113613
    ff %= LCM
    print(ff)
    hexy = hex(ff)[2:]
    if len(hexy) % 2 == 1:
        hexy = '0' + hexy
    if bytes.fromhex(hexy)[:4] == b'flag':
        print(bytes.fromhex(hexy))
        break
    assert(ff % m[0] == x[0] % m[0])
    assert(ff % m[1] == x[1] % m[1])
    assert(ff % m[2] == x[2] % m[2])

    s.add(And(r1 != s.model()[r1].as_long(), r2 != s.model()[r2].as_long(),r3 != s.model()[r3].as_long()))

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
N = 100
F = GF(2)

with open('output.txt') as f:
    output = f.read()
output = list(map(int, output))

R = [vector(F, N) for i in range(N)]
for i in range(N):
    for j in range(N):
        R[i][j] = output[i+j]
M = Matrix(F, R)

vec = [vector(F, 1) for i in range(N)]
for i in range(N):
    vec[i][0] = output[100+i]
N = Matrix(F, vec)

MM = M.inverse() * N

res = []
for i in range(100):
    res.append(MM[i][0])
print(int("0b" + "".join(map(str,res[::-1])), 2))

电脑被黑

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
from z3 import *

with open('flag.txt', 'rb') as f:
    cont = f.read()

LEN = len(cont)

flag = [BitVec('flag'+str(i), 8) for i in range(LEN)]

v4 = 34
v5 = 0

s = Solver()
for i in range(LEN):
    curr = flag[i]
    s.add(cont[i] == (v4 ^ (v5 + curr)))
    v4 += 34
    v5 = (v5 + 2) & 0xF

print(s.check())
print(s.model())

print("".join(map(lambda x: chr(s.model()[x].as_long()), flag)))