flag_check_appliance_v2_FINAL.raw — Hack.lu2026

Description

We put the flag into the kernel command line and the flag checker ...where???

The archive supplies a raw bootable disk, OVMF firmware files, and run.sh. Find the input accepted by the appliance without assuming the flag is stored as plaintext in the image.

Analysis

run.sh converts the supplied candidate, not a stored flag, into arguments ctf.byte.0=.. ctf.byte.1=.. and passes them via SMBIOS io.systemd.boot.kernel-cmdline-extra. The GPT EFI partition begins at sector 2048; the root-x86-64 partition begins at sector 75776 and contains SquashFS. The checker is not a single conventional executable: the extracted root has approximately 7,910 UUID-named services in usr/lib/systemd/system/ plus ten service templates.

Each graph node has OnSuccess and OnFailure edges; some have Requisite=<template>@<byte-index>.service. The templates use ConditionKernelCommandLine=ctf.byte.%i=<two-digit hex> for sets of byte values. Eight sets test individual bits, one permits every possible byte, and another tests whether ctf.byte.%i exists. Terminal units print CTF_RESULT=ACCEPT or CTF_RESULT=REJECT. Consequently, the graph implements an obfuscated byte-by-byte checker. The existence test at index 88 enforces the absence of a 89th byte.

Solution

Extract the root partition from the organizer's raw image, then unpack the filesystem:

dd if=public/flag_check_appliance_v2_FINAL.raw of=root.squashfs bs=512 skip=75776
unsquashfs -d rootfs root.squashfs

Represent each input byte as an 8-bit Z3 variable and each UUID service as a Boolean meaning "this node eventually accepts." A normal /usr/bin/true service takes its success edge; a node with a Requisite follows its success or failure edge according to the template predicate. Assert that the entry service accepts, constrain the public flag{...} format and length, and solve. Finally, evaluate the actual graph with the resulting bytes rather than trusting only the symbolic model. Run this script from the extraction directory after installing z3-solver:

#!/usr/bin/env python3
from pathlib import Path
import re
import z3

directory = Path('rootfs/usr/lib/systemd/system')
unit_name = re.compile(r'[0-9a-f]{8}(?:-[0-9a-f]+)+\.service\Z')
nodes = {
    file.name: dict(re.findall(r'(?m)^([A-Za-z]+)=(.*)$', file.read_text()))
    for file in directory.glob('*.service') if unit_name.fullmatch(file.name)
}
templates = {
    file.name: set(int(value, 16) for value in
                   re.findall(r'ctf\.byte\.%i=([0-9a-f]{2})', file.read_text()))
    for file in directory.glob('*@.service')
    if re.match(r'[0-9a-f]{8}-', file.name)
}

entry = 'c821258a-35fa-444e-8562-353fb1e10397.service'
accept = 'acad129c-47e0-4e2a-870d-890a47551dde.service'
reject = 'a0e15bd1-d456-4dd7-9f0f-10845dfcd1bd.service'
byte = [z3.BitVec(f'byte_{index}', 8) for index in range(88)]
state = {name: z3.Bool('accept_' + name[:-8].replace('-', '_'))
         for name in nodes}
solver = z3.Solver()
solver.set(timeout=180000)

def outcome(name):
    if name == accept:
        return z3.BoolVal(True)
    if name == reject or name not in state:
        return z3.BoolVal(False)
    return state[name]

def requirement(node):
    match = re.fullmatch(r'([0-9a-f-]+)@(\d+)\.service', node['Requisite'])
    if not match:
        raise ValueError(node['Requisite'])
    template, index = match.group(1) + '@.service', int(match.group(2))
    allowed = templates[template]
    if index >= len(byte):
        return z3.BoolVal(False)
    if not allowed:  # Presence-only ConditionKernelCommandLine=ctf.byte.%i
        return z3.BoolVal(True)
    if len(allowed) == 256:
        return z3.BoolVal(True)
    for bit in range(8):
        if allowed == {value for value in range(256) if value & (1 << bit)}:
            return (byte[index] & (1 << bit)) != 0
    raise ValueError('Unrecognized predicate: ' + template)

for name, node in nodes.items():
    if name in (accept, reject):
        continue
    success = outcome(node.get('OnSuccess'))
    failure = outcome(node.get('OnFailure'))
    expression = (z3.If(requirement(node), success, failure)
                  if node.get('Requisite') else success)
    solver.add(state[name] == expression)

solver.add(state[entry])
for index, value in enumerate(b'flag{'):
    solver.add(byte[index] == value)
solver.add(byte[-1] == ord('}'))
assert solver.check() == z3.sat
model = solver.model()
candidate = bytes(model.eval(value, model_completion=True).as_long()
                  for value in byte)

def trace(data):
    current, seen = entry, set()
    while current not in (accept, reject):
        if current in seen or current not in nodes:
            raise ValueError('cycle or missing service')
        seen.add(current)
        node = nodes[current]
        if 'Requisite' not in node:
            current = node['OnSuccess']
            continue
        match = re.fullmatch(r'([0-9a-f-]+)@(\d+)\.service', node['Requisite'])
        template, index = match.group(1) + '@.service', int(match.group(2))
        values = templates[template]
        passed = index < len(data) and (not values or data[index] in values)
        current = node['OnSuccess' if passed else 'OnFailure']
    return current, len(seen)

terminal, steps = trace(candidate)
mutated = candidate[:10] + bytes([candidate[10] ^ 1]) + candidate[11:]
assert terminal == accept and trace(mutated)[0] == reject
print(f'Accepted path: {steps} services; modified input rejects.')
print('Recovered candidate: flag{REDACTED}')

The local offline trace reaches the accepting terminal after 3,957 nodes; a one-byte change reaches the rejecting terminal. The recovered value is deliberately not stored in this writeup.

Key Indicators

• A candidate is split into ctf.byte.N=hex kernel-command-line entries rather than checked by a visible executable.
• The extracted root contains thousands of random-looking systemd services connected through Requisite, OnSuccess, and OnFailure.
• Template units group ConditionKernelCommandLine values into 128-element bit predicates, enabling a symbolic model of the entire checker.