Intro

암호학에서 영지식 증명(Zero-Knowledge Proof, ZKP)이란, 어떤 사실을 알고 있다는 점을 그 내용 자체는 전혀 누설하지 않고 검증자에게 증명하는 기법을 말합니다.

이러한 성질을 실제 시스템으로 구현하려면 코드로 로직을 작성해야 하지만, 문제는 코드 실행 결과 자체를 신뢰할 수 없다는 점입니다. 따라서 “이 코드가 올바르게 실행되었는가?”를 다시 코드로 검증하는 방식은 근본적인 해결책이 될 수 없습니다.

그래서 ZKP 시스템은 검증 대상을 코드가 아닌 수학적으로 검증 가능한 형태로 변환합니다. 이때 프로그램으로 구현된 함수 로직을 덧셈과 곱셈 게이트의 조합으로 분해하여 표현하고, 그 결과를 수학적으로 검증할 수 있는 구조로 만드는 과정이 바로 R1CS(Rank-1 Constraint System)입니다.

R1CS를 통해 “주어진 입력과 증명자가 주장하는 출력이 특정 연산 규칙을 만족한다”는 사실을 순수한 수학적 관계로 표현할 수 있으며, 이를 기반으로 영지식 증명이 가능해집니다.

개념적 명제(statement)

ZKP를 풀어서 설명하면, “특정 조건”을 “만족하는 데이터”를 공개하지 않고 그 사실을 알고 있음을 증명하는 기술입니다. 이를 조금 더 추상적인 명제로 표현하면 다음과 같습니다.

• “성인(20살 이상)임”을 “신분증”을 공개하지 않고 증명
• Alice가 Bob에게 1 BTC를 “전송했음”을 “트랜잭션”을 공개하지 않고 증명

여기서 “성인(20세 이상)임”이나 “전송했음”은 검증자가 확인하고 싶은 특정 조건에 해당하고, “신분증”이나 “트랜잭션”은 그 조건을 만족함을 입증하는 실제 데이터입니다.

이러한 증명 과정은 시스템 관점에서 봤을때, 결국 컴퓨팅 연산(computation)을 통해 수행됩니다. 이 관점에서 보면, “특정 조건”은 프로그래밍에서 하나의 함수(function)에 해당하며, 그 조건을 만족하는 “데이터”는 함수에 들어가는 입력(Input)과 출력(Output)이라고 볼 수 있습니다.

즉, 영지식 증명이란 어떤 함수에 대해 올바른 입력과 출력의 관계를 알고 있다는 사실을, 그 입력과 출력 자체는 공개하지 않은 채 증명하는 기술이라고 이해할 수 있습니다.

Computation

영지식 증명을 구현하기 위해서는 앞서 살펴본 것처럼 추상적인 명제(statement)를 그대로 다룰 수 없습니다. 따라서 이를 컴퓨팅 연산(computation)의 형태로 바꾸기 위한 수학적 컴파일 과정을 거치게 됩니다.

R1CS를 이해하기 위해, 업계에서 가장 자주 예제로 사용되는 함수인 $f(x)=x^3+x+5$ 공식을 통해 알아보겠습니다. 이 공식을 하나의 개념적 명제(statement)로 바꾸면 다음과 같이 표현할 수 있습니다.

“x=3일 때 결과가 35가 되는 특정 함수를 알고 있다.”

“x=3일 때 결과가 35가 되는 특정 함수를 알고 있다.”

function qeval(x) {
  const y = x ** 3;
  return x + y + 5;
}

아래는 주어진 함수를 컴퓨팅 연산 관점에서 구현된 JavaScript 예시입니다.

연산 회로(arithmetic circuit)

R1CS는 $A \times B = C$ 의 형태로 표현되며, 이를 벡터 관점에서 풀어 쓰면, $A \cdotp S * B \cdotp S - C \cdotp S = 0$ 을 만족해야 합니다. (왜 이러한 형태가 필요한지는 끝까지 읽어보면 이해할 수 있습니다.)

연산 회로란 주어진 수식을 사칙연산 단위로 풀어서 쓴 형태이며, 연산 회로에서는 곱셈(×)과 덧셈(+) 게이트를 회로는 $A \times B = C$의 형태로 표현하기에, 임의의 함수를 연산 회로 형태로 표현하는 것이 R1CS를 구성하는 출발점이 됩니다.

먼저 정해진 함수를 평탄화(Flattening)를 통해 $A \times B = C$ 형태로 만듭니다. $f(x)=x^3+x+5$의 경우 위와 같은 과정을 통해 연산 회로꼴고 변환할 수 있습니다.

게이트와 선으로 연산 과정을 시각화한 도해를 써킷(circuit)이라 부릅니다. 각 연산에서 도출되는 중간 변수와 최종 결과를 게이트와 선으로 연결해 표현한 써킷은 위와 같습니다.

Transcript

Transcript란 함수를 산술 회로로 변환하는 과정에서 정의된 입력, 출력, 중간 결과 를 의미하며, R1CS가 만족해야하는 $A \cdotp S * B \cdotp S - C \cdotp S = 0$ 의 $S$ 를 의미합니다. $f(x)=x^3+x+5$로 부터 정의된 Transcript는 위와 같이 6개입니다.

우리가 증명해야하는 명제 _“x=3일 때 결과가 35가 되는 특정 함수를 알고 있다.”_로 봤을때, Transcript는 x=3을 입력했을 때, 각 게이트를 거치며 값이 순차적으로 결정되고, 최종 출력으로 $out=35$가 도출되는 과정을 의미합니다.

이 값들은 모두 산술 회로로 연결되어 있기 때문에, x가 한 번 정해지면 중간 변수들의 값 역시 자동으로 결정됩니다. 따라서 임의로 값을 조작하거나 다른 값이 개입될 여지가 없으며, 계산 결과는 하나로 고정되는 고유성을 갖습니다.

R1CS / arithmetic circuit에서 Transcript(중간 결과 변수)는 “곱셈(x, ×) 게이트에서만 새로 생성된다.”
중간 결과 sym2는 x 게이트가 아니라 원래는 표현하지 않지만, 가독성을 위해 추가했다. 실제로는sym2는 없고 out = y + x + 5로 표현된다.

R1CS

다음 단계는 이렇게 사칙연산 게이트 단위로 표현된 연산 회로를 R1CS 형태로 변환하는 과정입니다. R1CS는 벡터($A,B,C$) 로 구성된 세 개의 벡터 그룹이 순서대로 나열된 구조 로 이루어져 있으며, R1CS의 해는 하나의 벡터 s입니다. 이때 벡터 $S$는 다음 방정식을 만족해야 합니다.

“$\cdotp$”는 _내적(dot product)_을 의미합니다.

아까 산술회로 단계에서 평탄화(Flattening)를 통해 $A \times B = C$ 형태로 총 4가지 게이트를 만들었습니다. 여기서 각 게이트를 제약사항(constrain)으로 표현합니다. 각 제약사항을 벡터($A,B,C$) 로 표현해야합니다.

먼저 가장 직관적인 이해를 위해 식 (4)를 표현하면 위와 같습니다. 가로 방향으로 나열된 벡터는 Transcript에 포함된 변수들을 의미합니다.

어떤 변수가 A, B, C에 포함되어 있다면, 해당 변수 앞에 곱해지는 상수값을 벡터에 넣으면 됩니다. 예를 들어 A의 $sym_2$의 상수는 1 ($1 \times sym_2)$는 이니까 백터에 1을, $1$의 상수는 5 ($5 \times 1$)니까 5가 됩니다.

A,B,C 각각의 백터를 S에 곱하여, $A \cdotp S * B \cdotp S - C \cdotp S = 0$라는 관계로 표현하면 위와 같습니다. 이처럼 함수에 대해 올바른 Transcript의 관계를 알고 있다는것을 증명할 수 있습니다.

반대로, 만약 증명자가 x=3, out=35를 R1CS에 대입해 겉보기에는 거짓말을 하지 않은 것처럼 보이더라도, 중간 단계에 해당하는 $sym_2$의 값을 임의로 조작한다면 위와 같이 $A \cdotp S * B \cdotp S - C \cdotp S = 0$를 만족할 수 없게 됩니다.

이처럼 입력과 출력뿐만 아니라 모든 중간 계산 과정까지 일관되게 만족하도록 강제하기 위해 R1CS 시스템을 활용합니다. R1CS는 연산 회로 전체에 대한 제약을 동시에 적용함으로써, 계산 과정 중 어느 한 단계라도 조작될 경우 검증을 통과할 수 없도록 설계되어 있습니다.

R1CS 최종 표현

이제 왜 R1CS가 이처럼 요상한(?) 형태의 벡터 구조를 사용하는지 이해했으니, 이어서 나머지 (1), (2), (3), (4) 제약사항을 전체적으로 표현해보겠습니다.

이렇게 $A, B, C$로 표현된 제약사항을 각 구성요소로 묶어서 배열의 형태로 만들어 보겠습니다.

우리는 4개의 제약사항과 6개의 Transcript가 정의됬으니, $4 \times6$ 형태의 배열로 구성된것을 알 수 있습니다. 이제 이를 $A \cdotp S * B \cdotp S - C \cdotp S = 0$를 만족하는 형태로 표현해보겠습니다.

각 배열에 대해 내적을 수행하면, 최종 결과가 $\begin{pmatrix} 0\\0\\0\\0 \end{pmatrix}$으로 도출되는 것을 확인할 수 있습니다. 이는 모든 제약식이 만족되었음을 의미합니다.

파란색 표시는 우리가 위에서 예시로 다뤘던 (4)제약사항을 표시해둔것입니다!

다음 시리즈 QAP를 위하여

R1CS는 시스템 상에서 코드를 수학적으로 검증 가능한 형태로 변환하기 위한 과정이며, 지금까지 그 과정을 살펴보았습니다. 이 과정에서 계산 결과가 하나로 고정되는 고유성의 성질을 통해, 임의로 값을 조작하거나 다른 값이 개입될 여지가 없다는 사실 또한 확인할 수 있었습니다.

하지만 개발자의 관점에서 보면, 여전히 시스템 차원의 한계를 고려해야 합니다. R1CS의 최종 형태는 증명자와 검증자라는 두 엔티티 간의 상호작용(Interactive) 과정에서 사용성이 떨어지며, 제약사항이 증가함에 따라 데이터의 크기 또한 매우 큽니다(Non-Succinct). 이러한 문제를 해결하기 위해 암호학에서는 수의 체계를 집합(유한체)과 다항식으로 구성해 보다 효율적인 검증 방식을 설계합니다.

다음 시리즈에서 다룰 Quadratic Arithmetic Programs(QAP)는 R1CS의 값과 증명 체계를 다항식 형태로 표현함으로써, “수천 개의 계산 제약을 단 하나의 수학적 사실로 압축해서 검증을 극단적으로 빠르게 만들기 위해서” 등장한 개념입니다. 다음 시리즈에서 자세하게 다뤄보겠습니다.