졸트 바이트코드 67개 중 60개 검증…크립토브리핑 보도

레이어제로 리서치가 Jolt zkVM의 RISC-V 바이트코드 확장 67개 가운데 60개를 검증했다는 내용이 전해졌다. 나머지 7개 명령어는 특정 엣지 케이스로 검증 대상에 남았다.

크립토브리핑(CryptoBriefing)은 레이어제로 리서치가 약 2개월 반 동안 Lean 정리증명기를 활용해 이 같은 검증을 진행했다고 보도했다. 다만 해당 수치와 검증 논문은 레이어제로 공식 채널에서 같은 내용으로 확인되지는 않았다.

형식 검증은 소프트웨어가 정해진 명세를 만족하는지를 테스트가 아니라 수학적 증명으로 확인하는 방식이다. zkVM에서는 명령어를 잘못 해석하거나 실행 과정에 오류가 생기면 잘못된 결과가 유효한 증명으로 처리될 수 있어 이 단계가 중요하다.

Jolt의 바이트코드 확장은 ELF 파일에 담긴 원시 RISC-V 명령어를 디코드해 피연산자와 주소, 회로 플래그, 룩업 플래그 등을 포함한 내부 표현으로 바꾸는 과정이다. Jolt 공식 문서는 바이트코드를 실행 대상 프로그램의 기준점으로 설명한다.

확장된 바이트코드 인덱스와 ELF 메모리 주소는 서로 다른 역할을 한다. 바이트코드 인덱스는 실행 사이클에서 명령어에 접근하는 데 쓰이고, ELF 메모리 주소는 프로그램 카운터 제약을 확인하는 데 사용된다.

실행 과정에서는 읽힌 명령어가 사전 처리된 바이트코드와 일치하는지도 증명한다. 따라서 바이트코드 확장 단계의 정확성은 이후 실행 추적과 증명 결과의 신뢰성에 영향을 줄 수 있다.

이번 검증이 Jolt 전체의 형식 검증을 끝냈다는 의미는 아니다. 안드리센호로위츠는 2024년 기술 글에서 Jolt의 검증 작업을 룩업 의미론, 다항식 대화형 증명, 제약 시스템, RISC-V 명세, 실제 Rust 구현 사이의 정합성을 단계적으로 확인하는 과정으로 설명했다.

안드리센호로위츠의 검증 로드맵은 형식화된 모델과 실제 구현 코드가 일치하는지 확인하는 작업도 별도 과제로 제시했다. Lean에서 형식 모델이 증명됐더라도 그 모델이 실제 구현을 정확히 반영하는지는 추가 검증이 필요하다는 뜻이다.

기존 연구에서는 ACL2 정리증명기를 활용해 Jolt의 RISC-V RV32I 명령어에 대한 룩업 의미론을 검증했다. 연구진은 명령어를 작은 룩업 테이블로 분해하는 과정이 RISC-V 명세와 일치하는지 확인했고, 일부 명령어에서 불필요한 룩업을 줄이는 최적화도 발견했다.

관련 연구는 전체 RV32I 명령어를 ACL2로 형식화하고 검증했다고 밝혔다. 이번 Lean 기반 작업은 기존 검증 연구와 다른 정리증명기를 사용해 바이트코드 확장 범위를 확인한 사례로 볼 수 있다.

레이어제로는 Zero 기술 문서에서 Jolt를 네트워크의 실행 증명 인프라로 활용한다고 설명했다. Zero의 실행 로직은 증명 생성과 검증 절차를 거치며, Jolt는 프로그램 실행 결과가 올바른지 증명하는 zkVM 역할을 맡는다.

다만 바이트코드 확장 검증만으로 Zero 네트워크 전체나 Jolt 전체의 보안성이 검증됐다고 볼 수는 없다. 실제 Rust 구현과 형식 모델의 일치 여부, 다른 증명 구성요소의 검증 범위가 별도로 남아 있기 때문이다.

레이어제로와 안드리센호로위츠가 공개한 아키타와 래티스 졸트 관련 기술 발표는 영지식 증명 인프라의 암호 구성요소를 다룬 사례다. 이번 작업은 다항식 커밋 방식보다 실행 과정의 명령어 해석과 바이트코드 변환에 초점을 맞췄다는 점에서 앞선 발표와 구분된다.

검증된 60개 명령어와 검증되지 않은 7개 명령어의 구체적인 목록은 공개되지 않았다. 특히 7개 명령어가 어떤 엣지 케이스에 해당하는지와 실제 구현 코드가 형식 모델과 어느 수준으로 일치하는지는 추가 자료가 필요한 부분이다.

이번 발표는 Jolt zkVM의 특정 구성요소에 대한 형식 검증 진전으로 정리할 수 있다. 전체 zkVM이나 Zero 네트워크의 보안성 검증 완료로 확대해석하기에는 검증 범위가 제한적이다.