Formally Verifying Noir Zero Knowledge Programs with NAVe

기술 요약: NAVe를 이용한 Noir 영지식 프로그램의 형식 검증

문제 정의
영지식(Zero-Knowledge, ZK) 증명 시스템은 프라이빗 입력 $W$가 관계 $R(X, W)$를 만족한다는 것을 $W$를 공개하지 않고 검증하기 위해 산술 회로(유한체 위의 다항식 방정식 집합)에 의존합니다. Noir와 같은 고수준 도메인 특화 언어(DSL)는 코드를 ACIR(Abstract Circuit Intermediate Representation)이라는 중간 표현으로 컴파일함으로써 이러한 회로 생성을 단순화합니다. 그러나 이러한 추상화는 미묘한 취약점을 도입할 수 있습니다. 구체적으로, Noir는 프로버(prover)의 계산 효율성을 높이기 위해 복잡한 연산을 프로버에게 오프로딩하도록 설계된 "제약 없는 코드(unconstrained code)"(unconstrained 함수 및 unsafe 블록을 통해 제공)를 지원합니다. 만약 개발자가 제약 없는 코드의 결과에 대해 상응하는 제약(예: assert 문을 통한)을 수동으로 추가하는 데 실패하면, 생성된 산술 회로가 의도한 관계를 정확하게 포착하지 못할 수 있습니다. 이러한 "미달 제약(under-constrained)" 버그는 프로버가 거짓된 명제에 대해 유효한 증명을 생성할 수 있게 하는 심각한 보안 취약점으로 이어질 수 있습니다. 기존의 형식 검증 도구들은 주로 Circom과 같은 저수준 회로 DSL을 대상으로 하거나 대화형 정리 증명을 요구하며, 메모리 조작 및 블랙박스 함수와 같은 고수위 Noir 프로그램에 대한 자동화되고 확장 가능한 검증 능력이 부족합니다.

방법론
저자들은 고수준 Noir 소스 코드가 아닌 ACIR 중간 표현에서 작동하는 오픈 소스 형식 검증 프레임워크인 NAVe(Noir Acir Verifier)를 제안합니다. 이러한 선택은 언어 진화에 대한 안정성을 보장하며, ACIR을 타겟으로 하는 다른 언어들을 지원할 수 있는 가능성을 열어줍니다.

1. SMT-LIB을 통한 정식화: NAVe의 핵심은 ACIR 서브셋의 오퍼코드(opcode)를 만족 가능성 모듈로 이론(Satisfiability Modulo Theories, SMT) 공식으로 정식화하는 것입니다. 저자들은 두 가지 별개의 인코딩을 구현했습니다:

   • 유한체 인코딩(Finite Field Encoding): cvc5 솔버에서 구현된 비표준 유한 체의 이론을 활용합니다. 이 접근 방식은 필드 산술을 직접 모델링하기 위해 ff.add, ff.mul, ff.bitsum과 같은 특정 연산자를 사용합니다.
   • 정수 산술 인코딩(Integer Arithmetic Encoding): SMT-LIB의 표준 정수 이론을 활용합니다. 이는 소수 차수 $p$를 갖는 유한체와 정수 modulo $p$ 사이의 동형성을 활용하여, 필드 연산을 모듈러 정수 산술(예: (mod (+ ...) p))로 인코딩합니다.

2. 오퍼코드 의미론(Opcode Semantics): 정식화는 주요 ACIR 오퍼코드를 다룹니다:

   • AssertZero: 0과 같다는 다항식 방정식 제약으로 인코딩됩니다.
   • BlackBoxFuncCall: Range 체크 오퍼코드에 대해 구체적으로 정식화되었습니다. 유한체 인코딩에서 이는 이진 분해(bitsum)를 사용하여 모델링되며, 비트가 0 또는 1임을 보장하는 제약을 포함합니다. 정수 인코딩에서는 표준 정수 순서 제약($x < 2^n$)을 사용하여 모델링됩니다.
   • MemoryOp 및 MemoryInit: 인덱스를 증거(witness) 값에 매핑하는 맵을 사용하여 배열 변형을 추적하고, 순차적인 읽기 및 쓰기 작업을 처리하도록 정식화되었습니다.
   • BrilligCall: 제약 없는 코드를 나타내며, 이들은 항상 만족되는 제약인 true(또-는 무시됨)로 번역됩니다. 이는 검증자의 목표가 제약 없는 블록 외부의 제약을 확인하는 것이기 때문입니다.

3. 검증 워크플로우:

   • 이 도구는 Noir의 패키지 매니저인 Nargo와 통합되어 formal-verify 명령어로 제공됩니다.
   • 개발자는 Noir 프로그램에 verify_assert(b: bool) 문을 주석으로 추가합니다. 표준 assert 문이 회로 제약을 생성하는 것과 달리, verify_assert는 증명 의무(proof obligation)를 생성합니다.
   • NAVe는 Noir 프로그램을 ACIR로 컴파일하고, ACIR 오퍼코드를 SMT 공식으로 번역한 뒤, 검증 공식 $F = \text{ACIR}_{\text{constraints}} \land \neg \text{verify\_assert}_{\text{condition}}$를 구성합니다.
   • cvc5 솔버는 $F$의 만족 가능성을 확인합니다. 만약 $F$가 불만족(unsatisfiable) 상태라면, 검증 조건이 성립합니다(프로그램이 올바르게 제약됨). 만 만약 $F$가 만족(satisfiable) 상태라면, 솔버는 조건을 위반하는 증거 할당을 보여주는 모델(반례)을 반환하여 디버깅을 돕습니다.

주요 기여

• ACIR의 정식화: 메모리 연산, 범위 체크, 그리고 제약 있는 코드와 제약 없는 코드의 구분을 포함하여, SMT-LIB을 사용하여 ACIR의 서브셋을 정식화한 최초의 사례입니다.
• 이중 인코딩 전략: 서로 다른 솔버 역량을 활용하기 위해 제안된 상호 보완적인 두 가지 인코딩(유한체 이론 및 정수 산술)입니다.
• NAVe 도구: 대화형 정리 증명이 필요 없이 개발자가 접근할 수 있도록 설계되었으며, Noir 생태계(Nargo)에 통합된 오픈 소스 자동 형식 검증기입니다.
• 실증적 평가: 다양한 제약 유형과 솔버 설정에 따른 성능을 분석하기 위해, 일련의 Noir 테스트 프로그램에 대해 NAVe를 종합적으로 평가했습니다.

결과
저자들은 cvc5 솔버를 사용하여 4가지 서로 다른 Noir 프로그램 세트(검증된 조건, 거짓된 조건, range 체크 포함 여부)에 대해 NAVe를 평가했습니다.

• 솔버 성능: 단일 백엔드(정수 인코딩, 유한체 --ff=gb, 또는 유한체 --ff=split)가 일관되게 우수한 성능을 보이지 않았습니다. 결과는 인코딩들이 상호 보완적임을 나타냅니다. 즉, 어떤 프로그램은 한 인코딩에서 더 빠르게 해결되는 반면, 다른 프로그램은 동일한 인코딩에서 타임아웃이 발생하지만 다른 인코딩에서는 성공합니다.
• 범위 체크의 영향: Range 체크(BlackBoxFuncCall 오퍼코드)를 포함하는 프로그램은 검증 시간을 크게 증가시켰습니다. 유한체 이론을 근사하는 --ff=split 설정은 기본 --ff=gb 설정보다 큰 범위 체크가 있는 프로그램에서 우수한 성능을 보였으나, 복잡한 경우 여전히 타임아웃이 발생했습니다.
• 반례 생성: 도구는 거짓된 조건에 대해 반례를 성공적으로 생성하여, 미달 제약 로직을 식별하는 데 유용함을 입증했습니다.

의의 및 주장
본 논문은 실세계의 취약점으로 이어진 클래스인 미달 제약 버그에 대해 고수위 ZK 프로그램을 검증하는 자동화되고 확장 가능한 방법을 제공함으로써, ZK 생태계의 중요한 공백을 메운다고 주장합니다. ACIR을 타겟으로 함으로써, 이 도구는 고수위 Noir 구문 변화에 견고하며 동일한 중간 표현을 타겟으로 하는 다른 언어에도 적용될 가능성이 있습니다.

저자들은 자신의 연구를 더 넓은 검증 능력을 향한 단계로 겸손하게 규정합니다. 현재의 정식화가 (재귀적 Call 오퍼코드와 Range를 제외한 대부분의 BlackBoxFuncCall을 제외한) ACIR의 일부만을 다루고 있음을 인정합니다. 또한 범위 체크를 검증하는 데 드는 높은 비용을 주요 한계점으로 지적하며, 향-후 연구가 이러한 복잡한 제약을 효율적으로 처리하기 위한 추상화나 근사법 개발에 집중해야 한다고 제안합니다. 논문은 NAVe를 모든 ZK 검증 요구를 충족하는 완전한 솔루션이 아니라, 고수위 Noir에 대한 자동 형식 검증의 타당성을 입증하고 복잡한 비트 수준 제약에 대한 솔버 핸들링을 개선하기 위한 경로를 제시하는 실용적이고 통합된 도구로 포지셔닝합니다.