풀이 날짜: 2026-09-15 (사용자 확정). 익스플로잇 성공은 2026-09-16 사용자 확인에 따른다. 아래 실행 결과는 보존된 원본 기록이며 이번 감사에서 새로 실행한 결과가 아니다.
Rust VM을 격자 문제로 환원
launcher와 raccoon은 역할이 다르다. launcher는 파일 무결성·입력·자식 결과를 처리하고, 실제 격자 검사는 raccoon의 명령 트리가 수행한다. VirtualMachine::new는 값 스택과 정수 레지스터·불리언 플래그를 초기화하고, CommandTree::get_closure는 트리를 실행 가능한 클로저로 묶는다. 명령 태그는 값 대입, 증가, 비교, 셀 읽기·쓰기, stack push/pop, 분기와 종료에 대응한다.
입력과 한 세대 갱신 규칙
입력은 48자리 hex이며 연속한 세 구간을 각각 8바이트, 즉 8×8 격자로 해석한다. 한 바이트가 한 행이고 열 0은 최하위 비트다.
grid[k][row][column] = (decoded[8*k + row] >> column) & 1
get_command는 자기 자신을 제외한 주변 셀을 센다. 경계를 벗어난 좌표는 제외하므로 torus처럼 반대편에 연결되지 않는다. State::run은 64개 셀의 다음 값을 모은 뒤 한꺼번에 반영한다. 앞 셀의 새 값을 다음 셀이 읽는 제자리 갱신과는 다르다.
N_t(r,c) = 유효한 이웃 좌표에 있는 live 셀 수
B_(t+1)(r,c) = (N_t(r,c) == 3)
OR (B_t(r,c) AND N_t(r,c) == 2)
이 규칙은 Conway 생명 게임이다. 명령 트리를 그대로 따라가는 대신 같은 의미의 격자 변환 F로 모델링할 수 있다.
입력 도출을 위한 제약 모델
세 입력 A, B, C는 각각 별도 State에서 검사되므로 조건도 독립적이다.
F(A) = T1
F(F(B)) = T2
F^12(C) = T3
기존 README는 첫 두 역상을 Z3 Boolean 제약으로 구했다고 기록한다. 아래는 그 모델을 설명하는 수도코드다. 목표값이나 정답 입력을 하드코딩하지 않는다.
각 시점 t, 각 셀 (r,c)에 Boolean B[t,r,c]를 둔다
각 이웃의 Boolean을 0/1 정수로 바꾸어 N[t,r,c]를 계산한다
모든 셀에 Game of Life 전이식을 제약으로 추가한다
마지막 시점의 B를 해당 목표 격자와 같게 둔다
만족하는 모델의 B[0]을 초기 격자로 읽는다
별도 구현의 F를 적용해 목표와 일치하는지 다시 검사한다
세 번째 목표는 5셀 글라이더라는 구조를 이용해 작은 3×3 패턴과 위치를 검토한 기록이다. 모든 64비트 격자를 무차별 탐색한 것으로 쓰지 않는다. 최종 입력은 verify_input.py 외에도 셀 집합 기반 구현으로 검산했다.
실패·성공 판정
입력 형태 검사, 격자 판정, 부모 출력은 분리해야 한다. 자식의 결과 0·1·5를 launcher가 각각 처리하지만 launcher 자체의 일반 실패 함수도 정상 종료할 수 있다. 따라서 부모 exit code 0만으로 성공을 판정하면 오답을 성공으로 오인한다.
배포 ZIP에 실제 flag.txt는 없고 그림의 예시 문자열도 정답 flag가 아니다. 기존 local_runs는 성공 경로와 주입한 테스트 값의 출력을 기록한다. 사용자는 익스플로잇 성공을 확인했으나 공식 flag 값은 이 배포물만으로 알 수 없다. 이번 감사는 수학적 모델과 기존 자료만 대조했고 solver·바이너리를 실행하지 않았다.
근거 자료
sources/raccoon/analysis/README.mdsources/raccoon/analysis/target_boards.jsonsources/raccoon/analysis/local_runs.json
원본 문서·solver·검증 로그는 전달 staging에 보존되어 있다. 이 경로들은 provenance이며 CMS의 다운로드 첨부 링크가 아니다.