Ironwood 이후의 위조 탐지

Project Tachyon이 Ironwood 이후 위조를 탐지하는 방법에 관한 글을 올렸다. 지난달 Shielded Labs의 Taylor Hornby가 Orchard의 위조 취약점을 발견했고, 이는 네트워크 업그레이드로 패치됐으며 악용은 없었던 것으로 믿어진다. 다만 악용이 탐지 불가능해 커뮤니티는 취약점이 패치된 채 새로 시작하는 Ironwood 풀을 만들기로 했다. 팀은 Ironwood를 형식 검증해 탐지 불가능한 위조 버그를 배제하는 작업을 맡았다.

글의 핵심은 탐지 불가능한 위조 버그가 오직 명세에만 존재할 수 있다는 관찰이다. 구현 버그는 탐지 가능한 위조만 낳는다. 블록이 증명을 포함한 모든 거래 내용을 커밋하므로, 수정된 소프트웨어로 기록을 재생하면 잘못 수락된 거래가 영구적 증거로 남기 때문이다. 반면 명세의 오류는 수학적으로 배제할 수 있고, 남는 것은 피할 수 없는 암호학적 가정뿐이다. Zcash는 신뢰 설정과 페어링 기반 암호를 쓰지 않는 새 풀로 가정을 줄여 왔다.

과거 사례도 정리했다. 2016년 Zerocash 명세의 InternalH 충돌 버그와 2018년 Sprout의 [BCTV14] 건전성 결함은 명세의 오류였고 악용이 탐지 불가능했다. 이번 Orchard 취약점은 zk-SNARK 회로의 건전성 버그다. 2016년 libsnark 부분군 검증 누락과 2025년 halo2_proofs 쿼리 충돌 버그는 악용되더라도 탐지 가능했다. 저자는 회로 코드가 아니라 검증자의 동작을 대수적으로 표현해 정확성을 증명하는 방식이 회로와 SNARK의 버그를 함께 잡는다고 설명했다.

팀은 Lean 같은 도구로 증명을 기계 검증하고, 사람이 이끄는 LLM으로 증명 작성 기간을 몇 주로 줄였다고 밝혔다. Tal Derei, zkSecurity의 Gregor Mitscha-Baude, Daira-Emma Hopwood와 함께 작업하며 최근 몇 주간 상당한 진전을 이뤘다. 글은 이것이 모든 위조 버그의 목록은 아니며, 명세 검증만으로 탐지 불가능한 위조를 배제할 수 있음을 보이는 것이라고 결론지었다. 지식 건전성과 실제 소프트웨어와의 비교는 다음 글에서 다룰 예정이다.