ACE - Codegate 2024 Finals

#Codegate_2024_Finals

ひたすらに関数を呼びまくっている

いい感じにPythonのコードに落とし込んでz3で解けば良い

落とし込む仕事が地獄だったのでangrとか使うと高速に溶けたかも

code: python

from const import unk_140311F61

from z3 import *

sub_1400011B0_arr = 0, 81, 1, 2, 0, 72, 1, 157, 2, 0, 45, 1, 2, 157, 0, 130, 157, 1, 2, 0, 22, 1, 2, 0, 135, 1, 2, 0, 14, 1, 2, 157, 0, 57, 1, 188, 30, 2, 0, 123, 1, 2, 0, 136, 157, 1, 188, 42, 2, 0, 137, 1, 2, 0, 93, 1, 2, 0, 157, 115, 157, 1, 2, 0, 5, 157, 1, 188, 25, 157, 2, 0, 138, 1, 2, 0, 188, 170, 157, 65, 1, 2, 0, 105, 157, 1, 2, 0, 30, 1, 2, 0, 188, 65, 42, 1, 2, 188, 131, 0, 149, 1, 2, 0, 118, 188, 204, 1, 2, 0, 46, 188, 10, 1, 157, 2, 157, 0, 188, 47, 184, 1, 2, 157, 0, 111, 188, 149, 1, 2, 0, 178, 1, 2, 0, 157, 11, 1, 2, 188, 205, 0, 164, 188, 148, 1, 2, 0, 176, 1, 2, 0, 121, 1, 2, 0, 73, 1, 2, 0, 156, 1, 2, 0, 34, 1, 2, 0, 125, 1, 2, 0, 188, 192, 102, 1, 2, 0, 155, 157, 1, 2, 157, 0, 82, 1, 2, 0, 18, 1, 2, 0, 33, 188, 12, 1, 2, 0, 99, 157, 1, 2, 0, 36, 157, 1, 188, 97, 2, 0, 92, 1, 2, 188, 224, 157, 0, 114, 1, 2, 0, 169, 1, 2, 0, 188, 18, 117, 1, 2, 0, 150, 1, 2, 0, 7, 1, 188, 167, 2, 0, 188, 233, 132, 1, 2, 0, 160, 1, 2, 0, 67, 1, 2, 0, 166, 1, 2, 0, 109, 1, 157, 2, 0, 96, 1, 188, 122, 2, 0, 66, 1, 2, 0, 4, 1, 2, 0, 112, 1, 2, 0, 75, 1, 2, 0, 108, 1, 2, 188, 171, 0, 28, 188, 165, 1, 2, 0, 3, 1, 2, 0, 35, 1, 2, 0, 148, 1, 2, 0, 146, 1, 2, 0, 157, 71, 1, 2, 188, 55, 0, 157, 127, 1, 2, 0, 47, 1, 2, 0, 58, 1, 2, 0, 188, 206, 94, 1, 2, 0, 100, 188, 154, 1, 2, 0, 59, 1, 2, 0, 120, 1, 2, 0, 86, 1, 2, 188, 27, 0, 152, 1, 2, 0, 162, 1, 2, 0, 188, 173, 25, 188, 166, 1, 2, 188, 156, 0, 54, 1, 2, 188, 226, 0, 27, 188, 125, 1, 2, 0, 52, 1, 2, 0, 133, 157, 1, 157, 2, 142, 30, 79, 129, 157, 142, 22, 13, 231, 142, 3, 172, 222, 142, 23, 183, 31, 142, 22, 157, 106, 106, 142, 7, 168, 211, 142, 2, 64, 167, 142, 11, 157, 119, 50, 142, 2, 24, 22, 188, 63, 142, 19, 91, 49, 142, 0, 185, 12, 142, 6, 32, 161, 142, 29, 145, 194, 188, 19, 29, 167, 142, 28, 53, 76, 142, 29, 17, 88, 142, 6, 187, 96, 142, 30, 97, 78, 142, 21, 95, 27, 142, 9, 154, 113, 142, 2, 177, 45, 142, 7, 153, 39, 142, 26, 98, 234, 142, 0, 161, 20, 142, 9, 69, 181, 142, 17, 159, 207, 142, 3, 83, 183, 142, 26, 76, 148, 142, 2, 147, 13, 142, 29, 163, 203, 142, 12, 180, 206, 142, 10, 21, 1, 142, 30, 188, 21, 116, 177, 26, 79, 142, 15, 90, 180, 142, 0, 15, 181, 142, 10, 74, 93, 142, 23, 175, 36, 188, 184, 142, 5, 157, 122, 204, 157, 142, 6, 60, 246, 142, 11, 88, 197, 142, 24, 140, 242, 142, 25, 49, 83, 142, 15, 101, 121, 157, 142, 5, 188, 107, 157, 80, 110, 142, 13, 9, 227, 77, 143, 142, 6, 31, 145, 142, 29, 87, 77, 142, 15, 134, 129, 181, 144, 38, 140, 142, 28, 107, 32, 142, 0, 39, 54, 142, 2, 40, 129, 142, 10, 70, 61, 142, 12, 48, 107, 142, 31, 61, 55, 188, 228, 142, 9, 144, 44, 142, 18, 182, 46, 157, 142, 24, 63, 11, 6, 219, 142, 21, 68, 18, 142, 5, 89, 144, 110, 82, 142, 29, 20, 74, 142, 18, 37, 110, 142, 28, 157, 139, 104, 142, 16, 8, 152, 142, 24, 104, 145, 142, 14, 43, 174, 188, 9, 142, 9, 113, 122, 142, 1, 165, 110, 142, 10, 170, 220, 142, 13, 131, 148, 157, 142, 23, 179, 233, 142, 2, 44, 34, 188, 69, 142, 18, 23, 197

sub_1400011B0_idx = 0

def sub_1400011B0(a1):

global sub_1400011B0_arr

global sub_1400011B0_idx

if sub_1400011B0_idx == len(sub_1400011B0_arr):

return None

sub_1400011B0_idx += 1

return sub_1400011B0_arrsub_1400011B0_idx - 1

def __ROL1__(a, b):

return ((a << b) | (a >> (8 - b))) & 0xff

def __ROR1__(a, b):

return ((a >> b) | (a << (8 - b))) & 0xff

def HIBYTE(a):

return a

def BYTE6(a):

return a

def func0(a1):

a172 = flag[a185]

a185 += 1

def func81(a1):

v2 = __ROL1__(a179, 1)

a179 = BYTE6(v2)

a173 = a187 ^ a172

v2 = __ROR1__(a177, 2)

a177 = HIBYTE(v2)

func1_list = []

def func1(a1):

global func1_list

a2 = a173

func1_list.append(a2)

a12 += 1

def func2(a1):

a187 = a173

def func72(a1):

a181 = __ROL1__(a181, 3);

a173 = __ROL1__(a172, a187 & 7);

a179 ^= 0xA1

result = a179 ^ 0xA1;

a179 = result;

def func157(a1):

v2 = __ROR1__(a177, 1)

a177 = HIBYTE(v2);

a187 ^= 0x3F

v2 = __ROL1__(a175, 3);

a175 = BYTE6(v2);

def func45(a1):

if a178 > 0x80:

a179 = __ROL1__(a179, 1);

result = a1;

a173 = __ROR1__(a172, a187 & 7);

a186 ^= 0x21

def func130(a1):

v2 = __ROR1__(a175, 3);

a175 = HIBYTE(v2);

a173 = a187 ^ a172;

v2 = __ROL1__(a186, 1);

a186 = BYTE6(v2);

def func22(a1):

a177 = __ROR1__(a177, 2);

a173 = __ROL1__(a172, a187 & 7);

result = a174 ^ 0xB5;

a174 = result;

if a175 < 0x40:

a186 -= 1

def func135(a1):

if a175 < 0x40:

a186 = __ROR1__(a186, 1);

a173 = a187 ^ a172;

a179 ^= 0xF4

def func14(a1):

if (a177 & 0x10) != 0:

a186 = __ROR1__(a186, 1);

a173 = __ROL1__(a172, a187 & 7);

a175 += 4;

def func57(a1):

a179 = __ROL1__(a179, 1);

a173 = __ROR1__(a172, a187 & 7);

result = a175 + 3;

a175 = result;

def func188(a1):

a179 = __ROR1__(a179, 2);

a184 = sub_1400011B0(a1);

result = __ROL1__(a175, 1);

a175 = result;

def func123(a1):

if a175 < 0x80:

a179 = __ROR1__(a179, 1);

a173 = a187 ^ a172;

a186 = __ROL1__(a186, 1);

def func136(a1):

v2 = __ROR1__(a186, 2);

a186 = HIBYTE(v2);

a173 = a187 ^ a172;

v2 = __ROL1__(a186, 3);

a186 = BYTE6(v2);

def func137(a1):

if (a181 & 1) != 0:

a179 = __ROL1__(a179, 1);

a173 = __ROL1__(a172, a187 & 7);

a177 = __ROR1__(a177, 1);

def func93(a1):

a174 = __ROL1__(a174, 2);

a173 = __ROR1__(a172, a187 & 7);

a179 ^= 0x8D

result = a179 ^ 0x8D;

a179 = result;

def func115(a1):

if (a181 & 0x10) != 0:

a186 += 3;

a173 = a187 ^ a172;

a179 ^= 0x76

def func5(a1):

if not a181:

a175 += 1;

a173 = __ROL1__(a172, a187 & 7);

a174 = __ROL1__(a174, 2);

result = a183 & 0x10;

if result:

a186 -= 1;

def func138(a1):

v2 = __ROR1__(a186, 2);

a186 = HIBYTE(v2);

a173 = a187 ^ a172;

a179 ^= 0x4F

def func65(a1):

a186 = __ROL1__(a186, 1);

a173 = __ROL1__(a172, a187 & 7);

result = __ROR1__(a179, 2);

a179 = result;

def func105(a1):

if a175 < 0x40:

a186 = __ROR1__(a186, 2);

a173 = __ROR1__(a172, a187 & 7);

a179 ^= 0xE7

def func30(a1):

v2 = __ROL1__(a174, 1);

a174 = HIBYTE(v2);

a173 = a187 ^ a172;

a179 += 3;

def func42(a1):

if (a179 & 4) != 0:

a181 = __ROL1__(a181, 1);

a173 = a187 ^ a172;

a186 ^= 0x8F

def func149(a1):

if a186 > 0x80:

a186 = __ROR1__(a186, 1);

a173 = __ROL1__(a172, a187 & 7);

a175 ^= 0xA3

def func118(a1):

a179 = __ROL1__(a179, 2);

a173 = __ROR1__(a172, a187 & 7);

result = a175 + 3;

a175 = result;

def func46(a1):

a174 += 3;

a173 = a187 ^ a172;

v2 = __ROL1__(a175, 2);

a175 = HIBYTE(v2);

def func184(a1):

a177 = __ROL1__(a177, 3);

a173 = __ROL1__(a172, a187 & 7);

result = __ROR1__(a179, 2);

a179 = result;

def func111(a1):

if a179 < 0x40:

a186 = __ROR1__(a186, 2);

a173 = a187 ^ a172;

a175 |= 0xB6

a186 = __ROL1__(a186, 2);

def func178(a1):

a186 = __ROR1__(a186, 1);

a173 = __ROL1__(a172, a187 & 7);

result = __ROL1__(a175, 3);

a175 = result;

def func11(a1):

if (a174 & 1) != 0:

a175 = __ROR1__(a175, 1);

a173 = __ROR1__(a172, a187 & 7);

a178 ^= 0xC0

def func164(a1):

v2 = __ROL1__(a186, 2);

a186 = BYTE6(v2);

a173 = a187 ^ a172;

v2 = __ROR1__(a179, 1);

a179 = HIBYTE(v2);

def func176(a1):

v2 = __ROR1__(a175, 2);

a175 = HIBYTE(v2);

a173 = a187 ^ a172;

v2 = __ROL1__(a179, 1);

a179 = BYTE6(v2);

def func121(a1):

if a175 > 0x40:

a177 = __ROR1__(a177, 2);

a173 = __ROL1__(a172, a187 & 7);

a179 ^= 0xE3

def func73(a1):

if a174 > 0x40:

a175 = __ROR1__(a175, 3);

a173 = __ROR1__(a172, a187 & 7);

a181 |= 0x2E

def func156(a1):

v2 = __ROL1__(a177, 1);

a177 = HIBYTE(v2);

a173 = a187 ^ a172;

a175 += 2;

def func34(a1):

a186 += 3;

a173 = __ROL1__(a172, a187 & 7);

result = __ROL1__(a177, 1);

a177 = result;

def func125(a1):

if a181 > 0x80:

a175 = __ROR1__(a175, 2);

a173 = a187 ^ a172;

a179 = __ROL1__(a179, 1);

def func102(a1):

a175 = __ROR1__(a175, 2);

a173 = __ROL1__(a172, a187 & 7);

a179 ^= 0x48

result = a179 ^ 0x48;

a179 = result;

def func155(a1):

a179 = __ROL1__(a179, 2);

a173 = __ROR1__(a172, a187 & 7);

result = __ROR1__(a177, 1);

a177 = result;

def func82(a1):

if (a183 & 4) != 0:

a186 += 1;

a173 = a187 ^ a172;

a179 ^= 0x77

def func18(a1):

a186 += 3;

a173 = a187 ^ a172;

a183 ^= 0x33

if (a177 & 0x20) != 0:

a175 -= 1;

def func33(a1):

if a176 < 0x20:

a183 = __ROR1__(a183, 1);

a173 = __ROL1__(a172, a187 & 7);

a175 ^= 0x6F

def func99(a1):

a175 = __ROR1__(a175, 3);

a173 = __ROR1__(a172, a187 & 7);

result = __ROL1__(a177, 1);

a177 = result;

def func36(a1):

a174 += 2;

a173 = a187 ^ a172;

v2 = __ROL1__(a179, 2);

a179 = HIBYTE(v2);

def func92(a1):

if (a179 & 2) != 0:

a186 = __ROR1__(a186, 1);

a173 = __ROL1__(a172, a187 & 7);

a177 = __ROL1__(a177, 1);

def func114(a1):

v2 = __ROL1__(a183, 2);

a183 = BYTE6(v2);

a173 = a187 ^ a172;

v2 = __ROR1__(a186, 1);

a186 = HIBYTE(v2);

def func169(a1):

a179 = __ROR1__(a179, 2);

a173 = __ROL1__(a172, a187 & 7);

result = __ROL1__(a186, 1);

a186 = result;

def func117(a1):

if a175 < 0x40:

a186 = __ROR1__(a186, 1);

a173 = __ROR1__(a172, a187 & 7);

a186 = __ROL1__(a186, 1);

def func150(a1):

v2 = __ROL1__(a179, 2);

a179 = HIBYTE(v2);

a173 = a187 ^ a172;

a177 += 2;

def func7(a1):

a186 += 7;

a173 = a187 ^ a172;

v2 = __ROL1__(a178, 3);

a178 = HIBYTE(v2);

def func132(a1):

a175 = __ROL1__(a175, 1);

a173 = __ROL1__(a172, a187 & 7);

a179 ^= 0x73

result = a179 ^ 0x73;

a179 = result;

def func160(a1):

a177 = __ROL1__(a177, 2);

a173 = __ROR1__(a172, a187 & 7);

result = __ROR1__(a179, 1);

a179 = result;

def func67(a1):

a186 += 2;

a173 = a187 ^ a172;

v2 = __ROL1__(a175, 1);

a175 = HIBYTE(v2);

def func166(a1):

a177 = __ROR1__(a177, 1);

a173 = __ROL1__(a172, a187 & 7);

result = __ROL1__(a186, 2);

a186 = result;

def func109(a1):

if a181 > 0x40:

a186 = __ROR1__(a186, 1);

result = a1;

a173 = a187 ^ a172;

a179 += 2;

def func96(a1):

if (a181 & 4) != 0:

a175 = __ROR1__(a175, 1);

a173 = __ROL1__(a172, a187 & 7);

a186 = __ROR1__(a186, 2);

def func66(a1):

if (a174 & 1) != 0:

a175 = __ROR1__(a175, 1);

result = a1;

a173 = __ROR1__(a172, a187 & 7);

a179 ^= 0x31

def func4(a1):

v2 = __ROR1__(a175, 3);

a175 = HIBYTE(v2);

a173 = a187 ^ a172;

a177 += 18;

a177 -= 18;

def func112(a1):

v2 = __ROL1__(a179, 1);

a179 = HIBYTE(v2);

a173 = a187 ^ a172;

a175 += 1;

def func75(a1):

if a174 < 0x20:

a181 = __ROR1__(a181, 1);

a173 = __ROL1__(a172, a187 & 7);

a177 += 1;

def func108(a1):

a175 = __ROL1__(a175, 2);

a173 = __ROR1__(a172, a187 & 7);

a179 ^= 0x99

result = a179 ^ 0x99;

a179 = result;

def func28(a1):

v2 = __ROR1__(a177, 3);

a177 = HIBYTE(v2);

a173 = a187 ^ a172;

a179 ^= 0xE2

def func3(a1):

a175 += 5;

if (a176 & 2) != 0:

a177 = __ROL1__(a177, 1);

a173 = __ROL1__(a172, a187 & 7);

a178 ^= 0xF0

if a179:

a181 -= 1;

def func35(a1):

if a178 > 0x7F:

a175 = __ROR1__(a175, 3);

a173 = a187 ^ a172;

a186 ^= 0x33

def func148(a1):

a179 = __ROR1__(a179, 2);

a173 = __ROL1__(a172, a187 & 7);

result = __ROL1__(a177, 3);

a177 = result;

def func146(a1):

a175 = __ROL1__(a175, 2);

a173 = __ROR1__(a172, a187 & 7);

a179 ^= 0x13

result = a179 ^ 0x13;

a179 = result;

def func71(a1):

if not a179:

a183 = __ROL1__(a183, 2);

a173 = a187 ^ a172;

a186 ^= 0x57

def func127(a1):

if a179 < 0x40:

a186 = __ROR1__(a186, 3);

a173 = a187 ^ a172;

a186 = __ROL1__(a186, 2);

def func47(a1):

a186 = __ROL1__(a186, 1);

a173 = __ROL1__(a172, a187 & 7);

a179 ^= 0x73

result = a179 ^ 0x73;

a179 = result;

def func58(a1):

if not a178:

a181 = __ROR1__(a181, 3);

a173 = __ROR1__(a172, a187 & 7);

a179 ^= 0xC8

def func94(a1):

if a175 > 0x80:

a177 += 2;

a173 = a187 ^ a172;

a186 |= 0xD2

def func100(a1):

a179 = __ROL1__(a179, 1);

a173 = __ROL1__(a172, a187 & 7);

a175 ^= 0x65

result = a175 ^ 0x65;

a175 = result;

def func59(a1):

v2 = __ROL1__(a177, 1);

a177 = HIBYTE(v2);

a173 = a187 ^ a172;

a174 -= 1;

def func120(a1):

a179 = __ROR1__(a179, 1);

a173 = __ROL1__(a172, a187 & 7);

result = a175 + 2;

a175 = result;

def func86(a1):

if a181 > 0x80:

a177 = __ROR1__(a177, 2);

a173 = __ROR1__(a172, a187 & 7);

a179 ^= 0xAE

def func152(a1):

v2 = __ROL1__(a179, 1);

a179 = HIBYTE(v2);

a173 = a187 ^ a172;

v2 = __ROL1__(a186, 2);

a186 = BYTE6(v2);

def func162(a1):

v2 = __ROR1__(a179, 1);

a179 = HIBYTE(v2);

a173 = a187 ^ a172;

v2 = __ROL1__(a177, 3);

a177 = BYTE6(v2);

def func25(a1):

a181 = __ROL1__(a181, 3);

a173 = __ROL1__(a172, a187 & 7);

a175 += 2;

result = a186 & 8;

if result:

a183 = __ROR1__(a183, 1);

def func54(a1):

if a186 > 0x80:

a183 += 3;

a173 = __ROR1__(a172, a187 & 7);

a175 ^= 0x82

def func27(a1):

if a175 < 0x80:

a186 += 1;

a173 = a187 ^ a172;

a178 = __ROL1__(a178, 1);

def func52(a1):

if a178 < 0x40:

a183 = __ROR1__(a183, 1);

a173 = __ROL1__(a172, a187 & 7);

a175 += 2;

def func133(a1):

if a181 > 0x80:

a186 = __ROR1__(a186, 3);

a173 = a187 ^ a172;

a175 = __ROR1__(a175, 1);

def func142(a1):

a186 = __ROL1__(a186, 3);

a180 = sub_1400011B0(a1);

result = a179 ^ 0xA6;

a179 = result;

def func160(a1):

a177 = __ROL1__(a177, 2);

a173 = __ROR1__(a172, a187 & 7);

result = __ROR1__(a179, 1);

a179 = result;

a1 = 0 * 256

a187 = 66

a184 = 63

flag = BitVec(f'flag{i}', 8) for i in range(78)

s = Solver()

while True:

op = sub_1400011B0(a1)

if op == None:

break

if func_offsetsop == None:

exec(f'func{op}(a1)')

else:

idx = sub_1400011B0(a1) + (a180 << 8)

offset = func_offsetsop

s.add(func1_listoffset == unk_140311F61idx)

print(s.check())

m = s.model()

print(''.join([chr(m[flagi].as_long()) for i in range(78)]))

# s = Solver()

# s.add(func1_list0 == 0)

# s.add(func1_list1 == 0)

# s.add(func1_list2 == 0)

# print(s.check())

# m = s.model()

# print([m[flagi] for i in range(78)])