HyperSonic CTF Writeup CTF/Wargame

HyperSonic CTF 2026 NORfuscated Writeup

HyperSonic CTF 2026 NORfuscated 문제 풀이HyperSonic CTF 2026 NORfuscated writeup

Part 12 of 17 3 min read4 min read
#HyperSonic CTF#CTF#Writeup#Reversing
Contents

개요

NORfuscated는 입력 검증 로직이 NOR gate 회로로 구성된 reversing 문제입니다. 제공된 프로그램은 심볼이 제거된 64비트 PIE ELF입니다. 프로그램은 입력을 받은 뒤 Wrong! 또는 Correct!를 출력합니다.

확인한 조건은 다음과 같습니다.

  • 카테고리: reversing
  • 목표: Correct!가 출력되는 68바이트 입력을 찾습니다.
  • 입력 조건: 개행을 제거한 뒤 길이가 정확히 68바이트여야 합니다.

검증은 직렬화된 Boolean 회로로 이루어집니다. 문자열을 직접 비교하는 부분은 보이지 않고, 입력 비트가 회로에 들어가 최종 출력 비트가 1인지 검사합니다.

문제 분석

풀이에서 사용하는 표기는 다음과 같습니다.

  • wire[i]: Boolean 회로의 i번 wire 값입니다.
  • gate: (dst, a, b) 형태의 NOR gate입니다.
  • input_groups: 각 입력 바이트의 비트가 어떤 wire에 대응되는지 나타내는 목록입니다.
  • outputs: 최종 출력으로 읽는 wire 목록입니다.

프로그램에서 바로 확인되는 출력 문자열은 다음과 같습니다.

text
Enter flag:
Wrong!
Correct!

이 문자열만으로는 정답을 비교하는 구조가 드러나지 않습니다. 실제 검증 흐름은 입력 길이를 확인한 뒤, 입력 비트를 회로의 입력 wire에 배치하고, NOR gate를 순서대로 평가하는 방식입니다.

회로에서 각 gate는 다음 연산을 수행합니다.

text
wire[dst] = NOT (wire[a] OR wire[b])

모든 연산은 NOR 하나로만 구성됩니다. 따라서 검증 로직 전체를 입력 비트에 대한 Boolean 제약식으로 바꿀 수 있습니다.

직렬화된 회로 데이터는 다음 형식으로 파싱합니다.

text
u32 gate_count
gate_count * (u32 dst, u32 a, u32 b)
u32 output_count
output_count * u32 output_wire
u32 input_group_count
input_group_count * (u32 bit_count, bit_count * u32 input_wire)

파싱 결과는 다음과 같습니다.

text
gate_count        = 344048
output_count      = 1
output_wire       = 344592
input_group_count = 68
bits per group    = 8
input_bits        = 544

파싱 결과를 보면 입력 68바이트가 총 544개의 입력 비트로 확장되고, 많은 NOR gate를 거쳐 하나의 출력 wire로 모입니다. 최종적으로 wire[344592]가 참이 되는 입력을 찾으면 됩니다.

핵심 아이디어

각 NOR gate의 입출력 관계는 Boolean 제약식 하나로 표현됩니다. 그래서 프로그램을 직접 역산하지 않고 회로 전체를 SAT 문제로 바꿨습니다.

전체 gate 수는 344048개로 많지만, 최종 출력 wire에 영향을 주지 않는 gate까지 모두 다룰 필요는 없습니다. outputs에서 시작해 각 gate의 입력 wire를 역방향으로 따라가면, 출력 계산에 필요한 wire 집합이 나옵니다. 이후 이 집합에 포함된 gate만 solver에 추가합니다.

풀이 전략은 다음과 같습니다.

text
1. 회로 데이터를 파싱한다.
2. 최종 출력 wire에 영향을 주는 wire만 역추적한다.
3. 입력 68바이트를 z3.BitVec로 둔다.
4. 각 입력 비트를 대응되는 wire에 연결한다.
5. NOR gate를 Boolean 제약식으로 추가한다.
6. 최종 출력 wire가 true가 되도록 solver에 요청한다.

복원된 입력은 실제로 제출 가능한 문자열이어야 하므로, solver에는 printable ASCII 조건을 함께 추가했습니다. 이 제한을 넣은 상태에서도 sat가 나왔고 검증을 통과했습니다.

풀이 과정

Step 1. 입력 길이와 출력 조건 확인

검증 로직은 개행을 제거한 뒤 입력 길이가 0x44, 즉 68바이트인지 확인합니다. 길이가 맞지 않으면 회로 평가까지 가지 못합니다.

따라서 solver에서 만들어야 하는 값은 68개의 바이트입니다. 각 바이트는 8개의 비트로 나뉘어 총 544개의 회로 입력 wire에 연결됩니다.

Step 2. 직렬화된 회로 파싱

회로 데이터는 u32 값들의 배열처럼 저장되어 있습니다. 처음에는 gate 개수가 나오고, 이후 (dst, a, b) 3개 값이 반복됩니다. 그 뒤에는 출력 wire 목록과 입력 비트 매핑이 이어집니다.

파싱 후 첫 번째 바이트는 wire[1]부터 wire[8]까지 연결되고, 두 번째 바이트는 wire[9]부터 wire[16]까지 연결되는 식입니다. 최종 출력은 하나이며, 대상 wire는 344592입니다.

이 단계에서 얻은 정보로 solver가 z3.BitVec로 표현한 입력 바이트와 회로 wire를 연결합니다.

Step 3. 출력 wire에 필요한 gate 추적

모든 gate를 solver에 넣어도 풀 수는 있지만, 불필요한 제약식이 많아집니다. 따라서 output_wire에서 시작해 해당 wire를 만드는 gate를 찾고, 그 gate의 입력인 a, b를 다시 추적합니다.

이를 반복하면 최종 출력에 영향을 주는 wire 집합을 얻습니다. 이후 gate를 순회하면서 dst가 이 집합에 포함된 경우에만 제약식을 추가합니다.

Step 4. NOR 제약식으로 변환

각 입력 바이트는 z3.BitVec로 만들고, input_groups에 따라 비트 단위로 Boolean wire에 대응시킵니다.

text
wire[input_wire] = selected input bit is 1

그 다음 NOR gate는 다음 Boolean 식으로 바꿉니다.

text
wire[dst] = Not(Or(wire[a], wire[b]))

마지막으로 wire[344592]가 true라는 조건을 추가하면, solver는 이를 만족하는 68바이트 입력을 찾을 수 있습니다.

Exploit / Solver

solver는 회로를 파싱하고, 출력에 필요한 gate만 골라 z3 제약식으로 변환한 뒤, 모델에서 바이트 값을 복원합니다. 회로 데이터의 시작 위치와 길이는 분석에서 확인한 0x4FFC, 0x3F08E0을 사용했습니다.

python
import struct

import z3


RODATA_OFF = 0x4FFC
RODATA_LEN = 0x3F08E0
INPUT_LEN = 68


def parse_circuit(program):
    blob = program[RODATA_OFF : RODATA_OFF + RODATA_LEN]
    pos = 0

    gate_count = struct.unpack_from("<I", blob, pos)[0]
    pos += 4

    gates = []
    for _ in range(gate_count):
        gates.append(struct.unpack_from("<III", blob, pos))
        pos += 12

    output_count = struct.unpack_from("<I", blob, pos)[0]
    pos += 4
    outputs = list(struct.unpack_from(f"<{output_count}I", blob, pos))
    pos += 4 * output_count

    input_group_count = struct.unpack_from("<I", blob, pos)[0]
    pos += 4

    input_groups = []
    for _ in range(input_group_count):
        bit_count = struct.unpack_from("<I", blob, pos)[0]
        pos += 4
        input_groups.append(list(struct.unpack_from(f"<{bit_count}I", blob, pos)))
        pos += 4 * bit_count

    return gates, outputs, input_groups


def output_cone(gates, outputs):
    by_dest = {dst: (a, b) for dst, a, b in gates}
    needed = set(outputs)
    stack = list(outputs)

    while stack:
        dst = stack.pop()
        if dst not in by_dest:
            continue

        for src in by_dest[dst]:
            if src not in needed:
                needed.add(src)
                stack.append(src)

    return needed


def solve(program):
    gates, outputs, input_groups = parse_circuit(program)
    needed = output_cone(gates, outputs)

    bytes_ = [z3.BitVec(f"b{i}", 8) for i in range(INPUT_LEN)]
    solver = z3.Solver()

    for b in bytes_:
        solver.add(b >= 0x20, b <= 0x7E)

    wires = {}
    for byte_index, group in enumerate(input_groups):
        for bit_index, wire in enumerate(group):
            if wire in needed:
                bit = z3.Extract(bit_index, bit_index, bytes_[byte_index])
                wires[wire] = bit == 1

    for dst, a, b in gates:
        if dst in needed:
            wires[dst] = z3.Not(z3.Or(wires[a], wires[b]))

    solver.add(wires[outputs[0]] == True)

    if solver.check() != z3.sat:
        raise RuntimeError("unsat")

    model = solver.model()
    return bytes(model.eval(b, model_completion=True).as_long() for b in bytes_)

이 코드는 검증 함수를 에뮬레이션하지 않고, gate 관계만 추출해 solver가 풀 수 있는 형태로 바꿉니다. NOR gate의 직렬화 순서가 평가 순서와 맞기 때문에, 필요한 wire를 앞에서부터 채워 나가며 제약식을 만들 수 있습니다.

결과

solver가 복원한 입력을 프로그램에 넣으면 다음과 같이 검증을 통과합니다.

text
HS{f89020f327be2051d14b23b5d26bf7433c86a499d3ec3f5b06d88a67e58c2d3e}
Correct!

flag는 다음과 같습니다.

text
HS{f89020f327be2051d14b23b5d26bf7433c86a499d3ec3f5b06d88a67e58c2d3e}

Overview

NORfuscated is a reversing challenge whose input-validation logic is built as a circuit of NOR gates. The provided binary is a stripped 64-bit PIE ELF. The program takes an input and then prints either Wrong! or Correct!.

The conditions are as follows.

  • Category: reversing
  • Goal: find a 68-byte input that makes Correct! print.
  • Input requirement: after stripping the newline, the length must be exactly 68 bytes.

Validation runs through a serialized Boolean circuit. Nothing compares strings directly: the input bits feed into the circuit, and the program checks whether the final output bit is 1.

Challenge analysis

Notation used below:

  • wire[i]: the value of wire number i in the Boolean circuit.
  • gate: a NOR gate in the form (dst, a, b).
  • input_groups: a list indicating which wire each bit of each input byte maps to.
  • outputs: the list of wires read as the final output.

The output strings visible directly in the program are as follows.

text
Enter flag:
Wrong!
Correct!

The strings alone don't reveal any comparison against the answer. The actual validation flow checks the input length, places the input bits onto the circuit's input wires, and evaluates the NOR gates in order.

In the circuit, each gate performs the following operation.

text
wire[dst] = NOT (wire[a] OR wire[b])

Every operation is a single NOR, so the entire validation logic can be turned into a set of Boolean constraints over the input bits.

The serialized circuit data has the following format.

text
u32 gate_count
gate_count * (u32 dst, u32 a, u32 b)
u32 output_count
output_count * u32 output_wire
u32 input_group_count
input_group_count * (u32 bit_count, bit_count * u32 input_wire)

The parse results are as follows.

text
gate_count        = 344048
output_count      = 1
output_wire       = 344592
input_group_count = 68
bits per group    = 8
input_bits        = 544

Looking at the parse results, the 68-byte input expands into a total of 544 input bits, which pass through many NOR gates and converge into a single output wire. The task is to find an input that makes wire[344592] true.

Core idea

Each NOR gate's input-output relationship is a single Boolean constraint, so instead of reversing the program directly, I turned the whole circuit into a SAT problem.

There are 344048 gates in total, but the ones that do not affect the final output wire can be skipped. Starting from outputs and following each gate's input wires backward, we can obtain the set of wires needed to compute the output. We then add only the gates in this set to the solver.

The strategy:

text
1. Parse the circuit data.
2. Trace back only the wires that affect the final output wire.
3. Represent the 68-byte input as z3.BitVec.
4. Connect each input bit to its corresponding wire.
5. Add the NOR gates as Boolean constraints.
6. Ask the solver to make the final output wire true.

The recovered input must be a string that is actually submittable, so I also added a printable-ASCII constraint to the solver. Even with this restriction, it returned sat and passed validation.

Solution walkthrough

Step 1. Checking the input length and output condition

The validation logic strips the newline and then checks whether the input length is 0x44, i.e. 68 bytes. If the length doesn't match, it never reaches the circuit evaluation.

So the value the solver must produce is 68 bytes. Each byte is split into 8 bits and connected to a total of 544 circuit input wires.

Step 2. Parsing the serialized circuit

The circuit data is stored like an array of u32 values. First comes the gate count, then the 3 values (dst, a, b) repeat. After that come the output wire list and the input-bit mapping.

After parsing, the first byte connects to wire[1] through wire[8], the second byte connects to wire[9] through wire[16], and so on. There is a single final output, and the target wire is 344592.

With the information from this stage, the solver connects the input bytes it represents as z3.BitVec to the circuit wires.

Step 3. Tracing the gates needed for the output wire

We could put all gates into the solver and still solve it, but that adds many unnecessary constraints. So, starting from output_wire, we find the gate that produces that wire, then trace back that gate's inputs a and b.

Repeating this gives the set of wires that affect the final output. Then, iterating over the gates, we add a constraint only when dst is in this set.

Step 4. Converting to NOR constraints

Each input byte is made as a z3.BitVec, and according to input_groups is mapped bit by bit onto a Boolean wire.

text
wire[input_wire] = selected input bit is 1

Then each NOR gate is turned into the following Boolean expression.

text
wire[dst] = Not(Or(wire[a], wire[b]))

Finally, adding the condition that wire[344592] is true lets the solver find a 68-byte input that satisfies it.

Exploit / Solver

The solver parses the circuit, picks only the gates needed for the output, converts them into z3 constraints, then recovers the byte values from the model. For the start offset and length of the circuit data, I used 0x4FFC and 0x3F08E0, which were determined during analysis.

python
import struct

import z3


RODATA_OFF = 0x4FFC
RODATA_LEN = 0x3F08E0
INPUT_LEN = 68


def parse_circuit(program):
    blob = program[RODATA_OFF : RODATA_OFF + RODATA_LEN]
    pos = 0

    gate_count = struct.unpack_from("<I", blob, pos)[0]
    pos += 4

    gates = []
    for _ in range(gate_count):
        gates.append(struct.unpack_from("<III", blob, pos))
        pos += 12

    output_count = struct.unpack_from("<I", blob, pos)[0]
    pos += 4
    outputs = list(struct.unpack_from(f"<{output_count}I", blob, pos))
    pos += 4 * output_count

    input_group_count = struct.unpack_from("<I", blob, pos)[0]
    pos += 4

    input_groups = []
    for _ in range(input_group_count):
        bit_count = struct.unpack_from("<I", blob, pos)[0]
        pos += 4
        input_groups.append(list(struct.unpack_from(f"<{bit_count}I", blob, pos)))
        pos += 4 * bit_count

    return gates, outputs, input_groups


def output_cone(gates, outputs):
    by_dest = {dst: (a, b) for dst, a, b in gates}
    needed = set(outputs)
    stack = list(outputs)

    while stack:
        dst = stack.pop()
        if dst not in by_dest:
            continue

        for src in by_dest[dst]:
            if src not in needed:
                needed.add(src)
                stack.append(src)

    return needed


def solve(program):
    gates, outputs, input_groups = parse_circuit(program)
    needed = output_cone(gates, outputs)

    bytes_ = [z3.BitVec(f"b{i}", 8) for i in range(INPUT_LEN)]
    solver = z3.Solver()

    for b in bytes_:
        solver.add(b >= 0x20, b <= 0x7E)

    wires = {}
    for byte_index, group in enumerate(input_groups):
        for bit_index, wire in enumerate(group):
            if wire in needed:
                bit = z3.Extract(bit_index, bit_index, bytes_[byte_index])
                wires[wire] = bit == 1

    for dst, a, b in gates:
        if dst in needed:
            wires[dst] = z3.Not(z3.Or(wires[a], wires[b]))

    solver.add(wires[outputs[0]] == True)

    if solver.check() != z3.sat:
        raise RuntimeError("unsat")

    model = solver.model()
    return bytes(model.eval(b, model_completion=True).as_long() for b in bytes_)

This code does not emulate the validation function. It extracts only the gate relationships and turns them into constraints for the solver. Because the serialization order of the NOR gates matches the evaluation order, we can build the constraints by filling in the needed wires from the front.

Result

Feeding the input the solver recovered into the program passes validation as follows.

text
HS{f89020f327be2051d14b23b5d26bf7433c86a499d3ec3f5b06d88a67e58c2d3e}
Correct!

The flag is as follows.

text
HS{f89020f327be2051d14b23b5d26bf7433c86a499d3ec3f5b06d88a67e58c2d3e}
Esc

Search titles, content and code.