忙了半天，就肝了两个Re，其中一个还是比赛结束后才出的，菜的令人发指，呜呜呜！！！
1、Fantasyapk逆向，查了一下，没有加固，直接在 jadx-gui 当中打开，可以看到核心算法都在Java层，这就比较舒服：
在check函数当中，wow 、ahhhhh 分别是一个 32 x 32 、 32 x 1 的数组，至于后面的校验算法，看着唬人，一番化简之后就没什么了：
public int check(String to_check) {
int[][] wow = {
new int[]{89, 88, 60, 91, 74, 111, 84, 96, 111, 124, 102, 95, 106, 126, 80, 122, 55, 125, 57, 32, 61, 96, 98, 106, 36, 113, 79, 86, 43, 71, 91, 117},
new int[]{100, 113, 38, 112, 78, 74, 44, 64, 37, 81, 40, 35, 78, 41, 46, 54, 82, 92, 46, 64, 73, 45, 43, 120, 58, 127, 123, 53, 58, 112, 37, 119},
new int[]{96, 53, 32, 75, 113, 62, 37, 65, 69, 76, 118, 97, 33, 121, 63, 87, 78, 113, 103, 88, 50, 60, 92, 53, 50, 60, 45, 121, 41, 69, 84, 122},
new int[]{82, 125, 67, 38, 112, 121, 118, 74, 48, 37, 108, 42, 59, 112, 85, 41, 103, 75, 34, 89, 37, 74, 124, 40, 62, 36, 114, 127, 91, 51, 110, 63},
new int[]{99, 35, 49, 36, 108, 56, 36, 70, 80, 78, 114, 76, 73, 78, 104, 56, 48, 47, 69, 62, 97, 47, 74, 62, 39, 90, 97, 56, 114, 90, 47, 111},
new int[]{117, 87, 70, 32, 110, 43, 60, 127, 114, 119, 117, 71, 59, 90, 55, 72, 46, 48, 63, 66, 110, 108, 111, 35, 43, 113, 124, 91, 45, 81, 64, 67},
new int[]{64, 114, 50, 54, 94, 60, 127, 81, 92, 101, 78, 91, 68, 72, 95, 92, 48, 91, 34, 37, 77, 62, 74, 122, 75, 37, 127, 66, 90, 86, 67, 115},
new int[]{77, 80, 71, 61, 124, 79, 124, 111, 109, 121, 119, 52, 82, 100, 109, 57, 76, 99, 61, 37, 94, 113, 49, 72, 84, 96, 88, 106, 55, 123, 63, 57},
new int[]{90, 73, 75, 44, 104, 111, 78, 53, 82, 97, 76, 33, 92, 73, 113, 124, 101, 57, 94, 34, 76, 103, 48, 79, 74, 58, 76, 86, 65, 83, 89, 81},
new int[]{78, 100, 109, 36, 83, 98, 109, 98, 39, 73, 61, 94, 32, 107, 59, 84, 100, 86, 95, 43, 75, 78, 70, 73, 85, 99, 121, 91, 116, 65, 78, 64},
new int[]{110, 109, 98, 40, 77, 57, 105, 75, 111, 51, 49, 36, 82, 42, 38, 95, 97, 81, 47, 93, 100, 52, 75, 65, 68, 110, 90, 46, 73, 113, 36, 98},
new int[]{77, 77, 126, 126, 107, 63, 108, 38, 103, 86, 79, 101, 117, 41, 117, 115, 61, 47, 100, 93, 89, 36, 111, 116, 87, 96, 125, 82, 88, 84, 68, 100},
new int[]{57, 53, 84, 116, 104, 127, 48, 115, 99, 124, 70, 92, 101, 120, 39, 125, 60, 127, 45, 76, 66, 66, 78, 71, 114, 104, 61, 33, 95, 123, 75, 75},
new int[]{44, 120, 39, 117, 58, 65, 52, 91, 62, 57, 89, 43, 79, 39, 55, 42, 88, 92, 37, 47, 88, 44, 34, 97, 38, 67, 109, 40, 92, 101, 33, 100},
new int[]{51, 86, 114, 62, 44, 42, 83, 120, 73, 113, 99, 39, 112, 92, 34, 120, 58, 110, 56, 81, 75, 88, 53, 116, 102, 126, 112, 40, 72, 64, 76, 52},
new int[]{110, 34, 95, 67, 35, 56, 38, 84, 124, 103, 49, 70, 105, 122, 125, 38, 97, 71, 49, 122, 104, 126, 112, 113, 65, 70, 80, 105, 97, 74, 123, 46},
new int[]{87, 58, 49, 63, 86, 95, 111, 85, 75, 40, 63, 86, 43, 117, 66, 54, 92, 118, 76, 68, 40, 97, 102, 81, 117, 55, 34, 86, 70, 86, 84, 64},
new int[]{40, 87, 88, 72, 55, 116, 112, 52, 70, 80, 34, 49, 125, 65, 33, 106, 121, 111, 100, 116, 119, 36, 116, 66, 36, 72, 96, 82, 32, 87, 114, 115},
new int[]{34, 43, 121, 56, 88, 116, 75, 90, 92, 110, 89, 115, 115, 103, 100, 72, 42, 84, 116, 40, 115, 84, 68, 125, 92, 37, 47, 116, 110, 40, 124, 38},
new int[]{33, 93, 39, 44, 69, 54, 86, 59, 80, 92, 35, 45, 103, 96, 51, 111, 58, 79, 51, 124, 45, 59, 121, 36, 46, 114, 41, 34, 110, 100, 65, 41},
new int[]{71, 70, 106, 46, 51, 66, 66, 78, 100, 102, 55, 42, 88, 113, 33, 51, 65, 73, 127, 117, 108, 84, 121, 110, 123, 101, 40, 57, 63, 113, 90, 100},
new int[]{72, 86, 41, 125, 49, 67, 63, 127, 52, 106, 77, 49, 63, 70, 84, 87, 99, 63, 39, 122, 105, 62, 46, 123, 108, 127, 40, 89, 83, 79, 48, 62},
new int[]{49, 83, 46, 113, 119, 39, 109, 96, 101, 73, 82, 124, 109, 93, 48, 82, 96, 126, 105, 37, 90, 86, 116, 115, 53, 32, 106, 92, 33, 53, 119, 68},
new int[]{67, 105, 109, 65, 36, 64, 33, 119, 116, 35, 61, 55, 70, 117, 120, 105, 98, 37, 83, 64, 88, 119, 55, 33, 56, 44, 46, 84, 86, 49, 78, 93},
new int[]{34, 97, 100, 33, 71, 109, 71, 93, 104, 39, 70, 53, 96, 109, 119, 73, 58, 111, 122, 125, 91, 66, 70, 75, 43, 42, 48, 85, 62, 97, 94, 97},
new int[]{119, 96, 75, 59, 115, 33, 99, 51, 56, 49, 84, 45, 112, 60, 87, 117, 66, 106, 113, 59, 105, 40, 94, 87, 93, 64, 52, 39, 109, 93, 120, 33},
new int[]{115, 113, 50, 95, 42, 88, 119, 59, 86, 127, 79, 89, 107, 45, 64, 112, 68, 102, 45, 39, 63, 95, 35, 119, 38, 110, 43, 56, 67, 124, 106, 125},
new int[]{78, 83, 98, 86, 50, 68, 73, 52, 49, 97, 60, 84, 54, 118, 91, 100, 44, 97, 97, 96, 127, 79, 94, 77, 76, 118, 49, 111, 87, 125, 73, 77},
new int[]{103, 45, 119, 36, 94, 99, 81, 35, 97, 51, 107, 110, 120, 71, 64, 88, 83, 33, 120, 89, 114, 36, 110, 80, 85, 40, 105, 37, 66, 73, 91, 59},
new int[]{122, 56, 111, 52, 33, 118, 89, 105, 61, 117, 60, 123, 125, 52, 63, 57, 124, 109, 64, 47, 52, 98, 96, 60, 86, 45, 51, 86, 123, 70, 104, 110},
new int[]{51, 127, 85, 43, 79, 44, 118, 89, 78, 95, 87, 103, 33, 44, 102, 100, 40, 40, 55, 58, 43, 76, 115, 81, 68, 123, 69, 48, 66, 74, 83, 119},
new int[]{79, 55, 88, 105, 81, 104, 105, 100, 46, 34, 87, 68, 36, 74, 48, 70, 57, 39, 125, 80, 102, 61, 127, 82, 90, 85, 120, 35, 126, 60, 105, 104}
};
int[] ahhhhh = {
195075, 164766, 168447, 176014, 161107, 175809, 178310, 189827, 181204, 182314, 168177, 196996, 185129, 152876, 171067, 185573,
166900, 184588, 182162, 148593, 180204, 169933, 182766, 166651, 178856, 175376, 187367, 182885, 177145, 189716, 169531, 178924
};
int ohh = 0;
for ( ohh = 0; ohh < 32; ohh++) {
int thats = 0;
for (int gooood = 0; gooood < 32; gooood++) {
int its = to_check.charAt(gooood) & 255;
thats = its*wow[ohh][gooood];
}
if (ahhhhh[ohh] != thats) {
break;
}
}
return ohh;
}
到这里就含明显了，就是一个32元一次方程组，flag 分别与 wow 中的每一行元素逐位相乘并累加，结果要与ahhhhh当中的值一致，用 z3 把结果跑出来就有flag了：
# -*- coding: utf-8 -*-
"""
Spyder Editor
This is a temporary script file.
"""
from z3 import *
v1 = Int('v1')
v2 = Int('v2')
v3 = Int('v3')
v4 = Int('v4')
v5 = Int('v5')
v6 = Int('v6')
v7 = Int('v7')
v8 = Int('v8')
v9 = Int('v9')
v10 = Int('v10')
v11 = Int('v11')
v12 = Int('v12')
v13 = Int('v13')
v14 = Int('v14')
v15 = Int('v15')
v16 = Int('v16')
v17 = Int('v17')
v18 = Int('v18')
v19 = Int('v19')
v20 = Int('v20')
v21 = Int('v21')
v22 = Int('v22')
v23 = Int('v23')
v24 = Int('v24')
v25 = Int('v25')
v26 = Int('v26')
v27 = Int('v27')
v28 = Int('v28')
v29 = Int('v29')
v30 = Int('v30')
v31 = Int('v31')
v32 = Int('v32')
cha = ["v1","v2","v3","v4","v5","v6","v7","v8","v9","v10","v11","v12","v13","v14","v15","v16","v17","v18","v19","v20","v21","v22","v23","v24","v25","v26","v27","v28","v29","v30","v31","v32"]
s = Solver()
s.add(89 * v1 + 88 * v2 + 60 * v3 + 91 * v4 + 74 * v5 + 111 * v6 + 84 * v7 + 96 * v8 + 111 * v9 + 124 * v10 + 102 * v11 + 95 * v12 + 106 * v13 + 126 * v14 + 80 * v15 + 122 * v16 + 55 * v17 + 125 * v18 + 57 * v19 + 32 * v20 + 61 * v21 + 96 * v22 + 98 * v23 + 106 * v24 + 36 * v25 + 113 * v26 + 79 * v27 + 86 * v28 + 43 * v29 + 71 * v30 + 91 * v31 + 117 * v32 == 195075)
s.add(100 * v1 + 113 * v2 + 38 * v3 + 112 * v4 + 78 * v5 + 74 * v6 + 44 * v7 + 64 * v8 + 37 * v9 + 81 * v10 + 40 * v11 + 35 * v12 + 78 * v13 + 41 * v14 + 46 * v15 + 54 * v16 + 82 * v17 + 92 * v18 + 46 * v19 + 64 * v20 + 73 * v21 + 45 * v22 + 43 * v23 + 120 * v24 + 58 * v25 + 127 * v26 + 123 * v27 + 53 * v28 + 58 * v29 + 112 * v30 + 37 * v31 + 119 * v32 == 164766)
s.add(96 * v1 + 53 * v2 + 32 * v3 + 75 * v4 + 113 * v5 + 62 * v6 + 37 * v7 + 65 * v8 + 69 * v9 + 76 * v10 + 118 * v11 + 97 * v12 + 33 * v13 + 121 * v14 + 63 * v15 + 87 * v16 + 78 * v17 + 113 * v18 + 103 * v19 + 88 * v20 + 50 * v21 + 60 * v22 + 92 * v23 + 53 * v24 + 50 * v25 + 60 * v26 + 45 * v27 + 121 * v28 + 41 * v29 + 69 * v30 + 84 * v31 + 122 * v32 == 168447)
s.add(82 * v1 + 125 * v2 + 67 * v3 + 38 * v4 + 112 * v5 + 121 * v6 + 118 * v7 + 74 * v8 + 48 * v9 + 37 * v10 + 108 * v11 + 42 * v12 + 59 * v13 + 112 * v14 + 85 * v15 + 41 * v16 + 103 * v17 + 75 * v18 + 34 * v19 + 89 * v20 + 37 * v21 + 74 * v22 + 124 * v23 + 40 * v24 + 62 * v25 + 36 * v26 + 114 * v27 + 127 * v28 + 91 * v29 + 51 * v30 + 110 * v31 + 63 * v32 == 176014)
s.add(99 * v1 + 35 * v2 + 49 * v3 + 36 * v4 + 108 * v5 + 56 * v6 + 36 * v7 + 70 * v8 + 80 * v9 + 78 * v10 + 114 * v11 + 76 * v12 + 73 * v13 + 78 * v14 + 104 * v15 + 56 * v16 + 48 * v17 + 47 * v18 + 69 * v19 + 62 * v20 + 97 * v21 + 47 * v22 + 74 * v23 + 62 * v24 + 39 * v25 + 90 * v26 + 97 * v27 + 56 * v28 + 114 * v29 + 90 * v30 + 47 * v31 + 111 * v32 == 161107)
s.add(117 * v1 + 87 * v2 + 70 * v3 + 32 * v4 + 110 * v5 + 43 * v6 + 60 * v7 + 127 * v8 + 114 * v9 + 119 * v10 + 117 * v11 + 71 * v12 + 59 * v13 + 90 * v14 + 55 * v15 + 72 * v16 + 46 * v17 + 48 * v18 + 63 * v19 + 66 * v20 + 110 * v21 + 108 * v22 + 111 * v23 + 35 * v24 + 43 * v25 + 113 * v26 + 124 * v27 + 91 * v28 + 45 * v29 + 81 * v30 + 64 * v31 + 67 * v32 == 175809)
s.add(64 * v1 + 114 * v2 + 50 * v3 + 54 * v4 + 94 * v5 + 60 * v6 + 127 * v7 + 81 * v8 + 92 * v9 + 101 * v10 + 78 * v11 + 91 * v12 + 68 * v13 + 72 * v14 + 95 * v15 + 92 * v16 + 48 * v17 + 91 * v18 + 34 * v19 + 37 * v20 + 77 * v21 + 62 * v22 + 74 * v23 + 122 * v24 + 75 * v25 + 37 * v26 + 127 * v27 + 66 * v28 + 90 * v29 + 86 * v30 + 67 * v31 + 115 * v32 == 178310)
s.add(77 * v1 + 80 * v2 + 71 * v3 + 61 * v4 + 124 * v5 + 79 * v6 + 124 * v7 + 111 * v8 + 109 * v9 + 121 * v10 + 119 * v11 + 52 * v12 + 82 * v13 + 100 * v14 + 109 * v15 + 57 * v16 + 76 * v17 + 99 * v18 + 61 * v19 + 37 * v20 + 94 * v21 + 113 * v22 + 49 * v23 + 72 * v24 + 84 * v25 + 96 * v26 + 88 * v27 + 106 * v28 + 55 * v29 + 123 * v30 + 63 * v31 + 57 * v32 == 189827)
s.add(90 * v1 + 73 * v2 + 75 * v3 + 44 * v4 + 104 * v5 + 111 * v6 + 78 * v7 + 53 * v8 + 82 * v9 + 97 * v10 + 76 * v11 + 33 * v12 + 92 * v13 + 73 * v14 + 113 * v15 + 124 * v16 + 101 * v17 + 57 * v18 + 94 * v19 + 34 * v20 + 76 * v21 + 103 * v22 + 48 * v23 + 79 * v24 + 74 * v25 + 58 * v26 + 76 * v27 + 86 * v28 + 65 * v29 + 83 * v30 + 89 * v31 + 81 * v32 == 181204)
s.add(78 * v1 + 100 * v2 + 109 * v3 + 36 * v4 + 83 * v5 + 98 * v6 + 109 * v7 + 98 * v8 + 39 * v9 + 73 * v10 + 61 * v11 + 94 * v12 + 32 * v13 + 107 * v14 + 59 * v15 + 84 * v16 + 100 * v17 + 86 * v18 + 95 * v19 + 43 * v20 + 75 * v21 + 78 * v22 + 70 * v23 + 73 * v24 + 85 * v25 + 99 * v26 + 121 * v27 + 91 * v28 + 116 * v29 + 65 * v30 + 78 * v31 + 64 * v32 == 182314)
s.add(110 * v1 + 109 * v2 + 98 * v3 + 40 * v4 + 77 * v5 + 57 * v6 + 105 * v7 + 75 * v8 + 111 * v9 + 51 * v10 + 49 * v11 + 36 * v12 + 82 * v13 + 42 * v14 + 38 * v15 + 95 * v16 + 97 * v17 + 81 * v18 + 47 * v19 + 93 * v20 + 100 * v21 + 52 * v22 + 75 * v23 + 65 * v24 + 68 * v25 + 110 * v26 + 90 * v27 + 46 * v28 + 73 * v29 + 113 * v30 + 36 * v31 + 98 * v32 == 168177)
s.add(77 * v1 + 77 * v2 + 126 * v3 + 126 * v4 + 107 * v5 + 63 * v6 + 108 * v7 + 38 * v8 + 103 * v9 + 86 * v10 + 79 * v11 + 101 * v12 + 117 * v13 + 41 * v14 + 117 * v15 + 115 * v16 + 61 * v17 + 47 * v18 + 100 * v19 + 93 * v20 + 89 * v21 + 36 * v22 + 111 * v23 + 116 * v24 + 87 * v25 + 96 * v26 + 125 * v27 + 82 * v28 + 88 * v29 + 84 * v30 + 68 * v31 + 100 * v32 == 196996)
s.add(57 * v1 + 53 * v2 + 84 * v3 + 116 * v4 + 104 * v5 + 127 * v6 + 48 * v7 + 115 * v8 + 99 * v9 + 124 * v10 + 70 * v11 + 92 * v12 + 101 * v13 + 120 * v14 + 39 * v15 + 125 * v16 + 60 * v17 + 127 * v18 + 45 * v19 + 76 * v20 + 66 * v21 + 66 * v22 + 78 * v23 + 71 * v24 + 114 * v25 + 104 * v26 + 61 * v27 + 33 * v28 + 95 * v29 + 123 * v30 + 75 * v31 + 75 * v32 == 185129)
s.add(44 * v1 + 120 * v2 + 39 * v3 + 117 * v4 + 58 * v5 + 65 * v6 + 52 * v7 + 91 * v8 + 62 * v9 + 57 * v10 + 89 * v11 + 43 * v12 + 79 * v13 + 39 * v14 + 55 * v15 + 42 * v16 + 88 * v17 + 92 * v18 + 37 * v19 + 47 * v20 + 88 * v21 + 44 * v22 + 34 * v23 + 97 * v24 + 38 * v25 + 67 * v26 + 109 * v27 + 40 * v28 + 92 * v29 + 101 * v30 + 33 * v31 + 100 * v32 == 152876)
s.add(51 * v1 + 86 * v2 + 114 * v3 + 62 * v4 + 44 * v5 + 42 * v6 + 83 * v7 + 120 * v8 + 73 * v9 + 113 * v10 + 99 * v11 + 39 * v12 + 112 * v13 + 92 * v14 + 34 * v15 + 120 * v16 + 58 * v17 + 110 * v18 + 56 * v19 + 81 * v20 + 75 * v21 + 88 * v22 + 53 * v23 + 116 * v24 + 102 * v25 + 126 * v26 + 112 * v27 + 40 * v28 + 72 * v29 + 64 * v30 + 76 * v31 + 52 * v32 == 171067)
s.add(110 * v1 + 34 * v2 + 95 * v3 + 67 * v4 + 35 * v5 + 56 * v6 + 38 * v7 + 84 * v8 + 124 * v9 + 103 * v10 + 49 * v11 + 70 * v12 + 105 * v13 + 122 * v14 + 125 * v15 + 38 * v16 + 97 * v17 + 71 * v18 + 49 * v19 + 122 * v20 + 104 * v21 + 126 * v22 + 112 * v23 + 113 * v24 + 65 * v25 + 70 * v26 + 80 * v27 + 105 * v28 + 97 * v29 + 74 * v30 + 123 * v31 + 46 * v32 == 185573)
s.add(87 * v1 + 58 * v2 + 49 * v3 + 63 * v4 + 86 * v5 + 95 * v6 + 111 * v7 + 85 * v8 + 75 * v9 + 40 * v10 + 63 * v11 + 86 * v12 + 43 * v13 + 117 * v14 + 66 * v15 + 54 * v16 + 92 * v17 + 118 * v18 + 76 * v19 + 68 * v20 + 40 * v21 + 97 * v22 + 102 * v23 + 81 * v24 + 117 * v25 + 55 * v26 + 34 * v27 + 86 * v28 + 70 * v29 + 86 * v30 + 84 * v31 + 64 * v32 == 166900)
s.add(40 * v1 + 87 * v2 + 88 * v3 + 72 * v4 + 55 * v5 + 116 * v6 + 112 * v7 + 52 * v8 + 70 * v9 + 80 * v10 + 34 * v11 + 49 * v12 + 125 * v13 + 65 * v14 + 33 * v15 + 106 * v16 + 121 * v17 + 111 * v18 + 100 * v19 + 116 * v20 + 119 * v21 + 36 * v22 + 116 * v23 + 66 * v24 + 36 * v25 + 72 * v26 + 96 * v27 + 82 * v28 + 32 * v29 + 87 * v30 + 114 * v31 + 115 * v32 == 184588)
s.add(34 * v1 + 43 * v2 + 121 * v3 + 56 * v4 + 88 * v5 + 116 * v6 + 75 * v7 + 90 * v8 + 92 * v9 + 110 * v10 + 89 * v11 + 115 * v12 + 115 * v13 + 103 * v14 + 100 * v15 + 72 * v16 + 42 * v17 + 84 * v18 + 116 * v19 + 40 * v20 + 115 * v21 + 84 * v22 + 68 * v23 + 125 * v24 + 92 * v25 + 37 * v26 + 47 * v27 + 116 * v28 + 110 * v29 + 40 * v30 + 124 * v31 + 38 * v32 == 182162)
s.add(33 * v1 + 93 * v2 + 39 * v3 + 44 * v4 + 69 * v5 + 54 * v6 + 86 * v7 + 59 * v8 + 80 * v9 + 92 * v10 + 35 * v11 + 45 * v12 + 103 * v13 + 96 * v14 + 51 * v15 + 111 * v16 + 58 * v17 + 79 * v18 + 51 * v19 + 124 * v20 + 45 * v21 + 59 * v22 + 121 * v23 + 36 * v24 + 46 * v25 + 114 * v26 + 41 * v27 + 34 * v28 + 110 * v29 + 100 * v30 + 65 * v31 + 41 * v32 == 148593)
s.add(71 * v1 + 70 * v2 + 106 * v3 + 46 * v4 + 51 * v5 + 66 * v6 + 66 * v7 + 78 * v8 + 100 * v9 + 102 * v10 + 55 * v11 + 42 * v12 + 88 * v13 + 113 * v14 + 33 * v15 + 51 * v16 + 65 * v17 + 73 * v18 + 127 * v19 + 117 * v20 + 108 * v21 + 84 * v22 + 121 * v23 + 110 * v24 + 123 * v25 + 101 * v26 + 40 * v27 + 57 * v28 + 63 * v29 + 113 * v30 + 90 * v31 + 100 * v32 == 180204)
s.add(72 * v1 + 86 * v2 + 41 * v3 + 125 * v4 + 49 * v5 + 67 * v6 + 63 * v7 + 127 * v8 + 52 * v9 + 106 * v10 + 77 * v11 + 49 * v12 + 63 * v13 + 70 * v14 + 84 * v15 + 87 * v16 + 99 * v17 + 63 * v18 + 39 * v19 + 122 * v20 + 105 * v21 + 62 * v22 + 46 * v23 + 123 * v24 + 108 * v25 + 127 * v26 + 40 * v27 + 89 * v28 + 83 * v29 + 79 * v30 + 48 * v31 + 62 * v32 == 169933)
s.add(49 * v1 + 83 * v2 + 46 * v3 + 113 * v4 + 119 * v5 + 39 * v6 + 109 * v7 + 96 * v8 + 101 * v9 + 73 * v10 + 82 * v11 + 124 * v12 + 109 * v13 + 93 * v14 + 48 * v15 + 82 * v16 + 96 * v17 + 126 * v18 + 105 * v19 + 37 * v20 + 90 * v21 + 86 * v22 + 116 * v23 + 115 * v24 + 53 * v25 + 32 * v26 + 106 * v27 + 92 * v28 + 33 * v29 + 53 * v30 + 119 * v31 + 68 * v32 == 182766)
s.add(67 * v1 + 105 * v2 + 109 * v3 + 65 * v4 + 36 * v5 + 64 * v6 + 33 * v7 + 119 * v8 + 116 * v9 + 35 * v10 + 61 * v11 + 55 * v12 + 70 * v13 + 117 * v14 + 120 * v15 + 105 * v16 + 98 * v17 + 37 * v18 + 83 * v19 + 64 * v20 + 88 * v21 + 119 * v22 + 55 * v23 + 33 * v24 + 56 * v25 + 44 * v26 + 46 * v27 + 84 * v28 + 86 * v29 + 49 * v30 + 78 * v31 + 93 * v32 == 166651)
s.add(34 * v1 + 97 * v2 + 100 * v3 + 33 * v4 + 71 * v5 + 109 * v6 + 71 * v7 + 93 * v8 + 104 * v9 + 39 * v10 + 70 * v11 + 53 * v12 + 96 * v13 + 109 * v14 + 119 * v15 + 73 * v16 + 58 * v17 + 111 * v18 + 122 * v19 + 125 * v20 + 91 * v21 + 66 * v22 + 70 * v23 + 75 * v24 + 43 * v25 + 42 * v26 + 48 * v27 + 85 * v28 + 62 * v29 + 97 * v30 + 94 * v31 + 97 * v32 == 178856)
s.add(119 * v1 + 96 * v2 + 75 * v3 + 59 * v4 + 115 * v5 + 33 * v6 + 99 * v7 + 51 * v8 + 56 * v9 + 49 * v10 + 84 * v11 + 45 * v12 + 112 * v13 + 60 * v14 + 87 * v15 + 117 * v16 + 66 * v17 + 106 * v18 + 113 * v19 + 59 * v20 + 105 * v21 + 40 * v22 + 94 * v23 + 87 * v24 + 93 * v25 + 64 * v26 + 52 * v27 + 39 * v28 + 109 * v29 + 93 * v30 + 120 * v31 + 33 * v32 == 175376)
s.add(115 * v1 + 113 * v2 + 50 * v3 + 95 * v4 + 42 * v5 + 88 * v6 + 119 * v7 + 59 * v8 + 86 * v9 + 127 * v10 + 79 * v11 + 89 * v12 + 107 * v13 + 45 * v14 + 64 * v15 + 112 * v16 + 68 * v17 + 102 * v18 + 45 * v19 + 39 * v20 + 63 * v21 + 95 * v22 + 35 * v23 + 119 * v24 + 38 * v25 + 110 * v26 + 43 * v27 + 56 * v28 + 67 * v29 + 124 * v30 + 106 * v31 + 125 * v32 == 187367)
s.add(78 * v1 + 83 * v2 + 98 * v3 + 86 * v4 + 50 * v5 + 68 * v6 + 73 * v7 + 52 * v8 + 49 * v9 + 97 * v10 + 60 * v11 + 84 * v12 + 54 * v13 + 118 * v14 + 91 * v15 + 100 * v16 + 44 * v17 + 97 * v18 + 97 * v19 + 96 * v20 + 127 * v21 + 79 * v22 + 94 * v23 + 77 * v24 + 76 * v25 + 118 * v26 + 49 * v27 + 111 * v28 + 87 * v29 + 125 * v30 + 73 * v31 + 77 * v32 == 182885)
s.add(103 * v1 + 45 * v2 + 119 * v3 + 36 * v4 + 94 * v5 + 99 * v6 + 81 * v7 + 35 * v8 + 97 * v9 + 51 * v10 + 107 * v11 + 110 * v12 + 120 * v13 + 71 * v14 + 64 * v15 + 88 * v16 + 83 * v17 + 33 * v18 + 120 * v19 + 89 * v20 + 114 * v21 + 36 * v22 + 110 * v23 + 80 * v24 + 85 * v25 + 40 * v26 + 105 * v27 + 37 * v28 + 66 * v29 + 73 * v30 + 91 * v31 + 59 * v32 == 177145)
s.add(122 * v1 + 56 * v2 + 111 * v3 + 52 * v4 + 33 * v5 + 118 * v6 + 89 * v7 + 105 * v8 + 61 * v9 + 117 * v10 + 60 * v11 + 123 * v12 + 125 * v13 + 52 * v14 + 63 * v15 + 57 * v16 + 124 * v17 + 109 * v18 + 64 * v19 + 47 * v20 + 52 * v21 + 98 * v22 + 96 * v23 + 60 * v24 + 86 * v25 + 45 * v26 + 51 * v27 + 86 * v28 + 123 * v29 + 70 * v30 + 104 * v31 + 110 * v32 == 189716)
s.add(51 * v1 + 127 * v2 + 85 * v3 + 43 * v4 + 79 * v5 + 44 * v6 + 118 * v7 + 89 * v8 + 78 * v9 + 95 * v10 + 87 * v11 + 103 * v12 + 33 * v13 + 44 * v14 + 102 * v15 + 100 * v16 + 40 * v17 + 40 * v18 + 55 * v19 + 58 * v20 + 43 * v21 + 76 * v22 + 115 * v23 + 81 * v24 + 68 * v25 + 123 * v26 + 69 * v27 + 48 * v28 + 66 * v29 + 74 * v30 + 83 * v31 + 119 * v32 == 169531)
s.add(79 * v1 + 55 * v2 + 88 * v3 + 105 * v4 + 81 * v5 + 104 * v6 + 105 * v7 + 100 * v8 + 46 * v9 + 34 * v10 + 87 * v11 + 68 * v12 + 36 * v13 + 74 * v14 + 48 * v15 + 70 * v16 + 57 * v17 + 39 * v18 + 125 * v19 + 80 * v20 + 102 * v21 + 61 * v22 + 127 * v23 + 82 * v24 + 90 * v25 + 85 * v26 + 120 * v27 + 35 * v28 + 126 * v29 + 60 * v30 + 105 * v31 + 104 * v32 == 178924)
sk = ""
if s.check() == sat:
result = s.model()
sk = str(result)
dict = {}
sk = sk.replace(",", "").replace("]", ",").replace("[", "")
for i in sk.split("n"):
if i == "":
continue
temp = i.replace(",","").strip().split(" = ")
dict[temp[0]] = temp[1]
print("flag{",end="")
for i in cha:
print(chr(eval(dict[i])),end="")
print("}")
# FLAG：flag{fd954d994c4955f5e9c0901460b38aee}
代码写的烂了点，也别嫌弃。
2、virtureIDA载入程序，没找到main函数，也没有发现目标字符串。从 start 往下跟，找到这个sub_4017E0()：
跟进 sub_401840 ，switch 加 while 1 循环，好家伙，绝对是 VM 没跑了：
再看了一下这个switch，30多个指令，2万多个字节的 opcode，我那一刻人都是麻的，但没办法，题还得肝，只能是硬着头皮往下分析。
按照个人习惯，第一步是，把opcode一条条的分割开来，这样方便阅读：
这题倒是没有我想象的那么丧心病狂，三十几个指令到头来只用到了十来个的样子
| 指令 | 作用 |
|---|---|
| 0x01 | 加法运算 |
| 0x02 | 乘法运算 |
| 0x09 | 转移指令，相当于 mov reg ， Dword |
| 0x0d | 异或运算 |
| 0x12 | 转移指令，相当于 mov [addr] , reg |
| 0x13 | 转移指令，相当于 mov reg ， Dword |
| 0x15 | 字符输出，相当于 putchar() |
| 0x16 | 字符输入，相当于 getchar() |
| 0x17 | 没摸清楚，可以确定的是有个比较的功能 |
| 0x1b | 退出，相当于 exit() |
| 0x20 | 条件跳转，但在那种条件下跳转不明 |
| 0x21 | 不等于跳转，相当于 jne |
程序的流程大概如下：
- 输出字符串 “Please input the key:”
- 接收32个字符的输入
- 检测输入是否合法
- 32 轮校验
我们重点来看校验这个部分，下面第一轮的校验指令，剩余的31轮除了参数不同，方法都一样：
09 01 00 00 00 00 mov num_32 , Dword 0 13 00 00 00 00 00 load char flag[00] 09 02 3e 00 00 00 load char 3e > 02 00 02 temp = 0x3e * flag[00] 01 01 00 num_32 += temp 13 00 01 00 00 00 load char flag[01] 09 02 21 00 00 00 load char 21 ! 02 00 02 temp = 0x21 * flag[01] 01 01 00 num_32 += temp 13 00 02 00 00 00 load char flag[02] 09 02 33 00 00 00 load char 33 3 02 00 02 temp = 0x33 * flag[02] 01 01 00 num_32 += temp 13 00 03 00 00 00 load char flag[03] 09 02 68 00 00 00 load char 68 h 02 00 02 temp = 0x68 * flag[03] 01 01 00 num_32 += temp 13 00 04 00 00 00 load char flag[04] 09 02 2a 00 00 00 load char 2a * 02 00 02 temp = 0x2a * flag[04] 01 01 00 num_32 += temp 13 00 05 00 00 00 load char flag[05] 09 02 25 00 00 00 load char 25 % 02 00 02 temp = 0x25 * flag[05] 01 01 00 num_32 += temp 13 00 06 00 00 00 load char flag[06] 09 02 50 00 00 00 load char 50 P 02 00 02 temp = 0x50 * flag[06] 01 01 00 num_32 += temp 13 00 07 00 00 00 load char flag[07] 09 02 42 00 00 00 load char 42 B 02 00 02 temp = 0x42 * flag[07] 01 01 00 num_32 += temp 13 00 08 00 00 00 load char flag[08] 09 02 2e 00 00 00 load char 2e . 02 00 02 temp = 0x2e * flag[08] 01 01 00 num_32 += temp 13 00 09 00 00 00 load char flag[09] 09 02 77 00 00 00 load char 77 w 02 00 02 temp = 0x77 * flag[09] 01 01 00 num_32 += temp 13 00 0a 00 00 00 load char flag[0a] 09 02 3f 00 00 00 load char 3f ? 02 00 02 temp = 0x3f * flag[0a] 01 01 00 num_32 += temp 13 00 0b 00 00 00 load char flag[0b] 09 02 5d 00 00 00 load char 5d ] 02 00 02 temp = 0x5d * flag[0b] 01 01 00 num_32 += temp 13 00 0c 00 00 00 load char flag[0c] 09 02 28 00 00 00 load char 28 ( 02 00 02 temp = 0x28 * flag[0c] 01 01 00 num_32 += temp 13 00 0d 00 00 00 load char flag[0d] 09 02 5f 00 00 00 load char 5f _ 02 00 02 temp = 0x5f * flag[0d] 01 01 00 num_32 += temp 13 00 0e 00 00 00 load char flag[0e] 09 02 45 00 00 00 load char 45 E 02 00 02 temp = 0x45 * flag[0e] 01 01 00 num_32 += temp 13 00 0f 00 00 00 load char flag[0f] 09 02 69 00 00 00 load char 69 i 02 00 02 temp = 0x69 * flag[0f] 01 01 00 num_32 += temp 13 00 10 00 00 00 load char flag[10] 09 02 36 00 00 00 load char 36 6 02 00 02 temp = 0x36 * flag[10] 01 01 00 num_32 += temp 13 00 11 00 00 00 load char flag[11] 09 02 24 00 00 00 load char 24 $ 02 00 02 temp = 0x24 * flag[11] 01 01 00 num_32 += temp 13 00 12 00 00 00 load char flag[12] 09 02 5d 00 00 00 load char 5d ] 02 00 02 temp = 0x5d * flag[12] 01 01 00 num_32 += temp 13 00 13 00 00 00 load char flag[13] 09 02 35 00 00 00 load char 35 5 02 00 02 temp = 0x35 * flag[13] 01 01 00 num_32 += temp 13 00 14 00 00 00 load char flag[14] 09 02 42 00 00 00 load char 42 B 02 00 02 temp = 0x42 * flag[14] 01 01 00 num_32 += temp 13 00 15 00 00 00 load char flag[15] 09 02 43 00 00 00 load char 43 C 02 00 02 temp = 0x43 * flag[15] 01 01 00 num_32 += temp 13 00 16 00 00 00 load char flag[16] 09 02 3e 00 00 00 load char 3e > 02 00 02 temp = 0x3e * flag[16] 01 01 00 num_32 += temp 13 00 17 00 00 00 load char flag[17] 09 02 41 00 00 00 load char 41 A 02 00 02 temp = 0x41 * flag[17] 01 01 00 num_32 += temp 13 00 18 00 00 00 load char flag[18] 09 02 50 00 00 00 load char 50 P 02 00 02 temp = 0x50 * flag[18] 01 01 00 num_32 += temp 13 00 19 00 00 00 load char flag[19] 09 02 75 00 00 00 load char 75 u 02 00 02 temp = 0x75 * flag[19] 01 01 00 num_32 += temp 13 00 1a 00 00 00 load char flag[1a] 09 02 32 00 00 00 load char 32 2 02 00 02 temp = 0x32 * flag[1a] 01 01 00 num_32 += temp 13 00 1b 00 00 00 load char flag[1b] 09 02 2b 00 00 00 load char 2b + 02 00 02 temp = 0x2b * flag[1b] 01 01 00 num_32 += temp 13 00 1c 00 00 00 load char flag[1c] 09 02 24 00 00 00 load char 24 $ 02 00 02 temp = 0x24 * flag[1c] 01 01 00 num_32 += temp 13 00 1d 00 00 00 load char flag[1d] 09 02 6b 00 00 00 load char 6b k 02 00 02 temp = 0x6b * flag[1d] 01 01 00 num_32 += temp 13 00 1e 00 00 00 load char flag[1e] 09 02 6c 00 00 00 load char 6c l 02 00 02 temp = 0x6c * flag[1e] 01 01 00 num_32 += temp 13 00 1f 00 00 00 load char flag[1f] 09 02 6f 00 00 00 load char 6f o 02 00 02 temp = 0x6f * flag[1f] 01 01 00 num_32 += temp 0d 01 89 1d 24 ac num_32 ^= Dword 0xac241d89 09 00 92 86 26 ac load Dword 0xac268692 17 00 01 cmp 0xac268692 , num_32 21 e7 4f 00 00 jne exit()
到这里应该能看出来了，和上一题一样，还是一个 32元一次方程，只是从 Java版换成了 VM 版，就离谱，出题人得是多好这一口！
再之后就简单了，将相关的参数提取出来，套用上面的脚本再跑一遍 z3 就是了：
# -*- coding: utf-8 -*-
"""
Spyder Editor
This is a temporary script file.
"""
from z3 import *
value1 = [
0xac241d89,0x3c748602,0xd050dee3,0x6437ffd9,
0x0d6f5ae8,0x8d08a075,0xbb43561f,0xa10913ca,
0x0d647c66,0x61cb01dd,0x51f6cf38,0x86009a31,
0xfb6afa06,0x26dfaeeb,0x76b24695,0xf3fde9a0,
0xd8934cc7,0xf1aa539d,0xac6ddc1d,0xf0caaf80,
0xf3401aff,0x980a0d4c,0x26e3a3bc,0x410f94d2,
0x738c4f02,0xa39ebcfe,0x64399bab,0xc7ac872a,
0xdc577d43,0xf82afcfd,0x993d28fc,0xb5aaf6b5]
value2 = [
0xac268692,0x3c7639ab,0xd053e7d4,0x64358e07,
0x0d6c5c0a,0x8d0a4298,0xbb405f60,0xa10a1755,
0x0d66dd24,0x61c9e122,0x51f4aad8,0x86023671,
0xfb681443,0x26dd5538,0x76b17016,0xf3ff3d06,
0xd891a50f,0xf1a8e0e8,0xac6f3e04,0xf0c8014b,
0xf342a73a,0x9808cfeb,0x26e1269a,0x410d7bec,
0x738e895c,0xa39c7998,0x643b4245,0xc7ae4d47,
0xdc55acf7,0xf82815ad,0x993fe1e1,0xb5a9c95c]
num_32 = []
for i in range(32):
num_32.append(value1[i]^value2[i])
cha = ["v1","v2","v3","v4","v5","v6","v7","v8","v9","v10","v11","v12","v13","v14","v15","v16","v17","v18","v19","v20","v21","v22","v23","v24","v25","v26","v27","v28","v29","v30","v31","v32"]
tab = [
[62, 33, 51, 104, 42, 37, 80, 66, 46, 119, 63, 93, 40, 95, 69, 105, 54, 36, 93, 53, 66, 67, 62, 65, 80, 117, 50, 43, 36, 107, 108, 111],
[ 91, 72, 76, 37, 63, 111, 56, 51, 95, 54, 98, 125, 34, 49, 34, 94, 62, 65, 69, 98, 97, 109, 88, 61, 63, 58, 126, 66, 117, 51, 98, 84],
[ 105, 78, 82, 62, 119, 118, 88, 66, 97, 100, 86, 43, 124, 93, 70, 123, 116, 40, 93, 121, 95, 104, 86, 58, 122, 120, 101, 38, 123, 99, 49, 66],
[ 67, 34, 108, 65, 70, 37, 65, 38, 88, 54, 97, 62, 82, 51, 63, 59, 126, 33, 91, 47, 106, 36, 77, 35, 77, 114, 71, 57, 36, 111, 62, 62],
[ 83, 66, 38, 59, 124, 73, 120, 119, 82, 79, 36, 106, 74, 120, 124, 116, 71, 120, 43, 89, 61, 114, 124, 64, 97, 92, 71, 76, 43, 93, 38, 96],
[ 86, 77, 79, 65, 79, 47, 116, 35, 34, 91, 68, 54, 80, 42, 34, 95, 56, 105, 54, 126, 118, 60, 98, 119, 103, 121, 90, 42, 105, 100, 101, 87],
[ 70, 114, 91, 34, 116, 84, 123, 80, 124, 49, 41, 110, 107, 109, 99, 64, 74, 107, 88, 43, 105, 122, 60, 87, 68, 127, 83, 56, 75, 83, 48, 42],
[ 83, 122, 47, 116, 79, 73, 54, 57, 38, 34, 125, 52, 110, 105, 124, 80, 124, 92, 117, 98, 93, 89, 95, 87, 49, 125, 84, 36, 80, 74, 106, 117],
[ 97, 71, 81, 53, 97, 55, 54, 72, 45, 87, 113, 99, 126, 36, 47, 55, 41, 83, 106, 71, 60, 97, 74, 52, 82, 68, 71, 35, 85, 114, 39, 72],
[ 70, 109, 76, 82, 74, 105, 96, 94, 85, 74, 72, 75, 57, 106, 99, 80, 107, 36, 78, 95, 96, 43, 51, 124, 98, 99, 58, 107, 90, 61, 43, 71],
[ 52, 58, 46, 111, 78, 41, 39, 47, 105, 44, 43, 45, 37, 69, 125, 35, 104, 63, 34, 50, 117, 66, 89, 55, 56, 106, 83, 123, 72, 42, 62, 97],
[ 109, 103, 106, 80, 58, 45, 100, 51, 109, 76, 66, 103, 61, 48, 37, 93, 50, 45, 105, 97, 45, 77, 38, 114, 69, 121, 85, 77, 53, 55, 38, 37],
[ 90, 45, 47, 124, 64, 97, 84, 52, 83, 39, 100, 122, 101, 57, 83, 53, 82, 123, 122, 83, 102, 60, 61, 77, 109, 59, 123, 85, 54, 98, 101, 72],
[ 95, 102, 105, 116, 70, 49, 94, 114, 106, 63, 58, 37, 74, 113, 112, 64, 115, 35, 89, 64, 90, 98, 41, 94, 48, 119, 59, 81, 122, 99, 80, 124],
[ 33, 107, 67, 107, 48, 118, 81, 113, 58, 127, 125, 40, 123, 76, 117, 109, 66, 90, 107, 34, 95, 119, 76, 99, 117, 85, 117, 48, 47, 120, 70, 76],
[ 52, 90, 76, 55, 119, 103, 34, 34, 47, 54, 84, 93, 61, 48, 118, 115, 72, 56, 66, 116, 110, 119, 122, 85, 75, 67, 98, 104, 93, 51, 36, 110],
[ 32, 72, 111, 41, 78, 44, 122, 66, 46, 118, 42, 98, 112, 75, 113, 78, 105, 78, 124, 67, 124, 106, 86, 79, 38, 112, 51, 95, 108, 35, 36, 44],
[ 53, 73, 69, 102, 64, 53, 104, 100, 34, 72, 96, 69, 49, 122, 102, 39, 119, 57, 49, 42, 61, 121, 39, 84, 124, 61, 125, 115, 57, 47, 116, 47],
[ 110, 70, 62, 114, 84, 107, 46, 106, 99, 96, 74, 52, 121, 58, 127, 37, 106, 77, 116, 112, 118, 59, 50, 113, 56, 83, 74, 46, 42, 43, 50, 66],
[ 69, 71, 55, 77, 84, 67, 123, 98, 120, 124, 105, 122, 88, 57, 99, 39, 35, 67, 42, 43, 41, 92, 103, 46, 84, 38, 43, 83, 33, 87, 79, 39],
[ 41, 49, 91, 71, 122, 83, 69, 82, 45, 92, 94, 114, 50, 58, 48, 66, 109, 88, 62, 63, 121, 46, 41, 91, 107, 104, 125, 35, 119, 41, 71, 50],
[ 67, 93, 83, 62, 127, 91, 103, 37, 62, 34, 72, 111, 112, 33, 93, 119, 112, 81, 57, 112, 64, 73, 120, 36, 63, 53, 76, 48, 106, 111, 44, 122],
[ 116, 85, 120, 43, 81, 55, 115, 62, 102, 34, 38, 88, 36, 76, 35, 114, 97, 127, 60, 75, 73, 34, 52, 77, 42, 56, 93, 49, 76, 125, 56, 73],
[ 77, 111, 116, 34, 85, 42, 37, 38, 89, 65, 115, 121, 116, 103, 108, 106, 126, 86, 107, 125, 110, 48, 60, 87, 35, 53, 100, 101, 50, 117, 56, 65],
[ 103, 34, 77, 46, 44, 86, 124, 109, 77, 90, 50, 127, 40, 77, 39, 103, 84, 112, 89, 56, 96, 82, 36, 44, 88, 58, 72, 38, 89, 54, 123, 87],
[ 43, 48, 54, 45, 79, 88, 33, 54, 103, 100, 54, 49, 127, 108, 116, 87, 127, 121, 117, 93, 60, 101, 108, 50, 32, 36, 76, 55, 111, 61, 47, 121],
[ 113, 114, 113, 50, 122, 111, 120, 50, 122, 35, 102, 90, 89, 42, 62, 60, 86, 95, 43, 72, 114, 78, 82, 53, 70, 93, 118, 34, 87, 96, 62, 57],
[ 67, 104, 82, 72, 109, 117, 53, 39, 85, 97, 33, 82, 59, 39, 102, 37, 103, 39, 104, 71, 86, 43, 108, 123, 37, 125, 107, 56, 96, 119, 36, 108],
[ 91, 64, 43, 97, 46, 105, 49, 68, 68, 109, 33, 54, 90, 103, 117, 98, 52, 96, 32, 97, 87, 66, 72, 118, 66, 76, 87, 83, 53, 119, 90, 119],
[ 65, 53, 85, 84, 94, 82, 77, 70, 68, 97, 94, 86, 124, 54, 38, 52, 50, 124, 92, 64, 74, 85, 45, 94, 97, 110, 49, 123, 76, 56, 89, 120],
[ 109, 114, 33, 33, 76, 41, 61, 48, 41, 123, 65, 59, 85, 32, 127, 97, 98, 114, 87, 32, 67, 68, 108, 120, 116, 63, 109, 54, 92, 72, 72, 32],
[ 68, 84, 102, 97, 121, 127, 110, 126, 90, 109, 54, 60, 126, 86, 98, 92, 48, 103, 75, 124, 103, 119, 52, 84, 84, 91, 94, 44, 124, 76, 57, 99]
]
v1 = Int('v1')
v2 = Int('v2')
v3 = Int('v3')
v4 = Int('v4')
v5 = Int('v5')
v6 = Int('v6')
v7 = Int('v7')
v8 = Int('v8')
v9 = Int('v9')
v10 = Int('v10')
v11 = Int('v11')
v12 = Int('v12')
v13 = Int('v13')
v14 = Int('v14')
v15 = Int('v15')
v16 = Int('v16')
v17 = Int('v17')
v18 = Int('v18')
v19 = Int('v19')
v20 = Int('v20')
v21 = Int('v21')
v22 = Int('v22')
v23 = Int('v23')
v24 = Int('v24')
v25 = Int('v25')
v26 = Int('v26')
v27 = Int('v27')
v28 = Int('v28')
v29 = Int('v29')
v30 = Int('v30')
v31 = Int('v31')
v32 = Int('v32')
s = Solver()
s.add(62 * v1 + 33 * v2 + 51 * v3 + 104 * v4 + 42 * v5 + 37 * v6 + 80 * v7 + 66 * v8 + 46 * v9 + 119 * v10 + 63 * v11 + 93 * v12 + 40 * v13 + 95 * v14 + 69 * v15 + 105 * v16 + 54 * v17 + 36 * v18 + 93 * v19 + 53 * v20 + 66 * v21 + 67 * v22 + 62 * v23 + 65 * v24 + 80 * v25 + 117 * v26 + 50 * v27 + 43 * v28 + 36 * v29 + 107 * v30 + 108 * v31 + 111 * v32 == 170779)
s.add(91 * v1 + 72 * v2 + 76 * v3 + 37 * v4 + 63 * v5 + 111 * v6 + 56 * v7 + 51 * v8 + 95 * v9 + 54 * v10 + 98 * v11 + 125 * v12 + 34 * v13 + 49 * v14 + 34 * v15 + 94 * v16 + 62 * v17 + 65 * v18 + 69 * v19 + 98 * v20 + 97 * v21 + 109 * v22 + 88 * v23 + 61 * v24 + 63 * v25 + 58 * v26 + 126 * v27 + 66 * v28 + 117 * v29 + 51 * v30 + 98 * v31 + 84 * v32 == 180137)
s.add(105 * v1 + 78 * v2 + 82 * v3 + 62 * v4 + 119 * v5 + 118 * v6 + 88 * v7 + 66 * v8 + 97 * v9 + 100 * v10 + 86 * v11 + 43 * v12 + 124 * v13 + 93 * v14 + 70 * v15 + 123 * v16 + 116 * v17 + 40 * v18 + 93 * v19 + 121 * v20 + 95 * v21 + 104 * v22 + 86 * v23 + 58 * v24 + 122 * v25 + 120 * v26 + 101 * v27 + 38 * v28 + 123 * v29 + 99 * v30 + 49 * v31 + 66 * v32 == 211255)
s.add(67 * v1 + 34 * v2 + 108 * v3 + 65 * v4 + 70 * v5 + 37 * v6 + 65 * v7 + 38 * v8 + 88 * v9 + 54 * v10 + 97 * v11 + 62 * v12 + 82 * v13 + 51 * v14 + 63 * v15 + 59 * v16 + 126 * v17 + 33 * v18 + 91 * v19 + 47 * v20 + 106 * v21 + 36 * v22 + 77 * v23 + 35 * v24 + 77 * v25 + 114 * v26 + 71 * v27 + 57 * v28 + 36 * v29 + 111 * v30 + 62 * v31 + 62 * v32 == 160222)
s.add(83 * v1 + 66 * v2 + 38 * v3 + 59 * v4 + 124 * v5 + 73 * v6 + 120 * v7 + 119 * v8 + 82 * v9 + 79 * v10 + 36 * v11 + 106 * v12 + 74 * v13 + 120 * v14 + 124 * v15 + 116 * v16 + 71 * v17 + 120 * v18 + 43 * v19 + 89 * v20 + 61 * v21 + 114 * v22 + 124 * v23 + 64 * v24 + 97 * v25 + 92 * v26 + 71 * v27 + 76 * v28 + 43 * v29 + 93 * v30 + 38 * v31 + 96 * v32 == 198370)
s.add(86 * v1 + 77 * v2 + 79 * v3 + 65 * v4 + 79 * v5 + 47 * v6 + 116 * v7 + 35 * v8 + 34 * v9 + 91 * v10 + 68 * v11 + 54 * v12 + 80 * v13 + 42 * v14 + 34 * v15 + 95 * v16 + 56 * v17 + 105 * v18 + 54 * v19 + 126 * v20 + 118 * v21 + 60 * v22 + 98 * v23 + 119 * v24 + 103 * v25 + 121 * v26 + 90 * v27 + 42 * v28 + 105 * v29 + 100 * v30 + 101 * v31 + 87 * v32 == 189165)
s.add(70 * v1 + 114 * v2 + 91 * v3 + 34 * v4 + 116 * v5 + 84 * v6 + 123 * v7 + 80 * v8 + 124 * v9 + 49 * v10 + 41 * v11 + 110 * v12 + 107 * v13 + 109 * v14 + 99 * v15 + 64 * v16 + 74 * v17 + 107 * v18 + 88 * v19 + 43 * v20 + 105 * v21 + 122 * v22 + 60 * v23 + 87 * v24 + 68 * v25 + 127 * v26 + 83 * v27 + 56 * v28 + 75 * v29 + 83 * v30 + 48 * v31 + 42 * v32 == 199039)
s.add(83 * v1 + 122 * v2 + 47 * v3 + 116 * v4 + 79 * v5 + 73 * v6 + 54 * v7 + 57 * v8 + 38 * v9 + 34 * v10 + 125 * v11 + 52 * v12 + 110 * v13 + 105 * v14 + 124 * v15 + 80 * v16 + 124 * v17 + 92 * v18 + 117 * v19 + 98 * v20 + 93 * v21 + 89 * v22 + 95 * v23 + 87 * v24 + 49 * v25 + 125 * v26 + 84 * v27 + 36 * v28 + 80 * v29 + 74 * v30 + 106 * v31 + 117 * v32 == 197791)
s.add(97 * v1 + 71 * v2 + 81 * v3 + 53 * v4 + 97 * v5 + 55 * v6 + 54 * v7 + 72 * v8 + 45 * v9 + 87 * v10 + 113 * v11 + 99 * v12 + 126 * v13 + 36 * v14 + 47 * v15 + 55 * v16 + 41 * v17 + 83 * v18 + 106 * v19 + 71 * v20 + 60 * v21 + 97 * v22 + 74 * v23 + 52 * v24 + 82 * v25 + 68 * v26 + 71 * v27 + 35 * v28 + 85 * v29 + 114 * v30 + 39 * v31 + 72 * v32 == 172354)
s.add(70 * v1 + 109 * v2 + 76 * v3 + 82 * v4 + 74 * v5 + 105 * v6 + 96 * v7 + 94 * v8 + 85 * v9 + 74 * v10 + 72 * v11 + 75 * v12 + 57 * v13 + 106 * v14 + 99 * v15 + 80 * v16 + 107 * v17 + 36 * v18 + 78 * v19 + 95 * v20 + 96 * v21 + 43 * v22 + 51 * v23 + 124 * v24 + 98 * v25 + 99 * v26 + 58 * v27 + 107 * v28 + 90 * v29 + 61 * v30 + 43 * v31 + 71 * v32 == 188671)
s.add(52 * v1 + 58 * v2 + 46 * v3 + 111 * v4 + 78 * v5 + 41 * v6 + 39 * v7 + 47 * v8 + 105 * v9 + 44 * v10 + 43 * v11 + 45 * v12 + 37 * v13 + 69 * v14 + 125 * v15 + 35 * v16 + 104 * v17 + 63 * v18 + 34 * v19 + 50 * v20 + 117 * v21 + 66 * v22 + 89 * v23 + 55 * v24 + 56 * v25 + 106 * v26 + 83 * v27 + 123 * v28 + 72 * v29 + 42 * v30 + 62 * v31 + 97 * v32 == 157152)
s.add(109 * v1 + 103 * v2 + 106 * v3 + 80 * v4 + 58 * v5 + 45 * v6 + 100 * v7 + 51 * v8 + 109 * v9 + 76 * v10 + 66 * v11 + 103 * v12 + 61 * v13 + 48 * v14 + 37 * v15 + 93 * v16 + 50 * v17 + 45 * v18 + 105 * v19 + 97 * v20 + 45 * v21 + 77 * v22 + 38 * v23 + 114 * v24 + 69 * v25 + 121 * v26 + 85 * v27 + 77 * v28 + 53 * v29 + 55 * v30 + 38 * v31 + 37 * v32 == 175168)
s.add(90 * v1 + 45 * v2 + 47 * v3 + 124 * v4 + 64 * v5 + 97 * v6 + 84 * v7 + 52 * v8 + 83 * v9 + 39 * v10 + 100 * v11 + 122 * v12 + 101 * v13 + 57 * v14 + 83 * v15 + 53 * v16 + 82 * v17 + 123 * v18 + 122 * v19 + 83 * v20 + 102 * v21 + 60 * v22 + 61 * v23 + 77 * v24 + 109 * v25 + 59 * v26 + 123 * v27 + 85 * v28 + 54 * v29 + 98 * v30 + 101 * v31 + 72 * v32 == 192069)
s.add(95 * v1 + 102 * v2 + 105 * v3 + 116 * v4 + 70 * v5 + 49 * v6 + 94 * v7 + 114 * v8 + 106 * v9 + 63 * v10 + 58 * v11 + 37 * v12 + 74 * v13 + 113 * v14 + 112 * v15 + 64 * v16 + 115 * v17 + 35 * v18 + 89 * v19 + 64 * v20 + 90 * v21 + 98 * v22 + 41 * v23 + 94 * v24 + 48 * v25 + 119 * v26 + 59 * v27 + 81 * v28 + 122 * v29 + 99 * v30 + 80 * v31 + 124 * v32 == 195539)
s.add(33 * v1 + 107 * v2 + 67 * v3 + 107 * v4 + 48 * v5 + 118 * v6 + 81 * v7 + 113 * v8 + 58 * v9 + 127 * v10 + 125 * v11 + 40 * v12 + 123 * v13 + 76 * v14 + 117 * v15 + 109 * v16 + 66 * v17 + 90 * v18 + 107 * v19 + 34 * v20 + 95 * v21 + 119 * v22 + 76 * v23 + 99 * v24 + 117 * v25 + 85 * v26 + 117 * v27 + 48 * v28 + 47 * v29 + 120 * v30 + 70 * v31 + 76 * v32 == 210563)
s.add(52 * v1 + 90 * v2 + 76 * v3 + 55 * v4 + 119 * v5 + 103 * v6 + 34 * v7 + 34 * v8 + 47 * v9 + 54 * v10 + 84 * v11 + 93 * v12 + 61 * v13 + 48 * v14 + 118 * v15 + 115 * v16 + 72 * v17 + 56 * v18 + 66 * v19 + 116 * v20 + 110 * v21 + 119 * v22 + 122 * v23 + 85 * v24 + 75 * v25 + 67 * v26 + 98 * v27 + 104 * v28 + 93 * v29 + 51 * v30 + 36 * v31 + 110 * v32 == 185510)
s.add(32 * v1 + 72 * v2 + 111 * v3 + 41 * v4 + 78 * v5 + 44 * v6 + 122 * v7 + 66 * v8 + 46 * v9 + 118 * v10 + 42 * v11 + 98 * v12 + 112 * v13 + 75 * v14 + 113 * v15 + 78 * v16 + 105 * v17 + 78 * v18 + 124 * v19 + 67 * v20 + 124 * v21 + 106 * v22 + 86 * v23 + 79 * v24 + 38 * v25 + 112 * v26 + 51 * v27 + 95 * v28 + 108 * v29 + 35 * v30 + 36 * v31 + 44 * v32 == 190920)
s.add(53 * v1 + 73 * v2 + 69 * v3 + 102 * v4 + 64 * v5 + 53 * v6 + 104 * v7 + 100 * v8 + 34 * v9 + 72 * v10 + 96 * v11 + 69 * v12 + 49 * v13 + 122 * v14 + 102 * v15 + 39 * v16 + 119 * v17 + 57 * v18 + 49 * v19 + 42 * v20 + 61 * v21 + 121 * v22 + 39 * v23 + 84 * v24 + 124 * v25 + 61 * v26 + 125 * v27 + 115 * v28 + 57 * v29 + 47 * v30 + 116 * v31 + 47 * v32 == 177013)
s.add(110 * v1 + 70 * v2 + 62 * v3 + 114 * v4 + 84 * v5 + 107 * v6 + 46 * v7 + 106 * v8 + 99 * v9 + 96 * v10 + 74 * v11 + 52 * v12 + 121 * v13 + 58 * v14 + 127 * v15 + 37 * v16 + 106 * v17 + 77 * v18 + 116 * v19 + 112 * v20 + 118 * v21 + 59 * v22 + 50 * v23 + 113 * v24 + 56 * v25 + 83 * v26 + 74 * v27 + 46 * v28 + 42 * v29 + 43 * v30 + 50 * v31 + 66 * v32 == 188953)
s.add(69 * v1 + 71 * v2 + 55 * v3 + 77 * v4 + 84 * v5 + 67 * v6 + 123 * v7 + 98 * v8 + 120 * v9 + 124 * v10 + 105 * v11 + 122 * v12 + 88 * v13 + 57 * v14 + 99 * v15 + 39 * v16 + 35 * v17 + 67 * v18 + 42 * v19 + 43 * v20 + 41 * v21 + 92 * v22 + 103 * v23 + 46 * v24 + 84 * v25 + 38 * v26 + 43 * v27 + 83 * v28 + 33 * v29 + 87 * v30 + 79 * v31 + 39 * v32 == 175819)
s.add(41 * v1 + 49 * v2 + 91 * v3 + 71 * v4 + 122 * v5 + 83 * v6 + 69 * v7 + 82 * v8 + 45 * v9 + 92 * v10 + 94 * v11 + 114 * v12 + 50 * v13 + 58 * v14 + 48 * v15 + 66 * v16 + 109 * v17 + 88 * v18 + 62 * v19 + 63 * v20 + 121 * v21 + 46 * v22 + 41 * v23 + 91 * v24 + 107 * v25 + 104 * v26 + 125 * v27 + 35 * v28 + 119 * v29 + 41 * v30 + 71 * v31 + 50 * v32 == 179653)
s.add(67 * v1 + 93 * v2 + 83 * v3 + 62 * v4 + 127 * v5 + 91 * v6 + 103 * v7 + 37 * v8 + 62 * v9 + 34 * v10 + 72 * v11 + 111 * v12 + 112 * v13 + 33 * v14 + 93 * v15 + 119 * v16 + 112 * v17 + 81 * v18 + 57 * v19 + 112 * v20 + 64 * v21 + 73 * v22 + 120 * v23 + 36 * v24 + 63 * v25 + 53 * v26 + 76 * v27 + 48 * v28 + 106 * v29 + 111 * v30 + 44 * v31 + 122 * v32 == 180903)
s.add(116 * v1 + 85 * v2 + 120 * v3 + 43 * v4 + 81 * v5 + 55 * v6 + 115 * v7 + 62 * v8 + 102 * v9 + 34 * v10 + 38 * v11 + 88 * v12 + 36 * v13 + 76 * v14 + 35 * v15 + 114 * v16 + 97 * v17 + 127 * v18 + 60 * v19 + 75 * v20 + 73 * v21 + 34 * v22 + 52 * v23 + 77 * v24 + 42 * v25 + 56 * v26 + 93 * v27 + 49 * v28 + 76 * v29 + 125 * v30 + 56 * v31 + 73 * v32 == 165158)
s.add(77 * v1 + 111 * v2 + 116 * v3 + 34 * v4 + 85 * v5 + 42 * v6 + 37 * v7 + 38 * v8 + 89 * v9 + 65 * v10 + 115 * v11 + 121 * v12 + 116 * v13 + 103 * v14 + 108 * v15 + 106 * v16 + 126 * v17 + 86 * v18 + 107 * v19 + 125 * v20 + 110 * v21 + 48 * v22 + 60 * v23 + 87 * v24 + 35 * v25 + 53 * v26 + 100 * v27 + 101 * v28 + 50 * v29 + 117 * v30 + 56 * v31 + 65 * v32 == 192318)
s.add(103 * v1 + 34 * v2 + 77 * v3 + 46 * v4 + 44 * v5 + 86 * v6 + 124 * v7 + 109 * v8 + 77 * v9 + 90 * v10 + 50 * v11 + 127 * v12 + 40 * v13 + 77 * v14 + 39 * v15 + 103 * v16 + 84 * v17 + 112 * v18 + 89 * v19 + 56 * v20 + 96 * v21 + 82 * v22 + 36 * v23 + 44 * v24 + 88 * v25 + 58 * v26 + 72 * v27 + 38 * v28 + 89 * v29 + 54 * v30 + 123 * v31 + 87 * v32 == 181854)
s.add(43 * v1 + 48 * v2 + 54 * v3 + 45 * v4 + 79 * v5 + 88 * v6 + 33 * v7 + 54 * v8 + 103 * v9 + 100 * v10 + 54 * v11 + 49 * v12 + 127 * v13 + 108 * v14 + 116 * v15 + 87 * v16 + 127 * v17 + 121 * v18 + 117 * v19 + 93 * v20 + 60 * v21 + 101 * v22 + 108 * v23 + 50 * v24 + 32 * v25 + 36 * v26 + 76 * v27 + 55 * v28 + 111 * v29 + 61 * v30 + 47 * v31 + 121 * v32 == 181606)
s.add(113 * v1 + 114 * v2 + 113 * v3 + 50 * v4 + 122 * v5 + 111 * v6 + 120 * v7 + 50 * v8 + 122 * v9 + 35 * v10 + 102 * v11 + 90 * v12 + 89 * v13 + 42 * v14 + 62 * v15 + 60 * v16 + 86 * v17 + 95 * v18 + 43 * v19 + 72 * v20 + 114 * v21 + 78 * v22 + 82 * v23 + 53 * v24 + 70 * v25 + 93 * v26 + 118 * v27 + 34 * v28 + 87 * v29 + 96 * v30 + 62 * v31 + 57 * v32 == 186862)
s.add(67 * v1 + 104 * v2 + 82 * v3 + 72 * v4 + 109 * v5 + 117 * v6 + 53 * v7 + 39 * v8 + 85 * v9 + 97 * v10 + 33 * v11 + 82 * v12 + 59 * v13 + 39 * v14 + 102 * v15 + 37 * v16 + 103 * v17 + 39 * v18 + 104 * v19 + 71 * v20 + 86 * v21 + 43 * v22 + 108 * v23 + 123 * v24 + 37 * v25 + 125 * v26 + 107 * v27 + 56 * v28 + 96 * v29 + 119 * v30 + 36 * v31 + 108 * v32 == 182893)
s.add(91 * v1 + 64 * v2 + 43 * v3 + 97 * v4 + 46 * v5 + 105 * v6 + 49 * v7 + 68 * v8 + 68 * v9 + 109 * v10 + 33 * v11 + 54 * v12 + 90 * v13 + 103 * v14 + 117 * v15 + 98 * v16 + 52 * v17 + 96 * v18 + 32 * v19 + 97 * v20 + 87 * v21 + 66 * v22 + 72 * v23 + 118 * v24 + 66 * v25 + 76 * v26 + 87 * v27 + 83 * v28 + 53 * v29 + 119 * v30 + 90 * v31 + 119 * v32 == 184756)
s.add(65 * v1 + 53 * v2 + 85 * v3 + 84 * v4 + 94 * v5 + 82 * v6 + 77 * v7 + 70 * v8 + 68 * v9 + 97 * v10 + 94 * v11 + 86 * v12 + 124 * v13 + 54 * v14 + 38 * v15 + 52 * v16 + 50 * v17 + 124 * v18 + 92 * v19 + 64 * v20 + 74 * v21 + 85 * v22 + 45 * v23 + 94 * v24 + 97 * v25 + 110 * v26 + 49 * v27 + 123 * v28 + 76 * v29 + 56 * v30 + 89 * v31 + 120 * v32 == 190800)
s.add(109 * v1 + 114 * v2 + 33 * v3 + 33 * v4 + 76 * v5 + 41 * v6 + 61 * v7 + 48 * v8 + 41 * v9 + 123 * v10 + 65 * v11 + 59 * v12 + 85 * v13 + 32 * v14 + 127 * v15 + 97 * v16 + 98 * v17 + 114 * v18 + 87 * v19 + 32 * v20 + 67 * v21 + 68 * v22 + 108 * v23 + 120 * v24 + 116 * v25 + 63 * v26 + 109 * v27 + 54 * v28 + 92 * v29 + 72 * v30 + 72 * v31 + 32 * v32 == 182557)
s.add(68 * v1 + 84 * v2 + 102 * v3 + 97 * v4 + 121 * v5 + 127 * v6 + 110 * v7 + 126 * v8 + 90 * v9 + 109 * v10 + 54 * v11 + 60 * v12 + 126 * v13 + 86 * v14 + 98 * v15 + 92 * v16 + 48 * v17 + 103 * v18 + 75 * v19 + 124 * v20 + 103 * v21 + 119 * v22 + 52 * v23 + 84 * v24 + 84 * v25 + 91 * v26 + 94 * v27 + 44 * v28 + 124 * v29 + 76 * v30 + 57 * v31 + 99 * v32 == 212969)
sk = ""
if s.check() == sat:
result = s.model()
sk = str(result)
else:
print("Error")
dict = {}
sk = sk.replace(",", "").replace("]", ",").replace("[", "")
for i in sk.split("n"):
if i == "":
continue
temp = i.replace(",","").strip().split(" = ")
dict[temp[0]] = temp[1]
print("flag{",end="")
for i in cha:
print(chr(eval(dict[i])),end="")
print("}")
# FLAG : flag{1772353aef6cd53c34c3decfdd2762c4}
