Logo
Overview
[SECCON CTF 14] Mini Bloat writeup

[SECCON CTF 14] Mini Bloat writeup

andso andso
December 14, 2025
4 min read
rev SECCON CTF 14 Quals

✨ 크립토 공짜 다운로드 ✨

TL;DR

The cilent bundle embeds 25 “boolean constraint puzzles” as a base64 + gzip JSON blob Each day asks for a 32bit unsigned integer satisfying several bitwise expression

Analysis

Main logic is dist/_next/static/chunks/app/page-fdcc665989738875.js

Inside the bundle there is a long string starting with H4sIA It is base64 encoded, gzip compressed, JSON after decompression

Analysis After decoding it

{ "day": 1, "eqExprs": [...], "maskExprs": [...] }

The page turns each string expression into a runtime predicate with new Function ("x", "return ("" + expr + ");")

Each predicate is a boolean check over a 32 bit value (x >>> 0 style) Every expression ends with === 1

Once all 25 solutions are correct, the app derives a key material and decrypts

  • pepper = "boolean-advent-2025-pepper"
  • solutions_bytes = concat_be32(solution[day]) for day=1..25 (100 bytes)
  • seed = SHA256(pepper || solutions_bytes || pepper)
  • ciphertext = base64decode("uJVY4mJFB6T9yppuCdGFmTW1O5GZ06yw4OTVml4VNOw=")
  • keystream = SHA256(seed || counter_be32) for counter = 0,1,2,... concatenated until long enough
  • plaintext = ciphertext XOR keystream

Exploit

  1. Extracts and decompresses the embedded JSON blob
  2. Parses the JS expressions into Z3 BitVec constraints
  3. Solves each day (and checks uniqueness)
  4. Re-implements the SHA-256 keystream XOR to print the final flag
#!/usr/bin/env python3
import base64
import gzip
import json
import re
from dataclasses import dataclass


from z3 import BitVec, BitVecVal, LShR, Solver, sat




JS_BUNDLE = "dist/_next/static/chunks/app/page-fdcc665989738875.js"




def extract_puzzles(bundle_path: str) -> list[dict]:
    with open(bundle_path, "r", encoding="utf-8", errors="ignore") as f:
        s = f.read()
    m = re.search(r'"(H4sIA[^"]+)"', s)
    if not m:
        raise RuntimeError("Could not find embedded base64 gzip puzzle blob")
    blob_b64 = m.group(1)
    raw = gzip.decompress(base64.b64decode(blob_b64))
    return json.loads(raw.decode("utf-8"))




@dataclass
class Token:
    kind: str
    value: str




def tokenize(expr: str) -> list[Token]:
    tokens: list[Token] = []
    i = 0
    while i < len(expr):
        ch = expr[i]
        if ch.isspace():
            i += 1
            continue
        if expr.startswith(">>>", i):
            tokens.append(Token("op", ">>>"))
            i += 3
            continue
        if expr.startswith("===", i):
            tokens.append(Token("op", "==="))
            i += 3
            continue
        if expr.startswith("<<", i):
            tokens.append(Token("op", "<<"))
            i += 2
            continue
        if expr.startswith(">>", i):
            tokens.append(Token("op", ">>"))
            i += 2
            continue
        if ch in "()~+-*^&|":
            tokens.append(Token("op", ch))
            i += 1
            continue
        if ch.isdigit():
            j = i + 1
            while j < len(expr) and expr[j].isdigit():
                j += 1
            tokens.append(Token("num", expr[i:j]))
            i = j
            continue
        if ch == "x":
            tokens.append(Token("id", "x"))
            i += 1
            continue
        raise RuntimeError(f"Unexpected character at {i}: {expr[i:i+20]!r}")
    return tokens




class Parser:
    def __init__(self, tokens: list[Token], x):
        self.tokens = tokens
        self.i = 0
        self.x = x


    def _peek(self) -> Token | None:
        return self.tokens[self.i] if self.i < len(self.tokens) else None


    def _eat(self, expected: str | None = None) -> Token:
        tok = self._peek()
        if tok is None:
            raise RuntimeError("Unexpected end of input")
        if expected is not None and tok.value != expected:
            raise RuntimeError(f"Expected {expected}, got {tok.value}")
        self.i += 1
        return tok


    def parse(self):
        out = self._parse_equality()
        if self._peek() is not None:
            raise RuntimeError(f"Trailing tokens at {self._peek()}")
        return out


    def _parse_equality(self):
        lhs = self._parse_or()
        op = self._peek()
        if op is None or op.value != "===":
            raise RuntimeError("Expected === at top-level (all constraints should end with '=== 1')")
        self._eat("===")
        rhs = self._parse_or()
        return lhs == rhs


    def _parse_or(self):
        node = self._parse_xor()
        while (tok := self._peek()) is not None and tok.value == "|":
            self._eat("|")
            node = node | self._parse_xor()
        return node


    def _parse_xor(self):
        node = self._parse_and()
        while (tok := self._peek()) is not None and tok.value == "^":
            self._eat("^")
            node = node ^ self._parse_and()
        return node


    def _parse_and(self):
        node = self._parse_shift()
        while (tok := self._peek()) is not None and tok.value == "&":
            self._eat("&")
            node = node & self._parse_shift()
        return node


    def _parse_shift(self):
        node = self._parse_add()
        while (tok := self._peek()) is not None and tok.value in ("<<", ">>", ">>>"):
            op = tok.value
            self._eat(op)
            rhs = self._parse_add()
            if op == "<<":
                node = node << rhs
            elif op == ">>":
                node = node >> rhs
            else:
                node = LShR(node, rhs)
        return node


    def _parse_add(self):
        node = self._parse_mul()
        while (tok := self._peek()) is not None and tok.value in ("+", "-"):
            op = tok.value
            self._eat(op)
            rhs = self._parse_mul()
            node = node + rhs if op == "+" else node - rhs
        return node


    def _parse_mul(self):
        node = self._parse_unary()
        while (tok := self._peek()) is not None and tok.value == "*":
            self._eat("*")
            node = node * self._parse_unary()
        return node


    def _parse_unary(self):
        tok = self._peek()
        if tok is not None and tok.value in ("~", "-"):
            op = tok.value
            self._eat(op)
            node = self._parse_unary()
            return ~node if op == "~" else -node
        return self._parse_primary()


    def _parse_primary(self):
        tok = self._peek()
        if tok is None:
            raise RuntimeError("Unexpected end of input in primary")
        if tok.kind == "num":
            self._eat()
            return BitVecVal(int(tok.value) & 0xFFFFFFFF, 32)
        if tok.kind == "id" and tok.value == "x":
            self._eat()
            return self.x
        if tok.value == "(":
            self._eat("(")
            node = self._parse_or()
            self._eat(")")
            return node
        raise RuntimeError(f"Unexpected token in primary: {tok}")




def parse_js_constraint(expr: str, x):
    tokens = tokenize(expr)
    return Parser(tokens, x).parse()




def solve_day(day: dict) -> int:
    x = BitVec("x", 32)
    s = Solver()
    for ex in day["eqExprs"] + day["maskExprs"]:
        s.add(parse_js_constraint(ex, x))
    if s.check() != sat:
        raise RuntimeError(f"Unsat for day {day['day']}")
    m = s.model()
    val = m[x].as_long() & 0xFFFFFFFF
    # Uniqueness check
    s2 = Solver()
    for ex in day["eqExprs"] + day["maskExprs"]:
        s2.add(parse_js_constraint(ex, x))
    s2.add(x != BitVecVal(val, 32))
    if s2.check() == sat:
        raise RuntimeError(f"Multiple solutions for day {day['day']} (one is {val})")
    return val




def sha256(data: bytes) -> bytes:
    import hashlib


    return hashlib.sha256(data).digest()




def derive_final_flag(solutions_by_day: dict[int, int]) -> str:
    on = "boolean-advent-2025-pepper".encode("utf-8")
    # 4 bytes per day, big-endian, in day order 1..25
    sol_bytes = bytearray()
    for day in range(1, 26):
        v = solutions_by_day[day] & 0xFFFFFFFF
        sol_bytes += bytes([(v >> 24) & 0xFF, (v >> 16) & 0xFF, (v >> 8) & 0xFF, v & 0xFF])
    seed = sha256(on + sol_bytes + on)


    ciphertext = base64.b64decode("uJVY4mJFB6T9yppuCdGFmTW1O5GZ06yw4OTVml4VNOw=")


    # Expand with SHA-256(seed || counter_be32) blocks
    keystream = bytearray()
    counter = 0
    while len(keystream) < len(ciphertext):
        ctr = counter.to_bytes(4, "big", signed=False)
        keystream += sha256(seed + ctr)
        counter += 1
    keystream = keystream[: len(ciphertext)]


    plaintext = bytes(c ^ k for c, k in zip(ciphertext, keystream))
    return plaintext.decode("utf-8", errors="strict")




def main():
    puzzles = extract_puzzles(JS_BUNDLE)
    solutions: dict[int, int] = {}
    for day in puzzles:
        d = int(day["day"])
        solutions[d] = solve_day(day)


    flag = derive_final_flag(solutions)
    print(flag)




if __name__ == "__main__":
    main()

flag