Loading...
시리즈: 형식 검증 시리즈 · 3부 중 2부 대상 독자: 입문자. 1부에서는 형식 검증을 소개했습니다. 여기서는 이것이 왜 시급해졌는지 보여 준 실제 버그를 살펴봅니다. 필요한 모든 내용은 처음부터 설명합니다. 이 글을 읽고 나면: 암호학적 증명 시스템에 어떻게 건전성 허점이 생길 수 있는지에 대한 직관적이면서도 정확한 이해, 2026년 Zcash의 "Orchard" 버그가 정확히 무엇이었는지, 이런 유형의 버그가 왜 수년간 숨을 수 있는지, 그리고 왜 이전에도 발생했는지를 알게 됩니다.
1부에서 우리는 테스트가 버그의 존재는 보여 줄 수 있지만 부재는 결코 증명할 수 없으며, 가장 위험한 버그는 시스템의 명세, 즉 그 기반 수학에 존재한다고 말했습니다. 이 글은 그 사례 연구입니다. 2026년, Zcash의 Orchard 실드 풀에서 공격자가 무제한의 위조 화폐를 보이지 않게 생성할 수 있었던 결함이 발견되었습니다. 이 결함은 4년과 반복적인 감사를 견뎌 냈습니다. 이것과 그 전례를 이해하는 것은 시스템의 정확성을 증명해야 하는 가장 명확한 동기입니다.
Zcash은 비공개 모드를 제공하는 암호화폐입니다. 실드 풀에서는 거래의 금액, 송신자, 수신자가 숨겨집니다. 이 프라이버시는 거래 내용을 드러내지 않으면서 거래가 모든 규칙을 따른다는 것을 증명하는 암호학적 증명인 영지식 증명으로 만들어집니다.
이 설계에는 양면성이 있습니다. Bitcoin처럼 투명한 원장에서는 누군가 무에서 코인을 만들어 낸다면 부풀려진 수치가 모두에게 보이고, 네트워크는 이를 포착해 되돌릴 수 있습니다. 실드 풀에서는 수치가 설계상 숨겨집니다. 따라서 증명 시스템 자체에 유효하지 않은 거래를 유효해 보이게 만드는 결함이 있다면, 위조는 탐지할 수 없게 됩니다. 원장은 의도적으로 불투명하므로 원장을 검사해서 이를 발견할 수 없습니다.
바로 이것이 Orchard에서 현실화된 위험입니다. 이를 이해하려면 영지식 증명이 실제로 무엇을 검사하는지 살펴봐야 합니다.
서류를 직접 보지 않고 여행자를 승인해야 하는 국경 관리관을 떠올려 보세요. 대신 각 여행자는 체크리스트를 작성하고, 관리관은 체크리스트가 모두 체크된 사람을 승인합니다. 이 체크리스트는 합법적인 여행자만 모든 칸을 체크할 수 있도록 설계되어 있습니다.
이제 체크리스트에 "여권이 만료되지 않았다"와 같은 중요한 항목 하나가 빠져 있다고 가정해 봅시다. 거의 모든 사람은 여전히 정직하게 작성하므로 아무 문제도 없어 보입니다. 하지만 만료된 여권을 가진 사람도 남은 모든 칸을 체크하고 통과할 수 있습니다. 일상적인 사용에서는 시스템이 멀쩡해 보입니다. 이 허점은 그것을 찾으려는 사람에게만 중요합니다.
영지식 증명은 그 체크리스트처럼 작동합니다. 비공개 세부 정보를 공개하지 않고, 그것들이 정해진 조건 집합을 만족하는지 검사합니다. 필요한 조건 하나가 실수로 빠지면 일부 유효하지 않은 입력도 통과할 수 있지만, 다른 모든 것은 계속 정상처럼 보입니다.
이제 "조건 체크리스트"를 정확히 정의해 봅시다. 버그가 정확히 거기에 있었습니다.
내부적으로 "이 거래는 유효하다"라는 명제는 회로로 인코딩됩니다. 회로란 숫자 위의 방정식으로 작성된 제약 조건이라는 고정된 산술 조건 모음입니다. 유효한 증명을 만들려면 증명자는 모든 제약 조건을 만족하는 비밀 값, 즉 증인을 제공해야 합니다. 증명은 검증자에게 그러한 증인이 존재함을 설득하지만, 증인 자체를 공개하지는 않습니다.
이 시스템에 필요한 속성에는 이름이 있습니다.
건전성: 거짓 명제에 대해 유효한 증명을 만드는 것은 불가능해야 합니다. 모든 제약 조건을 만족하는 증인을 가질 수 있는 것은 참인 명제뿐이어야 합니다.
건전성은 위조 방지 보장입니다. 건전성이 유지되면 유효한 증명은 실제로 규칙을 준수한 진짜 거래가 발생했음을 뜻합니다. 건전성에 틈이 생기면 유효한 증명은 아무 의미도 없을 수 있습니다.
제약 조건은 종종 값을 단순하게 강제해야 합니다. 흔한 예시는 값 b을 0 또는 1 중 하나인 단일 비트로 강제하는 것입니다. 이를 위한 표준적인 방법은 하나의 제약 조건입니다.
b × (b − 1) = 0
왜 이것이 작동할까요? 곱은 인수 중 하나가 0일 때만 0입니다. 따라서 b × (b − 1) = 0는 b = 0 또는 b = 1를 강제하며, 다른 값은 허용하지 않습니다. 17에서 순환하는 산술에서 0부터 16까지 모든 값을 검사하면, 이를 만족하는 값은 정확히 0과 1뿐입니다. ✓
이제 그 줄이 회로에서 실수로 빠졌다고 상상해 봅시다. 갑자기 b은 제약을 받지 않습니다. 부정직한 증명자는 b을 5이나 9, 또는 무엇이든 설정하면서도 나머지 제약 조건을 만족할 수 있습니다. 그 하나의 누락된 줄이 건전성 허점입니다. 이제 거짓 명제도 만족하는 증인을 갖게 됩니다.
이것은 가정이 아닙니다. 정확히 이런 종류의 불리언 제약 조건 누락이 Zcash의 최초 실드 설계인 Sprout에서 개발 중 발견되어 출시 전에 수정되었습니다. 제약 조건을 충분히 부여하지 않는 것은 이런 회로를 구축할 때 가장 흔하고 위험한 실수 중 하나입니다.
이것이 작은 규모에서 본 Orchard 버그의 전체 형태입니다. 이제 실제 사례를 보겠습니다.
Zcash의 실드 증명은 타원 곡선을 기반으로 구축됩니다. 타원 곡선은 점들을 결합하고 숫자로 "곱할" 수 있는 수학적 객체이며, 회로는 이러한 연산을 제약 조건으로 강제해야 합니다. 회로에는 타원 곡선 곱셈을 수행하고 그것이 올바르게 이루어졌는지 검사하는 가젯이 포함됩니다.
Shielded Labs와 연구자 Taylor Hornby의 공개에 따르면, Orchard 결함은 정확히 다음과 같았습니다.
Orchard 회로의 충분히 제약되지 않은 요소 때문에 임의의 거짓 입력을 타원 곡선 곱셈에 넣고도 곱셈 검사를 통과시키는 것이 가능했습니다.
쉽게 말하면, 회로의 체크리스트에 해당 곱셈을 확정했어야 할 항목들이 빠져 있었습니다. 이 허점 때문에 충분한 전문성을 갖춘 공격자는 거래가 무에서 가치를 생성했음에도 시스템이 받아들이는 거래 증명을 구성할 수 있었습니다. 이것은 위조이며, 실드 풀의 금액은 숨겨져 있으므로 원장에서 탐지할 수 없었을 것입니다. Tachyon 팀은 나중에 같은 결함을 코드 수준에서, 기반 방정식을 조용히 뒤섞는 회로의 누락된 줄로 설명했습니다.
체크리스트 이야기와의 유사점은 정확합니다.
| 체크리스트 이야기 | Orchard 버그 |
|---|---|
| "여권이 만료되지 않았다" 항목의 누락 | 타원 곡선 곱셈에 대한 제약 조건의 누락 |
| 만료된 여권의 여행자가 그래도 통과함 | 임의의 거짓 입력이 곱셈 검사를 통과함 |
| 다른 모든 사람은 영향받지 않아 아무 문제도 없어 보임 | 정상 거래는 완벽하게 작동하여 결함을 숨김 |
| 이를 찾는 사람만 허점을 발견함 | 전문가가 의도적으로 회로의 수학을 탐색해야 발견할 수 있었음 |
이것이 얼마나 심각했는지 분명히 하자면, 연구자는 AI의 도움을 받아 완전히 작동하는 익스플로잇을 작성했고, 로컬 테스트 네트워크에서 이것이 무제한의 탐지 불가능한 위조 코인을 생성함을 확인했습니다. 이는 이론적 우려가 아니라 실제로 악용 가능한 결함이었습니다.
이 버그는 2022년 5월 활성화된 때부터 2026년 6월 긴급 수정 때까지 Orchard에 존재했으며, 세계 최고 수준의 암호학자들이 수행한 반복적인 전문 감사를 통과했습니다. 어떻게 가능했을까요?
1부가 경고했듯이, 테스트는 사례를 표본 추출할 뿐이며, 이 결함은 아무도 표본으로 추출하지 않은 사례에 존재했기 때문입니다. 일반 거래는 누락된 제약 조건을 전혀 실행하지 않았으므로 모든 테스트는 통과했고 정상 운영의 매일은 흠잡을 데 없이 보였습니다. 이 결함은 허점을 정확히 겨냥한 비정상적인 증인을 의도적으로 구성해야만 도달할 수 있었습니다. 결국 이 결함은 테스트 실행이 아니라 회로의 수학을 추론하여 발견되었습니다.
발견 과정 자체는 보안의 향방을 보여 줍니다. 2026년 4월, Shielded Labs는 보안 연구자 Taylor Hornby에게 정확히 이런 종류의 결함을 찾도록 의뢰했습니다. 2026년 5월 말 새로운 프런티어 AI 모델(Anthropic의 Claude Opus 4.8)이 출시된 직후, Hornby는 맞춤형 분석 하니스와 전통적 방법을 함께 사용하여 Orchard 회로를 표적 검토했습니다. 2026년 5월 29일, 검토에서 취약점이 발견되었습니다.
공개 내용에서 냉정하게 짚어야 할 두 사실이 있습니다.
Orchard 버그는 반복적으로 나타나는 한 계열에 속합니다. 이 계열을 보면 형식 검증은 선택 사항이 아니라 필연처럼 느껴집니다. 위조 결함은 언제나 세 가지 원인 중 하나로 거슬러 올라갑니다(1부의 분류법): 명세(수학 자체), 구현(올바른 수학을 따르지 못한 코드), 또는 깨진 가정입니다. 그리고 결정적으로 다음이 성립합니다.
위조 버그가 탐지 불가능한 경우는 그것이 명세에 있을 때뿐입니다. 구현 버그는 모든 블록이 모든 거래의 전체 내용을 기록하므로 영구적인 공개 증거를 남기며, 수정된 소프트웨어로 이력을 재실행하면 버그가 있는 코드가 잘못 받아들인 모든 거래가 드러납니다.
Zcash 자체의 역사가 이 패턴을 보여 줍니다.
| 버그(연도) | 원인 | 탐지 가능 여부 |
|---|---|---|
| Zerocash 커밋먼트 결함(2016년, 출시 전) | 명세(잘린 해시가 바인딩 속성을 깨뜨림) | 탐지 불가능 |
| 신뢰할 수 있는 설정의 건전성 결함(2018년) | 명세(기반 zk-SNARK 논문의 오류) | 탐지 불가능 |
| 증명 시스템 쿼리 충돌(2025년) | 명세(증명 시스템의 누락된 검사) | 탐지 가능 |
| 곡선 부분군 검증 버그(2016년) | 구현(누락된 부분군 검사) | 탐지 가능 |
| Orchard의 충분히 제약되지 않은 곱셈(2026년) | 명세(회로) | 탐지 불가능 |
공통된 흐름은 뚜렷합니다. 영원히 숨을 수 있는 결함은 수학에 있는 결함입니다. 이것이 기계 검증된 명세 증명이 모든 사례를 한 번에 제거할 수 있는 정확한 종류의 결함입니다. 테스트와 감사는 표본을 추출할 뿐입니다. 수학을 증명해야만 모든 입력을 포괄합니다.
Zcash의 개발자들은 신속하게 단계적으로 움직였습니다.
두 번째 단계에서 형식 검증이 이 이야기로 들어오며, 그것이 3부의 주제입니다. 팀이 실천한 깨달음은 이 시리즈 전체를 연결하므로 미리 볼 가치가 있습니다.
탐지 불가능한 위조 결함은 프로토콜의 명세에만 존재할 수 있습니다. 따라서 명세가 위조를 배제함을 증명할 수 있다면, 여기에서 4년간 숨어 있던 버그의 전체 계열을 제거할 수 있습니다.
이것이 정확히 1부의 첫 번째 기둥 개념입니다. 명세를 검증하면 테스트가 결코 닫을 수 없던 틈을 닫게 됩니다.
우리는 의도적으로 단순화했습니다. 실제 회로는 수백 개의 영역과 수천 개의 제약 조건을 포함하며, 실제 결함은 비트 검사 하나가 누락된 것보다 기술적으로 더 복잡합니다. 하지만 비트 검사를 사용한 이유는 충분히 제약되지 않은 회로의 형태를 정확히 보여 주고, 바로 그 실수가 Zcash의 역사에서 실제로 있었기 때문입니다. 공식 공개에 따르면 정확한 Orchard 결함은 충분히 제약되지 않은 타원 곡선 곱셈이었습니다. 또한 공개 및 개선 조치 일정을 압축해 설명했습니다. 권위 있는 기술적 설명은 Shielded Labs 공개 자료와 Project Tachyon 글을 참고하세요.
b(b−1)=0는 b을 0 또는 1로 강제합니다. 이를 빼면 b은 무엇이든 될 수 있습니다. 이 정확한 계열의 버그는 Zcash의 역사에서 실제로 발생했습니다.)| 용어 | 쉬운 영어 의미 |
|---|---|
| Shielded pool | 금액과 당사자가 숨겨지는 Zcash의 비공개 모드 |
| Zero-knowledge proof | 숨겨진 명제가 유효함을 증명하면서 그 외에는 아무것도 공개하지 않는 증명 |
| Circuit | 유효한 거래가 만족해야 하는 고정된 산술 조건 집합 |
| Constraint | 회로 내부의 하나의 조건(방정식) |
| Witness | 제약 조건을 만족하는 비밀 값 |
| Soundness | 참인 명제만 유효한 증명을 생성할 수 있다는 보장 |
| Soundness gap | 거짓 명제가 통과하도록 하는 누락된 제약 조건 |
| Under-constrained | 필요한 조건이 누락된 회로 상태로, Orchard 버그의 근본 원인 |
| Detectable / undetectable | 악용이 공개 원장에 증거를 남기는지 여부 |
실제로 위조 Zcash이 생성되었나요? 악용의 증거는 발견되지 않았으며, 팀은 그 가능성이 낮다고 봅니다. 하지만 이 결함은 원장에서 탐지할 수 없었으므로 원장만으로는 절대 발생하지 않았음을 완전히 증명할 수 없습니다. 이것이 대응이 매우 철저했던 이유입니다.
금액을 숨기면 왜 버그가 더 심각해지나요? 투명한 체인에서는 발행된 코인이 보이므로 포착하고 되돌릴 수 있습니다. 프라이버시를 위해 금액을 숨기면 위조 버그는 눈에 보이는 이상 현상을 만들지 않으므로, 발견되지 않은 채 지속될 수 있습니다.
수년간의 감사에서 왜 발견하지 못했나요? 감사와 테스트는 대체로 현실적인 사례에서의 동작을 살펴봅니다. 이 결함은 수학적 경계 사례를 노린 의도적으로 구성된 비정상 입력에서만 드러났으며, 일상적인 검토에서는 실행되지 않았습니다. 테스트가 아니라 회로에 대한 표적 수학 추론으로 발견되었습니다.
제약 조건 하나가 빠진 것만으로 정말 충분한가요? 그렇습니다. 증명 시스템은 완전한 제약 조건 집합만큼만 강력합니다. 필요한 조건 하나가 빠지는 것만으로도 유효하지 않은 명제가 통과할 수 있습니다.
AI는 어떤 역할을 했나요? 한 연구자가 프런티어 AI 모델을 맞춤형 하니스와 전통적 방법과 함께 사용하여 회로의 수학을 검토하고 결함을 발견했습니다. AI는 보안의 양쪽 측면에서 점점 더 활용되고 있으며, 이는 시스템의 정확성을 증명하는 일이 지금 더욱 중요해진 이유 중 하나입니다.
실드 거래가 "들어온 돈은 나간 돈과 같다"를 증명해야 하는데, 회로가 출력값 하나를 제약하는 것을 잊었다고 가정해 봅시다. 부정직한 증명자는 무엇을 할 수 있으며, 공개 원장은 왜 완전히 정상으로 보일까요? (답은 아래에 있습니다.)
그 출력을 제약하지 않으면 증명자는 실제 입력이 허용하는 것보다 더 크게 설정하여 무에서 가치를 만들고 위조할 수 있습니다. 불균형을 잡아낼 유일한 것이 누락된 제약 조건이므로 증명은 여전히 검증됩니다. 그리고 실드 풀은 금액을 숨기므로 원장에는 "유효한 거래가 발생했다"는 사실만 보일 뿐, 경보를 울릴 만한 불균형은 보이지 않습니다. 위조는 실제이지만 보이지 않습니다. 이것이 회로의 건전성이 매우 중요한 이유이자, 테스트가 아니라 증명되어야 하는 이유입니다.
3부 · Ironwood: 수정은 단순한 패치가 아니었습니다. Zcash의 엔지니어들은 새로운 실드 풀을 구축하고, 명시된 가정 아래 위조 화폐를 생성할 수 없음을 보이는 Lean 증명 보조기에서 작성된 2,700개 이상의 정리에 걸친 기계 검증 수학 증명을 함께 제공했습니다. "균형 무결성"과 "지식 건전성"이 무엇을 의미하는지, 증명이 정확히 무엇을 다루고 무엇을 다루지 않는지, 그리고 기존 풀이 어떻게 안전하게 폐기되었는지를 살펴보겠습니다.
ZecHub을 위한 Formal Verification 시리즈의 일부입니다.