# Circuit Issues

> **“ZK-SNARK 회로? 막상 들어가보면 생각보다 복잡하다.”**

많은 개발자가 이 지점에서 난이도를 체감하며 한 번쯤 멈칫한다. 그러나 역설적이게도, 우리가 가장 부담을 느끼는 바로 그 **Circuit 레이어**가 ZK 시스템에서 가장 자주 취약점이 발생하는 핵심 구간이다.

왜 이런 일이 생길까?

사실 이유는 단순하다. 기존 개발 방식과 전혀 다른 사고를 요구할 뿐만 아니라, SNARK 비용을 줄이기 위해 회로를 극단적으로 최적화해야 하기 때문이다. 효율성을 조금만 놓쳐도 비용이 치솟고, 반대로 제약을 하나라도 빠뜨리면 치명적인 취약점으로 이어지기 쉽다.

이 글에서는 circuit 레이어에서 실제로 많이 발생하는 취약점들을 가볍게 정리한다. 어떤 문제들이 반복적으로 등장하는지, 그리고 왜 이런 문제들이 시스템 전체의 안전성을 흔들 수 있는지를 살펴본다. 이후에는 각 취약점을 구체적인 예시와 함께 설명하여, 회로 설계에서 반드시 의식해야 할 위험 요소들을 이해할 수 있도록 한다.

### 1. Under-constrained Circuits : 제약 조건 부족

Under-constrained 회로란 **증명자가 따라야 할 논리 규칙을 강제하는 제약 조건이 충분히 포함되지 않은 회로**를 말한다. 즉, 회로의 구성은 실제로 원하는 조건을 검증하지 못하며, 공격자가 임의의 값을 선택해도 증거가 생성될 수 있다.

제약 누락(Under-constraint)은 다음과 같은 설계 실수에서 가장 자주 발생한다.

* 값은 assign되었지만 이를 강제하는 산술 제약이 없음
* 특정 입력에 대해 기대한 범위를 검증하지 않음
* 서브 회로의 논리적 가정이 상위 회로에서 강제되지 않음
* 특정 조건(예: non-identity factor, positive value)이 기대됨에도 그 조건을 검증하는 제약이 없음

이 문제는 다른 회로 취약점의 직접적인 원인이 되기도 한다.

**예시**

제약 조건이 부족한(Under-constrained) 회로의 아주 기초적인 예시로 다음과 같은 `BadDivision` 회로를 들 수 있다.

```python
template BadDivision() {
    signal input dividend; // 피제수 (나누어지는 수)
    signal input divisor;  // 제수 (나누는 수)
    signal output quotient; // 몫

    quotient <-- dividend / divisor;

}

component main = BadDivision();
```

이 회로는 입력받은 두 수의 나눗셈 결과를 출력하도록 의도되었다. Circom에서 `<--` 연산자는 증인(Witness)을 생성하기 위해 값을 계산하여 변수에 할당하는 역할을 하지만, 이것이 수학적으로 올바른지 검증하는 R1CS 제약 조건(Constraints)을 생성하지는 않는다.

즉, 위 코드는 "몫(quotient)은 피제수를 제수로 나눈 값이다"라는 계산 로직만 있고, 검증자(Verifier)에게 "이 몫이 정말로 맞는지 확인하라"는 명령(`===`)이 없는 상태다.

이로 인해 공격자(악의적인 증명자)는 `dividend`나 `divisor` 값과 전혀 상관없는 임의의 숫자를 `quotient`에 넣어서 제출할 수 있으며, 검증 로직이 없기 때문에 해당 증명은 유효한 것으로 처리된다.

이러한 문제를 해결하기 위해서는 나눗셈이 올바르게 수행되었는지 확인하기 위해, 곱셈을 이용한 역연산 제약 조건을 반드시 추가해야 한다.

```python
quotient <-- dividend / divisor;
quotient * divisor === dividend; // 제약 조건 추가
```

**실제 사례**

* ZK Email: Regex 파싱 우회를 통한 이메일 스푸핑

  ZK Email 시스템은 정규표현식 처리를 위해 문자열 시작을 알리는 특수 값(`255`)을 사용하는데, 회로 내부에서 사용자 입력값에 이 값이 포함되지 않도록 막는 범위 확인(Range Check) 제약 조건이 누락되어 있었다. 공격자는 이 취약점을 이용해 이메일 제목(Subject)에 `\\xff`(`255`) 문자를 삽입함으로써, 회로의 파싱 상태(DFA)를 초기화시키고 이후 내용을 발신자(From) 헤더로 잘못 인식하게 만들었다. 결과적으로 공격자는 자신의 이메일 계정으로 메일을 발송했음에도 불구하고, 회로 상에서는 피해자의 이메일 주소에서 발송된 것처럼 보이게 하여 신원을 도용(Spoofing)할 수 있었다.

  ```python
  var num_bytes = msg_bytes+1;
  signal in[num_bytes];

  // 문자열의 시작을 알리기 위해 컴파일러가 255를 주입
  in[0]<==255;

  // [취약점 발생 지점]
  // 사용자의 입력(msg)을 in 배열로 옮기지만,
  // msg[i]가 255인지 아닌지 검증하는 범위 확인(Range Check) 제약 조건이 누락됨
  for (var i = 0; i < msg_bytes; i++) {
  	in[i+1] <== msg[i]; 
  }
  ```
* MACI 1.0: 투표 메시지와 상태 키 불일치를 이용한 검열

  MACI 시스템은 코디네이터가 투표를 집계하고 ZK로 증명하는데, 회로 내에서 투표 메시지의 `stateIndex`와 입력된 공개키의 인덱스가 반드시 일치해야 한다는 제약 조건이 누락되었거나 검증 순서가 잘못 구현되어 있었다. 악의적인 코디네이터는 이를 악용해 입력되는 공개키 배열(`currentStateLeaves`)의 순서를 임의로 조작하여, 특정 투표 메시지를 본래 주인이 아닌 엉뚱한 공개키와 매칭시켰다. 그 결과, 엉뚱한 키와 매칭된 투표는 서명 검증에 실패하여 "유효하지 않은 투표"로 처리되어 집계에서 제외되었고, 결과적으로 코디네이터는 증명 생성 실패 없이 특정 유권자의 표를 검열(삭제)할 수 있게 되었다.

  ```python
  template ProcessMessages(batchSize) {
      // 코디네이터가 임의로 순서를 정해서 입력할 수 있는 상태 리프(공개키 포함)
      signal input currentStateLeaves[batchSize];
      signal input msgs[batchSize];
      
      for (var i = 0; i < batchSize; i++) {
          // 메시지(msgs[i])가 현재 처리 중인 상태 리프(currentStateLeaves[i])에 
          // 해당하는지 확인하는 제약 조건이 누락됨.
          // 올바른 로직이라면 여기에 다음 줄이 있어야 함:
          // currentStateLeaves[i].index <== msgs[i].stateIndex;
          
          // 투표 처리 함수 호출 (서명 검증 등 수행)
          // 코디네이터가 currentStateLeaves[i]를 엉뚱한 것(예: 0번 리프)으로 바꿔치기하면,
          // 서명 검증이 실패하여 해당 메시지는 유효하지 않음(Invalid)으로 마킹됨.
          // 하지만 회로 검증 자체는 실패하지 않고 통과됨 (Censorship 성공).
          newStateLeaves[i] <== Transform(currentStateLeaves[i], msgs[i]);
      }
  }
  ```

### 2. Arithmetic Over/Underflow (산술 오버/언더플로우)

ZK(영지식) 암호학에서 모든 연산은 스칼라 필드(Scalar Field) 위에서 이루어지며, 이는 **모든 계산이 필드의 위수 p로 모듈러 연산(mod p)** 처리된다는 의미이다. Circom 회로 역시 같은 방식으로 동작하며, 사용되는 필드의 위수 p는 다음과 같은 거대한 소수이다.

```
p = 21888242871839275222246405745257275088548364400416034343698204186575808495617
```

이 말은, 개발자가 필드 연산의 특성을 정확히 이해하지 못하거나 오버플로우·언더플로우를 고려하지 않으면 **의도와 전혀 다른 결과가 회로에서 '참'으로 평가되는 상황이 발생할 수 있음**을 의미한다. 예를 들어 Circom에서는 다음과 같은 관계가 모두 참이다.

* $$(0 - 1) \equiv p - 1$$
* $$((p - 1) + 1) \equiv 0$$

이러한 모듈러 특성은 회로 설계에서 사소해 보이지만 치명적인 실수를 유발하기 쉽다.

**예시**

```python
template getNewBalance() {
   signal input currentBalance;
   signal input withdrawAmount;
   signal output newBalance;

   newBalance <== currentBalance - withdrawAmount;
}
```

만약 사용자가 현재 잔액(`currentBalance`)보다 더 큰 금액(`withdrawAmount`)을 입력하면, `newBalance` 출력값에서 언더플로우가 발생한다. 결과적으로 `newBalance`는 음수가 되는 것이 아니라, p에 가까운 **극도로 큰 양수**가 된다. 이는 회로 작성자가 전혀 의도하지 않은 결과이다.

**실제 사례**

* PSE & Scroll zkEVM: Missing Overflow Constraint

  PSE & Scroll zkEVM의 모듈로(Modulo) 가젯은 나눗셈 검증(`k * n + r == a`)을 위해 `2^256` 모듈러 연산을 수행하는 `MulAddWords`를 사용했으나, 연산 결과(`k * n + r`)가 `2^256`을 초과하여 오버플로우가 발생하는 것을 막는 제약 조건이 누락되어 있었다. 악의적인 증명자는 몫(`k`) 값을 조작하여 의도적으로 오버플로우를 발생시킴으로써, 실제로는 틀린 모듈로 연산(예: `0 = 2^255 mod 3`)이 회로 내에서는 `2^256` 모듈로 연산의 특성(`Wrap-around`)에 의해 성립하는 것처럼 조작할 수 있었다. 모듈로 연산은 zkEVM의 핵심 구성 요소이므로, 공격자는 이를 악용해 잘못된 상태 업데이트가 유효한 것처럼 검증자를 속일 수 있는 치명적인 문제가 발생했다.

  ```python
  template ModuloGadget() {
      signal input a; // 피제수 (Dividend)
      signal input n; // 제수 (Divisor)
      signal input r; // 나머지 (Remainder)
      signal input k; // 몫 (Quotient, 증명자가 입력)

      // MulAddWords는 내부적으로 다음을 검증한다: 
      // a * b + c == d (modulo 2^256)
      // 여기서는 k * n + r == a (modulo 2^256)을 검증하게 되다.
      component mulAdd = MulAddWords();
      mulAdd.a <== k;
      mulAdd.b <== n;
      mulAdd.c <== r; 
      mulAdd.d <== a;

      // (k * n + r)의 결과값이 2^256보다 작아 오버플로우가 발생하지 않음을 보장해야 한다.
      // 이 검증이 없어서 증명자는 k를 매우 큰 값(예: 2^255)으로 설정하여 
      // 오버플로우를 통해 잘못된 등식을 성립시킬 수 있다.
  }
  ```

### 3. Mismatching Bit Lengths

ZK 회로는 종종 특정 입력값이 n비트 이하라는 전제를 기반으로 내부 로직을 구성한다. 그러나 개발자가 입력값의 비트 길이를 강제하는 제약(Bit-length constraint)을 명시적으로 추가하지 않으면 문제가 발생한다.

**예시**

CircomLib의 유틸리티 회로(예: `LessThan`, `GreaterEq` 등)는 입력값이 특정 비트 수(n) 이내라고 가정하고 설계되어 있다. 만약 개발자가 이 회로를 사용할 때, 입력값에 대해 별도의 비트 수 제약(Bit-length Constraint)을 걸지 않으면, 공격자가 n비트를 초과하는 매우 큰 값을 입력하여 회로 내부의 연산 로직을 무력화하고 잘못된 결과를 유도할 수 있다.

```python
template LessThan(n) {
    assert(n <= 252);
    signal input in[2];
    signal output out;

    component n2b = Num2Bits(n+1);

    n2b.in <== in[0]+ (1<<n) - in[1];

    out <== 1-n2b.out[n];
}
```

위 코드에서 `1<<n`은 뺄셈 결과가 음수가 되는 것을 방지하기 위한 보정값이다. 하지만 `in[1]`이 n비트보다 큰 값(즉, `1<<n`보다 큰 값)이 들어오면, `Num2Bits`에 전달되는 값이 훼손되어 엉뚱한 비교 결과를 출력하게 된다.

**실제 사례**

* Dark Forest v0.3: RangeProof 입력값 비트 검증 누락 Dark Forest는 오버플로우 방지를 위해 `RangeProof`를 구현하면서 `LessThan` 회로를 사용했는데, `LessThan`은 입력값이 특정 비트 수 이내라고 가정하고 동작함에도 불구하고 실제 입력값(`in`, `max_abs_value`)에 대한 비트 길이 제약 조건이 누락되어 있었다. 공격자는 예상된 비트 수보다 훨씬 큰 값을 입력하여 `LessThan` 회로 내부의 비트 연산 로직(언더플로우/오버플로우 유발)을 무력화시킬 수 있었다. 결과적으로 공격자는 입력값이 허용 범위를 벗어났음에도 불구하고 `RangeProof`를 성공적으로 통과시켜, 게임 내에서 유효하지 않은 상태를 만들거나 로직을 우회할 수 있었다.

  ```python
  template RangeProof(bits, max_abs_value) {
      signal input in;

      // LessThan은 입력값이 bits 길이 이내라고 가정하지만,
      // 여기서 in이나 max_abs_value가 실제로 bits 길이인지 확인하는 제약 조건이 없음.
      component lowerBound = LessThan(bits);
      component upperBound = LessThan(bits);

      lowerBound.in[0] <== max_abs_value + in;
      lowerBound.in[1] <== 0;
      lowerBound.out === 0;

      upperBound.in[0] <== 2 * max_abs_value;
      upperBound.in[1] <== max_abs_value + in;
      upperBound.out === 0;
  }
  ```
* BigInt: BigMod 나머지(Remainder) 비트 검증 누락

  큰 수의 모듈러 연산을 수행하는 `BigMod` 회로는 몫(`div`)과 나머지(`mod`)를 계산하는데, 몫에 대해서는 비트 길이 제약 조건을 적용했으나 실수로 나머지에 대한 비트 길이 제약 조건은 누락했다. 공격자는 수학적으로 식은 성립하지만(검증 통과), 회로가 기대하는 포맷(Proper representation)보다 훨씬 큰 비트 수를 가진 비정상적인 값을 나머지로 제출할 수 있었다. 비트 길이가 검증되지 않은 나머지 값이 후속 회로로 전달되면서 데이터 표현 방식이 깨지게 되고, 이를 사용하는 프로토콜 전체의 예기치 못한 동작이나 오류를 유발할 수 있었다.

  ```python
  var longdiv[2][100] = long_div(n, k, k, a, b);
  for (var i = 0; i < k; i++) {
      div[i] <-- longdiv[0][i]; // Quotient
      mod[i] <-- longdiv[1][i]; // Remainder
  }
  div[k] <-- longdiv[0][k];

  component range_checks[k + 1];
  for (var i = 0; i <= k; i++) {
      range_checks[i] = Num2Bits(n);
      range_checks[i].in <== div[i];
  }

  // mod[] (나머지) 배열의 각 요소가 n비트 이내인지 확인하는 제약 조건이 누락됨.
  // 따라서 공격자는 n비트를 초과하는 값을 mod[i]에 넣을 수 있음.
  ```

### 4. Nondeterministic Circuits

비결정적 회로는 **제약 조건 부족(Under-constrained)** 회로의 일종으로, **하나의 결과(Outcome)에 대해 여러 가지 유효한 증명(Proof)을 생성할 수 있는 상태**를 의미한다. 회로 내에 필수적인 제약 조건이 누락되어 있어, 입력값이나 중간 계산 과정에서 수학적으로 동일하지만 표현이 다른 여러 값(Alias)을 허용할 때 발생한다.

**예시**

가장 대표적인 기술적 예시는 `circom-pairing` 라이브러리의 필드 요소 표현 방식이다. 정상적인 제약에서는 유한체(Field)의 요소 A는 소수 p보다 작아야 하므로, $$0 \le A < p$$ 조건을 만족해야 한다. 그런데 대부분 회로의 경우 최적화를 위해 $$0 \le A$$ 조건만 검사하고, $$A < p$$ 제약 조건을 생략하는 경우가 있다. 이 경우, A와 A + p는 수학적으로는 같은 값이지만, 컴퓨터 상으로는 서로 다른 비트열을 가진 두 개의 유효한 값(Alias)으로 취급되어 비결정성을 유발한다.

**실제 사례**

* 0xPARC StealthDrop: Nondeterministic Nullifier

  StealthDrop은 에어드랍 중복 수령을 막기 위해 사용자의 ECDSA 서명을 Nullifier(이중 지불 방지 값)로 사용했으나, ECDSA 서명 검증 방식 자체가 비결정적(Nondeterministic)이라 동일한 개인키와 메시지로도 수학적으로 유효한 서명을 여러 개 만들 수 있다는 점을 간과했다. 공격자는 이 취약점을 이용해 하나의 자격 증명(개인키)으로 서로 다른 형태의 유효한 서명들을 생성한 뒤, 이들을 각각 다른 Nullifier로 사용하여 여러 개의 SNARK 증명을 생성했다. 그 결과, 스마트 컨트랙트는 제출된 Nullifier(서명)들이 서로 다른 값이므로 이를 별개의 요청으로 인식하여 통과시켰고, 결과적으로 공격자는 한 번의 자격으로 에어드랍을 여러 번 중복 수령할 수 있었다.

  ```python
  template VulnerableClaim() {
      signal input userMessage;
      signal input userPubKey;
      
      // Nullifier로 사용될 서명을 외부 입력(Public Input)으로 받음
      signal input nullifierSignature; 

      // 서명 검증 컴포넌트
      component verifier = ECDSAVerify();
      verifier.msg <== userMessage;
      verifier.pubKey <== userPubKey;
      verifier.signature <== nullifierSignature;
      
      // 서명이 유효한지만 체크함 (Verify only)
      // ECDSA 특성상 동일한 키/메시지에 대해 다른 서명도(예: s vs -s, 다른 nonce k 사용 등)
      // 유효하다고 판단하므로, 다른 nullifierSignature 값을 넣어도 통과됨.
      verifier.isValid === 1;
  }
  ```

### 5. Unused Public Inputs Optimized Out : 최적화로 제거된 미사용 공개 입력

많은 회로들이 특정 변수를 공개 입력(Public Input)으로 선언하지만, 해당 변수에 대해 어떠한 제약 조건(Constraint)도 걸지 않는 실수를 범한다. 이 변수들은 증명 검증 시 중요한 키 정보로 사용될 의도였으나, **Circom 2.0 컴파일러의 기본 최적화(Optimizer)** 기능은 제약 조건에 관여하지 않는 변수를 회로에서 아예 제거(Optimize out)해 버린다.

결과적으로, R1CS(제약 시스템)에서 해당 변수가 사라지게 되며, 검증자(Verifier) 컨트랙트에 증명을 제출할 때 공격자가 해당 공개 입력 위치에 **어떤 값을 넣어도 검증이 성공**하는 치명적인 취약점이 발생한다.

**예시**

아래 코드는 `inThree`를 공개 입력으로 선언했지만, 정작 회로 로직(`out <== inOne + inTwo`)에는 사용하지 않은 경우이다.

```python
template UnusedPubInput() {
    signal inOne;
    signal inTwo;
    signal input inThree; // 제약 조건에 쓰이지 않음

    signal output out;

    out <== inOne + inTwo; 
    // inThree는 어디에도 관여하지 않음 -> 최적화 과정에서 삭제됨
}

component main{public [inThree]} = UnusedPubInput();
```

이 경우, 컴파일러는 `inThree`를 불필요한 변수로 간주하여 삭제한다. 공격자는 기존의 유효한 증명을 가져와서 `inThree` 자리에 원하는 임의의 값을 넣어 제출해도 검증을 통과할 수 있다.

**실제 예시**

* Semaphore

  Semaphore는 익명으로 그룹 멤버십을 증명하고 신호(Signal)를 보낼 수 있는 애플리케이션이다. 사용자가 보내는 메시지는 해시되어 `signalHash`라는 공개 입력으로 처리된다. 만약 개발자가 `signalHash`를 공개 입력으로만 선언하고 내부 제약 조건을 걸지 않았다면, 최적화 과정에서 이 변수가 삭제된다. 공격자는 정당한 사용자의 유효한 멤버십 증명을 가로챈 뒤, `signalHash` 값만 자신이 원하는 메시지(가짜 신호)로 바꿔치기하여 다시 제출할 수 있다. 회로는 `signalHash`를 검증하지 않으므로, 공격자가 조작한 메시지는 정당한 유저가 보낸 것처럼 처리된다.

  ```python
  template Semaphore(nLevels) {
      signal input identityNullifier;
      signal input identityTrapdoor;
      signal input treePathIndices[nLevels];
      signal input treeSiblings[nLevels];

      // 공개 입력(Public Input)으로 선언되었으나, 
      // 아래 로직에서 제약 조건(Constraint)에 직접적으로 사용되지 않음.
      signal input signalHash;
      signal input externalNullifier;

      signal output root;
      signal output nullifierHash;


      component calculateSecret = CalculateSecret();
      calculateSecret.identityNullifier <== identityNullifier;
      calculateSecret.identityTrapdoor <== identityTrapdoor;

      signal secret;
      secret <== calculateSecret.out;

    
      component calculateIdentityCommitment = CalculateIdentityCommitment();
      calculateIdentityCommitment.secret <== secret;

   
      component calculateNullifierHash = CalculateNullifierHash();
      calculateNullifierHash.identityNullifier <== identityNullifier;

      component inclusionProof = MerkleTreeInclusionProof(nLevels);
      inclusionProof.leaf <== calculateIdentityCommitment.out;

      for (var i = 0; i < nLevels; i++) {
          inclusionProof.siblings[i] <== treeSiblings[i];
          inclusionProof.pathIndices[i] <== treePathIndices[i];
      }

      root <== inclusionProof.root;
      nullifierHash <== calculateNullifierHash.out;

      // signalHash를 회로 내부에서 검증하는 로직(예: 제곱 등)이 전혀 없음.
      // 결과적으로 컴파일러는 signalHash를 불필요한 변수로 판단하여 삭제함.
  }

  component main {public [signalHash, externalNullifier]} = Semaphore(20);
  ```

### Reference

* <https://github.com/0xPARC/zk-bug-tracker>


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://upsidezkp.gitbook.io/upside-zkp-docs/step-5/zkp/circuit-issues.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.