제로지식 증명의 고급 형식 검증: 두 가지 제로지식 취약점에 대한 심층 분석

2024.05.30

제로지식 증명의 고급 형식 검증: 두 가지 제로지식 취약점에 대한 심층 분석

본문에서는 취약점을 발견하는 관점에 주목하여, 감사 및 검증 과정에서 발견된 구체적인 취약점들과 그로부터 얻은 경험과 교훈을 분석할 것이다.

2024.05.30 - 08:47:42

Web3 심층 보도에 집중하고 흐름을 통찰

본문에서는 취약점을 발견하는 관점에 주목하여, 감사 및 검증 과정에서 발견된 구체적인 취약점들과 그로부터 얻은 경험과 교훈을 분석할 것이다.

글: CertiK

이전 글에서 우리는 제로지식 증명(ZKP)의 고급 형식 검증 기법인 'zk 명령어 하나를 어떻게 검증하는가'에 대해 다뤘습니다. zkWasm 명령어 각각을 형식적으로 검증함으로써, 전체 zkWasm 회로의 기술적 안전성과 정확성을 완전히 보장할 수 있습니다. 본문에서는 취약점을 발견하는 관점에서 접근하여, 감사 및 검증 과정에서 밝혀진 구체적인 취약점들과 그로부터 얻은 교훈을 분석합니다. 제로지식 증명 블록체인에 대한 일반적인 형식 검증 논의는 「제로지식 증명 블록체인의 고급 형식 검증」 기사를 참고하시기 바랍니다.

ZK 취약점에 대해 논의하기 전에, 먼저 CertiK가 ZK 형식 검증을 수행하는 방식을 살펴보겠습니다. ZK 가상 머신(zkVM)과 같은 복잡한 시스템의 경우, 형식 검증(FV)의 첫 단계는 무엇을 검증해야 하며 어떤 성질을 만족시켜야 하는지를 명확히 하는 것입니다. 이를 위해 ZK 시스템의 설계, 코드 구현, 테스트 설정을 종합적으로 검토해야 합니다. 이 과정은 일반적인 감사와 일부 중첩되지만, 차이점은 이후 검증 목표와 성질을 명확히 정의해야 한다는 점입니다. CertiK에서는 이를 ‘검증 중심 감사(verification-oriented audit)’라고 부릅니다. 감사와 검증 작업은 일반적으로 통합되어 진행됩니다. zkWasm의 경우, 우리는 동시에 감사와 형식 검증을 수행했습니다.

ZK 취약점이란?

제로지식 증명 시스템의 핵심 특징은 오프라인 또는 비공개 환경에서 실행된 계산(예: 블록체인 트랜잭션)의 간단한 암호화된 증명을 생성하여 제로지식 증명 검증기에 전달하고, 해당 검증기가 이를 검사·승인함으로써 해당 계산이 선언된 대로 실제로 발생했음을 확신할 수 있게 하는 것입니다. 이런 맥락에서 ZK 취약점은 해커가 거짓 트랜잭션을 증명하는 위조된 ZK 증명을 제출하고, ZK 증명 검사기가 이를 수용하게 만드는 가능성을 의미합니다.

zkVM 프루퍼(prover) 입장에서 ZK 증명 과정은 프로그램 실행, 각 단계별 실행 기록 생성, 그리고 그 실행 기록을 일련의 숫자 테이블로 변환하는 것을 포함합니다. 이 과정을 ‘산술화(arithmetization)’라고 합니다. 이러한 숫자들 사이에는 일련의 제약 조건(즉 ‘회로’)을 충족해야 하며, 여기에는 특정 테이블 셀 간의 연관 방정식, 고정된 상수, 테이블 간 데이터베이스 조회 제약, 그리고 인접한 두 행 사이에 만족해야 하는 다항식 방정식(즉 ‘게이트’)이 포함됩니다. 체인 상의 검증자는 이를 통해 모든 제약 조건을 만족하는 테이블이 실제로 존재함을 확인할 수 있지만, 테이블 내 실제 숫자는 볼 수 없습니다.

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 검사기를 통과하여 블록체인에 의해 잘못된 진짜 트랜잭션으로 간주될 수 있습니다.

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

이 취약점은 ‘코드 취약점(code vulnerability)’으로 분류되며, 코드 작성에서 기인하며 국소적인 코드 수정으로 쉽게 해결될 수 있기 때문입니다. 아마 동의하실 테지만, 이러한 취약점은 상대적으로 더 눈에 잘 띕니다.

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

다른 취약점으로 넘어가 보겠습니다. 이번엔 zkWasm의 호출(call)과 반환(return)과 관련된 문제입니다. 호출과 반환은 기본적인 VM 명령어로, 현재 실행 중인 컨텍스트(예: 함수)가 다른 함수를 호출하고, 호출된 함수가 실행을 완료한 후 다시 원래 컨텍스트의 실행을 재개할 수 있게 해줍니다. 모든 호출은 이후 한 번의 반환으로 예상됩니다. zkWasm은 호출과 반환의 생애주기 동안 추적하는 동적 데이터를 ‘호출 프레임(call frame)’이라고 부릅니다. zkWasm은 명령어를 순차적으로 실행하므로, 모든 호출 프레임은 실행 시간 순서대로 정렬할 수 있습니다. 아래는 zkWasm에서 실행되는 호출/반환 코드의 예시입니다.

사용자는 buy_token() 함수를 호출하여 토큰을 구매할 수 있습니다(다른 가치 있는 자산을 지불하거나 이전하는 방식일 수 있음). 그 핵심 단계 중 하나는 add_token() 함수를 호출하여 실제 토큰 잔액을 1만큼 증가시키는 것입니다. ZK 프루퍼 자체가 호출 프레임 데이터 구조를 지원하지 않기 때문에, E-Table(실행 테이블)과 J-Table(점프 테이블)을 사용하여 이러한 호출 프레임의 전체 기록을 기록하고 추적해야 합니다.

위 그림은 buy_token()이 add_token()을 호출하고, add_token()에서 buy_token()으로 돌아오는 과정을 보여줍니다. 토큰 잔액이 1 증가한 것을 확인할 수 있습니다. 실행 테이블(E-Table)에서는 각 실행 단계가 한 행을 차지하며, 현재 실행 중인 호출 프레임 번호, 현재 컨텍스트 함수 이름(설명 용도), 해당 함수 내 현재 실행 중인 명령어 번호, 그리고 현재 명령어(설명 용도)를 포함합니다. 점프 테이블(J-Table)에서는 각 호출 프레임이 한 행을 차지하며, 호출자 프레임 번호, 호출자 함수 컨텍스트 이름(설명 용도), 호출자 프레임의 다음 명령어 위치(해당 프레임이 반환할 위치)를 저장합니다. 두 테이블 모두 jops 열을 갖고 있으며, 이는 현재 명령어가 호출/반환인지(실행 테이블), 혹은 해당 프레임에서 발생한 호출/반환 명령어의 총 수(jops 테이블)를 추적합니다.

예상대로, 모든 호출은 하나의 반환과 대응되어야 하며, 각 프레임은 하나의 호출과 하나의 반환만 가져야 합니다. 위 그림에서 점프 테이블의 1번 프레임의 jops 값은 2이며, 실행 테이블의 1행과 3행의 jops 값 1과 대응됩니다. 지금까지는 정상적으로 보입니다.

그러나 문제는 다음과 같습니다. 한 번의 호출과 한 번의 반환은 프레임의 jops 카운트를 2로 만들지만, 두 번의 호출이나 두 번의 반환 역시 jops 카운트를 2로 만들 수 있습니다. 한 프레임에서 두 번의 호출이나 두 번의 반환은 어이없어 보일 수 있지만, 해커는 바로 이러한 예상 밖의 행동을 하려는 존재라는 점을 기억해야 합니다.

지금쯤 흥분되셨을 수도 있지만, 정말로 문제를 찾은 걸까요?

결과적으로, 두 번의 호출은 문제가 되지 않습니다. 실행 테이블과 호출 테이블의 제약 조건 때문에 두 번의 호출이 동일한 프레임의 행에 인코딩될 수 없기 때문입니다. 매 호출마다 새로운 프레임 번호(현재 프레임 번호 + 1)가 생성되기 때문입니다.

그러나 두 번의 반환은 운이 좋지 않습니다. 반환 시에는 새로운 프레임이 생성되지 않기 때문에, 해커는 합법적인 실행 순서의 실행 테이블과 호출 테이블을 가져와 위조된 반환(및 해당 프레임)을 주입할 수 있습니다. 예를 들어, 앞선 buy_token()이 add_token()을 호출하는 예시는 해커에 의해 다음과 같이 변조될 수 있습니다.

해커는 실행 테이블에서 기존 호출과 반환 사이에 두 번의 위조된 반환을 삽입하고, 호출 테이블에 새로운 위조된 프레임 행을 추가합니다(원래 반환 이후의 실행 단계 번호는 실행 테이블에서 4씩 증가). 호출 테이블의 각 행의 jops 카운트가 모두 2이므로, 제약 조건이 충족되며 zkWasm 증명 검사기는 이 위조된 실행 순서의 ‘증명’을 수용합니다. 그림에서 보듯, 토큰 잔액이 1번이 아니라 3번 증가했습니다. 따라서 해커는 1개 토큰만 지불하고 3개를 얻을 수 있습니다.

이 문제를 해결하는 방법은 다양합니다. 가장 명백한 방법은 호출과 반환을 별도로 추적하고, 각 프레임이 정확히 한 번의 호출과 한 번의 반환만 갖도록 보장하는 것입니다.

아마도 지금쯤 이 취약점에 대한 코드를 단 한 줄도 보여주지 않았다는 점을 눈치채셨을 겁니다. 이유는 간단합니다. 문제가 있는 코드 라인이 전혀 없으며, 코드 구현은 테이블과 제약 조건 설계를 완벽히 따르고 있기 때문입니다. 문제는 설계 자체에 있으며, 수정도 설계 차원에서 이루어져야 합니다.

이 취약점은 당연히 드러날 것 같지만, 실제로는 그렇지 않습니다. ‘두 번의 호출이나 두 번의 반환도 jops 카운트를 2로 만든다’는 점과 ‘실제로 두 번의 반환은 가능하다’는 점 사이에는 갭이 존재합니다. 후자를 이해하려면 실행 테이블과 호출 테이블의 관련 제약 조건을 꼼꼼하고 완전하게 분석해야 하며, 비형식적 추론으로는 완전히 이해하기 어렵습니다.

두 취약점의 비교

‘Load8 데이터 주입 취약점’과 ‘위조 반환 취약점’은 모두 해커가 ZK 증명을 조작하여 허위 트랜잭션을 생성하고, 증명 검사기를 속이며, 자산을 탈취하거나 장악할 수 있게 만듭니다. 그러나 그 성격과 발견 방식은 극명하게 다릅니다.

‘Load8 데이터 주입 취약점’은 zkWasm 감사 과정에서 발견되었습니다. 6,000줄 이상의 Rust 코드와 수백 개의 zkWasm 명령어에 대한 수백 개의 제약 조건을 검토해야 했기 때문에 결코 쉬운 일이 아니었지만, 이 취약점은 상대적으로 쉽게 발견되고 확인될 수 있었습니다. 이 취약점은 형식 검증 시작 전에 이미 수정되었기 때문에, 검증 과정에서는 만나지 못했습니다. 만약 감사 중에 발견되지 않았다면, Load8 명령어의 검증 과정에서 밝혀졌을 것으로 예상됩니다.

‘위조 반환 취약점’은 감사 이후의 형식 검증 과정에서 발견되었습니다. 우리가 감사 중에 이를 발견하지 못한 부분적인 이유는, zkWasm에 jops와 매우 유사한 ‘mops’라는 메커니즘이 존재하기 때문입니다. 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 체인 또는 브릿지 반대편에 배포된 스마트 컨트랙트가 있습니다. zkVM 기반 vs 비기반

우리가 수행한 zkWasm의 감사 및 형식 검증 작업은 zkWasm 회로에만 초점을 맞췄습니다. 그러나 ZK 애플리케이션의 전체 보안 관점에서 보면, 스마트 컨트랙트에 대한 감사 및 형식 검증도 매우 중요합니다. 어쨌든 회로 보안을 위해 많은 노력을 했음에도 불구하고 스마트 컨트랙트에서 경계를 늦추어 결국 애플리케이션이 피해를 입는다면 매우 안타까운 일입니다.

특별히 주목해야 할 두 가지 유형의 스마트 컨트랙트가 있습니다. 첫째는 ZK 증명을 직접 처리하는 스마트 컨트랙트입니다. 규모는 작을 수 있지만 위험은 매우 큽니다. 둘째는 zkVM 위에서 실행되는 중대형 스마트 컨트랙트입니다. 이들은 때때로 매우 복잡할 수 있으며, 특히 체인 상에서 실행 세부 사항을 볼 수 없는 만큼 가치가 큰 것들은 반드시 감사 및 검증을 받아야 합니다. 다행히 오랜 개발을 거쳐, 스마트 컨트랙트의 형식 검증은 이제 실용 단계에 도달했으며 적절한 고가치 대상에 준비되어 있습니다.

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