영지식 증명의 고급 형식 검증: ZK 명령어 검증 방법

정식 검증 기술이 zkVM(영지식 가상 머신)에 어떻게 적용되는지 깊이 이해하기 위해 이번 글에서는 단일 명령의 검증에 중점을 두겠습니다. ZKP(영지식 증명)의 고급 형식 검증에 대한 전반적인 상황은 동시에 게시된 "영지식 증명 블록체인의 고급 형식 검증" 기사를 참조하시기 바랍니다.

ZK 지침 검증이란 무엇입니까?

zkVM(영지식 가상 머신)은 특정 프로그램이 특정 입력에서 실행되고 성공적으로 종료될 수 있다는 증거로 간단한 증명 개체를 생성할 수 있습니다. Web3.0 분야에서 zkVM을 적용하면 L1 노드가 스마트 계약의 입력 상태에서 출력 상태로의 전환에 대한 간단한 증명만 검증하면 되고 실제 계약 코드 실행은 오프체인에서 완료될 수 있기 때문에 높은 처리량이 가능합니다.

zkVM 증명자는 먼저 프로그램을 실행하여 각 단계의 실행 기록을 생성한 다음 실행 기록 데이터를 일련의 수치 테이블로 변환합니다(이 프로세스를 "산술화"라고 함). 이러한 숫자는 특정 테이블 셀 간의 연결 방정식, 고정 상수, 테이블 간의 데이터베이스 검색 제약 조건 및 인접한 테이블 행의 각 쌍 간에 충족되어야 하는 제약 조건을 포함하는 일련의 제약 조건(예: 회로)을 충족해야 합니다. 방정식(일명 "게이트"). 온체인 검증을 통해 실제로 모든 제약 조건을 충족하는 테이블이 있는지 확인할 수 있으며, 동시에 테이블의 특정 숫자가 표시되지 않도록 할 수 있습니다.

각 VM 명령어의 실행에는 이러한 많은 제약이 따릅니다. 여기서는 VM 명령어의 이러한 제약 조건 집합을 "ZK 명령어"라고 합니다. 다음은 Rust로 작성된 zkWasm 메모리 로드 명령 제약 조건의 예입니다.

ZK 지침의 공식적인 검증은 먼저 형식 언어로 번역된 이러한 코드에 대한 형식적 추론을 수행하여 수행됩니다.

단일 제약 조건에만 오류가 포함되어 있어도 공격자가 악의적인 ZK 증명을 제출할 수 있습니다. 악의적인 증명에 해당하는 데이터 테이블은 스마트 계약의 합법적인 작동과 일치하지 않습니다. 서로 다른 EVM(Ethereum Virtual Machine) 구현을 실행하는 많은 노드가 있어 동일한 버그가 동시에 같은 장소에서 발생할 가능성이 거의 없는 Ethereum과 같은 비 ZK 체인과 달리 zkVM 체인에는 단일 VM 구현만 있습니다. . 이러한 관점만으로도 ZK 체인은 기존 Web3.0 시스템보다 더 취약합니다.

더 나쁜 점은 ZK가 아닌 체인과 달리 zkVM 거래의 계산 세부 사항이 체인에 제출 및 저장되지 않기 때문에 공격이 발생한 후에는 공격의 구체적인 세부 사항을 발견하는 것이 매우 어려울 뿐만 아니라 공격을 식별하는 것 자체도 매우 어려울 수 있습니다.

zkVM 시스템은 매우 엄격한 검사가 필요합니다. 불행하게도 zkVM 회로의 정확성은 보장하기 어렵습니다.

ZK 지침을 확인하는 것이 왜 어려운가요?

VM(Virtual Machine)은 Web3.0 시스템 아키텍처에서 가장 복잡한 부분 중 하나입니다. 스마트 계약의 강력한 기능은 Web3.0 기능을 지원하는 핵심입니다. 그 힘은 유연하고 복잡한 기본 VM에서 나옵니다. 일반 컴퓨팅 및 스토리지 작업을 완료하려면 이러한 VM이 수많은 지침을 지원할 수 있어야 합니다. 그리고 상태. 예를 들어 EVM의 geth 구현에는 7,500줄 이상의 Go 언어 코드가 필요합니다. 마찬가지로, 이러한 명령의 실행을 제한하는 ZK 회로도 똑같이 크고 복잡합니다. zkWasm 프로젝트와 마찬가지로 ZK 회로를 구현하려면 6000줄 이상의 Rust 코드가 필요합니다.

zkWasm 회로 아키텍처

특정 애플리케이션(예: 개인 결제)을 위해 설계된 ZK 시스템에 사용되는 전용 ZK 회로와 비교하면 zkVM 회로는 크기가 훨씬 더 큽니다. 바인딩 규칙 개수는 1개일 수 있습니다. 또는 2배 더 큰 규모이며, 산술 테이블에는 수백만 개의 숫자 셀을 포함하는 수백 개의 열이 포함될 수 있습니다.

ZK 지침 확인은 무엇을 의미하나요?

여기서는 zkWasm의 XOR 명령이 올바른지 확인하고 싶습니다. 기술적으로 말하면, zkWasm의 실행 테이블은 합법적인 Wasm VM 실행 순서에 해당합니다. 따라서 거시적 관점에서 우리가 확인하고 싶은 것은 이 명령어가 실행될 때마다 새로운 적법한 zkVM 상태가 항상 생성된다는 것입니다. 테이블의 각 행은 VM의 적법한 상태에 해당하고 다음 행은 항상 생성됩니다. 해당 VM 명령어를 실행하여 생성됩니다. 아래 그림은 XOR 명령의 정확성에 대한 공식 정리를 보여줍니다.

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

ZK 명령을 확인하는 방법은 무엇입니까?

정수의 계산 의미는 XOR 계산을 수행한 다음 계산된 새 정수를 동일한 스택에 다시 저장합니다. 또한 이 명령의 실행 단계는 전체 스마트 계약 실행 프로세스에 통합되어야 하며 실행 순서와 타이밍이 정확해야 합니다.

따라서 XOR 명령어의 실행 효과는 데이터 스택에서 두 개의 숫자를 팝하고 XOR 결과를 푸시하는 동시에 스마트 계약의 다음 명령어를 가리키도록 프로그램 카운터를 증가시키는 것입니다.

여기서 정확성 속성의 정의가 일반적으로 기존 바이트 코드 VM(예: Ethereum L1 노드의 EVM 인터프리터)을 확인할 때 직면하는 상황과 매우 유사하다는 것을 쉽게 알 수 있습니다. 이는 기계 상태(여기서는 스택 메모리 및 실행 흐름)에 대한 높은 수준의 추상 정의와 각 명령의 예상 동작(여기서는 산술 논리)에 대한 정의에 의존합니다.

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

1단계: 스택 메모리

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

zkVM은 동적 데이터를 표현하기 위해 복잡한 체계를 사용합니다. 왜냐하면 ZK 증명자는 기본적으로 스택이나 배열과 같은 데이터 구조를 지원하지 않기 때문입니다. 반대로, 스택에 푸시된 각 값에 대해 메모리 테이블은 별도의 행을 기록하고 일부 열은 항목의 유효 시간을 나타내는 데 사용됩니다. 물론 이러한 테이블의 데이터는 공격자가 제어할 수 있으므로 테이블 항목이 계약 실행 시 실제 스택 명령과 실제로 일치하는지 확인하기 위해 몇 가지 제약 조건을 적용해야 합니다. 이는 프로그램 실행 중 스택 푸시 수를 신중하게 계산하여 달성됩니다. 각 명령어를 확인할 때 이 개수가 항상 올바른지 확인해야 합니다. 또한 단일 명령에 의해 생성된 제약 조건을 스택 작업을 구현하는 테이블 조회 및 시간 범위 확인과 연결하는 일련의 기본 정리가 있습니다. 최상위 수준에서는 메모리 작업에 대한 계산 제약 조건이 다음과 같이 정의됩니다.

2단계: 산술 연산

기존 VM과 유사하게 비트별 XOR 연산이 올바른지 확인하려고 합니다. 모든 물리적 컴퓨터 CPU가 이 작업을 한 번에 수행할 수 있기 때문에 이는 쉬운 것처럼 보입니다.

하지만 zkVM의 경우 이는 실제로 간단하지 않습니다. ZK 증명자가 기본적으로 지원하는 유일한 산술 명령어는 덧셈과 곱셈입니다. 이진 비트 작업을 수행하기 위해 VM은 한 테이블이 고정된 바이트 수준 작업 결과를 저장하고 다른 테이블은 여러 테이블 행에서 작업을 수행하는 방법을 보여주는 "스크래치 패드" 역할을 하는 다소 복잡한 방식을 사용합니다. 64비트 숫자는 8바이트로 분할된 후 다시 조합되어 결과를 제공합니다.

ZkWasm 비트 테이블 사양 조각

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

3단계: 실행 흐름

기존 VM과 유사하게 프로그램 카운터 값이 올바르게 업데이트되었는지 확인해야 합니다. XOR과 같은 순차 명령어의 경우 프로그램 카운터는 각 단계마다 1씩 증가해야 합니다.

zkWasm은 Wasm 코드를 실행하도록 설계되었으므로 실행 전반에 걸쳐 Wasm 메모리의 불변 특성이 유지되도록 보장합니다.

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

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

이 명령어를 확인하세요

모든 단계를 종합하여 zkWasm XOR 명령어의 엔드투엔드 정확성 정리를 확인해 보겠습니다. 다음 검증은 모든 형식적 구성 및 논리적 추론 단계가 가장 엄격한 기계 점검을 거치는 대화형 증명 환경에서 완료됩니다.

위에서 본 것처럼 zkVM 회로의 정식 검증이 가능합니다. 그러나 이는 많은 복잡한 불변 속성을 이해하고 추적해야 하는 어려운 작업입니다. 이는 검증되는 소프트웨어의 복잡성을 반영합니다. 검증과 관련된 모든 보조정리는 회로 개발자가 올바르게 처리해야 합니다. 관련된 높은 이해관계를 고려할 때, 사람의 신중한 검토에만 의존하기보다는 공식적인 검증 시스템을 통해 기계로 점검하는 것이 가치 있을 것입니다.

위 내용은 영지식 증명의 고급 형식 검증: ZK 명령어 검증 방법의 상세 내용입니다. 자세한 내용은 PHP 중국어 웹사이트의 기타 관련 기사를 참조하세요!