[Reverse] ARM - Cew

xp0int Posted on Apr 29 2021

程序需要输入key和flag，key & 0xff作为参数传递进srand，flag按字节异或一连串值，然后调用42*42次rand函数，rand函数返回的值+1 & 0xff作为系数，最后可以化简为42*42的矩阵乘以异或后的flag，求出的结果如果和output.txt的值一样就为正确解。
方法：爆破255次随机数种子，获取42*42次rand返回的值，然后用z3-solver求解，最终得到的种子是82。
```
// get 42 * 42 rand()
// gcc exp.c -o exp
#include <stdlib.h>
#include <stdio.h>

int main(){
    // if brute i = 1; i < 256; i++
    for(unsigned int i=82;i<83;i++){
        srand(i);  
        printf("%d -> ", i);
        for(int j=0;j<42*42;j++){
            printf("%d, ", (rand() + 1)&0xff);
        }
        printf("\n");
    }
}
```
```
from z3 import *
import subprocess
from subprocess import Popen
output = [775008, 736965, 579982, 832102, 739711, 689694, 621261, 786007, 687380, 870278, 671072, 705346, 695702, 726075, 693811, 726115, 797388, 839688, 798029, 773858, 732406, 632966, 740936, 775656, 710214, 858672, 686622, 608896, 815068, 521720, 693197, 560581, 885102, 635306, 732285, 770318, 702253, 632762, 839978, 813599, 651986, 875709]
s = Popen("./exp", stdout=subprocess.PIPE, stdin=subprocess.PIPE)
content = s.stdout.read().decode()
content = content.split('\n')[:-1]
#b = np.array(output)
for i in range(len(content)):
    row = content[i]
    cur = row.split(' -> ')
    key = int(cur[0])
    mat = cur[1][:-2].split(', ')
    mat = [int(_) for _ in mat]
    mat = [mat[i:i+42] for i in range(0, len(mat), 42)]
    print(len(mat), len(mat[0]))
    s = Solver()
    x = [Int("x{}".format(_)) for _ in range(42)]
    for j in range(42):
        s.add(x[j] >= 0)
        s.add(x[j] <= 255)
    for j in range(42):
        s.add(mat[j][0]*x[0]+mat[j][1]*x[1]+mat[j][2]*x[2]+mat[j][3]*x[3]+mat[j][4]*x[4]+mat[j][5]*x[5]+mat[j][6]*x[6]+mat[j][7]*x[7]+mat[j][8]*x[8]+mat[j][9]*x[9]+mat[j][10]*x[10]+mat[j][11]*x[11]+mat[j][12]*x[12]+mat[j][13]*x[13]+mat[j][14]*x[14]+mat[j][15]*x[15]+mat[j][16]*x[16]+mat[j][17]*x[17]+mat[j][18]*x[18]+mat[j][19]*x[19]+mat[j][20]*x[20]+mat[j][21]*x[21]+mat[j][22]*x[22]+mat[j][23]*x[23]+mat[j][24]*x[24]+mat[j][25]*x[25]+mat[j][26]*x[26]+mat[j][27]*x[27]+mat[j][28]*x[28]+mat[j][29]*x[29]+mat[j][30]*x[30]+mat[j][31]*x[31]+mat[j][32]*x[32]+mat[j][33]*x[33]+mat[j][34]*x[34]+mat[j][35]*x[35]+mat[j][36]*x[36]+mat[j][37]*x[37]+mat[j][38]*x[38]+mat[j][39]*x[39]+mat[j][40]*x[40]+mat[j][41]*x[41]==output[j])
    isCheck = s.check()
    print(isCheck)
    if isCheck == sat:
        print(s.model())

'''
结果
[x20 = 241, x22 = 57, x7 = 7, x9 = 63, x17 = 75, x38 = 252, x11 = 127, x2 = 219, x24 = 49, x21 = 173, x41 = 91, x18 = 96, x12 = 134, x19 = 180, x15 = 131, x27 = 9, x39 = 249, x32 = 1, x37 = 171, x13 = 5, x16 = 109, x23 = 211, x25 = 224, x8 = 239, x14 = 247, x26 = 157, x28 = 34, x10 = 97, x1 = 136, x6 = 152, x34 = 31, x35 = 17, x36 = 157, x40 = 64, x33 = 244, x31 = 199, x29 = 243, x3 = 156, x4 = 107, x5 = 228, x0 = 198, x30 = 129]
'''
x = [0]*42
x[0] = 198
x[1] = 136
x[2] = 219
x[3] = 156
x[4] = 107
x[5] = 228
x[6] = 152
x[7] = 7
x[8] = 239
x[9] = 63
x[10] = 97
x[11] = 127
x[12] = 134
x[13] = 5
x[14] = 247
x[15] = 131
x[16] = 109
x[17] = 75
x[18] = 96
x[19] = 180
x[20] = 241
x[21] = 173
x[22] = 57
x[23] = 211
x[24] = 49
x[25] = 224
x[26] = 157
x[27] = 9
x[28] = 34
x[29] = 243
x[30] = 129
x[31] = 199
x[32] = 1
x[33] = 244
x[34] = 31
x[35] = 17
x[36] = 157
x[37] = 171
x[38] = 252
x[39] = 249
x[40] = 64
x[41] = 91

key = [0xa0,0xe4,0xba,0xfb,0x10,0xdd,0xac,0x65,
0x8d,0x0b,0x57,0x1a,0xe4,0x28,0x96,0xb3,
0x0c,0x79,0x4d,0x80,0x90,0x99,0x58,0xfe,
0x50,0xd3,0xf9,0x3c,0x0f,0xc1,0xe3,0xa6,
0x39,0xc3,0x28,0x75,0xf8,0xc9,0xc8,0xcd,
0x78,0x26,0x09,0x00,0xf8,0xba]

x = [x[_] ^ key[_] for _ in range(42)]
bytes(x)
# b'flag{94bb46eb-a0a2-4a4a-a3d5-2ba877deb448}'
```
flag{94bb46eb-a0a2-4a4a-a3d5-2ba877deb448}

打赏还是打残，这是个问题