2022强网杯 ”Reverse“ WP

Reverse

1.【game】

考点

  • Android逆向分析， Android网络请求，Web数据

解法

  • 下载程序解压，发现是"ab"结尾的文件推测是安卓备份文件，用010Editor打开看一下，发现有明显的标识 ”ANDROID BACKUP“ 。

  • 直接用android-backup-extractor提取出数据

  • 提取之后发现有两个文件其中一个是apk文件直接用Jeb打开apk安装包

  • 打开Manifest清单文件找到启动Act直接双击，tab键转成Java代码

  • 根据Android生命周期可以知道onCreate是第一个启动的函数，直接找onCreate函数

  • 经过分析发现在App启动的时候会自动登录，如果登陆失败则会跳转到LoginAct，否则跳转到MainAct

  • 本想跟进autoLogin查看是如何登录的，结果发现了关键字眼函数”getFlag“

  • 那就先分析getFlag，发现需要传入三个参数然后通过发包获取Flag。根据后面的Api.class发现远程文件名

  • 文件名搞到手了，剩下的是远程服务器地址了。直接暴力搜索http，找到了远程地址

  • 根据getFlag可知，需要获取Flag就需要传入三个参数，分别是：

    • code
    • account
    • username

  • 尝试随便填看看服务器返回的结果发现不允许。

  • 发现App可以注册，直接注册一个账号再尝试发现不行

  • 猜测可能需要用到管理员的账号才可以，尝试获取管理员账号。打开App发现有个排行榜。有个名为 “admin” 的账号积分刚好是9999。根据Game页面中的提示 ”获得超过9999分能获得Flag哦!“

  • 推测应该是管理员用户名，但是getFlag需要三个参数。剩下两个参数。从刚刚的Api中可以找到一个ScoreBoard.php的请求文件并且还是GET方法。直接用Postman请求查看是否有数据在排行榜上没显示出来。

  • 发现有好几个admin， 根据排行榜显示的数据。找到排行榜best(最佳)是9999的，发现其code是”123125“

  • 第二个参数到手，第三个参数一样的方法去其他Api中看看是否能获取到。经过分析发现有个AddFriend只需要传入一个参数code即可。尝试用Postman对其发包。获取到两个参数分别是

    • account
    • username

  • 然而两个参数都加密了。

  • 分析发现在登录和注册的时候实在本地进行了数据的加密。双击到OooOoo0

  • 发现有解密操作，但再跟进OooooOOo发现其是native函数。但不影响操作

  • 直接把apk的dex2jar后需要的class保留其余全部删了。新建一个AndroidStudio工程直接把jar和so文件导入AS调用函数解密。

  • 编译后发现无法解密

  • 直接上动态调试，用工具把apk中Manifest文件中的debuggable改成true。

  • 再用Apktiool对apk反汇编成smali

1
java -jar apktool.jar d FilePath

  • 反编译后用AndroidStudio打开，定位到关键地方下断点

  • adb调试模式启动apk

  • AS对其附加


  • 待断点断下后，把刚刚AddFriend返回的两个数据分别复制

  • 按F2修改p0寄存器，按F9运行断在了String实例化后

  • 根据smali指令return-object v0得知实例化后数据放在了v0寄存器。v0寄存器就是我们需要的数据直接复制备用

  • 根据同样的方法得出username，其实不需要解密username因为刚刚的排行榜就已经显示了

  • 经过一系列的操作后得到以下数据：

    • code: 123125
    • account: &Od987$2sPa?>l<k^j
    • username: admin

  • 直接发包到GetFlag.php得到Flag

2. 【GameMaster】

考点

  • C#程序的逆向，PE文件结构，程序逻辑分析

解法

  • 用IDA打开发现是.NET架构的程序，直接使用dnSpy打开程序。找到Main函数。发现读取了一个文件

  • 读取文件字节流存放到了Program.memory全局变量里面

  • 直接点击Program，使用搜索功能全词匹配模式搜索memory，发现有两个地方使用了该变量

  • 将memory的数据异或解密存放回memory中

  • 将数据进行解密放到Program.m中

  • 将m中的数据反序列化加载

  • 根据代码中的AchivePoint推断出执行顺序，直接上c#写代码对文件进行解密

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
// See https://aka.ms/new-console-template for more information
using System.Runtime.Serialization.Formatters.Binary;
using System.Security.Cryptography;

Console.WriteLine("Hello, World!");
byte[] memory;

// Token: 0x04000002 RID: 2
byte[] m;

byte[] key = new byte[]
{
	66,
	114,
	97,
	105,
	110,
	115,
	116,
	111,
	114,
	109,
	105,
	110,
	103,
	33,
	33,
	33
};
ICryptoTransform cryptoTransform = new RijndaelManaged
{
	Key = key,
	Mode = CipherMode.ECB,
	Padding = PaddingMode.Zeros
}.CreateDecryptor();

FileStream file = File.OpenRead("gamemessage");
int len = (int)file.Length;
memory = new byte[len];

file.Position = 0;
file.Read(memory, 0, len);

m = new byte[len];

for (int i = 0; i < len; i++)
	m[i] = (byte)(memory[i] ^ 34);

m = cryptoTransform.TransformFinalBlock(m, 0, m.Length);

FileStream fileStream = File.Create("gamemessage2");

fileStream.Write(m, 0, m.Length);

  • 用010Editor查看一下文件发现有一些字符串像是可执行文件，尝试搜索MZ头看看是否是PE文件。发现确实是PE文件。把MZ头前面的数据删去保存

  • 使用dnSpy打开刚刚的文件，发现在T1中存在Flag字眼。推测这里就是Flag

  • 经过分析发现，首先是使用Check1对三个变量num,num2,num3进行编码加密写入到array2中，再用first的字节流和array2的字节流进行比对

  • 那么这里可以直接用z3得出三个变量分别是：

    • array[0] = 156324965
    • array[1] = 868387187
    • array[2] = 3131229747
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
import z3

  

first = [
    101, 5, 80, 213, 163, 26, 59, 38, 19, 6, 173, 189, 198, 166, 140, 183, 42, 247, 223, 24, 106, 20, 145, 37, 24, 7, 22, 191, 110, 179, 227, 5, 62, 9, 13, 17, 65, 22, 37, 5

]

tmp = [0] * len(first)

x = z3.BitVec("v1", 64)

y = z3.BitVec("v2", 64)

z = z3.BitVec("v3", 64)

  

num = -1

for i in range(320):

    x = (((x >> 29 ^ x >> 28 ^ x >> 25 ^ x >> 23) & 1) | x << 1)

    y = (((y >> 30 ^ y >> 27) & 1) | y << 1)

    z = (((z >> 31 ^ z >> 30 ^ z >> 29 ^ z >> 28 ^ z >> 26 ^ z >> 24) & 1) | z << 1)

    if i % 8 == 0:

        num += 1

    tmp[num] = ((tmp[num] << 1) | (

        ((z >> 32 & 1 & (x >> 30 & 1)) ^ (((z >> 32 & 1) ^ 1) & (y >> 31 & 1)))))

  

solver = z3.Solver()

for i in range(len(first)):

    solver.add(first[i] == tmp[i])

  

if solver.check() == z3.sat:

    model = solver.model()

    print(model)
   

  • 从代码中很明显发现把刚刚解密出来的三个变量经过ParseKey转换成密钥对数据进行解密

  • 计算Key

1
2
3
4
5
6
7
8
9
10
11
12
13
v = [156324965, 868387187, 3131229747]

key = [0] * 12

for i in range(3):

    for j in range(4):

        key[i * 4 + j] = (v[i] >> j * 8 & 255)

  

print(key)
  • 解密数据
1
2
3
4
5
6
7
8
9
10
11
12
  

flag = [

    60, 100, 36, 86, 51, 251, 167, 108, 116, 245, 207, 223, 40, 103, 34, 62, 22, 251, 227

]

  

for i, v in enumerate(flag):
    print(chr(v ^ key[i % len(key)]), end='')

3. 【find_basic】

考点

  • 类似虚拟保护的switch混淆执行逻辑分析

解法

  • 用IDA直接打开程序，来到start中跳转到main。

  • 发现调用了很多子程序，随便进去一个发现使用了switch结构混淆了执行的过程

  • main函数领空下个断点不断F8直到程序打印出 “basic secret”

  • 发现在调用了sub_565D84FA后程序进入了阻塞状态，因此判断该函数执行完就开始获取用户输入的数据。发现程序会发出一个时钟信号，直接忽略

  • 随便输入数据之后，程序继续断下来。断下来后打开IDA的指令跟踪功能。

  • 在下一个子程序后面下断点，直接F9运行到断点

  • 将跟踪记录导出，对其进行溯源分析

  • 发现使用了_rand产生了一个随机数后逻辑与0xFF，不断地比较。如果小于就自增一在继续判断，不断地循环直到和产生的随机数相等再推出循环。经过分析该循环体内没有需要的数据。直接修改 随机数产生后的与逻辑，patch与逻辑成异或清空数据后trace再次运行程序。

  • 但发现这样的随机不止一个，直接定位到rand函数的领空

  • 打开交叉引用

  • 分别对两个地方的调用进行断点，把 "break"去掉勾选。“condition”中填入eax = 0。

  • 这样做保证每次随机数产生后都被置0，记得要在函数调用后断点否则无效

  • 分析函数，将用户输入的数据压入堆栈中

  • 在数据的地方下个断点

  • 分析整理，根据trace发现用sub指令和数据进行了比对

  • 往后一样的操作分析，使用z3即可算出所求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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
import z3

  

result = []

  

flag = []

  

for i in range(32):

    x = z3.BitVec("%d" % i, 32)

    flag.append(x)

  

def append(model):

    for i in range(len(model)):

        result.append(model[flag[i]].as_long())

  

solver = z3.Solver()

tmp_flag = result + flag

solver.add(tmp_flag[0x00] * 0x00042b45 == 0x01a93d7e)

solver.add(tmp_flag[0x01] * 0x0003b10f + tmp_flag[0x00] * 0x0001e4e0 == 0x024fe394)

solver.add(tmp_flag[0x00] * 0x00031fc4 + tmp_flag[0x01] * 0xfffdb038 + tmp_flag[0x02] * 0x0001390f == 0x00bb9e67)

solver.add(tmp_flag[0x00] * 0x00032494 + tmp_flag[0x03] * 0xfffe5a07 + tmp_flag[0x01] * 0x0000a4e6 + tmp_flag[0x02] * 0x00006ba7 == 0x01052718)

solver.add(tmp_flag[0x01] * 0xfffe0c3f + tmp_flag[0x02] * 0x00043e32 + tmp_flag[0x00] * 0x0003f49d + tmp_flag[0x03] * 0x0000c094 + tmp_flag[0x04] * 0xfffb7eff == 0x007fb225)

solver.add(tmp_flag[0x05] * 0x00033e5b + tmp_flag[0x01] * 0x000157f8 + tmp_flag[0x04] * 0x0000d4eb + tmp_flag[0x02] * 0xfffc9ad6 + tmp_flag[0x03] * 0x00009c95 + tmp_flag[0x00] * 0xfffd8c2e == 0x0006a31d)

solver.add(tmp_flag[0x06] * 0x00006d8c + tmp_flag[0x04] * 0xfffedd66 + tmp_flag[0x05] * 0x00046fd4 + tmp_flag[0x01] * 0xfffc79bb + tmp_flag[0x03] * 0xfffbe7f5 + tmp_flag[0x02] * 0x00014cde + tmp_flag[0x00] * 0xfffc4acd + 0x03083b63 == 0)

solver.add(tmp_flag[0x04] * 0x000129fd + tmp_flag[0x07] * 0x0002a3cd + tmp_flag[0x05] * 0x000052a1 + tmp_flag[0x06] * 0x000087de + tmp_flag[0x03] * 0x000357c1 + tmp_flag[0x00] * 0xfffbe625 + tmp_flag[0x01] * 0xfffec17b + tmp_flag[0x02] * 0x00008039 == 0x00d3b6ed)

solver.add(tmp_flag[0x04] * 0xfffe590f + tmp_flag[0x06] * 0xfffc6bb7 + tmp_flag[0x00] * 0x0002aec8 + tmp_flag[0x07] * 0xfffd58b1 + tmp_flag[0x03] * 0xfffcf131 + tmp_flag[0x08] * 0xfffc0fae + tmp_flag[0x01] * 0xfffcf46a + tmp_flag[0x02] * 0xfffbbb98 + tmp_flag[0x05] * 0xfffc9913 + 0x07a4d9d3 == 0)

solver.add(tmp_flag[0x06] * 0x00003cb6 + tmp_flag[0x05] * 0xfffc5201 + tmp_flag[0x09] * 0xfffdec99 + tmp_flag[0x08] * 0x000195a8 + tmp_flag[0x04] * 0xfffbcea6 + tmp_flag[0x07] * 0xfffd4f63 + tmp_flag[0x00] * 0x0003852e + tmp_flag[0x03] * 0x00036c09 + tmp_flag[0x02] * 0xfffdffc6 + tmp_flag[0x01] * 0xffffbb8f + 0x027b7033 == 0)

solver.add(tmp_flag[0x08] * 0xfffb7a1c + tmp_flag[0x0a] * 0xffff35fe + tmp_flag[0x04] * 0xfffe5693 + tmp_flag[0x03] * 0xfffdb9f4 + tmp_flag[0x05] * 0x0000bd38 + tmp_flag[0x01] * 0x00025b89 + tmp_flag[0x02] * 0x0003074d + tmp_flag[0x07] * 0xfffe5f6f + tmp_flag[0x09] * 0x0001400e + tmp_flag[0x00] * 0xfffcd14c + tmp_flag[0x06] * 0x0004036d + 0x000a8256 == 0)

if solver.check() == z3.sat:

    append(solver.model())

  
  
  

solver = z3.Solver()

tmp_flag = result + flag

solver.add(tmp_flag[0x07] * 0x0002da7a + tmp_flag[0x02] * 0xfffbfd56 + tmp_flag[0x09] * 0xffff0011 + tmp_flag[0x00] * 0xfffce077 + tmp_flag[0x03] * 0x00034d5d + tmp_flag[0x05] * 0xfffb8def + tmp_flag[0x0a] * 0xffff2d4e + tmp_flag[0x04] * 0x000237a3 + tmp_flag[0x01] * 0x000386e1 + tmp_flag[0x06] * 0x0000fb89 + tmp_flag[0x08] * 0x0002e485 + tmp_flag[0x0b] * 0x00042574 == 0x024df62a)

if solver.check() == z3.sat:

    append(solver.model())

  
  
  

solver = z3.Solver()

tmp_flag = result + flag

solver.add(tmp_flag[0x0a] * 0x00021c5e + tmp_flag[0x01] * 0x00032144 + tmp_flag[0x0b] * 0x000420e3 + tmp_flag[0x03] * 0x0003f6d0 + tmp_flag[0x00] * 0x0001a459 + tmp_flag[0x02] * 0xfffc900e + tmp_flag[0x08] * 0x0003fd03 + tmp_flag[0x07] * 0x00043d16 + tmp_flag[0x05] * 0xfffe4105 + tmp_flag[0x06] * 0xfffd400a + tmp_flag[0x09] * 0xffffc29b + tmp_flag[0x04] * 0x0002f9f0 + tmp_flag[0x0c] * 0x00019432 == 0x06f9b293)

solver.add(tmp_flag[0x01] * 0xfffca694 + tmp_flag[0x00] * 0xfffce151 + tmp_flag[0x09] * 0x00030418 + tmp_flag[0x0b] * 0x0002f6aa + tmp_flag[0x04] * 0x0001b619 + tmp_flag[0x08] * 0x000022e4 + tmp_flag[0x07] * 0xfffe1384 + tmp_flag[0x0a] * 0xffffa664 + tmp_flag[0x03] * 0x00013e07 + tmp_flag[0x02] * 0xfffc46de + tmp_flag[0x05] * 0x000079d6 + tmp_flag[0x0c] * 0x0004372b + tmp_flag[0x0d] * 0x00003d1d + tmp_flag[0x06] * 0x00004d41 == 0x0176513c)

solver.add(tmp_flag[0x07] * 0x00029b04 + tmp_flag[0x03] * 0xfffd2684 + tmp_flag[0x02] * 0xfffd9a2f + tmp_flag[0x0a] * 0xfffd79fc + tmp_flag[0x0d] * 0x0002594e + tmp_flag[0x0c] * 0x00041c45 + tmp_flag[0x06] * 0xfffc9c57 + tmp_flag[0x05] * 0xfffc5f95 + tmp_flag[0x0b] * 0xfffec65c + tmp_flag[0x0e] * 0xffffb642 + tmp_flag[0x01] * 0xfffcb527 + tmp_flag[0x00] * 0x0002792e + tmp_flag[0x04] * 0xfffe1bb7 + tmp_flag[0x08] * 0x000445a1 + tmp_flag[0x09] * 0xfffd25cc + 0x05338cd6 == 0)

if solver.check() == z3.sat:

    append(solver.model())

  
  
  

solver = z3.Solver()

tmp_flag = result + flag

solver.add(tmp_flag[0x0e] * 0xfffd399c + tmp_flag[0x03] * 0xffff3edb + tmp_flag[0x0b] * 0x00026b94 + tmp_flag[0x0d] * 0xfffcee81 + tmp_flag[0x04] * 0xfffefe93 + tmp_flag[0x05] * 0xfffcdfa4 + tmp_flag[0x06] * 0xfffe2a42 + tmp_flag[0x00] * 0x00010ba4 + tmp_flag[0x0a] * 0x00038e1d + tmp_flag[0x0c] * 0x00014c1e + tmp_flag[0x07] * 0xffffce4a + tmp_flag[0x08] * 0xfffd2a4b + tmp_flag[0x09] * 0x000041fc + tmp_flag[0x01] * 0xfffedbac + tmp_flag[0x02] * 0xfffeab6a + tmp_flag[0x0f] * 0xfffe4e59 + 0x0299ff72 == 0)

solver.add(tmp_flag[0x0e] * 0xfffdc67b + tmp_flag[0x01] * 0xffffb1fc + tmp_flag[0x0c] * 0xffff59be + tmp_flag[0x08] * 0x00003684 + tmp_flag[0x05] * 0x000202c2 + tmp_flag[0x0a] * 0x00002e43 + tmp_flag[0x06] * 0xffff3a46 + tmp_flag[0x07] * 0x00006a23 + tmp_flag[0x02] * 0x0000ebfb + tmp_flag[0x00] * 0xfffbb78a + tmp_flag[0x0f] * 0x0000d44a + tmp_flag[0x0d] * 0x000385eb + tmp_flag[0x0b] * 0xfffee046 + tmp_flag[0x09] * 0xfffeb282 + tmp_flag[0x04] * 0xfffde639 + tmp_flag[0x03] * 0xfffd6738 + tmp_flag[0x10] * 0xffff1aa3 + 0x04728350 == 0)

solver.add(tmp_flag[0x01] * 0x00028c9c + tmp_flag[0x04] * 0xfffdc4ae + tmp_flag[0x03] * 0x000278ad + tmp_flag[0x11] * 0x000326ca + tmp_flag[0x07] * 0xfffd423d + tmp_flag[0x0f] * 0xfffc96fc + tmp_flag[0x0a] * 0xfffeeb1a + tmp_flag[0x09] * 0xfffc2ee0 + tmp_flag[0x05] * 0x000106be + tmp_flag[0x06] * 0xffff5d67 + tmp_flag[0x08] * 0x00000027 + tmp_flag[0x0b] * 0xfffbc3b6 + tmp_flag[0x0c] * 0xfffd163c + tmp_flag[0x0d] * 0xfffb9b47 + tmp_flag[0x02] * 0x0001e6ed + tmp_flag[0x00] * 0xfffc6c6f + tmp_flag[0x10] * 0x0003b32b + tmp_flag[0x0e] * 0x0002feea + 0x048d1119 == 0)

solver.add(tmp_flag[0x03] * 0xfffc2bb3 + tmp_flag[0x00] * 0xfffce76f + tmp_flag[0x04] * 0xfffca692 + tmp_flag[0x01] * 0xfffdf4bc + tmp_flag[0x0e] * 0x000192f9 + tmp_flag[0x11] * 0xfffe5a1e + tmp_flag[0x0f] * 0xfffed4f3 + tmp_flag[0x07] * 0xffff94f8 + tmp_flag[0x06] * 0xfffc717e + tmp_flag[0x09] * 0xfffed29b + tmp_flag[0x0a] * 0xfffd28d9 + tmp_flag[0x08] * 0x000218df + tmp_flag[0x02] * 0x00028e00 + tmp_flag[0x0c] * 0xfffdd0af + tmp_flag[0x0d] * 0x00025d22 + tmp_flag[0x0b] * 0x00042ebb + tmp_flag[0x05] * 0xffff1382 + tmp_flag[0x12] * 0x00007404 + tmp_flag[0x10] * 0xfffe2dff + 0x060245a5 == 0)

if solver.check() == z3.sat:

    append(solver.model())

  
  
  

solver = z3.Solver()

tmp_flag = result + flag

solver.add(tmp_flag[0x05] * 0x00021061 + tmp_flag[0x00] * 0xfffbcb01 + tmp_flag[0x13] * 0xffff7442 + tmp_flag[0x03] * 0x00024568 + tmp_flag[0x06] * 0x0001b201 + tmp_flag[0x0d] * 0x0002d232 + tmp_flag[0x0e] * 0x00013777 + tmp_flag[0x07] * 0xfffee013 + tmp_flag[0x08] * 0xfffc7505 + tmp_flag[0x02] * 0x000264ed + tmp_flag[0x01] * 0x00033b4f + tmp_flag[0x0b] * 0x000286d8 + tmp_flag[0x11] * 0x00033e8b + tmp_flag[0x0c] * 0x00021529 + tmp_flag[0x10] * 0xfffb7c1a + tmp_flag[0x12] * 0xfffd07a3 + tmp_flag[0x0a] * 0xffff8453 + tmp_flag[0x04] * 0x00009754 + tmp_flag[0x09] * 0xfffd603d + tmp_flag[0x0f] * 0xfffdd85b == 0x0254e142)

solver.add(tmp_flag[0x00] * 0xfffe206e + tmp_flag[0x0c] * 0x0002f048 + tmp_flag[0x08] * 0xfffc19fa + (tmp_flag[0x04]<<6)+tmp_flag[0x04] + tmp_flag[0x07] * 0x0000370d + tmp_flag[0x0d] * 0xfffd9c2f + tmp_flag[0x06] * 0xfffdb413 + tmp_flag[0x14] * 0x00030e0a + tmp_flag[0x12] * 0xfffe07f8 + tmp_flag[0x09] * 0xfffedfd5 + tmp_flag[0x0a] * 0xfffee6f6 + tmp_flag[0x03] * 0x00046247 + tmp_flag[0x01] * 0x0002b8ed + tmp_flag[0x10] * 0x0002d291 + tmp_flag[0x05] * 0xfffdc54d + tmp_flag[0x0f] * 0xfffc5b55 + tmp_flag[0x0e] * 0xfffb8061 + tmp_flag[0x0b] * 0x00043913 + tmp_flag[0x02] * 0xffffe191 + tmp_flag[0x11] * 0xfffd276e + tmp_flag[0x13] * 0xfffe5841 + 0x00ce53e7 == 0)

solver.add(tmp_flag[0x14] * 0xfffed971 + tmp_flag[0x15] * 0x00046741 + tmp_flag[0x12] * 0xfffbac8c + tmp_flag[0x01] * 0xfffeb4e7 + tmp_flag[0x0d] * 0x0001026b + tmp_flag[0x0c] * 0xfffe7d86 + tmp_flag[0x06] * 0xfffd5fec + tmp_flag[0x03] * 0x00048ddb + tmp_flag[0x10] * 0xfffc6bc1 + tmp_flag[0x11] * 0x00037ece + tmp_flag[0x08] * 0x00041105 + tmp_flag[0x02] * 0xfffe6667 + tmp_flag[0x13] * 0xfffe75b2 + tmp_flag[0x04] * 0x000061b0 + tmp_flag[0x0e] * 0xffffd602 + tmp_flag[0x0b] * 0xfffbce29 + tmp_flag[0x00] * 0xffff07d7 + tmp_flag[0x05] * 0x00034c8e + tmp_flag[0x0f] * 0x00032996 + tmp_flag[0x0a] * 0x00049530 + tmp_flag[0x07] * 0x00033822 + tmp_flag[0x09] * 0xfffce161 + 0x0042666b == 0)

solver.add(tmp_flag[0x08] * 0xfffe06e8 + tmp_flag[0x0c] * 0xfffd0441 + tmp_flag[0x02] * 0x00016357 + tmp_flag[0x03] * 0x0001d95f + tmp_flag[0x16] * 0xffff89d3 + tmp_flag[0x01] * 0xfffba022 + tmp_flag[0x10] * 0x00046180 + tmp_flag[0x04] * 0xffff4240 + tmp_flag[0x05] * 0x000199c5 + tmp_flag[0x15] * 0xffff442c + tmp_flag[0x11] * 0xfffc2fac + tmp_flag[0x0a] * 0x00032600 + tmp_flag[0x13] * 0x0001d03a + tmp_flag[0x09] * 0x00019435 + tmp_flag[0x0f] * 0xfffd1667 + tmp_flag[0x12] * 0x00035d1d + tmp_flag[0x00] * 0x000096c4 + tmp_flag[0x0b] * 0x0002fa24 + tmp_flag[0x07] * 0x0000b20c + tmp_flag[0x06] * 0x0000ebee + tmp_flag[0x14] * 0x000428a6 + tmp_flag[0x0e] * 0xfffceb8a + tmp_flag[0x0d] * 0x00022784 == 0x03604a63)

solver.add(tmp_flag[0x00] * 0x0001e3e2 + tmp_flag[0x09] * 0x0001cfb9 + tmp_flag[0x06] * 0x0000c3f7 + tmp_flag[0x0a] * 0x000094cd + tmp_flag[0x16] * 0xfffc7fd0 + tmp_flag[0x02] * 0x00021165 + tmp_flag[0x17] * 0xfffcfb41 + tmp_flag[0x0e] * 0xffff819d + tmp_flag[0x05] * 0xfffbeb76 + tmp_flag[0x01] * 0x00016751 + tmp_flag[0x13] * 0x00000e1a + tmp_flag[0x11] * 0x000238a0 + tmp_flag[0x0c] * 0x00028f99 + tmp_flag[0x08] * 0x000045bc + tmp_flag[0x14] * 0xffffcb18 + tmp_flag[0x0f] * 0x00032d58 + tmp_flag[0x0b] * 0xffffe4bc + tmp_flag[0x10] * 0xfffeea95 + tmp_flag[0x0d] * 0x00044f3a + tmp_flag[0x12] * 0x0000b047 + tmp_flag[0x07] * 0xfffcfc36 + tmp_flag[0x15] * 0x00001719 + tmp_flag[0x04] * 0x0001b011 + tmp_flag[0x03] * 0xfffea265 == 0x02918269)

if solver.check() == z3.sat:

    append(solver.model())

  
  
  

solver = z3.Solver()

tmp_flag = result + flag

solver.add(tmp_flag[0x0f] * 0xfffbf307 + tmp_flag[0x08] * 0xffff2847 + tmp_flag[0x06] * 0xfffcfd31 + tmp_flag[0x02] * 0x00040f96 + tmp_flag[0x16] * 0x0002b265 + tmp_flag[0x05] * 0xfffc7802 + tmp_flag[0x03] * 0x0001b103 + tmp_flag[0x04] * 0x00042452 + tmp_flag[0x0e] * 0x00003c5d + tmp_flag[0x01] * 0x00015b55 + tmp_flag[0x09] * 0xfffeb722 + tmp_flag[0x0d] * 0x0001d9a9 + tmp_flag[0x17] * 0x000028df + tmp_flag[0x0c] * 0xfffc89eb + tmp_flag[0x0a] * 0xfffe1221 + tmp_flag[0x07] * 0x0004462a + tmp_flag[0x13] * 0x00023353 + tmp_flag[0x15] * 0x0003c514 + tmp_flag[0x00] * 0x000316a4 + tmp_flag[0x0b] * 0x000176e1 + tmp_flag[0x14] * 0x0000cf0e + tmp_flag[0x12] * 0x00046b55 + tmp_flag[0x18] * 0xffffbcc1 + tmp_flag[0x11] * 0x0000f2a7 + tmp_flag[0x10] * 0x0001d33c == 0x05df35b6)

solver.add(tmp_flag[0x03] * 0xfffbf624 + tmp_flag[0x16] * 0xfffec87a + tmp_flag[0x02] * 0x00019aaa + tmp_flag[0x17] * 0x00005f14 + tmp_flag[0x14] * 0xfffcfc43 + tmp_flag[0x10] * 0xfffbe879 + tmp_flag[0x0f] * 0xfffdfc92 + tmp_flag[0x0e] * 0xffffc258 + tmp_flag[0x00] * 0xfffd02fd + tmp_flag[0x05] * 0x00012560 + tmp_flag[0x0d] * 0x0000ae46 + tmp_flag[0x07] * 0xfffeb6f5 + tmp_flag[0x0c] * 0x00030c11 + tmp_flag[0x11] * 0xfffcb4ae + tmp_flag[0x18] * 0x0002a00a + tmp_flag[0x06] * 0xfffc76de + tmp_flag[0x15] * 0x00004162 + tmp_flag[0x0a] * 0xfffe95b2 + tmp_flag[0x19] * 0xfffe60e7 + tmp_flag[0x13] * 0xffff908d + tmp_flag[0x04] * 0xfffb7f42 + tmp_flag[0x0b] * 0x00001c31 + tmp_flag[0x01] * 0xffff900c + tmp_flag[0x08] * 0x0002ad6e + tmp_flag[0x09] * 0xfffd7c6d + tmp_flag[0x12] * 0x0000c499 + 0x083646cd == 0)

solver.add(tmp_flag[0x0c] * 0x00026b02 + tmp_flag[0x03] * 0xfffb92e5 + tmp_flag[0x11] * 0x00030dd1 + tmp_flag[0x12] * 0xfffe4c7b + tmp_flag[0x00] * 0xffff0433 + tmp_flag[0x01] * 0x000276b1 + tmp_flag[0x09] * 0xfffc241e + tmp_flag[0x05] * 0xfffe3fdc + tmp_flag[0x08] * 0xfffee787 + tmp_flag[0x0a] * 0x0000230c + tmp_flag[0x15] * 0xfffd53f8 + tmp_flag[0x04] * 0xfffc108c + tmp_flag[0x0e] * 0xffffbac1 + tmp_flag[0x1a] * 0xffff0bdb + tmp_flag[0x0f] * 0xfffbc5e2 + tmp_flag[0x13] * 0x0000a1f6 + tmp_flag[0x10] * 0x0001e758 + tmp_flag[0x16] * 0x0001725f + tmp_flag[0x17] * 0x0003387e + tmp_flag[0x14] * 0x0000087b + tmp_flag[0x02] * 0xfffd8475 + tmp_flag[0x0d] * 0x0003776a + tmp_flag[0x18] * 0xffff4515 + tmp_flag[0x0b] * 0x0001a454 + tmp_flag[0x06] * 0xfffbf3a1 + tmp_flag[0x19] * 0x00025174 + tmp_flag[0x07] * 0xfffbccc2 + 0x052dfb3f == 0)

solver.add(tmp_flag[0x19] * 0x0002f139 + tmp_flag[0x14] * 0x00021b53 + tmp_flag[0x0f] * 0x0002ad74 + tmp_flag[0x09] * 0xfffba19b + tmp_flag[0x10] * 0x0001ac4e + tmp_flag[0x1b] * 0x0002208e + tmp_flag[0x0d] * 0xfffdd738 + tmp_flag[0x0b] * 0xfffdfb9f + tmp_flag[0x08] * 0xfffe4b65 + tmp_flag[0x05] * 0x00010937 + tmp_flag[0x0a] * 0xfffbfdf3 + tmp_flag[0x0c] * 0x0003cc1a + tmp_flag[0x17] * 0xfffe93ee + tmp_flag[0x02] * 0xfffe3b8a + tmp_flag[0x0e] * 0xfffe792c + tmp_flag[0x06] * 0x0003e9ff + tmp_flag[0x15] * 0x000128e6 + tmp_flag[0x03] * 0x0000574b + tmp_flag[0x18] * 0x00016707 + tmp_flag[0x13] * 0x0003fe4c + tmp_flag[0x11] * 0xfffed658 + tmp_flag[0x07] * 0x0003cc8c + tmp_flag[0x16] * 0x000458b4 + tmp_flag[0x01] * 0xfffd74d0 + tmp_flag[0x12] * 0x00022e02 + tmp_flag[0x04] * 0xffff098d + tmp_flag[0x00] * 0x00030b99 + tmp_flag[0x1a] * 0xfffba5e9 == 0x038186f4)

if solver.check() == z3.sat:

    append(solver.model())

  
  
  

print("".join([chr(i) for i in result]))