두 개의 ZK 취약점 심층 분석

저자: CertiK

이전 기사에서는 제로 지식 증명의 고급 형식 검증에 대해 논의했습니다: ZK 명령어를 어떻게 검증하는지. 각 zkWasm 명령어를 형식적으로 검증함으로써 우리는 전체 zkWasm 회로의 기술적 안전성과 정확성을 완전히 검증할 수 있었습니다. 본문에서는 취약점 발견의 관점에 초점을 맞추어 감사 및 검증 과정에서 발견된 구체적인 취약점과 그로부터 얻은 경험과 교훈을 분석합니다. 제로 지식 증명(ZKP) 블록체인의 고급 형식 검증에 대한 일반적인 논의는 제로 지식 증명 블록체인의 고급 형식 검증 문서를 참조하십시오.

ZK 취약점에 대해 논의하기 전에 CertiK가 ZK 형식 검증을 어떻게 수행하는지 알아보겠습니다. ZK 가상 머신(zkVM)과 같은 복잡한 시스템에 대해 형식 검증(FV)의 첫 번째 단계는 검증해야 할 내용과 그 성격을 명확히 하는 것입니다. 이는 ZK 시스템의 설계, 코드 구현 및 테스트 설정에 대한 포괄적인 검토를 필요로 합니다. 이 과정은 일반적인 감사와 겹치는 부분이 있지만, 검토 후 검증의 목표와 성격을 확립해야 한다는 점에서 다릅니다. CertiK에서는 이를 검증 지향 감사라고 부릅니다. 감사와 검증 작업은 일반적으로 하나의 전체로 이루어집니다. zkWasm에 대해서는 감사와 형식 검증을 동시에 수행했습니다.

ZK 취약점이란 무엇인가?

제로 지식 증명 시스템의 핵심 특징은 오프라인 또는 비공식적으로 실행된 계산(예: 블록체인 거래)의 간단한 암호화 증명을 제로 지식 증명 검증자에게 전달하고, 이를 검토 및 확인하여 해당 계산이 실제로 선언된 대로 발생했음을 확신할 수 있도록 하는 것입니다. 이 점에서 ZK 취약점은 해커가 허위 거래를 증명하기 위해 위조된 ZK 증명을 제출할 수 있게 하며, ZK 증명 검사기가 이를 수용하게 만듭니다.

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

zkWasm 산술화 표

각 제약 조건의 정확성은 매우 중요합니다. 제약 조건 중 하나라도 오류가 있거나 누락되면 해커는 오해를 불러일으키는 증명을 제출할 수 있으며, 이러한 표는 스마트 계약의 유효한 실행을 나타내는 것처럼 보일 수 있지만 실제로는 그렇지 않습니다. 전통적인 VM과 비교할 때, zkVM 거래의 불투명성은 이러한 취약점을 확대합니다. 비ZK 체인에서는 거래의 계산 세부 사항이 블록에 공개적으로 기록되지만, zkVM은 이러한 세부 사항을 체인에 저장하지 않습니다. 투명성의 결여는 공격의 구체적인 상황을 파악하기 어렵게 만들며, 공격이 실제로 발생했는지조차 확인하기 어렵습니다.

zkVM 명령어 규칙을 실행하는 ZK 회로는 매우 복잡합니다. zkWasm의 경우, ZK 회로의 구현은 6,000줄 이상의 Rust 코드와 수백 개의 제약 조건을 포함합니다. 이러한 복잡성은 일반적으로 여러 개의 취약점이 발견되기를 기다리고 있음을 의미합니다.

zkWasm 회로 아키텍처

실제로 우리는 zkWasm 감사 및 형식 검증을 통해 여러 개의 이러한 취약점을 발견했습니다. 아래에서는 두 가지 대표적인 사례를 논의하고 그들 간의 차이점을 설명하겠습니다.

코드 취약점: Load8 데이터 주입 공격

첫 번째 취약점은 zkWasm의 Load8 명령어와 관련이 있습니다. zkWasm에서 힙 메모리의 읽기는 LoadN 명령어 집합을 통해 수행되며, 여기서 N은 로드할 데이터의 크기입니다. 예를 들어, Load64는 zkWasm 메모리 주소에서 64비트 데이터를 읽어야 합니다. Load8은 메모리에서 8비트 데이터(즉, 1바이트)를 읽고, 0으로 접두사를 붙여 64비트 값을 생성해야 합니다. zkWasm 내부에서는 메모리를 64비트 바이트 배열로 표현하므로, 메모리 배열의 일부를 "선택"해야 합니다. 이를 위해 네 개의 중간 변수(u16_cells)가 사용되며, 이 변수들은 함께 완전한 64비트 로드 값을 구성합니다.

이 LoadN 명령어의 제약 조건은 다음과 같이 정의됩니다:

이 제약 조건은 Load32, Load16 및 Load8의 세 가지 경우로 나뉩니다. Load64는 메모리 셀 자체가 64비트이기 때문에 제약이 없습니다. Load32의 경우, 코드는 메모리 셀의 상위 4바이트(32비트)가 반드시 0이어야 한다고 보장합니다.

Load16의 경우, 메모리 셀의 상위 6바이트(48비트)가 반드시 0이어야 합니다.

Load8의 경우, 메모리 셀의 상위 7바이트(56비트)가 0이어야 합니다. 불행히도, 코드에서는 그렇지 않습니다.

보시다시피, 상위 9비트에서 16비트만 0으로 제한되어 있습니다. 나머지 상위 48비트는 임의의 값일 수 있으며, 여전히 "메모리에서 읽은" 것처럼 가장할 수 있습니다.

이 취약점을 이용하여 해커는 합법적인 실행 시퀀스의 ZK 증명을 변조하여 Load8 명령어의 실행이 이러한 예기치 않은 바이트를 로드하게 하여 데이터 손상을 초래할 수 있습니다. 또한 주변 코드와 데이터를 정교하게 배치하면 허위 실행 및 전송을 유발하여 데이터와 자산을 탈취할 수 있습니다. 이러한 위조 거래는 zkWasm 검사기의 검사를 통과할 수 있으며, 블록체인에서 잘못된 거래로 인식될 수 있습니다.

이 취약점을 수정하는 것은 실제로 매우 간단합니다.

이 취약점은 "코드 취약점"이라고 불리는 취약점의 한 종류를 나타내며, 이는 코드 작성에서 발생하며, 작은 지역 코드 수정으로 쉽게 수정할 수 있습니다. 여러분이 동의할 수 있듯이, 이러한 취약점은 상대적으로 더 쉽게 발견될 수 있습니다.

설계 취약점: 위조 반환 공격

다음으로 zkWasm의 호출 및 반환에 관한 또 다른 취약점을 살펴보겠습니다. 호출 및 반환은 기본 VM 명령어로, 실행 중인 컨텍스트(예: 함수)가 다른 함수를 호출하고, 호출된 함수가 실행을 완료한 후 호출자 컨텍스트의 실행을 복원할 수 있게 합니다. 각 호출은 나중에 반환될 것으로 예상됩니다. zkWasm에서 호출 및 반환의 생애 주기 동안 추적되는 동적 데이터는 "호출 프레임(call frame)"이라고 합니다. zkWasm은 명령어를 순차적으로 실행하므로 모든 호출 프레임은 실행 과정에서 발생한 시간에 따라 정렬할 수 있습니다. 아래는 zkWasm에서 실행되는 호출/반환 코드의 예입니다.

사용자는 buytoken() 함수를 호출하여 토큰을 구매할 수 있습니다(아마도 지불하거나 다른 가치 있는 것을 이전하여). 그 핵심 단계 중 하나는 addtoken() 함수를 호출하여 실제로 토큰 계좌 잔액을 1 증가시키는 것입니다. ZK 증명기 자체는 호출 프레임 데이터 구조를 지원하지 않기 때문에 실행 표(E-Table)와 점프 표(J-Table)를 사용하여 이러한 호출 프레임의 전체 이력을 기록하고 추적해야 합니다.

위 그림은 buytoken()이 addtoken()을 호출하는 실행 과정과 addtoken()에서 buytoken()으로 반환하는 과정을 보여줍니다. 토큰 계좌 잔액이 1 증가한 것을 볼 수 있습니다. 실행 표에서 각 실행 단계는 한 행을 차지하며, 여기에는 현재 실행 중인 호출 프레임 번호, 현재 컨텍스트 함수 이름(여기서는 설명을 위해만 사용됨), 해당 함수 내 현재 실행 명령어의 번호, 그리고 표에 저장된 현재 명령어(여기서는 설명을 위해만 사용됨)가 포함됩니다. 점프 표에서는 각 호출 프레임이 한 행을 차지하며, 표에는 호출자 프레임의 번호, 호출자 함수 컨텍스트 이름(여기서는 설명을 위해만 사용됨), 호출자 프레임의 다음 명령어 위치(해당 프레임이 반환할 수 있도록) 등이 저장됩니다. 이 두 표 모두 jops 열이 있으며, 이는 현재 명령어가 호출/반환인지(실행 표에서) 및 해당 프레임(점프 표에서)에서 발생한 호출/반환 명령어의 총 수를 추적합니다.

사람들이 예상하는 바와 같이, 각 호출에는 해당하는 반환이 있어야 하며, 각 프레임에는 호출과 반환이 각각 한 번씩만 있어야 합니다. 위 그림에서 점프 표의 첫 번째 프레임의 jops 값은 2로, 실행 표의 첫 번째 행과 세 번째 행에 해당하며, 그곳의 jops 값은 1입니다. 현재로서는 모든 것이 정상으로 보입니다.

하지만 실제로는 문제가 있습니다: 한 번의 호출과 한 번의 반환이 프레임의 jops 카운트를 2로 만들지만, 두 번의 호출이나 두 번의 반환도 카운트를 2로 만들 수 있습니다. 각 프레임에 두 번의 호출이나 두 번의 반환이 있는 것은 다소 터무니없게 들릴 수 있지만, 해커가 예상된 것을 깨뜨리려는 것이 바로 이것임을 기억해야 합니다.

지금 여러분은 약간 흥분할지도 모르지만, 우리는 정말로 문제를 찾았나요?

결과적으로 두 번의 호출은 문제가 아니며, 실행 표와 호출 표의 제약 조건은 두 호출이 동일한 프레임의 행에 인코딩될 수 없도록 합니다. 각 호출은 새로운 프레임 번호를 생성하므로, 현재 호출 프레임 번호에 1을 더한 값이 됩니다.

하지만 두 번의 반환의 경우는 그렇게 운이 좋지 않습니다: 반환 시 새로운 프레임이 생성되지 않기 때문에 해커는 합법적인 실행 시퀀스의 실행 표와 호출 표를 가져와 위조된 반환(및 해당 프레임)을 주입할 수 있습니다. 예를 들어, 이전 실행 표와 호출 표에서 buytoken()이 addtoken()을 호출하는 예는 해커에 의해 다음과 같이 변조될 수 있습니다:

해커는 실행 표에서 원래 호출과 반환 사이에 두 번의 위조된 반환을 주입하고, 호출 표에 새로운 위조된 프레임 행을 추가했습니다(원래 반환 및 후속 명령어의 실행 단계 번호는 실행 표에서 4를 더해야 합니다). 호출 표의 각 행의 jops 카운트가 2이므로 제약 조건을 충족하며, zkWasm 증명 검사기는 이 위조된 실행 시퀀스의 "증명"을 수용하게 됩니다. 그림에서 볼 수 있듯이, 토큰 계좌 잔액이 1이 아니라 3으로 증가했습니다. 따라서 해커는 1개의 토큰을 지불하고 3개의 토큰을 얻을 수 있게 됩니다.

이 문제를 해결하는 방법은 여러 가지가 있습니다. 한 가지 명백한 방법은 호출과 반환을 각각 개별적으로 추적하고, 각 프레임에 정확히 한 번의 호출과 한 번의 반환이 있도록 보장하는 것입니다.

여러분은 지금까지 이 취약점의 코드 한 줄도 보여주지 않았다는 점을 주목했을 것입니다. 주된 이유는 문제가 있는 코드 한 줄이 없기 때문이며, 코드 구현은 표와 제약 설계에 완전히 부합합니다. 문제는 설계 자체에 있으며, 수정 방법도 마찬가지입니다.

여러분은 이 취약점이 명백해야 한다고 생각할 수 있지만, 실제로는 그렇지 않습니다. 이는 "두 번의 호출 또는 두 번의 반환도 jops 카운트를 2로 만들 수 있다"와 "실제로 두 번의 반환이 가능하다" 사이에 공백이 존재하기 때문입니다. 후자는 실행 표와 호출 표에서 관련된 다양한 제약 조건을 상세하고 완전하게 분석해야 하며, 완전한 비형식적 추론을 수행하기 어렵습니다.

두 개의 취약점 비교

"Load8 데이터 주입 취약점"과 "위조 반환 취약점"은 모두 해커가 ZK 증명을 조작하고, 허위 거래를 생성하며, 증명 검사기를 속이고, 도난 또는 탈취를 수행할 수 있게 할 수 있습니다. 그러나 그들의 성격과 발견된 방식은 완전히 다릅니다.

"Load8 데이터 주입 취약점"은 zkWasm 감사 중에 발견되었습니다. 이는 결코 쉬운 일이 아니며, 6,000줄 이상의 Rust 코드와 수백 개의 zkWasm 명령어의 수백 개 제약 조건을 검토해야 했기 때문입니다. 그럼에도 불구하고 이 취약점은 상대적으로 쉽게 발견되고 확인되었습니다. 이 취약점은 형식 검증이 시작되기 전에 수정되었기 때문에 검증 과정에서 마주치지 않았습니다. 감사 과정에서 이 취약점을 발견하지 못했다면, Load8 명령어의 검증에서 발견할 것으로 예상할 수 있습니다.

"위조 반환 취약점"은 감사 이후의 형식 검증 중에 발견되었습니다. 우리가 감사 중에 이를 발견하지 못한 부분적인 이유는 zkWasm에 jops와 매우 유사한 메커니즘인 "mops"가 존재하기 때문입니다. 이는 zkWasm 실행 중 각 메모리 셀의 역사적 데이터에 해당하는 메모리 접근 명령어를 추적합니다. mops의 카운트 제약 조건은 올바르며, 이는 메모리 쓰기라는 한 종류의 메모리 명령어만 추적하기 때문입니다. 또한 각 메모리 셀의 역사적 데이터는 불변이며 한 번만 기록됩니다(mops 카운트는 1). 그러나 감사 기간 동안 이 잠재적 취약점을 주목했더라도, 모든 관련 제약 조건에 대한 엄격한 형식적 추론을 수행하지 않으면 각 가능성을 쉽게 확인하거나 배제할 수 없었습니다. 왜냐하면 실제로는 문제가 있는 코드 한 줄이 없기 때문입니다.

결론적으로, 이 두 가지 취약점은 각각 "코드 취약점"과 "설계 취약점"에 해당합니다. 코드 취약점은 상대적으로 명백하여 발견하기 쉽고(오류 코드), 추론 및 확인이 더 쉽습니다. 설계 취약점은 매우 은밀할 수 있으며 발견하기 어렵고(오류 코드가 없음), 추론 및 확인이 더 어렵습니다.

ZK 취약점을 발견하기 위한 모범 사례

zkVM 및 기타 ZK 및 비ZK 체인에 대한 감사 및 형식 검증 경험에 따라, ZK 시스템을 최적으로 보호하는 방법에 대한 몇 가지 조언은 다음과 같습니다:

코드 및 설계 점검

앞서 언급했듯이, ZK의 코드와 설계에는 취약점이 존재할 수 있습니다. 이 두 가지 유형의 취약점은 모두 ZK 시스템에 피해를 줄 수 있으므로 시스템이 운영되기 전에 이를 제거해야 합니다. 비ZK 시스템과 비교할 때, ZK 시스템의 한 가지 문제는 모든 공격이 드러나고 분석하기 더 어렵다는 것입니다. 왜냐하면 계산 세부 사항이 공개되지 않거나 체인에 보존되지 않기 때문입니다. 따라서 사람들은 해킹 공격이 발생했다는 것을 알 수 있지만, 기술적으로 어떻게 발생했는지는 알 수 없습니다. 이는 모든 ZK 취약점의 비용을 매우 높게 만듭니다. 따라서 ZK 시스템의 안전성을 사전에 보장하는 것의 가치는 매우 높습니다.

감사 및 형식 검증 수행

우리가 여기에서 소개한 두 가지 취약점은 각각 감사와 형식 검증을 통해 발견되었습니다. 누군가는 형식 검증을 사용하면 감사가 필요 없다고 생각할 수 있습니다. 왜냐하면 모든 취약점이 형식 검증에서 발견될 것이기 때문입니다. 실제로 우리의 권장 사항은 두 가지 모두 수행하는 것입니다. 본문 시작 부분에서 설명한 바와 같이, 고품질의 형식 검증 작업은 코드와 설계에 대한 철저한 검토, 점검 및 비공식적 추론에서 시작됩니다. 이 작업 자체는 감사와 겹칩니다. 또한 감사 기간 동안 더 간단한 취약점을 발견하고 제거하면 형식 검증이 더 간단하고 효율적으로 진행될 수 있습니다.

ZK 시스템에 대해 감사와 형식 검증을 모두 수행하려면, 두 작업을 동시에 수행하는 것이 최상의 시점입니다. 감사자와 형식 검증 엔지니어가 효율적으로 협력할 수 있도록 하여(형식 검증의 객체와 목표가 고품질 감사 입력을 필요로 하므로) 더 많은 취약점을 발견할 수 있습니다.

여러분의 ZK 프로젝트가 이미 감사(좋음)를 받았거나 여러 번 감사(매우 좋음)를 받았다면, 우리의 권장 사항은 이전 감사 결과를 바탕으로 회로에 대해 형식 검증을 수행하는 것입니다. 우리는 zkVM 및 기타 ZK와 비ZK 프로젝트의 감사 및 형식 검증 경험을 통해 검증이 종종 감사에서 놓치기 쉬운 취약점을 포착할 수 있음을 여러 번 확인했습니다. ZKP의 특성으로 인해 ZK 시스템은 비ZK 솔루션보다 더 나은 블록체인 안전성과 확장성을 제공해야 하지만, 그 자체의 안전성과 정확성의 중요성은 전통적인 비ZK 시스템보다 훨씬 높습니다. 따라서 ZK 시스템에 대한 고품질 형식 검증의 가치는 비ZK 시스템보다 훨씬 높습니다.

회로 및 스마트 계약의 안전성 보장

ZK 애플리케이션은 일반적으로 회로와 스마트 계약의 두 부분으로 구성됩니다. zkVM 기반 애플리케이션의 경우, 일반적인 zkVM 회로와 스마트 계약 애플리케이션이 있습니다. 비zkVM 기반 애플리케이션의 경우, 애플리케이션 특정 ZK 회로와 L1 체인 또는 브리지의 반대편에 배포된 스마트 계약이 있습니다.

우리는 zkWasm의 감사 및 형식 검증 작업에서 zkWasm 회로만 다루었습니다. ZK 애플리케이션의 전체적인 안전성 관점에서 스마트 계약에 대한 감사 및 형식 검증도 매우 중요합니다. 결국 회로의 안전성을 보장하기 위해 많은 노력을 기울인 후, 스마트 계약에서 경계를 소홀히 하여 애플리케이션이 최종적으로 손상되는 것은 매우 유감스러운 일입니다.

특별히 주목해야 할 두 가지 유형의 스마트 계약이 있습니다. 첫 번째는 ZK 증명을 직접 처리하는 스마트 계약입니다. 비록 규모가 크지 않을 수 있지만, 위험이 매우 높습니다. 두 번째는 zkVM 위에서 실행되는 중대형 스마트 계약입니다. 우리는 이들이 때때로 매우 복잡할 수 있으며, 그 중 가장 가치 있는 것들은 감사 및 검증을 받아야 한다는 것을 알고 있습니다. 특히 사람들은 체인에서 이들의 실행 세부 사항을 볼 수 없기 때문입니다. 다행히도, 수년간의 발전을 통해 스마트 계약의 형식 검증은 이제 실용적이며 적합한 고가치 목표를 위해 준비되었습니다.

다음 설명을 통해 형식 검증(FV)이 ZK 시스템 및 그 구성 요소에 미치는 영향을 요약해 보겠습니다.