HALCTF Kanto — Lessons Learned (team ghoztdiver)

A small, reproducible record of what actually worked for us at DEF CON 34's AI Village HALCTF Kanto, where an autonomous agent driven by a small model (qwen3.6-35b-a3b, ~8k context) solves sandboxed challenges and submits flags.

We did not build a custom Go harness. We used the competition's builtin agent and found a deployment discipline that let a small, unreliable model drive a deterministic solver through a frequently-degraded inference backend. This repo is that discipline, plus the exact artifacts that scored.

Confirmed captures: Bill's PC (450) + Cerulean Cave (300) = 750 pts. Cerulean was solved and submitted correct in 39 seconds once the technique and a healthy backend window lined up.

The one idea

Never let the small model compose anything long or clever. Pre-build and locally validate a self-contained solver, then deliver it as short, quote-safe chunks the model can emit verbatim.

local:   solver.py  --(gzip+base64)-->  blob  --(split)-->  N short chunks
agent:   printf %s 'chunk1'  >/tmp/b
         printf %s 'chunk2' >>/tmp/b
         ...
         python3 -c "import gzip,base64;exec(gzip.decompress(base64.b64decode(open('/tmp/b','rb').read())))"

One Python process then does everything (fetch target, solve, verify locally, submit) so the run touches the flaky model backend as few times as possible.

Why this beat everything else we tried

Three failure modes, observed repeatedly in real runs (see docs/FAILURE_MODES.md and docs/BACKEND_EVIDENCE.md):

Failure	Root cause	What fixed it
Syntax error: Unterminated quoted string	model truncates long/heredoc commands mid-stream	short quote-safe printf chunks, each < ~180 chars
Agent loops / sprays guessed endpoints	model "explores" and burns steps + context	one deterministic script; no model-driven curls
POST /llm/chat/completions -> 499, 3-strike abort	shared inference backend overloaded	not a code fix — only launch in a healthy window

The decisive evidence that our solutions were never the problem: the identical chunked package failed at 09:42 and 10:28 (backend 499s) but succeeded in 39s at 09:08 when the backend was healthy. Same challenge, same model, same bytes.

What's here

tools/pack.py               The packager: solver.py -> chunked deploy commands
solvers/cerulean_sat.py     The winning Cerulean solver (z3 3-SAT over /api/lattice)
solvers/test_cerulean_logic.py  Offline proof the SAT encoding/indexing is correct
recon/universal_recon.py    Auto-detects single- or multi-host targets, dumps API
mock/cerulean_mock.py       Offline server to validate the SAT solver end-to-end
mock/silph_mock.py          Offline 3-host (lobby/mainframe/vault) server
examples/cerulean_deploy.txt  The exact 6 commands that scored Cerulean
docs/FAILURE_MODES.md       Catalog of failures and mitigations
docs/BACKEND_EVIDENCE.md    Run-by-run backend instability report (redacted flag)

Reproduce it

Everything is validated offline with mocks before it ever touches the real grader — that is the whole point.

pip install z3-solver

# 1. Prove the solver logic is correct, no network needed
python3 solvers/test_cerulean_logic.py          # -> LOGIC_OK

# 2. Run the real solver against a local mock of the challenge
python3 mock/cerulean_mock.py &                 # listens on :8099
HAL_TARGET_IP=127.0.0.1 HAL_TARGET_PORT=8099 python3 solvers/cerulean_sat.py
#   -> START / LAT n=120 w=504 / VERIFY ok / ENTER_RESPONSE {...flag...} / DONE

# 3. Produce the chunked deploy the agent runs verbatim
python3 tools/pack.py solvers/cerulean_sat.py

The operating checklist we converged on

1. Pre-build the solver; validate against a mock before any live run.
2. Package with pack.py; keep each emitted command well under ~180 chars.
3. Give the agent one directive: "run these N commands verbatim, in order — no heredocs, no improvising."
4. Do the whole solve in one Python process to minimize model round-trips.
5. Verify locally before submitting. Never submit a guessed flag.
6. Check backend health first; a run that can't clear step 1 cleanly means the backend is degraded — stop and wait for a healthy window.
7. If the model fails 3 steps in a row it's the backend, not you. Retry later.

Scope & honesty

This is a lessons-learned artifact, not a polished framework. The solvers are minimal on purpose. The mocks approximate the real challenges from observed responses; they exist to make the technique reproducible, not to replicate the graders exactly. Flag values are redacted from the public docs.

License: MIT.