영지식 증명의 고급 공식 검증: ZK 명령어를 검증하는 방법

출처: CertiK 중국 커뮤니티

정식 검증 기법이 zkVM(영지식 가상 머신) 위에 어떻게 적용되는지 더 깊이 이해하기 위해 이 글에서는 단일 명령어의 검증에 초점을 맞추고자 합니다. 영지식 증명 블록체인을 위한 고급 공식 검증에 대한 일반적인 개요는 동시 발행된 "영지식 증명 블록체인을 위한 고급 공식 검증"을 참조하시기 바랍니다.

ZK 인스트럭션 검증이란 무엇인가요?

zkVM(영지식 가상 머신)은 특정 프로그램이 특정 입력에서 실행되고 성공적으로 종료될 수 있다는 증거로 사용할 수 있는 짧은 증명 객체를 생성할 수 있습니다. 웹 3.0에서는 스마트 컨트랙트가 입력 상태에서 출력 상태로 전환되는 짧은 증명만 확인하면 되고, 컨트랙트 코드의 실제 실행은 오프체인에서 이루어질 수 있기 때문에 zkVM을 적용하면 높은 처리량을 구현할 수 있습니다.

zkVM 증명자는 먼저 프로그램을 실행하여 각 단계에 대한 실행 기록을 생성한 다음, 실행 기록의 데이터를 숫자 테이블로 변환합니다("산술화"라고 알려진 프로세스). 이러한 숫자는 특정 테이블 셀 간의 연결 방정식, 고정 상수, 테이블 간의 데이터베이스 조회 제약 조건, 인접한 테이블 행의 각 쌍 사이에서 만족해야 하는 다항식(즉, "게이트") 등 일련의 제약 조건(즉, 회로)을 만족해야 합니다. 따라서 체인 유효성 검사는 모든 제약 조건을 만족하는 테이블이 실제로 존재하는지 확인하는 동시에 테이블에 정확한 숫자가 표시되지 않도록 보장합니다.

각 VM 명령어는 실행 시 이러한 여러 제약 조건에 직면하게 되며, 여기서는 이를 "ZK 명령어"라고 부릅니다. 다음은 Rust로 작성된 zkWasm 메모리 로드 명령어 제약 조건의 예시입니다.

ZK 명령어의 형식적 유효성 검사는 이러한 코드에 대한 형식적 추론에 의해 수행됩니다. 형식적 추론을 통해 이루어지며, 이 추론은 먼저 형식적 언어로 번역됩니다.

단 하나의 제약 조건에만 오류가 포함되어 있더라도 공격자는 악의적인 ZK 증명을 제출할 위험이 있습니다. 악성 증명에 해당하는 데이터 테이블은 스마트 콘트랙트의 정상적인 실행과 일치하지 않습니다. 이더리움과 같이 서로 다른 EVM(이더리움 가상 머신) 구현을 실행하는 노드가 많기 때문에 같은 시간에 같은 장소에서 동일한 오류가 발생할 가능성이 낮은 비-ZK 체인과 달리, zkVM 체인에는 단일 VM 구현이 있습니다. 이러한 이유만으로도 ZK 체인은 기존 웹 3.0 시스템보다 더 취약합니다.

더 심각한 문제는 ZK 체인이 아닌 경우와 달리 zkVM 트랜잭션의 계산 세부 정보가 체인에 제출 및 저장되지 않기 때문에 공격이 발생한 후에는 공격의 정확한 세부 정보를 발견하기가 매우 어려울 뿐만 아니라 공격 자체를 식별하는 것조차 매우 어려울 수 있다는 것입니다.

zkVM 시스템은 매우 엄격한 조사가 필요하며, 안타깝게도 zkVM 회로의 정확성을 보장하기는 매우 어렵습니다.

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

가상 머신(VM)은 웹 3.0 시스템 아키텍처에서 가장 복잡한 부분 중 하나입니다. 웹 3.0의 기능을 뒷받침하는 핵심인 스마트 컨트랙트의 힘은 유연하면서도 복잡한 기본 VM에서 비롯됩니다. 범용 연산 및 저장 작업을 수행하려면 이러한 VM이 다양한 지시문과 상태를 지원할 수 있어야 합니다. 예를 들어, EVM의 geth 구현에는 7,500줄 이상의 Go 언어 코드가 필요합니다. 마찬가지로 이러한 명령어의 실행을 제한하는 ZK 회로도 마찬가지로 크고 복잡합니다. zkWasm 프로젝트에서와 마찬가지로, ZK 회로 구현에는 6000줄 이상의 Rust 코드가 필요했습니다.

zkWasm 회로 아키텍처

특정 애플리케이션(예: 개인 결제)을 위해 설계된 ZK 시스템에서 사용되는 전용 ZK 회로와 비교할 때, zkVM 회로는 제약 규칙의 수가 전자보다 한두 배 더 많을 수 있으며 산술화된 테이블은 수백만 개의 숫자 셀이 포함된 수백 개의 열로 구성될 수 있으므로 그 규모가 상당히 더 큽니다. 셀을 포함하는 수백 개의 열로 구성될 수 있습니다.

ZK 명령의 유효성 검사는 무엇을 의미하나요?

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

Here. "state_rel i st"는 상태 "st"가 단계 "i"에서 스마트 컨트랙트의 합법적인 zkVM 상태임을 나타냅니다. 짐작할 수 있듯이 "state_rel (i+1) ..."을 증명하는 것은 쉽지 않습니다.

ZK 명령의 유효성을 어떻게 검증하나요?

XOR 명령의 계산 의미는 두 정수의 비트 단위 XOR을 계산하고 정수 결과를 반환하는 단순하지만, 먼저 스택 메모리에서 두 정수를 꺼내서 XOR을 계산한 다음 이 계산의 결과인 새로운 정수를 다시 같은 스택에 저장해야 하는 등 더 많은 측면이 있습니다. 또한 이 명령의 실행 단계는 전체 스마트 콘트랙트 실행 흐름에 통합되어야 하며, 실행 순서와 타이밍이 정확해야 합니다.

따라서 XOR 명령 실행의 효과는 데이터 스택에서 두 개의 숫자를 꺼내고, 해당 숫자의 XOR 결과를 누르고, 프로그램 카운터가 스마트 컨트랙트의 다음 명령을 가리키도록 증가시키는 것입니다.

여기에서 정확성 속성의 정의가 일반적으로 기존 바이트코드 VM을 검증할 때 사용하는 것과 유사하다는 것을 알기란 어렵지 않습니다. 이더넷 L1 노드의 EVM 인터프리터)는 기존 바이트코드 VM을 검증할 때 직면하는 문제와 매우 유사합니다. 이는 머신 상태(여기서는 스택 메모리 및 실행 흐름)에 대한 높은 수준의 추상적 정의와 각 명령어의 예상 동작(여기서는 산술 논리)에 대한 정의에 의존합니다.

그러나 아래에서 살펴보겠지만, ZKP와 zkVM의 특수한 특성으로 인해 그 정확성을 검증하는 과정은 일반 VM의 그것과 매우 다른 경우가 많습니다. 여기서 단일 명령어를 검증하는 것만으로도 zkWASM의 많은 테이블, 즉 값의 크기를 제한하는 범위 테이블, 이진 비트 계산의 중간 결과를 위한 비트 테이블, 각 행에 일정한 크기의 VM 상태를 저장하는 실행 테이블(물리적 CPU의 레지스터 및 래치에 있는 데이터와 유사), 동적으로 가변 크기 VM 상태(메모리, 데이터 스택, 호출 스택)를 나타내는 테이블, 메모리 테이블과 점프 테이블이 있습니다.

1단계: 스택 메모리

기존 VM과 마찬가지로 스택에서 명령어의 두 정수 매개변수를 읽을 수 있는지, 그리고 그 결과 값이 스택에 올바르게 다시 기록되는지 확인해야 합니다. 스택의 형식적 표현은 전역 메모리 및 힙 메모리와 함께 상당히 친숙해 보이지만, XOR 명령어는 이를 사용하지 않습니다.

zkVM은 복잡한 체계를 사용하여 동적 데이터를 표현합니다. 동적 데이터를 표현하기 위해 복잡한 체계를 사용하는데, 이는 ZK 증명자가 기본적으로 스택이나 배열과 같은 데이터 구조를 지원하지 않기 때문입니다. 대신 스택에 누르는 각 값에 대해 메모리 테이블이 별도의 행에 기록되며, 특정 열은 해당 테이블 항목이 유효한 시점을 나타내는 데 사용됩니다. 물론 이러한 테이블의 데이터는 공격자가 제어할 수 있으므로 컨트랙트 실행 중에 테이블 항목이 실제 스택을 누르는 명령과 실제로 일치하는지 확인하기 위해 몇 가지 제약 조건도 적용해야 합니다. 이는 프로그램 실행 중에 스택의 수를 주의 깊게 세어 확인함으로써 달성할 수 있습니다. 각 명령어를 검증할 때 이 카운트가 항상 정확한지 확인해야 합니다. 또한, 단일 명령어에서 생성된 제약 조건을 스택 연산을 구현하는 테이블 조회 및 시간 범위 확인과 연관시키는 일련의 레마가 있습니다. 최상위 수준에서 메모리 연산에 대한 개수 제약 조건은 다음과 같이 정의됩니다.

2단계: 산술 연산

기존 VM과 마찬가지로 비트 동형성의 산술 연산이 올바른지 확인해야 합니다. 물리적 컴퓨터 CPU는 이 연산을 한 번에 수행할 수 있기 때문에 이 작업은 충분히 쉬워 보입니다.

zkWasm 비트 테이블 사양의 세그먼트

기존 프로그래밍 언어에서는 매우 간단한 변칙 연산은 이러한 보조 테이블의 정확성을 검증하기 위해 많은 레마가 필요하지만, 여기서는 많은 레마가 필요합니다. 지침은 다음과 같습니다.

3단계: 실행 스트림

기존 VM과 마찬가지로 프로그램 카운터 값이 올바르게 업데이트되는지 확인해야 합니다. XOR과 같은 순차적 명령어의 경우 각 실행 단계마다 프로그램 카운터에 1을 더해야 합니다.

zkWasm은 Wasm 코드를 실행하도록 설계되었으므로 실행 내내 Wasm 메모리의 불변성이 항상 유지되는지 확인하는 것도 중요합니다.

기존 프로그래밍 언어는 부울 값, 8비트 정수, 64비트 정수 등과 같은 데이터 유형을 기본적으로 지원하지만, ZK 회로에서는 변수가 항상 큰 소수(≈ 2254)의 정수 모듈로 변하는 범위에서 변합니다. VM은 일반적으로 64비트 숫자로 실행되므로 회로 개발자는 올바른 숫자 범위를 확보하기 위해 제약 시스템을 사용해야 하며, 공식 검증 엔지니어는 검증 프로세스 전반에 걸쳐 이러한 범위에 대한 불변 속성을 추적해야 합니다. 실행 흐름과 실행 테이블에 대한 추론에는 다른 모든 보조 테이블이 포함되므로 모든 테이블 데이터의 범위가 올바른지 확인해야 합니다.

메모리 연산 횟수 관리의 경우와 유사합니다. 의 경우와 유사하게 zkVM에서도 제어 흐름을 확인하기 위해 유사한 프리미티브 집합이 필요합니다. 특히 각 호출 및 반환 명령어에는 호출 스택을 사용해야 합니다. 호출 스택은 데이터 스택과 유사한 테이블 체계를 사용하여 구현됩니다. XOR 명령어의 경우 호출 스택을 수정할 필요가 없지만 전체 명령어를 검증할 때는 여전히 제어 흐름 연산 횟수가 올바른지 추적하고 확인해야 합니다.

이 명령어 검증하기

모든 단계를 종합하여 zkWasm XOR 명령어의 엔드투엔드 정확성 정리를 검증해 보겠습니다. 다음 검증은 대화형 증명 환경에서 이루어지며, 각 형식적 구성과 논리적 추론 단계는 가장 엄격한 기계 검사를 거칩니다.

위에서 보았듯이, zkVM 회로의 공식적인 검증은 가능합니다. 그러나 많은 복잡한 불변 속성을 이해하고 추적해야 하는 어려운 작업입니다. 이는 검증 대상 소프트웨어 자체의 복잡성을 반영하는 것으로, 회로 개발자는 검증과 관련된 모든 렘마를 올바르게 처리해야 합니다. 관련된 높은 위험을 고려할 때, 신중한 수동 검토에만 의존하기보다는 공식적인 검증 시스템에 의해 기계적으로 검사하는 것이 좋습니다.