ZKCraft: TCCT 기반 ZK 퓨징을 위한 프롬프트 유도형 LLM 을 제로샷 변형 패턴 오라클로 활용하는 기술 요약

이 논문은 zkCraft라는 새로운 프레임워크를 제안합니다. zkCraft 는 제로지식 (Zero-Knowledge, ZK) 회로의 구현 오류, 특히 증기 생성기 (witness generator) 와 회로 제약 조건 간의 불일치로 인한 **의미론적 불일치 (semantic inconsistencies)**를 탐지하기 위해 설계되었습니다. 이 프레임워크는 결정론적 R1CS 인식 로컬라이제이션, 증명 기반 검색, 그리고 프롬프트 유도형 LLM 기반 변형 템플릿을 결합하여 기존 방법론의 한계를 극복합니다.

1. 문제 정의 (Problem)

제로지식 회로는 사생활 보호와 확장성을 가능하게 하지만,Witness(증거) 계산과 회로 제약 조건 간의 정밀한 정렬이 요구되기 때문에 구현이 어렵습니다. 정렬이 실패할 때 두 가지 주요 유형의 오류가 발생합니다.

• Under-constrained (과소 제약) 오류: 제약 조건이 유효한 Witness 가 생성할 수 없는 실행 경로를 허용하는 경우.
• Over-constrained (과다 제약) 오류: 유효한 Witness 를 생성하는 실행이 제약 조건에 의해 거부되는 경우.

기존의 정적 분석, SMT 기반 검증, 또는 퓨징 (Fuzzing) 기법들은 각각 다음과 같은 한계가 있었습니다:

• 정적 분석: 문법적 오류는 찾을 수 있으나, Witness 생성 시나 특정 입력에서만 나타나는 의미론적 오류는 놓치기 쉽습니다.
• 형식 검증/SMT: 강력한 보장을 제공하지만 대규모 회로에는 확장성이 부족하며, 프로그램 수정과 입력 할당의 조합된 검색 공간 처리가 어렵습니다.
• 기존 퓨징: 많은 비용이 드는 솔버 (Solver) 호출에 의존하거나, 무작위 변형으로 인해 저품질 후보를 많이 생성하여 비효율적입니다.

2. 방법론 (Methodology)

zkCraft 는 ZK 네이티브 파이프라인을 통해 소규모 취약점 유발 편집 (edit) 을 찾는 문제를 단일 대수적 존재 문장으로 매핑하고, 이를 **Violation IOP(Interactive Oracle Proof)**로 인증합니다.

핵심 구성 요소

1. Stage 1: 희소 지문 추출 (Sparse Signature Extraction)

   • 각 제약 행 (constraint row) 에 대해 R1CS 행렬의 비영 (nonzero) 인덱스 지원 (support) 을 분석합니다.
   • Witness 변수와 상수/간단한 표현 간의 상호작용을 기반으로 진단 점수 ($s_i$) 를 계산하여 취약점이 발생할 가능성이 높은 행을 선별합니다.
   • LLM 기반 오라클 (Mutation-Oracle) 을 사용하여 엣지 케이스 (edge cases) 로 편향된 변형 템플릿을 생성하고, 이를 통해 후보 풀 (Candidate Pool) 을 좁힙니다.

2. Stage 2: Row-Vortex Commitment 및 Violation IOP (ZK-Native Engine)

   • Row-Vortex 다항식: 선별된 후보 행과 치환 상수를 하나의 이변수 다항식 $R(X, Y)$로 인코딩합니다.
   • Violation IOP: 솔버 호출을 반복하는 대신, 수정된 제약 조건을 만족하면서 원래의 공개 출력과 다른 출력 ($y' \neq y$) 을 생성하는 Witness 의 존재를 증명하는 단일 ZK 상호작용 프로토콜을 실행합니다.
   • Sum-Check 프로토콜: 대수적 합 (algebraic sum) 을 검증하여 편집의 존재와 출력 차이를 동시에 증명합니다.

3. Proof-as-Counterexample (증명으로서의 반례)

   • 검증자가 성공적으로 증명을 검증하면, 해당 증명 ($\pi$) 은 취약점의 존재를 인증할 뿐만 아니라 구체적인 반례 (concrete counterexample) 를 포함합니다.
   • 추출기 (Extractor): 증명에서 열린 값 (openings) 을 통해 편집된 Witness 와 치환 상수를 복원하고, 이를 바탕으로 구체적인 입력/출력 쌍 $(x', z', y')$을 재구성합니다. 이는 별도의 TCCT (Trace-Constraint Consistency Test) 재실행 없이도 디버깅이 가능하게 합니다.

4. LLM 오라클 (Deterministic Template Generator)

   • LLM 은 솔버가 아니라 제로샷 변형 패턴 오라클로 작동합니다.
   • 결정론적 프롬프트 (Temperature 0, Greedy decoding) 를 사용하여 일관된 변형 템플릿을 생성하며, 생성된 코드는 문법 검사를 거친 후 ZK 엔진에 입력됩니다. 이는 LLM 의 비결정론적 오류를 방지하면서도 탐색을 엣지 케이스로 유도합니다.

3. 주요 기여 (Key Contributions)

• ZK 네이티브 검색 프레임워크: 소규모 취약점 편집 탐색을 Row-Vortex 다항식으로 인코딩된 단일 대수적 존재 문장으로 변환하고, Violation IOP 로 인증하는 새로운 접근법 제시.
• 결정론적 LLM 오라클: 증명 생성과 분리된 상태에서 LLM 을 변형 템플릿 오라클로 활용하여 검색 효율성을 높이고, LLM 의 불확실성을 배제.
• 구현 기술: 행별 지문 (per-row fingerprinting), 스코어링 휴리스틱, 증명 내 인코딩으로부터 구체적인 치환을 복원하는 결정론적 유한체 합성 (finite-field synthesis) 기술 개발.
• Proof-as-Counterexample: 검증 가능한 증명과 동시에 구체적인 디버깅 정보를 제공하는 효율적인 메커니즘 구축.

4. 실험 결과 (Results)

452 개의 실제 Circom 테스트 스위트와 다양한 크기의 회로 (소형 ~ 초대형) 를 대상으로 평가했습니다.

• 탐지 성능: zkCraft 는 기존 도구 (Circomspect, ZKAP, Picus, ZKFUZZ 등) 대비 최고의 참 긍정 (True Positive) 수를 기록했습니다.
  • 전체 벤치마크에서 88 개의 고유 버그를 발견 (기존 도구들은 14~79 개 사이).
  • 정밀도 (Precision) 100%: 거짓 긍정 (False Positive) 이 전혀 발생하지 않았습니다.
• 속도 및 효율성:
  • 기존 퓨징 도구들이 수 시간 걸리는 탐색을 100 초 이내에 수렴하여 대부분의 버그를 발견했습니다.
  • 비용이 많이 드는 솔버 호출을 대폭 줄였으며, ZK 네이티브 모드는 전체 실행 시간의 93% 를 차지하며 TCCT 재실행 오버헤드를 3% 미만으로 유지했습니다.
• 미발견 버그 (Previously Unknown Bugs):
  • 기존에 알려지지 않은 65 개의 새로운 취약점을 발견했으며, 이는 소유권 위조 (Ownership Forgery), 암호화 계산 오류 등 실제 시스템에 치명적인 결함이었습니다.
• 증명 크기: HyperPlonk+ 백엔드를 사용할 경우, 회로 크기에 관계없이 약 96 바이트의 고정된 증명 크기를 유지하며, 생성 시간은 $O(|C|^{0.7})$로 서-선형 (sub-linear) 증가했습니다.

5. 의의 및 결론 (Significance)

zkCraft 는 형식 검증과 자동화된 디버깅 사이의 간극을 메우는 획기적인 도구입니다.

1. 확장성: 대규모 ZK 회로에서도 솔버 호출 없이 효율적으로 오류를 탐지할 수 있어, 실제 프로덕션 환경에서의 ZK 회로 개발에 실용적인 솔루션을 제공합니다.
2. 신뢰성: LLM 을 활용하되 그 결과를 ZK 증명으로 엄격하게 검증함으로써, AI 기반 도구의 신뢰성 문제를 해결했습니다.
3. 개발자 경험: 증명 자체가 구체적인 반례를 포함하므로, 개발자가 버그의 원인을 즉시 파악하고 수정할 수 있어 디버깅 시간을 단축합니다.

결론적으로, zkCraft 는 ZK 회로의 보안과 견고성을 높이기 위한 차세대 표준 프레임워크로 자리 잡을 잠재력을 가지며, 특히 대규모 시스템에서의 자동화된 취약점 탐지 패러다임을 변화시킬 것으로 기대됩니다.