기술 요약: ZKFUZZ: 영지식 회로의 효과적인 퍼징을 위한 기반 및 프레임워크

1. 문제 제기

영지식 (ZK) 회로는 개인정보 보호 계산을 위한 핵심 요소로, 익명 암호화폐부터 검증 가능한 머신러닝에 이르기까지 다양한 응용 분야에서 간결한 증명과 효율적인 검증을 가능하게 합니다. 그러나 범용 계산 논리와 유한체 다항식 제약 조건 간의 불일치로 인해 올바른 ZK 회로를 개발하는 것은 매우 어렵습니다.

주요 취약점 클래스는 두 가지입니다:

• 제약이 부족한 회로 (Under-constrained circuits): 제약 조건이 너무 느슨하여 악의적인 증명자가 잘못된 증명을 위한 유효한 증명을 생성할 수 있게 합니다 (정합성 위반).
• 제약이 과도한 회로 (Over-constrained circuits): 제약 조건이 너무 엄격하여 정직한 증명자의 유효한 증명을 시스템이 거부하게 합니다 (완전성 위반).

기존 탐지 방법은 다음과 같은 중대한 한계에 직면해 있습니다:

• 정적 분석: Circomspect 및 ZKAP 와 같은 도구는 높은 오탐지율을 겪으며, 특히 중간 계산이나 비정상적인 프로그램 종료와 관련된 깊은 의미론적 문제를 포착하지 못합니다.
• 형식적 방법: SMT 솔버에 의존하는 도구 (예: Picus, ConsCS) 는 실제 세계의 회로 규모로 확장하는 데 어려움을 겪으며, 종종 취약점에 대한 불완전한 정의에 의존합니다. 이는 제약 조건 내의 비결정성에만 초점을 맞추고, 계산이 중단되거나 중간 값이 불일치하는 경우는 무시합니다.
• 정의의 공백: ZK 버그에 대한 이전의 형식적 정의는 불완전합니다. 이러한 정의들은 종종 "비정상 종료" (계산은 충돌하지만 제약 조건은 여전히 만족되는 경우) 를 무시하고, 중간 값을 포함한 전체 실행 궤적 세트를 고려하지 못합니다.

2. 방법론

2.1 이론적 기반: 궤적 - 제약 일관성 테스트 (TCCT)

저자들은 TCCT를 소개합니다. 이는 ZK 취약점을 두 집합 간의 불일치로 정의하는 언어 독립적인 형식적 프레임워크입니다:

1. 궤적 집합 $T(P)$: 증인 계산 프로그램 $P$가 생성하는 모든 가능한 실행 궤적 (입력, 중간 값, 출력) 의 집합.
2. 제약 만족 집합 $S(C)$: 회로 제약 조건 $C$를 만족하는 모든 튜플 (입력, 중간 값, 출력) 의 집합.

TCCT 는 다음과 같은 경우에만 회로를 잘 제약된 것으로 정의합니다:

• 제약 부족 없음: $S(C)$의 입력 - 출력 쌍에 대한 투영이 $T(P)$의 투영의 부분집합이어야 합니다. 이는 잘못된 궤적이 허용되지 않도록 보장합니다.
• 제약 과잉 없음: $T(P)$가 $S(C)$의 부분집합이어야 합니다. 이는 모든 유효한 궤적 (특정 중간 값을 포함) 이 허용되도록 보장합니다.

이 공식화는 계산 중단 ( $P$는 실패하지만 $C$는 입력을 허용하는 경우) 과 중간 값 불일치로 인한 취약점을 포착하며, 이는 이전 정의들이 놓친 부분입니다. 저자들은 제약 부족 또는 과잉을 결정하는 문제가 NP-완전임을 증명했으며, 전체 TCCT 는 co-NP-완전임을 보였습니다.

2.2 시스템 설계: ZKFUZZ

ZKFUZZ 는 결합 프로그램 변형 및 입력 생성 접근 방식을 사용하여 TCCT 위반을 탐지하는 동적 분석 프레임워크입니다. 입력만 변형하는 전통적인 퍼징과 달리, ZKFUZZ 는 프로그램 논리와 입력 모두를 변형합니다.

핵심 워크플로우:

1. 변형: 시스템은 원래 계산 프로그램 ($P$) 의 변형체 ($P'$) 를 생성합니다. 변형에는 어설션 제거, 할당 변환 (예: 연산자 또는 값 교체), 약한 할당 수정 등이 포함됩니다.
2. 실행: 원래 프로그램 ($P$) 과 변형체 ($P'$) 를 모두 샘플링된 입력 ($x$) 에서 실행합니다.
3. 검증:
   • 제약 과잉 탐지: $P(x)$가 유효한 궤적을 생성하지만 $C$를 통과하지 못하면, 회로는 제약이 과도한 것입니다.
   • 제약 부족 탐지: $P'(x)$가 다른 출력 ($y' \neq y$) 을 가진 궤적을 생성하지만 여전히 $C$를 만족하면, 회로는 제약이 부족한 것입니다 (변형된 논리는 의미론적으로 다르므로 출력이 허용되어서는 안 되기 때문입니다).
4. 가이드된 탐색: 거대한 소수 필드와 무한한 변형 가능성의 탐색 공간을 탐색하기 위해 ZKFUZZ 는 유전 알고리즘을 사용합니다:
   • 적합도 함수: 새로운 최소 - 합 적합도 함수는 주어진 궤적에 대해 모든 제약 조건에 걸친 제약 오류의 합을 계산합니다. 변형체는 샘플링된 입력에 걸쳐 최소 오류 합으로 점수를 매깁니다. 이는 이전의 최대값 전용 방법과 다르며 결합 변형에 더 적합합니다.
   • 타겟 선택기: 시스템은 정적 분석을 사용하여 변형 및 입력 생성을 고위험 패턴으로 안내합니다.
     • 0 나눗셈: 분자와 분모가 모두 0 이 되는 입력 생성.
     • 해시 확인: 해시 동등성 제약 조건을 만족하도록 입력 강제.
     • 편향된 분포: 0, 1 및 필드 모듈로 $q$ 근처의 값과 같은 엣지 케이스로 입력 생성 편향.
     • 화이트리스트: IsZero, Num2Bits와 같이 알려진 안전한 템플릿을 건너뛰고 오류가 발생하기 쉬운 코드에 집중.

3. 주요 기여

1. TCCT 프레임워크: 이전 정의를 포괄하고 비정상 종료 및 중간 값 불일치로 인한 ZK 버그의 전체 공간을 포착하는 통합된 언어 중립 형식 모델.
2. ZKFUZZ 시스템: 결합 프로그램 및 입력 변형을 통해 TCCT 위반을 탐지하는 새로운 퍼징 프레임워크로, 최소 - 합 적합도 함수와 가이드된 탐색 휴리스틱을 활용합니다.
3. 실증적 검증: 452 개의 실제 Circom 회로에 대한 평가로, 최첨단 도구보다 우수한 성능을 입증했습니다.
4. Noir 프로토타입: 다른 ZK DSL 인 Noir 에 대한 예비 구현으로, 프레임워크의 언어 독립성 잠재력을 보여줍니다.

4. 결과

저자들은 ZKFUZZ 를 452 개의 실제 Circom 회로에서 평가하여 Circomspect, ZKAP, Picus, ConsCS 와 같은 네 가지 최첨단 도구와 비교했습니다.

• 버그 탐지: ZKFUZZ 는 85 개의 고유한 버그를 식별했으며, 이 중 59 개는 이전에 알려지지 않은 제로데이 취약점이었습니다. 이 중 39 개는 개발자에 의해 확인되었고 14 개는 수정되었습니다.
• 비교: ZKFUZZ 는 다양한 회로 크기에 걸쳐 기존 도구보다 30% 에서 300% 더 많은 버그를 발견했습니다.
• 정확도: ZKFUZZ 는 **100% 정확도 (오탐지 0)**를 달성한 반면, Circomspect 및 ZKAP 와 같은 정적 분석기는 높은 오탐지율을 보였습니다 (정확도 범위 0.06 에서 0.75).
• 속도: ZKFUZZ++ (타겟 선택기 포함) 는 100 초 이내에 90% 이상의 버그를 식별하여 형식적 방법 및 정적 분석기를 크게 능가했습니다.
• 영향: 발견된 버그에는 zk-regex 및 passport-zk-circuits와 같은 프로젝트의 중요한 제약 부족 취약점이 포함되어 있어, 공격자가 증명을 위조하거나 자금을 인출할 수 있었습니다.

5. 중요성 및 주장

이 논문은 ZKFUZZ 가 이전 취약점 정의의 근본적인 불완전성을 해결함으로써 ZK 회로 보안에서 중요한 진전을 이루었다고 주장합니다. 버그를 궤적 - 제약 불일치 (TCCT) 로 형식화함으로써 저자들은 제약 비결정성에만 초점을 맞춘 도구로는 이전에 탐지되지 않았던 광범위한 취약점 클래스 (평가에서 실제 세계 버그의 약 50%) 를 드러냈습니다.

오탐지가 없는 버그 탐지 능력으로 인해 ZKFUZZ 는 오탐지가 높은 정적 분석기의 경고들을 종종 무시하는 개발자들에게 실용적인 도구가 됩니다. 또한 Noir 회로에서의 성공적인 버그 탐지는 TCCT 프레임워크와 ZKFUZZ 아키텍처가 Circom 에 국한되지 않고 표준화된 제약 형식으로 컴파일되는 다른 ZK 언어에도 일반화될 수 있음을 시사합니다.

저자들은 그들의 작업이 계산과 제약 간의 불일치 (정합성 및 완전성) 로 인한 취약점에 초점을 맞추고 있으며, 기본 증명 시스템의 버그, 순수 논리 오류 (사용되지 않는 입력 등) 또는 프로토콜 수준의 영지식 유출은 명시적으로 제외한다고 강조합니다.