서틱, zkWasm 회로 형식 검증…일부 로직은 제외

이준한 기자2026.09.28 23:52

토포AI로 이 기사 더 깊이 읽기

서틱(CertiK)이 2024년 완료한 zkWasm 핵심 회로의 형식 검증 성과가 재조명됐다. 다만 이는 2026년 새로 완료된 작업이 아니라 기존 연구 결과를 다시 소개한 내용이다.

서틱은 2024년 기술 블로그에서 zkWasm의 Halo2 회로가 유효한 제약조건을 만족하면 WebAssembly(Wasm) 실행 규칙에 부합하는 상태를 나타내는지 검증했다고 밝혔다. 개발사 델피너스 랩(Delphinus Lab)도 2024년 5월 2일 자체 zkWasm 구현이 형식 검증됐다고 발표했다.

zkWasm은 Wasm 프로그램을 실행한 뒤 전체 계산 과정을 다시 수행하지 않고도 결과의 유효성을 확인할 수 있도록 영지식 증명을 생성하는 시스템이다. 프로그램 실행 추적은 Halo2의 여러 테이블로 바뀌며, 검증자는 각 테이블이 정해진 산술 제약을 만족하는지 확인한다.

형식 검증은 일반적인 코드 감사와 다르다. 알려진 취약점 패턴을 찾는 데 그치지 않고, 특정 조건에서 프로그램이 정의된 규칙대로 작동하는지를 기계가 확인할 수 있는 수학적 명제로 바꾸는 절차다.

zkVM에서는 하나의 회로가 다양한 프로그램 실행을 처리한다. 따라서 회로의 제약조건이 실제 Wasm 실행 의미론과 일치하는지 확인하는 작업이 증명 결과의 건전성을 판단하는 핵심 단계가 된다.

서틱의 공개 저장소는 Coq로 작성한 형식 검증이 실행 테이블, 메모리 테이블, 호출 스택, 비트 연산 등 zkWasm 회로의 주요 구성요소를 다룬다고 설명한다. 목표는 회로 제약조건이 모두 충족될 경우 실행 추적의 각 행이 Wasm 실행 규칙에 맞는 상태를 나타낸다는 점을 증명하는 것이다.

검증 과정에서 회로의 메모리 접근과 호출·복귀 구조에서 문제가 발견돼 수정됐다는 내용도 공개됐다. 이는 형식 검증이 단순히 기존 코드를 확인하는 데 그치지 않고, 명세와 구현 사이의 불일치를 찾아내는 과정임을 보여준다.

다만 'zkWasm 전체가 완전히 검증됐다'고 해석해서는 안 된다. 공개 저장소에는 Coq 모델과 증명 코드, 컴파일 절차가 포함돼 있지만 Rust로 작성된 알고리즘 전체는 검증 대상에서 제외됐다.

공개성에도 한계가 있다. 저장소에 검증 코드가 공개돼 있더라도 일부 회로 구성과 명령어 디코딩 로직, Wasmi 인터프리터와 Halo2 동작은 가정하거나 검증 범위에서 제외됐다.

Wasmi 인터프리터와 Halo2 자체, 일부 제약조건 생성 코드도 검증 대상에서 제외됐다. 외부 호출 기능과 일부 명령어 디코딩 로직 역시 별도 가정이나 수동 검토에 의존한다.

서틱은 대응하는 내부 저장소에 총 3만3080줄의 Coq 코드가 있다고 설명했다. 코드 규모가 공개됐다는 사실과 증명 범위 전체가 공개됐다는 것은 별개의 문제다.

서틱의 2024년 연례 보고서는 검증 대상이 144개 명령어로 구성된 zkWasm 회로였으며, 영지식 증명 생태계에서 첫 번째 완전 형식 검증이라고 평가했다. 이 표현은 서틱의 자체 설명으로, 독립적인 비교 기준이나 동료평가 결과까지 확인된 것은 아니다.

서틱은 해당 형식 검증 프레임워크를 다른 zkVM과 zkEVM에도 적용할 수 있다고 설명했다. 다만 이는 적용 가능성에 대한 회사 측 설명이며, 다른 시스템에 대한 검증이 완료됐다는 뜻은 아니다.

델피너스 랩은 자체 zkWasm 구현의 형식 검증 사실을 공유하며 서틱의 기술 문서를 연결했다. 개발사 차원의 긍정적 반응은 확인되지만, 검증 범위가 소프트웨어 스택 전체로 확대됐다는 의미는 아니다.

서틱은 이후 Verus를 이용해 과거 zkWasm 증명의 일부를 재구현하고 코드 규모를 2440줄에서 595줄로 줄였다고 소개했다. 이 작업은 최초 검증 완료 발표와 별개인 후속 연구로, 원래 검증의 공개 범위를 넓힌 결과로 보기는 어렵다.

관련 연구는 ACM CCS 2026 프로그램에 'Formal Verification of Circuit-Soundness in zkWasm, a General Purpose zkVM'이라는 제목으로 게재 예정 논문으로 등록됐다. 논문에는 서틱, 델피너스 랩, NVIDIA, 컬럼비아대, 예일대 연구진이 참여했으며, 논문 전문과 심사 결과의 세부 내용은 공개 자료만으로 확인되지 않는다.

이번 사례의 핵심은 zkVM 인프라에서 회로의 정확성을 수학적으로 설명하려는 시도가 구체적인 연구 성과로 이어졌다는 점이다. 동시에 공개된 검증 범위와 재현 가능성을 소프트웨어 전체의 안전성으로 확대하지 않는 구분도 필요하다.