제로 지식 증명의 고급 형식 검증: ZK 명령을 어떻게 검증할 것인가

작성자: Certik

형식 검증 기술이 zkVM(제로 지식 가상 머신)에 어떻게 적용되는지를 깊이 이해하기 위해, 본 문서는 단일 명령어의 검증에 초점을 맞출 것입니다. ZKP(제로 지식 증명)의 고급 형식 검증에 대한 전반적인 내용은 동시 발표된 "제로 지식 증명 블록체인의 고급 형식 검증" 기사를 참조하시기 바랍니다.

ZK 명령어 검증이란 무엇인가?

zkVM(제로 지식 가상 머신)은 특정 프로그램이 특정 입력에서 실행되고 성공적으로 종료될 수 있음을 증명하기 위한 증거로서 짧은 증명 객체를 생성할 수 있습니다. Web3.0 분야에서 zkVM의 적용은 처리량을 증가시키는데, 이는 L1 노드가 입력 상태에서 출력 상태로의 변환 과정에 대한 짧은 증명만 검증하면 되기 때문이며, 실제 계약 코드 실행은 오프체인에서 수행될 수 있습니다.

zkVM 증명기는 먼저 프로그램을 실행하여 각 단계의 실행 기록을 생성한 다음, 실행 기록의 데이터를 숫자 테이블 집합으로 변환합니다(이 과정을 "산술화"라고 합니다). 이 숫자들 사이에는 특정 제약 조건(즉, 회로)을 충족해야 하며, 여기에는 구체적인 표 셀 간의 관계 방정식, 고정된 상수, 표 간의 데이터베이스 조회 제약, 그리고 인접한 표 행 간에 충족해야 할 다항식 방정식(즉, "게이트")이 포함됩니다. 체인 상의 검증은 모든 제약 조건을 충족할 수 있는 표가 실제로 존재함을 확인할 수 있으며, 동시에 표의 구체적인 숫자를 볼 수 없도록 보장합니다.

각 VM 명령어의 실행은 이러한 많은 제약 조건에 직면하며, 여기서 VM 명령어의 이 집합을 "ZK 명령어"라고 간단히 부릅니다. 아래는 Rust 언어로 작성된 zkWasm 메모리 로드 명령어 제약의 예시입니다.

ZK 명령어의 형식 검증은 이러한 코드를 형식적으로 추론함으로써 수행되며, 우리는 먼저 이를 형식 언어로 번역합니다.

단 하나의 제약 조건에 오류가 포함되어 있더라도, 공격자는 악의적인 ZK 증명을 제출할 가능성이 있습니다. 악의적인 증명에 해당하는 데이터 표는 스마트 계약의 합법적인 실행과 일치하지 않습니다. 이더리움과 같은 비 ZK 체인과는 달리, 후자는 여러 노드가 서로 다른 EVM(이더리움 가상 머신) 구현을 실행하므로 동시에 동일한 오류가 발생할 가능성이 적지만, zkVM 체인은 단일 VM 구현만 존재합니다. 이러한 관점에서 볼 때, ZK 체인은 전통적인 Web3.0 시스템보다 더 취약합니다.

더욱이 비 ZK 체인과는 달리, zkVM 거래의 계산 세부 사항이 체인에 제출되어 저장되지 않기 때문에 공격 발생 후 공격의 구체적인 세부 사항을 발견하는 것이 매우 어렵고, 심지어 공격 자체를 식별하는 것도 매우 도전적입니다.

zkVM 시스템은 매우 엄격한 검토가 필요하며, 불행히도 zkVM 회로의 정확성을 보장하기는 어렵습니다.

ZK 명령어 검증이 어려운 이유는 무엇인가?

VM(가상 머신)은 Web3.0 시스템 아키텍처에서 가장 복잡한 부분 중 하나입니다. 스마트 계약의 강력한 기능은 Web3.0의 핵심 역량을 지원하며, 그 힘은 기본 VM에서 비롯됩니다. 이들은 유연하고 복잡합니다: 일반적인 계산 및 저장 작업을 완료하기 위해 이러한 VM은 많은 명령어와 상태를 지원해야 합니다. 예를 들어, EVM의 geth 구현은 7500줄 이상의 Go 언어 코드를 필요로 합니다. 이와 유사하게, 이러한 명령어 실행을 제약하는 ZK 회로도 방대하고 복잡합니다. zkWasm 프로젝트에서는 ZK 회로의 구현이 6000줄 이상의 Rust 코드를 필요로 합니다.

zkWasm 회로 아키텍처

특정 응용 프로그램(예: 개인 결제)을 위해 설계된 ZK 시스템에서 사용되는 전용 ZK 회로와 비교할 때, zkVM 회로의 규모는 훨씬 더 큽니다: 그 제약 규칙의 수는 전자의 1~2배에 이를 수 있으며, 그 산술화 테이블은 수백 개의 열과 수백만 개의 숫자 셀을 포함할 수 있습니다.

ZK 명령어 검증은 무엇을 의미하는가?

우리는 여기서 zkWasm의 XOR 명령어의 정확성을 검증하고자 합니다. 기술적으로, zkWasm의 실행 표는 합법적인 Wasm VM 실행 시퀀스에 해당합니다. 따라서 거시적으로 볼 때, 우리가 검증하고자 하는 것은: 이 명령어를 실행할 때마다 항상 새로운 합법적인 zkVM 상태가 생성된다는 것입니다: 표의 각 행은 VM의 합법적인 상태에 해당하며, 그 다음 행은 항상 해당 VM 명령어를 실행하여 생성됩니다. 아래 그림은 XOR 명령어 정확성의 형식적 정리를 보여줍니다.

여기서 "staterel i st"는 상태 "st"가 단계 "i"에서 스마트 계약의 합법적인 zkVM 상태임을 나타냅니다. 당신이 추측할 수 있듯이, "staterel (i+1) …"을 증명하는 것은 결코 쉬운 일이 아닙니다.

ZK 명령어를 어떻게 검증하는가?

XOR 명령어의 계산 의미는 매우 간단하여 두 정수의 비트 단위 XOR를 계산하고 정수 결과를 반환하는 것이지만, 관련된 측면은 많습니다: 먼저, 스택 메모리에서 두 정수를 꺼내어 XOR 계산을 수행한 다음, 이 계산으로 얻은 새로운 정수를 동일한 스택에 다시 저장해야 합니다. 또한, 이 명령어의 실행 단계는 전체 스마트 계약의 실행 흐름에 통합되어야 하며, 그 실행 순서와 시점이 정확해야 합니다.

따라서 XOR 명령어의 실행 효과는 데이터 스택에서 두 수를 팝하고, 그들의 XOR 결과를 푸시하며, 프로그램 카운터를 증가시켜 스마트 계약의 다음 명령어를 가리키도록 해야 합니다.

여기서 정확성 속성 정의는 전통적인 바이트코드 VM(예: 이더리움 L1 노드의 EVM 인터프리터)을 검증할 때 직면하는 상황과 매우 유사합니다. 이는 머신 상태(여기서는 스택 메모리와 실행 흐름)의 고급 추상 정의와 각 명령어의 예상 행동에 대한 정의(여기서는 산술 논리)에 의존합니다.

그러나 아래에서 볼 수 있듯이, ZKP와 zkVM의 특성으로 인해 그 정확성 검증 과정은 일반 VM의 검증과 매우 다릅니다. 여기서 단일 명령어를 검증하기 위해서는 zkWASM의 많은 표의 정확성에 의존해야 합니다: 그 중 하나는 숫자 크기를 제한하는 범위 표, 또 하나는 이진 비트 계산 중간 결과를 저장하는 비트 표, 각 행이 고정 크기의 VM 상태를 저장하는 실행 표(물리적 CPU의 레지스터와 플립플롭의 데이터와 유사), 그리고 동적으로 가변 크기의 VM 상태(메모리, 데이터 스택 및 호출 스택)를 나타내는 메모리 표와 점프 표가 있습니다.

첫 번째 단계: 스택 메모리

전통적인 VM과 유사하게, 우리는 명령어의 두 정수 매개변수가 스택에서 읽을 수 있고, 그 XOR 결과 값이 스택에 올바르게 기록되도록 해야 합니다. 스택의 형식적 표현은 상당히 익숙해 보입니다(전역 메모리와 힙 메모리도 있지만, XOR 명령어는 이를 사용하지 않습니다).

zkVM은 동적 데이터를 표현하기 위해 복잡한 방식을 사용합니다. 이는 ZK 증명기가 스택이나 배열과 같은 데이터 구조를 원래 지원하지 않기 때문입니다. 대신, 스택에 푸시된 각 숫자에 대해 메모리 표는 별도의 행을 사용하여 기록하며, 그 중 일부 열은 해당 표 항목의 유효 시간을 나타냅니다. 물론, 이러한 표의 데이터는 공격자가 제어할 수 있으므로, 표 항목이 계약 실행 중 실제 푸시 명령어에 진정으로 대응하도록 보장하기 위해 몇 가지 제약 조건을 추가해야 합니다. 이는 프로그램 실행 과정에서 푸시 횟수를 정교하게 계산하여 달성됩니다. 각 명령어를 검증할 때, 우리는 이 카운트가 항상 올바른지 확인해야 합니다. 또한, 우리는 단일 명령어 생성의 제약 조건을 스택 작업을 구현하는 표 조회 및 시간 범위 검사와 연결하는 일련의 보조 정리를 가지고 있습니다. 최상위에서, 메모리 작업의 카운트 제약은 다음과 같이 정의됩니다.

두 번째 단계: 산술 연산

전통적인 VM과 유사하게, 우리는 비트 XOR 연산이 올바르게 수행되도록 보장하고자 합니다. 이는 쉬워 보이지만, 결국 우리의 물리적 컴퓨터 CPU는 이 작업을 한 번에 수행할 수 있습니다.

하지만 zkVM에게는 실제로 간단하지 않습니다. ZK 증명기가 원래 지원하는 유일한 두 가지 산술 명령어는 덧셈과 곱셈입니다. 이진 비트 연산을 수행하기 위해 VM은 상당히 복잡한 방식을 사용하며, 하나의 표는 고정 바이트 수준의 연산 결과를 저장하고, 다른 표는 "초안" 역할을 하여 여러 표 행에서 64비트 숫자를 8개의 바이트로 분해한 다음 결과를 다시 조합하는 방법을 보여줍니다.

zkWasm 비트 표 규격의 일부

전통적인 프로그래밍 언어에서 매우 간단한 XOR 연산이 여기서는 이러한 보조 표의 정확성을 검증하기 위해 많은 보조 정리를 필요로 합니다. 우리의 명령어에 대해 우리는 다음과 같은 내용을 가지고 있습니다:

세 번째 단계: 실행 흐름

전통적인 VM과 유사하게, 우리는 프로그램 카운터의 값이 올바르게 업데이트되도록 해야 합니다. XOR와 같은 순차 명령어의 경우, 각 실행 단계 후 프로그램 카운터는 1씩 증가해야 합니다.

zkWasm는 Wasm 코드를 실행하도록 설계되었으므로, 전체 실행 과정에서 Wasm 메모리의 불변 특성이 항상 유지되도록 해야 합니다.

전통적인 프로그래밍 언어는 불리언 값, 8비트 정수, 64비트 정수와 같은 데이터 유형에 대해 원래 지원하지만, ZK 회로에서는 변수는 항상 큰 소수(≈ 2254) 모드의 정수 범위 내에서 변동합니다. VM이 일반적으로 64비트 숫자로 실행되기 때문에, 회로 개발자는 이들이 올바른 숫자 범위를 가지도록 보장하기 위해 제약 시스템을 사용해야 하며, 형식 검증 엔지니어는 전체 검증 과정에서 이러한 범위에 대한 불변 특성을 추적해야 합니다. 실행 흐름 및 실행 표에 대한 추론은 모든 다른 보조 표와 관련이 있으므로, 우리는 모든 표 데이터의 범위가 올바른지 확인해야 합니다.

메모리 작업 수 관리와 유사하게, zkVM은 제어 흐름을 검증하기 위해 유사한 보조 정리를 필요로 합니다. 구체적으로, 각 호출 및 반환 명령어는 호출 스택을 사용해야 합니다. 호출 스택은 데이터 스택과 유사한 표 방식을 사용하여 구현됩니다. XOR 명령어의 경우, 우리는 호출 스택을 수정할 필요는 없지만, 전체 명령어를 검증할 때 여전히 제어 흐름 작업 카운트가 올바른지 추적하고 검증해야 합니다.

이 명령어 검증하기

모든 단계를 통합하여 zkWasm XOR 명령어의 엔드 투 엔드 정확성 정리를 검증해 봅시다. 다음 검증은 상호작용 증명 환경에서 완료되었으며, 여기서 각 형식적 구성 및 논리 추론 단계는 가장 엄격한 기계 검사를 거쳤습니다.

위에서 보듯이, zkVM 회로의 형식 검증은 가능하지만, 이는 복잡한 불변 특성을 이해하고 추적해야 하는 힘든 작업입니다. 이는 검증되는 소프트웨어 자체의 복잡성을 반영합니다: 검증에 관련된 각 보조 정리는 회로 개발자의 올바른 처리를 필요로 합니다. 그 위험이 매우 크기 때문에, 이를 형식 검증 시스템에 의해 기계적으로 검증하도록 하고, 단순히 신중한 수동 검토에 의존하는 것보다 훨씬 더 가치가 있습니다.