Simple ZK Static Program Analysis

Aug 16, 2024

들어가며

8월 16일 금요일의 PSE Core Program off-line meet 시간에는 ZKP 를 활용한 미니 해커톤이 진행되었다. 나는 Orion 논문을 읽다가 발견했던 흥미로운 주제인 ZK Static Program Analysis 로 미니 해커톤에 참가했다. 결과물로 구현하고자 하는 것은 아래와 같다.

임의의 Rust 프로그램 소스코드에 division by zero를 일으킬 수 있는 코드가 없음을 ZKP로 증명 하는 프로그램

ZKP 프로젝트인만큼 원본 소스코드에 관해서는 zero-knowledge인 것이 특징이다. 안전한 소스코드 임을 직접 제출할 필요 없이도 증명할 수 있는 것이다.

Parser와 Circuit은 아래와 같이 설게 및 구현되었다.

  1. Parser: Rust 코드를 분석해 Circuit의 입력값으로 변환하는 단계
  2. Circuit: 분석된 Rust코드를 통해 정적 분석을 수행하는 단계

구현물은 https://github.com/c0np4nn4/simple_zk_spa 에서 확인할 수 있다.

구현 상세

1. Parser

Parser는 Rust 문법으로 작성된 소스코드를 읽고 각 줄을 분석하여 아래 형태의 배열로 변환한다.

원소 1원소 2원소 3원소 4
Op Type
명령어 종류		lhs elem
좌항 원소		rhs elem 1
우항 원소 1		rhs elem 2
우항 원소 2

아주 간단한 형태의 예시 프로그램 사용을 가정했기에 분석기도 매우 간결하게 구현하였다. 명령어의 종류는 아래와 같이 총 4개로만 설계했다.

명령어 번호명령어 종류명령어 설명
0NoOp프로그램 종료를 의미하는 동작 코드
모든 배열의 원소가 $0$ ([0, 0, 0, 0])
1Assign좌항 원소에 우항 원소 1을 저장
이 때, 우항 원소 2는 무조건 $0$
2Addition좌항 원소에 우항 원소 1과 우항 원소 2의 덧셈 결과를 저장
3Division좌항 원소에 우항 원소 1과 우항 원소 2의 나눗셈 결과를 저장

또, 변수(variable)와 값(value)를 아래와 같이 구분했다.

  • 변수는 모두 홀수로 표기한다.
  • 값은 모두 $2$를 곱한 값으로 배열 원소에 저장한다.

1-1. Example

아래와 같은 예제 소스 코드 example.rs가 있다고 해보자.

fn main() {
	let x: i64 = 7;
	let y: i64 = -7;
	let z: i64 = x + y;
	let a: i64 = 4 / z;
}

각각의 줄은 다음과 같이 해석된다.

{
	[1, 1,  14, 0], # [  'assign',  'x',  7 * 2,  nil]
	[1, 3, -14, 0], # [  'assign',  'y', -7 * 2,  nil]
	[2, 5,   1, 3], # ['addition',  'z',    'x',  'y']
	[3, 7,   8, 5]  # ['division',  'a',  4 * 2,  'z']
}

값에 해당하는 $7, -7, 4$ 는 모두 2배 곱해져서 배열로 정리되어 있음을 확인할 수 있다.

2. Circuit

Parser는 단순하게 구현만 하면 됐지만, Circuit에서는 정적분석의 방법을 정하고 이를 구현해야 했다. 이에 관해 "정적 분석은 계산 안하기 하는 것이라 생각할 수 있다." 라는 조언을 바탕으로 아래와 같이 분석 방법을 정했다.

  • 양수인 값은 $+$로 둔다.
  • 음수인 값은 $-$로 둔다.
  • 덧셈의 피연산자에 관해 아래 세 가지 경우로 나뉠 수 있다.
    • (양수) + (양수) = 양수, 즉 $+$ 가 된다.
    • (음수) + (음수) = 음수, 즉 $-$가 된다.
    • (양수) + (음수) = ??

양수와 음수를 더한 경우 결과를 $T$라고 두었으며, 이는 ${+, -, 0}$ 중 하나이다.

division by zero 는 나눗셈의 제수(분모)가 $0$일 때 발생한다. 하지만,정확한 계산 수행없이 에러 발생의 가능성을 분석하기 위해서는 '제수가 $T$ 인지'를 검사하는 것으로 충분하다.

만약 검사하는 코드가 우주선이나 비행기에 들어가는 코드라고 생각해보자. division by zero 에러로 인해 프로그램이 정지하거나 문제를 일으키는 경우, 우주비행사 또는 비행기 탑승객들의 생명에 직접적인 영향을 끼칠 수 있다. 따라서, 실제로 에러가 발생할지 여부는 확실치 않더라도 가능성을 검출하는 것은 경우에 따라 대단히 중요해질 수 있음을 생각할 수 있다.

2-1. 변수 값 저장

홀수로 표시한 변수는 결국 어떠한 정보를 갖게 된다.

정적 분석에서는 실제 계산이 없이 분석이 진행되야 하므로, Circuit 내에서는 아래와 같은 작업이 이뤄진다.

값의 크기는 잊고 부호만 변수에 저장

예를 들어, 아래와 같은 코드가 있다고 해보자.

fn main() {
	let p: i64 = +11;
}

이를 Parser를 통해 배열로 변환하면 아래와 같은 결과를 얻는다.

{
	[1, 1, 22, 0] # ['assign',  'p',  11 * 2,  nil]
}

그리고 이를 Circuit 내부에서는 값의 크기인 $11$은 잊어버리고 그 부호인 $+$만 남긴다.

p = +

2-2. $T$ 계산 과정

$T$값은 덧셈연산을 통해 얻을 수 있다.

따라서, Op Type이 Addition 인 경우에 rhs elem 1과 rhs elem 2의 부호정보를 확인하고 ${+, -, T}$ 중 하나의 결과를 lhs elem에 저장하는 식으로 circuit을 구성했다.

결과

Please check the github repo: Link

https://c0np4nn4.github.io/posts/feed.xml