Gemini와 Z3 제약 솔버로 fuzzing이 놓치는 Go 버그를 찾는 방법

이 방법은 다음과 같은 흐름으로 진행된다. GOOS=linux GOARCH=riscv64 로 Go 코드를 컴파일하고, SSA의 prove 패스를 통과하고도 남는 runtime.panicBounds 트랩을 목록으로 만든다. Go 소스와 디스어셈블리를 모두 Gemini 4 Argon에 전달하면, 각 트랩에 이르는 경로를 나타내는 Z3 스크립트와 버그가 있을 경우 패치된 함수가 반환된다. Z3가 sat을 반환하면 구체적인 바이트 열을 얻을 수 있고, go test로 실제 함수에 넣어 재현을 확인한다. Argon의 변환에는 함수당 약 1분이 걸리지만, Z3 자체는 수 밀리초에 끝난다.

이 방법이 완전한 정확성의 증명을 주는 것은 아니다. unsat은 '아마도 올바르다'를 의미할 뿐이지만, sat의 경우 go test에서 panic이 발생하면 재현 가능한 버그가 확정된다. 저자는 Anthropic이 제시한 Rocq 증명을 통한 C/C++ 형식 검증을 언급하며, 이보다 가벼운 수단으로 이 방법을 위치시킨다. 검증은 64바이트의 새 슬라이스에서, cap(buf) == len(buf) 조건 아래 수행되었다.

심어 둔 버그 중 하나인 ParseTwoChunkFrame에서는 uint8끼리의 hdrLen + bodyLen이 MOVBU에서 256을 법으로 래핑되는 반면, endBody는 64비트 정수로 계산된다. Z3는 hdrLen = 48, bodyLen = 236을 포함한 59바이트의 반례를 반환했다. 이때 모든 (hdrLen, bodyLen) 조합의 19.4%가 충돌을 일으키지만, unseeded go test -fuzz는 3초 실행과 60초 3회 실행 어느 쪽에서도 이를 놓쳤다. 원인은 Go의 슬라이스 식이 길이가 아니라 capacity에 대해 검사된다는 점에 있다. 10초간의 조사에서는 386,741회 호출 중 89%가 약 100 MB 공유 버퍼의 뷰였고, cap == len인 입력은 0.07%에 불과했다.

대책은 fuzz 함수 안에서 data = data[:len(data):len(data)]로 capacity를 길이에 맞추는 한 줄이다. 이로써 ParseTwoChunkFrame과 ExtractQuotedToken은 3회 실행 모두에서 충돌했고, 중앙값은 각각 0.28초와 0.17초였다. 부호 있는 int8 길이 버그를 가진 ParseMagicPacket은 capacity와 무관하게 항상 검출되었다.

skill-lint 본체에서는 CLI 전체가 너무 커서, Functional Core의 사고방식에 따라 파일 I/O를 제외한 순수 함수만 솔버에 넘겼다. 5개 함수 중 2개의 스캐너는 unsat이었고, 나머지 3개에는 버그가 있었다. ApplyReplacementChunks는 StartLine으로 정렬해도 중복 청크를 막지 못해, 범위 오류와 앞선 편집의 덮어쓰기를 일으킨다. 로컬 fixer에서는 삭제 후 슬라이스가 줄어드는 점이, 프롬프트 패커에서는 고정 100바이트 할당이 2 MB 예산을 넘는 점이 문제였다. 모듈 단위로 검사할 때는 호출 측이 담당하는 사전 조건 검사도 대상에 포함해야 한다. 이를 포함하자 Z3가 처음 반환한 sat의 대입은 모두 실제 panic을 일으켰다. 주석을 제거해도 결과는 달라지지 않았다.

용도별로 나누면, 많은 Go 코드에서는 capacity를 길이에 맞춘 순수 함수의 fuzzing으로 경계 버그를 수 초 만에 잡을 수 있다. 여러 필드로 이루어진 헤더나 행 범위로 오프셋을 계산하는 파서나 에디터에서, 컴파일러의 prove 패스와 간이 fuzzing을 모두 통과한 트랩에는 솔버에 추가로 1분을 쓸 만한 가치가 있다고 저자는 말한다. 데이터 경합이나 데드락은 솔버로 다룰 수 없으므로, 동시성 코드에는 race detector 등을 함께 사용해야 한다.