Loading...
시리즈: 형식 검증 · 3부작 중 3부 대상 독자: 입문자. 1부와 2부에서는 형식 검증과 Orchard 버그를 다뤘습니다. 이 마지막 글에서는 두 아이디어가 실제 시스템에서 만나는 모습을 보여 줍니다. 필요한 내용은 진행하며 모두 다시 설명합니다. 이 글을 읽고 얻게 될 것: Zcash가 새 "Ironwood" 풀에 관해 실제로 무엇을 증명했는지, 그 증명이 어떻게 구성되는지, 무엇을 다루고 무엇을 다루지 않는지, 기존 풀을 어떻게 안전하게 폐기했는지, 그리고 이것이 암호화폐 구축의 새로운 기준을 시사하는 이유를 정확히 이해하게 됩니다.
1부에서는 시스템이 올바르다는 것을 증명한다는 의미를 배웠습니다. 2부에서는 테스트가 4년 동안 놓친 실제 결함, 즉 무제한의 보이지 않는 위조를 허용할 수 있었던 제약이 불충분한 타원곡선 곱셈을 살펴봤습니다. 이 글은 그 문제의 해법입니다. Zcash가 단순한 패치가 아니라, 해당 버그 유형 전체가 사라졌음을 기계 검증 증명으로 어떻게 해결했는지 다룹니다.
버그가 돈을 위협할 때 일반적인 대응은 패치한 뒤 넘어가는 것입니다. Zcash는 더 야심 찬 일을 했습니다. 2026년 7월 28일 활성화된 Ironwood라는 새 실드 풀과 함께, 엔지니어들은 명시된 가정 아래 새 풀이 위조 코인을 만들 수 없음을 확립하는 기계 검증 수학적 증명을 공개했습니다. 이 증명은 Lean 증명 보조기에서 작성된 2,700개 이상의 정리로 이루어져 있습니다. 증명은 오픈소스 ironwood 저장소에 공개되어 있으며, 세 팀의 연구원과 암호학자가 한 달이 훨씬 넘는 기간 동안 완성했습니다.
이는 Zcash를 넘어 중요한 의미를 가집니다. 실제 금융 시스템을 대상으로 "위조 불가"의 의미를 정확히 정의하고, 테스트가 충분했기를 바라는 대신 이를 증명할 수 있음을 보여 주는 가장 명확한 현실 사례 중 하나입니다. 약속을 정리로 바꾸는 일입니다.
2부는 이를 가능하게 한 통찰로 끝났습니다. 여기의 모든 내용이 그것에 기반하므로 다시 떠올려 봅시다.
탐지 불가능한 위조 버그는 프로토콜의 명세, 즉 회로가 강제해야 하는 것을 수학적으로 설명한 내용에만 존재할 수 있습니다. 탐지 가능한 문제라면 공개 회계에 나타날 것입니다. 그러므로 명세의 건전성을 증명하면 숨겨진 위조 버그라는 유형 전체를 한 번에 제거할 수 있습니다.
왜 "명세에만" 존재할 수 있을까요? 모든 블록은 증명을 포함해 모든 거래의 전체 내용을 영구적으로 기록하기 때문입니다. 소프트웨어가 잘못된 거래를 승인했다면 누구나 수정된 소프트웨어로 기록 전체를 재실행하여 확인할 수 있습니다. 그 증거는 영구적이고 공개적입니다. 반면 근본적인 수학의 결함만이 영원히 숨을 수 있습니다. 대조할 "올바른 버전"이 없기 때문입니다. 형식 검증이 겨냥하는 결함이 바로 이것입니다.
테스트는 표본으로 선택된 입력에서의 동작을 확인하며, Orchard 버그는 정확히 어떤 표본 입력도 그것을 건드리지 않았기에 숨을 수 있었습니다. 명세에 대한 증명은 아무도 시도할 생각을 못 했을 경계 사례까지 포함하여 모든 입력을 동시에 다룹니다. 4년 된 보이지 않는 결함을 확신을 갖고 폐기하려면 이 정도로 강한 보증이 필요합니다.
이 증명은 그 아래에 있는 더 깊은 속성에 기반한 하나의 핵심 속성을 확립합니다.
잔액 무결성: 실드 풀에 저장된 숨겨진 가치는 그 풀로 유입된 순공개 가치를 결코 초과하지 않습니다.
이는 평이한 형태의 위조 방지 속성입니다. 돈은 실드 풀에 들어갈 수 있고(공개적으로 보임) 나갈 수도 있지만(공개적으로 보임), 금액이 숨겨진 내부에서는 어떤 가치도 무에서 만들어질 수 없습니다. 검증된 산술이 적용된 작은 원장으로 구체화해 봅시다.
5 + 3 = 8인 입력이 가치가 4 + 4 = 8인 출력을 만듭니다. 유입 가치와 유출 가치가 같습니다. 잔액 무결성이 성립합니다. ✓8의 입력이지만, 출력은 4 + 4 + 2 = 10입니다. 이는 무에서 2 단위를 발행하게 됩니다. 잔액 무결성은 이를 금지합니다. 풀은 유입된 것보다 더 많이 지불할 수 없습니다. ✗잔액 무결성은 두 번째 시나리오가 결코 유효한 거래를 만들 수 없다는 수학적 진술입니다.
잔액 무결성을 보장하기 위해 연구원들은 먼저 영지식 증명 시스템 자체에 관한 더 깊고 미묘한 속성을 증명해야 했습니다. 일반적인 건전성(2부의 "참인 진술만 증인을 가진다")은 흥미로운 이유로 실드 풀에 충분하지 않은 것으로 드러납니다. 숨겨진 거래에는 무엇이든 담길 수 있으므로 거의 모든 진술이 기술적으로는 어떤 증인을 갖기 때문입니다. 그래서 연구원들은 더 강한 속성을 증명했습니다.
지식 건전성: 유효한 거래 증명을 만들 수 있는 사람은 실제로 유효한 증인, 즉 올바르게 도출되어 적절한 주소에 있는 실제 코인을 보유해야 합니다.
이를 위한 형식 도구는 추출기입니다. 검증자를 설득할 수 있는 임의의 증명자가 주어졌을 때, 그로부터 실제 증인을 끌어내는 절차입니다. 언제나 증인을 추출할 수 있다면, 설득력 있는 증명자는 실제로 증인을 갖고 있었음이 분명합니다. 2부의 표현으로 말하면, 지식 건전성은 거짓 진술이 통과하게 만들 누락된 제약, 즉 건전성 격차가 없음을 보장하는 형식적 약속입니다. 이것은 바로 Orchard 버그에서 부재했던 속성입니다. 가능한 모든 증명자에 대해 이 속성이 존재함을 증명하는 것이 그 문을 완전히 닫습니다.
이 검증은 버튼 하나를 누르면 나오는 결과가 아니라, 상당한 인간의 노력이 들어간 작업이었습니다.
ironwood 저장소에서 공개적으로 확인할 수 있습니다.이 속성을 추론하기 위해 Lean 모델은 각 거래의 액션, 선언된 공개 가치, 서명을 담은 거래 목록으로 전체 원장을 기술합니다. 연구원들이 ValidLedger라고 부르는 술어는 네트워크의 합의 규칙을 직접 옮깁니다. 모든 액션의 증인은 요구 조건을 충족해야 하고, 어떤 지출 표식(nullifier)도 두 번 나타날 수 없으며, 참조되는 모든 트리 상태는 시스템이 실제로 도달했던 상태여야 하고, 모든 서명은 검증되어야 합니다. 이후 정리들은 모든 유효한 원장에 대해 정량화합니다. "모든 유효한 원장"이라는 표현이 핵심입니다. 표본이 아니라, 실제 공격자가 구성할 수 있는 어떤 경우도 포함하는 전체입니다.
잔액 무결성 결과는 여러 원장 수준 정리로 조립됩니다. 각 정리는 위조 경로 하나가 차단되었음을 증명합니다. 모든 지출이 실제 이전 출력에 대응한다는 점, 총가치가 보존된다는 점, 받은 노트는 계속 지출 가능하며 도난당할 수 없다는 점, 지출에는 적절한 권한 부여가 필요하다는 점입니다. 별도의 구성 요소인 바인딩 서명은 각 거래의 숨겨진 가치를 거래가 선언한 공개 금액에 연결하므로, 숨겨진 회계와 공개 회계가 조용히 불일치할 수 없습니다.
미묘하지만 정당한 질문이 있습니다. 증명은 수학적 모델에 관한 것이지만 네트워크는 Rust 코드를 실행합니다. 코드가 모델과 일치한다는 것을 어떻게 알 수 있을까요?
팀은 검증자의 핑거프린트라고 부르는 신중한 경계를 설정했습니다. 경계 위에서는 Lean 증명이 검증자를 정확한 수학적 객체로 다룹니다. 그 아래에는 일반적인 Rust 구현이 있습니다. 핵심 논증은 2부와 동일합니다.
실제 소프트웨어가 증명된 모델에서 벗어날 수 있는 모든 방식은 구현 버그이며, 구현 버그는 오직 탐지 가능한 위조만 만들어 낼 수 있습니다. 승인된 모든 증명은 영구적으로 기록되고 수정된 소프트웨어로 재실행될 수 있기 때문입니다.
따라서 증명은 탐지 불가능한 유형(명세)을 다루고, 영구적인 공개 기록은 탐지 가능한 유형(구현)을 다룹니다. 둘 사이에는 탐지 불가능한 위조 버그가 숨을 곳이 없습니다. 팀은 실제 검증자를 실행하고, 캡처된 사례에서 핑거프린트를 정확히 재현하는지 확인하여 교차 검증도 수행했습니다.
1부에서는 증명이 명시된 가정 아래에서 시스템이 명세를 충족함을 보장할 뿐, "버그가 절대 없다"는 의미는 결코 아니라고 강조했습니다. Zcash 팀은 바로 이 점을 훌륭할 정도로 정확히 설명했으며, 정직한 교육 글도 마찬가지여야 합니다.
이 증명은 Ironwood의 보안을 작고 표준적이며 명확히 이름 붙인 가정 집합으로 환원합니다. 특히 건전성은 Ironwood가 사용하는 타원곡선에서의 이산 로그 문제의 어려움에 기반합니다. 이는 잘 연구된 가정으로, 현재 알려진 최선의 공격도 대략 2^126회의 연산을 요구하므로 실현 가능한 계산 범위를 훨씬 벗어납니다. 또한 해시 함수에 관한 표준 모델링 가정도 필요합니다. 다음 두 경계는 분명히 말할 가치가 있습니다.
이러한 경계를 명시하는 것은 성취를 약화하는 것이 아니라 신뢰할 수 있게 만드는 요소입니다. 주장은 정확합니다. 표준 암호학적 가정 아래 이 풀은 탐지 불가능한 위조 코인을 만들 수 없습니다. 이는 희망이 아니라 정리이며, 그 정확한 범위가 공개적으로 명시되어 있습니다.
새 풀의 건전성을 증명했더라도 질문은 남습니다. 결함이 4년 동안 존재했던 기존 Orchard 풀은 어떻게 될까요? 과거를 드러낼 수는 없습니다. 그러나 미래는 제한할 수 있습니다.
Zcash는 턴스타일이라는 메커니즘을 도입했습니다. 규칙은 단순하면서도 강력합니다.
기존 풀에서는 검증 가능하게 유입된 금액까지만 가치가 나갈 수 있습니다.
실드 풀 안팎으로 이동하는 돈은 공개적으로 보이므로(숨겨지는 것은 내부 활동뿐입니다), 턴스타일은 지금까지 유입된 것보다 더 많은 가치가 나가지 않는지 네트워크 전체가 확인할 수 있게 합니다. 기존 풀 내부에서 위조 코인이 만들어졌다면 이 한도에 걸려 나갈 수 없습니다. 또한 정상 자금이 빠져나가고 초과분이 나타나지 않으면, 공동체는 그 결함이 악용되지 않았다는 강력한 공개 증거를 얻게 됩니다. 프라이버시를 깨지 않고 비공개 풀의 공급량을 감사하는 데 가장 가까운 방식이며, Zcash의 프라이버시를 유지하면서 공급 무결성을 Bitcoin과 같은 체인의 투명한 모델에 더 가깝게 만듭니다.
Ironwood 자체는 수정된 증명 회로를 재사용하고, 빈 풀에서 새로 시작하며, 미래를 위한 보호 장치를 추가합니다. 여기에는 언젠가 미래의 양자 컴퓨터가 오늘날의 암호기술을 위협하더라도 자금을 복구 가능한 상태로 유지할 수 있도록 하는 조항도 포함됩니다. 이제 새로운 실드 활동은 Ironwood를 통과하며, 기존 Orchard 풀은 출금 용도로만 제한됩니다.
Ironwood는 Zcash의 구축 방식에서 일어나는 더 넓은 변화의 일부입니다. 재귀적 증명과 Ragu라는 툴킷에 기반한 Tachyon이라는 아키텍처로 구성된 차세대 확장 노력은, 때때로 고보증 암호기술이라 불리는 철학 아래 개발되고 있습니다. 이는 기계 검증 형식 검증을 사후 고려 사항이 아니라 새로운 암호 시스템을 출시하는 표준 과정으로 다루는 접근입니다.
그 논리는 설득력 있습니다. 최첨단 암호기술은 인간의 직관이 가장 약하고, Orchard가 보여 주었듯 미묘하고 테스트되지 않은 경계 사례가 수년간 숨을 수 있는 바로 그 영역입니다. 명세를 증명하는 것은 "가능한 모든 입력"으로 확장할 수 있으며, 설계 단계에서 이러한 격차를 없애는 유일한 기법입니다. 팀은 시간이 지나며 구현과 그 너머까지 이 검토를 확장할 의도를 밝혔습니다. 이 기준은 Zcash 안팎에서 더 널리 채택될 것으로 예상됩니다.
명확성을 위해 단순화했습니다. 실제 Lean 개발은 여기의 개요보다 훨씬 상세하며, 액션, 진술, 커밋먼트, nullifier, 서명에 대한 정확한 정의를 포함합니다. "잔액 무결성"과 "지식 건전성"에는 여기서 말로만 설명한 정확한 형식 정의가 있습니다. 이산 로그의 어려움으로의 환원은 여러 중간 모델(증명자의 대수적 모델과 해시의 랜덤 오라클 모델)을 거치지만, 이를 "표준 가정"으로 압축했습니다. 핑거프린트와 턴스타일 역시 개념적 수준에서 설명했습니다. 이 어느 것도 본질적 이야기를 바꾸지 않습니다. "위조 없음"의 명세, 모든 유효한 원장에 대한 기계 검증 증명, 범위와 가정에 관한 명시적이고 정직한 설명, 그리고 결함이 있던 풀의 안전한 폐기입니다. 권위 있는 설명은 Project Tachyon이 공개한 검증 문서와 ironwood 증명 저장소를 참고하세요.
| 용어 | 쉬운 설명 |
|---|---|
| Ironwood | 결함이 있던 Orchard 풀을 대체하는 Zcash의 새 실드 풀(2026) |
| Balance integrity | 풀은 공개적으로 유입된 가치보다 더 많은 가치를 결코 지불하지 않음 |
| Knowledge soundness | 유효한 증명에는 증명자가 진짜 증인을 보유해야 함 |
| Extractor | 설득력 있는 모든 증명자로부터 증인을 끌어내는 절차 |
| Lean | 검증을 기계적으로 확인하는 데 사용된 증명 보조기 |
| ValidLedger | 정리가 추론하는 합의 규칙의 형식 모델 |
| Fingerprint | 증명된 수학과 실행 중인 Rust 소프트웨어 사이의 경계 |
| Under stated assumptions | 이름이 명시된 암호학적 가정이 성립하는 한 증명이 성립함 |
| Turnstile | 풀의 출금을 검증 가능한 예치금으로 제한하는 규칙 |
| High-assurance cryptography | 형식 검증을 표준 단계로 삼아 암호기술을 구축하는 방식 |
이 증명은 Ironwood에 버그가 없다는 뜻인가요? 아닙니다. 또한 그렇게 주장하지도 않습니다. 이 증명은 명시된 가정 아래 잔액 무결성이라는 하나의 정확한 속성을 증명합니다. 이는 탐지 불가능한 위조를 배제하지만, 상상할 수 있는 모든 버그를 배제하지는 않습니다.
이 증명은 내 거래가 비공개임을 보장하나요? 아닙니다. 이 검증은 공급 건전성(가짜 돈이 없음)을 다루며, 풀의 별도 프라이버시 보증은 다루지 않습니다. 프라이버시는 다른 방식으로 논증됩니다.
사람(및 AI)이 작성한 증명을 왜 신뢰해야 하나요? 기계 검증되기 때문입니다. Lean 증명 보조기는 모든 단계를 기계적으로 확인하므로, 신뢰는 각 단계에서 사람이나 AI가 얼마나 주의 깊었는지가 아니라 명세와 명명된 가정에 기반합니다.
기존 Orchard 풀에 아직 남아 있는 코인은 어떻게 되나요? 출금할 수 있지만, 턴스타일에 의해 검증 가능하게 유입된 금액까지만 가능합니다. 이는 공급 무결성을 보호하고 기존 결함이 악용되지 않았음을 보여 주는 데도 도움이 됩니다.
이것으로 이야기가 끝인가요? 이는 이정표이지 결승선이 아닙니다. Zcash의 미래 아키텍처(Tachyon 및 Ragu 툴킷)는 형식 검증을 표준 관행으로 삼아 구축되고 있으며, 이 접근을 더 확장합니다.
누군가 이렇게 주장합니다. "Ironwood는 형식 검증되었으므로 이제 Zcash에서 무엇이든 잘못될 가능성은 영원히 없습니다." 세 부분의 아이디어를 활용하여, 이 주장이 지나치게 강한 서로 다른 이유 두 가지를 제시해 보세요. (답은 아래에 있습니다.)
첫째, 이 증명은 명시된 가정 아래 특정 속성인 잔액 무결성을 다룹니다. 그 가정은 이산 로그의 어려움과 표준 해시 모델링입니다. 암호학적 가정이 깨지거나, 명세에 포함되지 않은 문제(예를 들어 프라이버시, 지갑 소프트웨어, 또는 증명되지 않은 구성 요소)가 발생한다면 증명은 그것에 관해 아무 말도 하지 않습니다. 둘째, 형식 검증은 시스템이 작성된 명세를 충족함을 보장합니다. 그 명세 자체가 실제 요구 사항을 포착하지 못했다면, 증명은 잘못된 것을 충실하게 인증하게 됩니다. 두 가지 모두 1부의 단서를 다시 말한 것입니다. 증명은 정확하고 범위가 한정되어 있으며, 그 범위가 정직하기 때문에 강력합니다. 아무것도 절대 잘못될 수 없다는 포괄적 보증이 아닙니다.
세 부분에 걸쳐 우리는 일반적인 아이디어에서 실제 적용으로 나아갔습니다. 소프트웨어를 테스트하는 대신 올바름을 증명한다는 의미(1부), 실제 제약 부족 회로가 보이지 않는 돈을 어떻게 발행할 수 있었는지(2부), 그리고 잔액 무결성의 기계 검증 증명이 그 버그 유형을 영구히 어떻게 폐기했는지(3부)를 다뤘습니다. 이 시리즈를 관통하는 것은 하나의 정직한 약속입니다. "버그가 절대 없다"가 아니라, "명시된 가정 아래 이 정확한 속성이 모든 경우에 성립한다"는 것입니다. 자체 금액을 숨기는 돈에 있어, 바로 이 약속이 증명할 가치가 있는 약속입니다.
ZecHub를 위한 Formal Verification 시리즈의 일부입니다.