2026 Hacktheon Sejong CTF 대회

0. 개요

문제 바이너리 challenge는 x86-64 PIE ELF이며, OCaml native로 컴파일되어 있다.
심볼은 stripped 상태지만 OCaml 런타임/모듈의 dynamic symbol이 남아 있어서
camlMain__..., camlProc_a_..., camlProc_b_... 같은 함수명을 그대로 활용할 수 있었다.

최종 플래그:

1

hacktheon2026{ovajumher0erwkl28_i8eecp!hb5enitsj6ly5hx05qel7a2z1gb6y8vi4fd4l93}

1. 실행 환경

로컬 glibc가 바이너리 요구 버전보다 낮아서 Ubuntu 24.04의 loader/libc를 /tmp/until_glibc에 준비해 실행했다.

1

/tmp/until_glibc/ld-linux-x86-64.so.2 --library-path /tmp/until_glibc ./challenge

검증:

1
2

printf 'ovajumher0erwkl28_i8eecp!hb5enitsj6ly5hx05qel7a2z1gb6y8vi4fd4l93\n' \
  | /tmp/until_glibc/ld-linux-x86-64.so.2 --library-path /tmp/until_glibc ./challenge

출력:

1

hacktheon2026{ovajumher0erwkl28_i8eecp!hb5enitsj6ly5hx05qel7a2z1gb6y8vi4fd4l93}

2. 입력 조건

camlMain__input_ok_288에서 입력 길이를 검사한다. OCaml string length가 tagged int로 계산되며, 비교값 0x81은 raw length 64를 의미한다.
허용 문자 집합은 camlShared_types__1에 있다.

1

abcdefghijklmnopqrstuvwxyz_0123456789!

정답 입력은 위 문자 집합으로 이루어진 64글자이며, camlMain__output_flag_of_input_595에서 다음 prefix/suffix를 붙여 출력한다.

1

hacktheon2026{ + input + }

3. 전체 구조

camlMain__entry는 입력 검증 뒤 두 자식 프로세스를 fork한다.

  • Proc_a_engine: target digest 0x8436f275
  • Proc_b_engine: target digest 0x36857515

두 자식이 모두 exit status 0이어야 플래그가 출력된다.
처음에는 GDB로 fork child를 따라가며 비교 지점에 breakpoint를 걸었다.
A 프로세스의 실제 per-constraint 비교는 camlProc_a_handlers__fun_1003 안의 cmp rax, rbx였다.

주요 주소:

1
2
3
4
5

camlProc_a_handlers__build_with_index_647  0x63300
camlProc_a_handlers__state_advance_a_614   0x62b80
camlProc_a_handlers__fun_1003 cmp          0x6205b
camlProc_a_handlers__final_digest_a_627    0x63100
camlProc_b_handlers__base_verify_610       0x60790

4. OCaml 값 표현

OCaml native int는 tagged int라서 raw integer n은 (n << 1) | 1 형태다.
이 바이너리는 대부분의 내부 연산을 & 0x1ff로 제한해서 tagged 8-bit 값처럼 다룬다.

예:

1
2
3

raw 0  -> 0x01
raw 1  -> 0x03
raw 64 -> 0x81

문자도 OCaml char/int 형태로 2 * ord(c) + 1처럼 전달되고,
camlShared_ops__char_index_285가 허용 alphabet에서의 index를 tagged int로 돌려준다.

5. 핵심 연산

공용 모듈 Shared_ops에 검증용 primitive가 모여 있었다.

  • char_index
  • rol8, ror8
  • gf_mul
  • sbox
  • hash1, hash2
  • split_metric
  • hash1i, hash2i

sbox는 대략 다음 형태다.

1
2
3
4
5
6

def sbox(x):
    base = x & 0x1ff
    y = (base * 0xc5 + 0x32) & 0x1ff
    y = rol8(y, 7) ^ 0x14b
    y ^= (base * 0x11 - 0x10) & 0x1ff
    return (y | 1) & 0x1ff

gf_mul은 tagged 8-bit 값 위에서 동작하는 GF-style multiplication이다.
모든 결과가 & 0x1ff로 정규화되기 때문에 Python 모델로 그대로 옮겨 검증할 수 있었다.

6. A 검증기 복원

Proc_a_handlers에는 64개짜리 상수 배열 두 개가 있다.

1
2

0xf0e18: A1 expected array
0xf1020: A2 expected array

각 문자 처리 과정은 다음과 같다.

  1. 현재 위치 pos, 현재 문자 index, 이전 state list의 hash로 mode k를 계산한다.
  2. mode별 함수 m3_k가 첫 번째 constraint 값을 만든다.
  3. metric_remain 계열 함수가 두 번째 constraint 값을 만든다.
  4. state_advance_a가 다음 state를 만든다.
  5. 모든 위치에서 (actual == expected)가 되어야 한다.
  6. 마지막에 final_digest_a == 0x8436f275도 통과해야 한다.

중요한 점은 constraint가 현재 문자 하나만 보지 않는다는 것이다.
일부 constraint는 다음 3글자 window와 state list를 참조한다. 그래서 단순 greedy로는 앞부분 몇 글자 이후 plateau가 생긴다.

해결은 Python으로 A 검증기를 모델링한 뒤 DFS를 돌렸다. 위치 i에서 m3_k constraint를 먼저 만족하는 문자만 남기고,
i >= 3부터는 i - 3 위치의 window constraint가 확정되므로 즉시 가지치기했다.

의사코드:

1
2
3
4
5
6
7
8
9
10
11
12
13

dfs(i):
    for c in alphabet:
        k = calc_mode(i, c, state_history)
        if m3(k, i, c, state_history) != A2[i]:
            continue

        if i >= 3:
            if metric_remain(i - 3, known_window) != A1[i - 3]:
                continue

        push_state(c)
        dfs(i + 1)
        pop_state()

이 가지치기가 매우 강해서 사실상 거의 한 경로만 남았다.

1

ovajumher0erwkl28_i8eecp!hb5enitsj6ly5hx05qel7a2z1gb6y8vi4fd4l93

이 후보는 A의 모든 per-position constraint와 digest를 만족했다.

7. 최종 확인

A만으로 얻은 후보를 실제 바이너리에 넣었고, B 자식 프로세스까지 포함한 전체 검증을 통과했다.

1
2

printf 'ovajumher0erwkl28_i8eecp!hb5enitsj6ly5hx05qel7a2z1gb6y8vi4fd4l93\n' \
  | /tmp/until_glibc/ld-linux-x86-64.so.2 --library-path /tmp/until_glibc ./challenge

결과:

1

hacktheon2026{ovajumher0erwkl28_i8eecp!hb5enitsj6ly5hx05qel7a2z1gb6y8vi4fd4l93}