Ironwood 형식 검증 완료

Project Tachyon이 NU6.3의 일부로 오늘 활성화되는 새 차폐 풀 Ironwood에 대한 형식 검증을 마쳤다고 발표했다. 직전 글에서 형식 검증이 탐지 불가능한 위조 버그를 없앨 수 있음을 보였고, 이번에는 Lean으로 작성된 기계 검증 증명을 공개했다. 증명은 ironwood 저장소에서 볼 수 있으며 2,700개가 넘는 정리로 이루어져 있고 세 연구팀이 한 달 넘게 매달려 완성했다.

이 작업의 목표는 균형 무결성(balance integrity)이라는 하나의 보안 속성이다. 차폐 풀이 공개적으로 유입된 가치보다 많이 지급하지 않는다는 뜻이다. 노력의 대부분은 Ironwood zk-SNARK의 지식 건전성(knowledge soundness) 증명에 들어갔다. 대수적 증명자 모델과 랜덤 오라클 모델에서 Fiat-Shamir 변환을 분석했고, 증명의 일부는 11라운드 내적 논증(IPA)의 챌린지를 다룬다. 결과는 이산로그 문제에 대한 구체적인 보안 한계로 환원되며, 글쓴이는 약 123비트 작업량의 보수적 보안 목표를 제시한다.

증명이 실제 소프트웨어와 맞물리도록 검증자 지문(fingerprint)이라는 경계를 둔다. Rust 검증자가 반환하는 다중 스칼라 곱셈(MSM)을 증명 문자열에서 도출한 정규 조합으로 정의하고, halo2 실행을 기록한 값과 일치함을 Lean으로 확인했다. 구현 오류가 있어도 블록이 모든 증명을 포함하므로 과거 증명을 재검증해 위조를 사후 탐지할 수 있다는 논리다. 회로는 395개 영역을 Lean으로 옮겨 Action 문장이 성립함을 증명했고, 검증 키와의 일치도 증명했다.

마지막 계층은 원장 수준의 정리들이다. 모든 지출은 이전에 생성된 출력이고, 가치는 보존되며, 받은 노트는 계속 쓸 수 있고(Faerie Gold 공격 차단), 지출에는 승인이 필요하다는 속성을 유효한 원장 모두에 대해 증명했으며, 위반은 이산로그나 랜덤 오라클 같은 가정의 붕괴로 환원된다. 값 범위 증명이 모듈러 래핑을 막아 정수 수준의 균형을 보장한다. 이 증명은 위조 방지(건전성)만 다루며 프라이버시 속성은 범위 밖이다.

공로자로 zkSecurity의 Gregor Mitscha-Baude와 ZODL의 암호학자 Daira-Emma Hopwood, 형식화를 주도한 Tal Derei, 병렬로 독립 증명을 진행한 Guillaume Claret와 Valerii Huhnin을 언급한다. 증명은 ArkLib, VCV-io, Mathlib에서 영감을 받은 정의를 사용하며 Clean으로 회로를 분석했다. 남은 가정(랜덤 오라클로서의 BLAKE2b 등)은 문서에 이름으로 명시되어 있다.