Solution files for Fourcore reversing chall - operator

ida_extract_constraints.py

import idautils
import idaapi
import idc

f = open('chall_constraints.txt', 'w+')

for func_addr in idautils.Functions():
    func_name = idc.get_func_name(func_addr)
    if "flag" in func_name:
        print(f"[+] Extracting constraints from {func_name}")
        func_dec = idaapi.decompile(func_addr)
        lines = str(func_dec).split('\n')
        line4 = lines[4]
        line5 = lines[5]
        constraint = line4.replace("result = (unsigned int)", "").strip(';')
        result = line5.replace("  if ( (_DWORD)result != ","").strip(')')
        if "result != " not in line5:
            f.write(f"{func_name} : ERROR!\n")
        else:
            f.write(f"{func_name} : {constraint} == {result}\n")

f.close()

solve.py

from z3 import *
s = Solver()
a1 = []

for i in range(29):
    b = BitVec("%d" % i, 16)
    a1.append(b)

s.add((a1[15] * a1[23] * a1[3] + a1[24]) == 652205 )
s.add((a1[21] * a1[25] - a1[2] + a1[8]) == 3267 )
s.add((a1[16] - a1[11] * a1[1] * a1[24]) == -1609392 )
s.add((a1[6] + a1[17] - a1[21] * a1[13]) == -3051 )
s.add((a1[6] + a1[23] * a1[22] + a1[4]) == 5454 )
s.add((a1[13] * a1[3] - a1[16] * a1[13]) == 570 )
s.add((a1[11] * a1[1] + a1[20] + a1[9]) == 13106 )
s.add((a1[19] - a1[21] * a1[10] * a1[2]) == -127361 )
s.add((a1[0] - a1[15] * a1[21] - a1[9]) == -1728 )
s.add((a1[6] - a1[16] - a1[26] * a1[27]) == -12711 )
s.add((a1[23] + a1[7] - a1[2] + a1[6]) == 143 )
s.add((a1[20] * a1[4] * a1[0] + a1[4]) == 1455459 )
s.add((a1[21] + a1[10] * a1[22] + a1[26]) == 1728 )
s.add((a1[15] + a1[17] * a1[14] + a1[10]) == 3979 )
s.add((a1[5] + a1[11] - a1[24] + a1[25]) == 205 )
s.add((a1[17] + a1[0] * a1[19] - a1[23]) == 5227 )
s.add((a1[27] + a1[26] - a1[20] - a1[7]) == 10 )
s.add((a1[26] * a1[11] * a1[23] - a1[12]) == 1416239 )
s.add((a1[23] - a1[25] - a1[3] * a1[20]) == -13213 )
s.add((a1[27] - a1[25] - a1[6] * a1[10]) == -1668 )
s.add((a1[0] + a1[16] + a1[14] * a1[5]) == 13780 )
s.add((a1[2] + a1[16] + a1[17] * a1[10]) == 1314 )
s.add((a1[17] - a1[9] * a1[5] + a1[15]) == -13025 )
s.add((a1[25] + a1[3] + a1[0] * a1[8]) == 12147 )
s.add((a1[26] * a1[18] * a1[7] + a1[0]) == 1099002 )
s.add((a1[1] * a1[20] - a1[6] + a1[3]) == 12939 )
s.add((a1[3] - a1[0] - a1[15] + a1[18]) == 60 )
s.add((a1[26] * a1[27] * a1[7] - a1[9]) == 1252632 )
s.add((a1[3] - a1[22] - a1[16] + a1[0]) == 60 )
s.add((a1[27] + a1[2] * a1[28] + a1[28]) == 12032 )
s.add((a1[27] - a1[25] * a1[14] - a1[23]) == -11678 )
s.add((a1[6] + a1[25] * a1[9] + a1[24]) == 11462 )
s.add((a1[12] + a1[19] - a1[14] * a1[6]) == -5845 )
s.add((a1[15] * a1[26] + a1[10] - a1[9]) == 5691 )
s.add((a1[15] * a1[22] - a1[13] + a1[20]) == 2517 )
s.add((a1[25] + a1[0] - a1[26] - a1[20]) == -26 )
s.add((a1[24] - a1[18] * a1[28] + a1[14]) == -9857 )
s.add((a1[16] + a1[0] - a1[2] * a1[16]) == -12426 )
s.add((a1[14] + a1[15] + a1[24] + a1[27]) == 409 )
s.add((a1[7] + a1[0] + a1[7] - a1[3]) == 186 )
s.add((a1[8] + a1[25] - a1[7] * a1[19]) == -4932 )
s.add((a1[16] - a1[14] + a1[12] * a1[6]) == 6161 )
s.add((a1[9] + a1[7] * a1[10] - a1[16]) == 3273 )
s.add((a1[22] * a1[0] * a1[1] * a1[9]) == 61953984 )
s.add((a1[2] - a1[24] - a1[3] - a1[16]) == -230 )
s.add((a1[10] + a1[5] - a1[6] + a1[20]) == 213 )
s.add((a1[18] - a1[5] - a1[12] - a1[1]) == -247 )
s.add((a1[24] - a1[11] * a1[16] + a1[7]) == -12304 )
s.add((a1[21] * a1[4] * a1[21] * a1[5]) == 15403905 )
s.add((a1[0] * a1[18] * a1[8] - a1[5]) == 1193285 )
s.add((a1[27] * a1[24] + a1[12] + a1[23]) == 14481 )
s.add((a1[27] - a1[8] * a1[5] * a1[27]) == -1533756 )
s.add((a1[1] + a1[8] + a1[0] + a1[17]) == 363 )
s.add((a1[7] * a1[28] - a1[15] * a1[20]) == 3967 )
s.add((a1[1] - a1[19] * a1[11] * a1[9]) == -687537 )
s.add((-a1[22] - a1[2]) == -165 )
s.add((a1[20] * a1[6] + a1[4] * a1[19]) == 12312 )
s.add((a1[28] - a1[25] - a1[18] + a1[27]) == 16 )
s.add((a1[0] + a1[21] + a1[4] - a1[13]) == 163 )
s.add((a1[11] + a1[16] + a1[4] + a1[4]) == 470 )
s.add((a1[24] + a1[3] + a1[9] - a1[17]) == 320 )
s.add((a1[28] * a1[16] + a1[1] * a1[17]) == 14571 )
s.add((a1[0] - a1[8] * a1[19] + a1[14]) == -5864 )
s.add((a1[11] + a1[22] * a1[23] * a1[26]) == 586196 )
s.add((a1[10] * a1[9] * a1[25] - a1[12]) == 372317 )
s.add((a1[28] * a1[4] * a1[22] - a1[9]) == 596190 )
s.add((a1[7] - a1[15] * a1[6] - a1[9]) == -2667 )
s.add((a1[10] - a1[10] * a1[1] * a1[1]) == -406560)
s.add((a1[28] - a1[8] * a1[1] - a1[5]) == -13001 )
s.add((a1[19] * a1[14] * a1[17] * a1[11]) == 23488608 )
s.add((a1[25] * a1[14] - a1[0] * a1[23]) == 462 )
s.add((a1[1] + a1[9] - a1[23]) == a1[5])
s.add((a1[8] * a1[27] - a1[14] - a1[9]) == 13106 )
s.add((a1[23] - a1[1] * a1[1] + a1[5]) == -12096 )
s.add((a1[0] + a1[28] - a1[13] - a1[23]) == -2 )
s.add((a1[24] - a1[6] * a1[16] * a1[17]) == -181639 )
s.add((a1[14] - a1[11] - a1[24] + a1[21]) == -90 )
s.add((a1[28] + a1[4] - a1[0] * a1[12]) == -12118 )
s.add((a1[18] + a1[27] * a1[24] + a1[8]) == 14467 )
s.add((a1[18] + a1[17] - a1[16] + a1[1]) == 136 )
s.add((a1[8] * a1[11] - a1[22] * a1[28]) == 8724 )
s.add((a1[5] * a1[14] * a1[27] * a1[4]) == 190278540 )
s.add((a1[16] + a1[27] + a1[3] + a1[12]) == 457 )
s.add((a1[7] * a1[15] * a1[0] - a1[11]) == 524980 )
s.add((a1[12] * a1[11] * a1[0] - a1[12]) == 1431551 )
s.add((a1[24] * a1[18] + a1[18] * a1[6]) == 17600 )
s.add((a1[9] + a1[9] - a1[23] + a1[13]) == 213 )
s.add((a1[7] - a1[22] * a1[13] + a1[22]) == -4413 )
s.add((a1[15] - a1[7] - a1[7] + a1[5]) == -31 )
s.add((a1[7] - a1[2] - a1[22] + a1[23]) == 44 )
s.add((a1[16] + a1[24] - a1[3] - a1[1]) == 8 )
s.add((a1[16] - a1[0] * a1[2] * a1[19]) == -620460 )
s.add((a1[9] - a1[10] * a1[27] - a1[13]) == -3743 )
s.add((a1[18] * a1[20] + a1[13] - a1[15]) == 11643 )
s.add((a1[0] - a1[19] * a1[20] - a1[17]) == -5963 )
s.add((a1[5] + a1[1] - a1[28] - a1[12]) == 4 )
s.add((a1[12] + a1[8] + a1[14] * a1[21]) == 4132 )
s.add((a1[18] + a1[24] * a1[26] * a1[23]) == 1526350 )
s.add((a1[18] + a1[2] - a1[19] + a1[27]) == 279 )
s.add((a1[19] - a1[14]) == -66 )

if(s.check() == sat):
    sol = s.model()
    flag = ""
    for i in range(len(a1)):
        c = a1[i]
        flag += chr(int(str(sol[c])))

print(flag)

#four{s3cur!ty_v4l!d4t!0n}core