SmileyCTF 2025

Success

Rev

avoid it at all costs

from z3 import *

solver = Solver()
chars = [BitVec(f'c_{i}', 32) for i in range(39)]

solver.add(chars[37] * chars[15] == 3366)
solver.add(chars[8] + chars[21] == 197)
solver.add(chars[8] * chars[13] == 9215)
solver.add(chars[0] * chars[3] == 2714)
solver.add(chars[3] + chars[21] == 159)
solver.add(chars[1] * chars[20] == 5723)
solver.add((chars[6] | chars[37]) == 105)
solver.add(chars[11] * chars[7] == 11990)
solver.add((chars[29] & chars[25]) == 100)
solver.add((chars[16] | chars[29]) == 127)
solver.add(chars[20] - chars[6] == -8)
solver.add(chars[21] + chars[20] == 197)
solver.add(chars[2] + chars[36] == 77)
solver.add(chars[35] * chars[11] == 3630)
solver.add(chars[4] * chars[3] == 2714)
solver.add((chars[35] ^ chars[6]) == 72)
solver.add(chars[25] + chars[24] == 221)
solver.add(chars[14] * chars[36] == 3465)
solver.add((chars[15] - chars[11]) - 148 == -156)
solver.add(chars[37] + chars[17] == 138)
solver.add((chars[1] ^ chars[38]) == 70)
solver.add(chars[9] + chars[29] == 212)
solver.add(chars[30] - chars[10] == 7)
solver.add(chars[10] + chars[33] == 206)
solver.add(chars[7] * chars[15] == 11118)
solver.add(chars[28] * chars[14] * 55 == 641025)
solver.add(((chars[7] | chars[4]) | 216) == 255)
solver.add(chars[24] + chars[4] == 151)
solver.add(chars[2] * chars[30] == 4928)
solver.add(chars[5] + chars[22] == 224)
solver.add((chars[18] | chars[36]) == 127)
solver.add(chars[13] + chars[34] == 195)
solver.add((chars[9] | chars[17]) == 111)
solver.add(chars[12] * chars[9] == 10403)
solver.add((chars[25] ^ chars[27]) == 23)
solver.add((chars[13] ^ chars[34]) == 59)
solver.add(chars[18] + chars[31] == 200)
solver.add(chars[17] + chars[32] == 213)
solver.add(chars[2] * chars[12] == 4444)
solver.add(chars[24] * chars[31] == 11025)
solver.add(chars[5] * chars[0] == 5658)
solver.add((chars[10] + chars[32]) + 228 == 441)
solver.add(chars[35] * chars[0] == 1518)
solver.add((chars[30] | chars[8]) == 113)
solver.add(chars[28] - chars[34] == 11)
solver.add(chars[26] * chars[14] == 9975)
solver.add(chars[31] * chars[22] == 10605)
solver.add(chars[26] * chars[32] * 239 == 2452140)
solver.add(chars[28] * chars[38] == 13875)
solver.add(chars[18] + chars[16] == 190)
solver.add((chars[27] + chars[26]) + 96 == 290)
solver.add(chars[22] - chars[38] == -24)
solver.add(chars[33] + chars[5] == 224)
solver.add(chars[19] * chars[16] == 10355)
solver.add(chars[27] + chars[1] == 158)
solver.add(chars[33] + chars[12] == 202)
solver.add(chars[19] * chars[23] == 10355)

result = solver.check()
model = solver.model()
flag = ''.join(chr(model[chars[i]].as_long()) for i in range(39))
print(flag)

└─$ .;,;.{imagine_if_i_made_it_compiled!!!}

fORtran

Rev

forensics and fortran... basically the same right?

dword_4020 = [
    0xBF, 0xF3, 0x3B, 0x25, 0xB3, 0x2F, 0x97, 0x1A, 0xD9, 0xBF,
    0xAA, 0xA2, 0xA6, 0x55, 0xC4, 0xCA, 0x15, 0x90, 0x93, 0x51,
    0x8B, 0x34, 0x41, 0x6E, 0x0B, 0x24, 0xF1, 0xBB
]

for key_sum in range(768, 8065):
    v27 = key_sum
    flag = ""
    
    for byte_val in dword_4020:
        v27 = (4919 * v27) & 0xFFFFFFFF
        v27 ^= 0xDEADBEEF
        flag_byte = byte_val ^ (v27 & 0xFF)
        
        if not (31 < flag_byte <= 126):
            break
        
        flag += chr(flag_byte)
    else:
        print(flag)
        break

└─$.;,;.{t00_e4sy_h4h4_f0rtr4n}

rorecovery1

Forensics | DidNotSolve

I wasn’t able to find the flag, but this was a very creative challenge involving analysis of a Roblox binary.

We were given a corrupted Roblox binary. Upon inspecting the file, both the header and footer contained an unusual rblxsignature. By referencing the Roblox Binary Model Format and comparing it with a sample file downloaded from Roblox Studio, we are able to reconstruct the original binary structure.

given rorecovery1

sample.rbxl

fixed_rorecovery1.rbxl