back to homepage

SmileyCTF 2025

I played a few challenges in smileyCTF.

rev/Success

We are given Haskell code of this form, consisting of 70 nested if statements involving arithmetic and bitwise operations on random character pairs:

checkFlag :: String -> IO ()
checkFlag flag = do
    if length flag /= 39
        then do
            putStrLn "bruh its 39 characters long"
            exitFailure
        else do
            let chars :: [Integer]
                chars = map fromIntegral . map fromEnum $ flag
            if (*) (chars !! 37) (chars !! 15) == 3366 then do
                if (+) (chars !! 8) (chars !! 21) == 197 then do
                    if (*) (chars !! 8) (chars !! 13) == 9215 then do
                        if (*) (chars !! 0) (chars !! 3) == 2714 then do
                            if (+) (chars !! 3) (chars !! 21) == 159 then do
                                if (*) (chars !! 1) (chars !! 20) == 5723 then do
                                    if (.|.) (chars !! 6) (chars !! 37) == 105 then do
                                        if (*) (chars !! 11) (chars !! 7) == 11990 then do
                                            if (.&.) (chars !! 29) (chars !! 25) == 100 then do
... etc.

We can simply copy these constraints into a Z3 script to solve for the flag.

from z3 import *

s = Solver()
v = [BitVec(f"v{i}", 32) for i in range(39)]

s.add(v[37] * v[15] == 3366)
s.add(v[8] + v[21] == 197)
s.add(v[8] * v[13] == 9215)
s.add(v[0] * v[3] == 2714)
s.add(v[3] + v[21] == 159)
s.add(v[1] * v[20] == 5723)
s.add(v[6] | v[37] == 105)
s.add(v[11] * v[7] == 11990)
s.add(v[29] & v[25] == 100)
... # more conditions

assert s.check() == sat
print("".join(chr(s.model().eval(c).as_long()) for c in v))
# result: .;,;.{imagine_if_i_made_it_compiled!!!}

rev/fORtran

IDA gives this code for the main function:

It seems all of the function calls are red herrings, as they do nothing to effect the program. Cleaning up the decompilation, we are left with essentially this:

The program collapses the input into a single number (by summing) then iterates some process on this number, where the residuals must be ASCII. Again, a simple Z3 script is sufficient.

from z3 import *

dword_4020 = [...]

s = BitVec("s", 32)

solver = Solver()
v = s
for i in range(28):
    v = (4919 * v) ^ 0xDEADBEEF
    res = dword_4020[i] ^ (v & 0xFF)
    solver.add(res >= 32)
    solver.add(res <= 126)

assert solver.check() == sat
v = solver.model()[s].as_long()
for i in range(28):
    v = (4919 * v) ^ 0xDEADBEEF
    res = dword_4020[i] ^ (v & 0xFF)
    print(end=chr(res))
print()
# result: .;,;.{t00_e4sy_h4h4_f0rtr4n}

rev/Easy Come Easy Go

So IDA gives this disgusting code:

From it we see what appears to be a length check on the input followed by goroutines running on the input. These are the goroutines:

The third goroutine is important; it seems to use the other two. The elem array forms a permutation. Each index i is permuted by elem and passed into the first channel. The result is XORed with the input byte. Then, this data is passed into the second channel which XORs with some array. We want this byte to be equal to expected_results. Essentially, its just a bunch of XORs. We could probably solve this by XORing manually, but here is a Z3 script nevertheless.

from z3 import *

magic_data = [...] # v5 from main_main_func1
xor_data = [...] # v5 from main_main_func2
expected_results = [...] # v10 from main_main_func3
elem = [...] # elem from main_main_func3

s = Solver()
input = [BitVec(f"v{i}", 8) for i in range(24)]
for i in range(24):
    s.add(magic_data[elem[i]] ^ input[i] ^ xor_data[i] == expected_results[i])

assert s.check() == sat
print("".join(chr(s.model()[c].as_long()) for c in input))
# result: .;,;.{goh3m1an_rh4p50dy}

crypto/never enough

The point of this challenge is quite obvious, the difficultly lies in the fact that we are given occluded (top 20 bits) samples. Indeed, the program notes itself that we are 328 bits short of the 19968 bits needed to fully solve for the state.

from random import getrandbits
from Crypto.Cipher import AES
from hashlib import sha256
danger = 624*32 # i hear you need this much.
given = []
key = ""
for _ in range(danger//20 - 16): # should be fine if im only giving u this much :3
    x = getrandbits(32)
    # we share <3
    key += str(x % 2**12)
    given.append(x >> 12)

key = key[:100]
key = sha256(key.encode()).digest()
flag = open("flag.txt", "rb").read().strip()
cipher = AES.new(key, AES.MODE_ECB)
print(given)
print(cipher.encrypt(flag + b"\x00" * (16 - len(flag) % 16)).hex())

This challenge actually gave me an opportunity to look at Mersenne twister in more depth. I understand it better now. I wrote this general solver, adopted from the code given by icemonster:

Its ~30x faster since I swapped out Z3 for bitwuzla. Also, we don't need to fully solve for the state (its not going to be right anyway since we have so few bits). Instead, we just extract the numbers from the first internal state. Empirically, I found it to be completely correct except for the first number, which is wrong for some reason. Not a problem; we can just bruteforce it. Here is the code for the challenge, it takes only 8 seconds:

ut = Untwister()
for x in given:
    ut.submit(bin(x)[2:] + 12 * '?')

guess = ut.solve()
for i in range(2**12):
    key = str(i)
    for x in guess[1:]:
        key += str(x % 2**12)
    key = key[:100]
    key = sha256(key.encode()).digest()
    cipher = AES.new(key, AES.MODE_ECB)
    s = cipher.decrypt(bytes.fromhex(encrypted_data))
    if s[0] == ord('.'):
        print(s) # prints 17 lines, one of which contains the actual flag.