영지식 증명의 고급 공식 검증 에 관한 이 블로그 시리즈에서 우리는 ZK 지침을 검증하는 방법을 논의하고 두 가지 ZK 취약점에 대해 심층적으로 살펴보았습니다 . 모든 zkWasm 명령을 공식적으로 검증함으로써 우리는 모든 취약점을 발견하고 수정했으며 공개 보고서 및 코드 베이스 에 표시된 대로 전체 zkWasm 회로의 기술적 안전성과 정확성을 완전히 검증할 수 있었습니다.
우리는 zkWasm 명령을 검증하는 과정을 시연하고 관련 프로젝트의 예비 개념을 소개했지만, 공식 검증에 익숙한 독자는 다른 소규모 ZK 시스템이나 다른 유형의 바이트코드 VM을 사용한 zkVM 검증을 이해하는 데 더 관심이 있을 수 있습니다. 에. 이 기사에서는 zkWasm 메모리 하위 시스템을 검증할 때 직면하게 되는 몇 가지 기술적 사항에 대해 심도 있게 논의할 것입니다. 메모리는 zkVM의 가장 독특한 부분이며 이를 처리하는 것은 다른 모든 zkVM 검증에 중요합니다.
공식 검증: 가상 머신(VM) 대 ZK 가상 머신(zkVM)
우리의 궁극적인 목표는 일반 바이트코드 해석기(이더리움 노드에서 사용하는 EVM 해석기와 같은 VM)의 정확성 정리와 유사한 zkWasm의 정확성을 검증하는 것입니다. 즉, 인터프리터의 각 실행 단계는 언어의 연산 의미에 따른 적법한 단계에 해당합니다. 아래 그림과 같이 바이트코드 인터프리터의 데이터 구조의 현재 상태가 SL이고, 이 상태가 Wasm 머신의 상위 수준 사양에서 상태 SH로 표시되어 있다면, 인터프리터가 상태 SL로 단계를 밟을 때, 해당 법적 상위 수준 상태 SH여야 하며, Wasm 사양에서는 SH가 SH로 단계를 밟아야 한다고 규정합니다.
마찬가지로, zkVM은 유사한 정확성 정리를 가지고 있습니다. 즉, zkWasm 실행 테이블의 각각의 새로운 행은 언어의 작동 의미에 기반한 합법적인 단계에 해당합니다. 아래 그림과 같이 실행 테이블의 데이터 구조 행의 현재 상태가 SR이고, 이 상태가 Wasm 머신의 상위 사양에서 상태 SH로 표현된다면, SR 상태는 실행 테이블의 다음 행은 상위 수준 상태 SH에 해당해야 하며 Wasm 사양에서는 SH가 SH로 단계를 밟아야 한다고 규정합니다.
상위 수준 상태 및 Wasm 단계의 사양은 VM이든 zkVM이든 일관되므로 프로그래밍 언어 해석기 또는 컴파일러를 사용한 이전 검증 경험을 활용할 수 있습니다. zkVM 검증을 특별하게 만드는 것은 시스템의 하위 수준 상태를 구성하는 데이터 구조 유형입니다.
첫째, 이전 블로그 게시물 에서 언급했듯이 zk 증명자는 기본적으로 큰 소수 모듈로 정수 연산을 수행하는 반면, Wasm 사양과 일반 인터프리터는 32비트 또는 64비트 정수를 처리합니다. 대부분의 zkVM 구현에는 이것이 포함되므로 해당 처리도 검증 중에 수행되어야 합니다. 그러나 이는 로컬 문제입니다. 각 코드 줄은 처리해야 하는 산술 연산으로 인해 더욱 복잡해지지만 코드와 증명의 전체 구조는 변경되지 않습니다.
또 다른 주요 차이점은 동적으로 크기가 조정된 데이터 구조를 처리하는 방법입니다. 일반 바이트코드 인터프리터에서 메모리, 데이터 스택 및 호출 스택은 모두 변경 가능한 데이터 구조로 구현됩니다. 마찬가지로 Wasm 사양은 메모리를 get/set 메서드가 있는 데이터 유형으로 나타냅니다. 예를 들어 Geth의 EVM 인터프리터에는 물리적 메모리를 나타내는 바이트 배열로 구현되고 Set 32 및 GetPtr 메서드를 통해 쓰고 읽는 Memory 데이터 유형이 있습니다. 메모리 저장 명령을 구현하기 위해 Geth는 Set 32를 호출하여 물리적 메모리를 수정합니다.
func opMstore(pc *uint 64, 인터프리터 *EVMInterpreter, 범위 *ScopeContext) ([]byte, error) {
//스택의 값 팝
mStart, val := 범위.Stack.pop(), 범위.Stack.pop()
범위.메모리.세트 32(mStart.Uint 64(), val)
0을 반환, 0
}
위 인터프리터의 정확성 증명에서는 인터프리터의 구체적인 메모리와 사양의 추상 메모리에 값을 할당한 후 상위 수준 상태와 하위 수준 상태가 서로 일치함을 증명했습니다.
그러나 zkVM을 사용하면 상황이 더욱 복잡해집니다.
zkWasm의 메모리 테이블과 메모리 추상화 계층
zkVM에는 고정 크기 데이터(CPU의 레지스터와 유사)에 대한 실행 테이블 열이 있지만 보조 테이블을 검색하여 구현되는 동적인 크기의 데이터 구조를 처리하는 데 사용할 수 없습니다. zkWasm의 실행 테이블에는 값이 1, 2, 3...인 EID 열이 있으며 메모리 데이터와 호출 스택을 각각 나타내는 데 사용되는 메모리 테이블과 점프 테이블이라는 두 개의 보조 테이블이 있습니다.
다음은 탈퇴 프로그램을 구현하는 방법의 예입니다.
int 잔액, 금액;
무효 메인 () {
잔액 = 100;
금액 = 10;
잔액 -= 금액; // 인출
}
실행 테이블의 내용과 구조는 매우 간단합니다. 여기에는 6개의 실행 단계(EID 1~6)가 있으며, 각 단계에는 opcode를 나열하는 행이 있으며, 명령이 메모리 읽기 또는 쓰기인 경우 해당 주소와 데이터가 있습니다.
메모리 테이블의 각 행에는 주소, 데이터, 시작 EID 및 종료 EID가 포함됩니다. 시작 EID는 이 데이터를 이 주소에 쓰는 실행 단계의 EID이고, 종료 EID는 이 주소를 쓸 다음 실행 단계의 EID입니다. (나중에 자세히 설명하는 개수도 포함되어 있습니다.) Wasm 메모리 읽기 명령 회로의 경우 조회 제약 조건을 사용하여 읽기 명령의 EID가 테이블에 적절한 항목이 있는지 확인합니다. 처음부터 끝까지 범위 내부. (마찬가지로 점프 테이블의 각 행은 호출 스택의 프레임에 해당하며 각 행에는 이를 생성한 호출 명령 단계의 EID가 표시됩니다.)
이 메모리 시스템은 일반 VM 인터프리터와 크게 다릅니다. 점진적으로 업데이트되는 가변 메모리 대신 메모리 테이블에는 실행 추적 전체에 걸쳐 모든 메모리 액세스 기록이 포함됩니다. 프로그래머의 작업을 단순화하기 위해 zkWasm은 두 가지 편리한 입력 기능을 통해 구현된 추상화 계층을 제공합니다. 그들은:
alloc_memory_table_lookup_write_cell
그리고
Alloc_memory_table_lookup_read_cell
해당 매개변수는 다음과 같습니다.
예를 들어, zkWasm에서 메모리 저장 명령을 구현하는 코드에는 write alloc 함수에 대한 호출이 포함되어 있습니다.
memory_table_lookup_heap_write1 = 할당자
.alloc_memory_table_lookup_write_cell_with_value(
저장 쓰기 해상도 1,
제약_빌더,
이드,
이동 |____| Constant_from!(LocationType::Heap as u 64),
이동 |meta|load_block_index.expr(meta), // 주소
move |____| Constant_from!(0), // 32비트입니다.
move |____| Constant_from!( 1), // (항상) 활성화됨
);
store_value_in_heap1 = memory_table_lookup_heap_write1.value_cell을 두십시오.
`alloc` 함수는 테이블 간의 조회 제약 조건과 현재 `eid`를 메모리 테이블 항목과 관련된 산술 제약 조건을 처리하는 역할을 합니다. 이를 통해 프로그래머는 이러한 테이블을 일반 메모리로 취급할 수 있으며 코드가 실행된 후 `store_value_in_heap1` 값이 `load_block_index` 주소에 할당되었습니다.
마찬가지로, 메모리 읽기 명령은 `read_alloc` 함수를 사용하여 구현됩니다. 위의 예제 실행 시퀀스에는 각 로드 명령에 대한 읽기 제약 조건과 각 저장 명령에 대한 쓰기 제약 조건이 있으며 각 제약 조건은 메모리 테이블의 항목에 의해 충족됩니다.
mtable_lookup_write(1.eid 행, 1.store_addr 행, 1.store_value 행)
⇐ (1.eid= 1 행 ∧ 1.store_addr=잔액 ∧ 1.store_value= 100 ∧ ...)
mtable_lookup_write(2.eid행, 2.store_addr행, 2.store_value행)
⇐ (2.eid= 2 행 ∧ 2.store_addr=금액 ∧ 2.store_value= 10 ∧ ...)
mtable_lookup_read(3.eid행, 3.load_addr행, 3.load_value행)
⇐ ( 2<3.eid≤ 6 ∧ 3행.load_addr=금액 ∧ 3행.load_value= 100 ∧ ...)
mtable_lookup_read(4.eid행, 4.load_addr행, 4.load_value행)
⇐ ( 1<행 4.eid≤ 6 ∧ 행 4.load_addr=balance ∧ 행 4.load_value= 10 ∧ ...)
mtable_lookup_write(6.eid행, 6.store_addr행, 6.store_value행)
⇐ (6행.eid= 6 ∧ 6.store_addr=잔액 ∧ 6행.store_value= 90 ∧ ...)
공식 검증의 구조는 검증 중인 소프트웨어에 사용된 추상화와 일치해야 하며, 그래야 증명이 코드와 동일한 논리를 따를 수 있습니다. zkWasm의 경우 이는 메모리 테이블 회로를 검증하고 가변 메모리처럼 인터페이스하는 모듈로서 읽기/쓰기 셀 할당 기능을 확인해야 함을 의미합니다. 이러한 인터페이스가 제공되면 각 명령 회로의 검증은 일반 인터프리터와 유사한 방식으로 수행될 수 있으며, 추가적인 ZK 복잡성은 메모리 하위 시스템 모듈에 캡슐화됩니다.
검증에서는 메모리 테이블이 실제로 변경 가능한 데이터 구조로 간주될 수 있다는 아이디어를 구현했습니다. 즉, 메모리 테이블을 완전히 스캔하고 해당 주소 데이터 매핑을 구성하는 `memory_at type` 함수를 작성합니다. (여기서 type 변수의 값 범위는 Wasm 메모리 데이터의 세 가지 다른 유형: 힙, 데이터 스택 및 전역 변수입니다.) 그런 다음 alloc 함수에 의해 생성된 메모리 제약 조건이 set 및 get을 사용하는 것과 동일하다는 것을 증명합니다. 해당 주소 데이터 매핑에 의해 이루어진 데이터 변경입니다. 우리는 다음을 증명할 수 있습니다:
각 eid에 대해 다음 제약 조건이 적용되는 경우
memory_table_lookup_read_cell eid 유형 오프셋 값
하지만
get (memory_at eid type) offset = 일부 값
그리고, 다음과 같은 제약조건이 성립한다면
memory_table_lookup_write_cell eid 유형 오프셋 값
하지만
memory_at (eid+ 1) 유형 = (memory_at eid 유형) 오프셋 값 설정
그런 다음 각 명령어의 검증은 ZK가 아닌 바이트코드 인터프리터와 유사하게 주소 데이터 맵의 가져오기 및 설정 작업을 기반으로 이루어질 수 있습니다.
zkWasm의 메모리 쓰기 계산 메커니즘
그러나 위의 간략한 설명에서는 메모리 테이블과 점프 테이블의 내용이 모두 드러나지 않습니다. zkVM의 프레임워크에서 이러한 테이블은 공격자가 조작할 수 있으며, 공격자는 데이터 행을 삽입하여 임의의 값을 반환하도록 메모리 로드 명령을 쉽게 조작할 수 있습니다.
출금 프로그램을 예로 들면, 공격자는 출금 작업 전 $110의 메모리 쓰기 작업을 위조하여 계정 잔액에 허위 데이터를 주입할 기회를 갖게 됩니다. 이 프로세스는 메모리 테이블에 데이터 행을 추가하고 메모리 테이블과 실행 테이블에 있는 기존 셀의 값을 수정하여 수행할 수 있습니다. 수술 후에도 계정 잔액이 여전히 $100로 유지되므로 무료 인출이 가능합니다.
메모리 테이블(및 점프 테이블)에 실제로 실행되는 메모리 쓰기(및 호출 및 반환) 명령에 의해 생성된 유효한 항목만 포함되도록 하기 위해 zkWasm은 특수 계산 메커니즘을 사용하여 항목 수를 모니터링합니다. 특히, 메모리 테이블에는 메모리에 기록된 총 항목 수를 추적하는 전용 열이 있습니다. 동시에 실행 테이블에는 각 명령어에 대해 예상되는 메모리 쓰기 작업 수를 계산하는 카운터도 포함되어 있습니다. 동등 제약 조건을 설정하여 두 개수가 일치하는지 확인하세요. 이 방법의 논리는 매우 직관적입니다. 메모리에서 쓰기 작업이 수행될 때마다 한 번 계산되며 메모리 테이블에 해당 레코드가 있어야 합니다. 따라서 공격자는 메모리 테이블에 추가 항목을 삽입할 수 없습니다.
위의 논리적 진술은 다소 모호하며, 기계화된 증명 과정에서 더 정확해질 필요가 있습니다. 먼저 위에서 언급한 메모리 쓰기 보조정리의 설명을 수정해야 합니다. 주어진 `eid` 및 `type`을 사용하여 메모리 테이블 항목을 계산하기 위해 `mops_at eid type` 함수를 정의합니다(대부분의 명령어는 eid`에서 0 또는 1개의 항목을 생성합니다). 정리의 전체 설명에는 가짜 메모리 테이블 항목이 없다는 추가 전제 조건이 있습니다.
다음 제약 조건이 적용되는 경우
(memory_table_lookup_write_cell eid 유형 오프셋 값)
그리고 다음과 같은 새로운 제약 조건이 설정됩니다.
(mops_at eid 유형) = 1
하지만
(memory_at(eid+ 1) 유형) = (memory_at eid 유형) 오프셋 값 설정
이를 위해서는 이전 사례보다 더 정확한 검증이 필요합니다. 단순히 메모리 테이블 항목의 총 개수가 실행 시 총 메모리 쓰기 개수와 동일하다는 등식 제약 조건을 도출하는 것만으로는 검증을 완료하는 데 충분하지 않습니다. 명령어의 정확성을 증명하려면 각 명령어가 올바른 메모리 테이블 항목 수에 해당하는지 알아야 합니다. 예를 들어, 공격자가 실행 시퀀스의 명령어에 대한 메모리 테이블 항목을 생략하고 관련되지 않은 다른 명령어에 대해 악의적인 새 메모리 테이블 항목을 생성할 수 있는지 여부를 배제해야 합니다.
이를 증명하기 위해 우리는 하향식 접근 방식을 사용하여 주어진 명령어에 해당하는 메모리 테이블 항목 수를 제한하며, 이는 세 단계를 포함합니다. 먼저, 명령어 유형에 따라 실행 시퀀스에서 해당 명령어에 대해 생성되어야 하는 항목 수를 추정합니다. i번째 단계부터 실행이 끝날 때까지 예상되는 쓰기 수를 instructions_mops i라고 하고, i번째 명령어부터 실행이 끝날 때까지 메모리 테이블의 해당 항목 수를 cum_mops(eid i)라고 합니다. 각 명령어의 검색 제약 조건을 분석함으로써 예상보다 적은 항목을 생성하지 않는다는 것을 증명할 수 있으며, 따라서 추적된 각 세그먼트 [i... numRows]가 예상보다 적은 항목을 생성하지 않는다는 결론을 내릴 수 있습니다.
기본정리 cum_mops_bound: 모든 ni에 대해,
0 ≤ 나는 ->
i + Z.of_nat n = etable_numRow ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) ≥ Instructions_mops i n.
둘째, 테이블에 예상보다 많은 항목이 없다는 것을 증명할 수 있다면 테이블의 항목 수가 정확하게 올바른 것입니다.
기본정리 cum_mops_equal: 모든 ni에 대해,
0 ≤ 나는 ->
i + Z.of_nat n = etable_numRow ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) ≤ Instructions_mops in ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) = Instructions_mops i n.
이제 3단계로 진행하세요. 우리의 정확성 정리는 임의의 n에 대해 cum_mops 및 Instructions_mops가 행 n에서 테이블 끝까지 항상 일관적이라고 명시합니다.
기본정리 cum_mops_equal : 모든 n에 대해,
0 <= Z.of_nat n < etable_numRow ->
MTable.cum_mops (etable_values eid_cell (Z.of_nat n)) (max_eid+ 1) = Instructions_mops (Z.of_nat n)
검증은 n을 요약하여 수행됩니다. 테이블의 첫 번째 행은 zkWasm의 동등 제약 조건으로, 메모리 테이블의 총 항목 수가 정확함을 나타냅니다. 즉, cum_mops 0 = Instructions_mops 0 입니다. 다음 라인에 대해 귀납적 가설은 우리에게 다음을 알려줍니다.
cum_mops n = 지침_mops n
그리고 우리는 증명하기를 희망합니다
cum_mops (n+ 1) = Instructions_mops (n+ 1)
여기에 주목하세요
cum_mops n = mop_at n + cum_mops (n+ 1)
그리고
Instructions_mops n = Instruction_mops n + Instruction_mops (n+ 1)
그러므로 우리는 얻을 수 있습니다
mops_at n + cum_mops (n+ 1) = Instruction_mops n + Instructions_mops (n+ 1)
이전에는 각 명령이 예상되는 항목 수보다 적지 않은 항목을 생성한다는 것을 보여주었습니다.
mops_at n ≥ Instruction_mops n.
그래서 결론을 내릴 수 있다
cum_mops (n+ 1) ≤ Instructions_mops (n+ 1)
여기서 우리는 위의 두 번째 보조정리를 적용해야 합니다.
(점프 테이블을 검증하기 위해 유사한 보조정리를 사용하면 각 호출 명령이 점프 테이블 항목을 정확하게 생성할 수 있음을 증명할 수 있으므로 이 증명 기술은 일반적으로 적용 가능합니다. 그러나 반환 정확성을 증명하려면 여전히 추가 검증 작업이 필요합니다. 반환된 eid는 호출 프레임을 생성한 호출 명령어의 eid와 다르므로 실행 시퀀스 중에 eid 값이 한 방향으로 증가한다고 선언하는 추가 불변 속성 도 필요합니다.
증명 프로세스를 이렇게 자세히 설명하는 것은 공식적인 검증의 전형적인 현상이며 특정 코드 부분을 검증하는 데 코드를 작성하는 것보다 시간이 더 오래 걸리는 이유이기도 합니다. 하지만 그만한 가치가 있나요? 이 경우에는 증명 중에 점프 테이블 계산 메커니즘에서 심각한 버그를 발견했기 때문에 가치가 있었습니다. 이 버그는 이전 기사 에서 자세히 설명했습니다. 요약하면 이전 버전의 코드는 호출 및 반환 명령을 모두 담당했으며 공격자는 실행 순서에 반환 명령을 추가하여 공간을 확보하여 가짜 점프를 만들 수 있었습니다. . 잘못된 계산 메커니즘이 모든 호출 및 반환 명령어가 계산된다는 직관을 만족시킬 수 있지만 이러한 직관을 보다 정확한 정리문으로 정제하려고 하면 문제가 발생합니다.
증명 과정을 모듈화하세요
위의 논의에서 우리는 각 명령어의 회로에 대한 증명과 실행 테이블의 카운트 열에 대한 증명 사이에 순환 종속성이 있음을 알 수 있습니다. 명령 회로의 정확성을 증명하려면 메모리 쓰기에 대해 추론해야 합니다. 즉, 특정 EID의 메모리 테이블 항목 수를 알아야 하며, 메모리 쓰기 작업 개수를 증명해야 합니다. 실행 테이블이 정확하며 이는 또한 각 명령어가 최소한의 메모리 쓰기 횟수를 수행한다는 것을 증명하는 데 필요합니다.
또한 고려해야 할 또 다른 요소가 있습니다. zkWasm 프로젝트는 규모가 상당히 크기 때문에 여러 검증 엔지니어가 작업을 분할할 수 있도록 검증 작업을 모듈화해야 합니다. 따라서 계산 메커니즘의 증명을 분해할 때 복잡성에 특별한 주의를 기울여야 합니다. 예를 들어 LocalGet 명령어의 경우 다음과 같은 두 가지 정리가 있습니다.
정리 opcode_mops_correct_local_get : 모든 i에 대해,
0 <= 나는 ->
etable_values eid_cell i > 0 ->
opcode_mops_corright LocalGet i.
정리 LocalGetOp_corlect: 모든 i st y xs에 대해,
0 <= 나는 ->
etable_values enabled_cell i = 1 ->
mops_at_corright 나는 ->
etable_values (ops_cell LocalGet) i = 1 ->
state_rel i st ->
wasm_stack st = xs ->
(etable_values offset_cell i) > 1 ->
nth_error xs (Z.to_nat (etable_values offset_cell i - 1)) = 일부 y ->
state_rel (i+ 1) (update_stack (incr_iid st) (y::xs)).
첫 번째 정리 진술
opcode_mops_corright LocalGet i
확장되면 이는 명령이 라인 i에 하나 이상의 메모리 테이블 항목을 생성한다는 것을 의미합니다(숫자 1은 zkWasm의 LocalGet opcode 사양에 지정됨).
두 번째 정리는 명령어에 대한 완전한 정확성 정리입니다.
mops_at_올바른 나
가설로서 이는 명령어가 정확히 하나의 메모리 테이블 항목을 생성한다는 것을 의미합니다.
검증 엔지니어는 이 두 가지 정리를 독립적으로 증명한 다음 이를 실행 테이블에 대한 증명과 결합하여 전체 시스템의 정확성을 증명할 수 있습니다. 개별 명령어에 대한 모든 증명은 메모리 테이블의 특정 구현을 알지 못해도 읽기/쓰기 제약 조건 수준에서 수행될 수 있다는 점은 주목할 가치가 있습니다. 따라서 프로젝트는 독립적으로 처리할 수 있는 세 부분으로 나누어집니다.
요약하다
zkVM의 회로를 한 줄씩 검증하는 것은 다른 도메인의 ZK 애플리케이션을 검증하는 것과 근본적으로 다르지 않습니다. 두 가지 모두 산술 제약 조건에 대해 비슷한 추론이 필요하기 때문입니다. 높은 수준에서 zkVM 검증에는 프로그래밍 언어 해석기 및 컴파일러에 사용되는 것과 동일한 많은 공식 검증 방법이 필요합니다. 여기서 가장 큰 차이점은 동적으로 크기가 조정되는 가상 머신 상태입니다. 그러나 구현에 사용된 추상화 계층과 일치하도록 검증 구조를 신중하게 구성함으로써 이러한 차이점의 영향을 최소화할 수 있으며, 각 명령어는 일반 해석기 화학적 검증과 마찬가지로 get-set 인터페이스를 기반으로 하는 독립적인 모듈이 될 수 있습니다.
