배경지식

• 3. 유한체의 기본 정리
• Elliptic Curve Cryptography
• Basic Protocols (Schnorr, Groth16 구조)
• 준비물: SageMath, Circom, SnarkJS, Solidity

1. 개요

CTF 씬은 거대한 지각 변동을 겪고 있다. 전통적인 시스템 해킹이 메모리 주소를 조작하여 제어 흐름을 탈취하는 싸움이었다면, 영지식 증명 해킹은 다항식과 유한체 위에서 연산의 무결성을 무너뜨리는 싸움이다.

공격의 본질이 변했다:

• Target: saved_rip나 heap chunk가 아니라, Ax×Bx=Cx (R1CS) 제약 조건 그 자체다.
• Weapon: 쉘코드 대신, 가짜 증명과 조작된 Witness가 무기가 된다.
• Goal: 루트 권한 획득이 아니라 비밀을 모르면서도 검증자를 속여 통과하는 것이다.

이 문서는 ZK 시스템을 공격하기 위한 체계적인 방법론을 제시한다. 수학적 기반부터 회로 논리, 구현 레벨까지 전 계층을 아우르는 공격 기법을 다루며, 실전 CTF 문제 해결에 직접 적용할 수 있는 방법론을 제공한다.

2. Attack Surface Analysis

ZK 시스템을 공격하기 위해서는 먼저 공격 표면을 체계적으로 분석해야 한다. CTF 문제에서 제공되는 아티팩트들을 올바른 순서로 분석하고, 각 계층에서 발생할 수 있는 취약점 유형을 이해하는 것이 핵심이다.

2.1 아티팩트 분석 순서

CTF 문제에서는 일반적으로 다음과 같은 파일들이 제공된다. 각 파일은 서로 다른 계층의 취약점을 담고 있을 수 있으므로, 체계적인 분석 순서가 중요하다.

2.1.1 circuit.circom

회로의 논리적 구조와 제약 조건을 분석하여 under-constrained 변수나 논리적 허점을 찾는다.

분석 방법:

• 입력 검증 확인: 모든 signal input에 대해 적절한 범위 체크나 타입 검증이 있는지 확인한다.
  • 예: age 입력이 0~150 범위인지 검증하는가?
  • 예: 비트 배열의 각 원소가 실제로 {0, 1}인지 검증하는가?
• 출력 제약 확인: 계산된 중간 변수나 최종 출력이 <==가 아닌 ===로 제약되어 있는지 확인한다.
  • <==는 할당만 하고 검증하지 않는다.
  • ===는 R1CS 제약 조건을 생성하여 검증한다.
• 템플릿 인스턴스화 추적: component로 생성된 하위 회로들이 올바르게 연결되어 있는지 확인한다.
  • 신호가 전달되지 않는 고립된 변수가 있는가?
  • 순환 참조나 미사용 출력이 있는가?
• 특수 케이스 테스트: 경계값(0, p-1)이나 특수 입력(음수 표현)을 넣었을 때 회로가 예상대로 동작하는지 시뮬레이션한다.

도구:

• circom 컴파일러로 R1CS 생성 후 제약 조건 개수 확인
• snarkjs wtns calculate로 witness 생성 테스트
• Ecne, Picus 같은 정적 분석 도구 사용

2.1.2 verifier.sol (온체인 구현 분석)

Solidity로 구현된 검증자 컨트랙트에서 구현 버그나 가스 최적화로 인한 보안 허점을 찾는다.

분석 방법:

• 입력 검증 로직:
  • verifyProof 함수의 파라미터 길이 체크가 있는가?
  • Public input 배열의 크기가 예상과 일치하는지 검증하는가?
  • 입력값이 필드 크기 $p$ 미만인지 확인하는가?
• 페어링 연산 검증:
  • Pairing.pairing 또는 bn256Add/Mul 프리컴파일 사용이 올바른가?
  • 페어링 방정식이 수학적으로 정확한가? (Groth16: $e(A, B) = e(\alpha, \beta) \cdot e(L, \gamma) \cdot e(C, \delta)$)
• 가스 최적화 부작용:
  • unchecked 블록 사용으로 인한 오버플로우 가능성
  • 인라인 어셈블리 코드의 메모리 안전성
• 재진입 공격 가능성: 검증 후 상태 변경 로직이 있다면 CEI 패턴이 지켜지는가?