Proving Circuit Functional Equivalence in Zero Knowledge

이 논문은 제로지식 증명 (ZKP) 과 형식 검증을 결합하여 IP 벤더의 설계 기밀성을 유지하면서도 제 3 자 IP 의 기능적 동등성을 공식적으로 검증할 수 있는 최초의 프라이버시 보호 프레임워크인 'ZK-CEC'를 제안하고 그 유효성을 실험적으로 입증합니다.

핵심

🏭 배경: 칩 공장에서의 '신뢰의 딜레마'

현대 사회의 모든 전자제품 (스마트폰, 자동차, AI) 은 수많은 '반도체 칩'으로 만들어집니다. 이 칩들은 한 회사가 혼자 다 만들지 않고, 여러 전문 업체 (IP 벤더) 가 부품을 만들어 공급합니다.

• 구매자 (시스템 통합자): "이 부품이 정말로 안전하고, 해커가 몰래 심어둔 '악성 코드 (하드웨어 트로이 목마)'가 없나요?"라고 확인하고 싶습니다.
• 판매자 (IP 벤더): "우리의 설계도는 우리 회사의 핵심 비밀 (비밀 레시피) 입니다. 보여드리면 도용당할 수 있으니 절대 보여드릴 수 없습니다."

이렇게 구매자는 안전을 확인하고 싶고, 판매자는 비밀을 지키고 싶어 서로가 서로를 믿지 못하는 '신뢰의 deadlock(교착 상태)'이 발생합니다.

🕵️‍♂️ 기존 방법의 한계: "요리 시식" vs "완전 검증"

지금까지의 해결책은 주로 **"시식 (Simulation)"**에 의존했습니다.

• 비유: 판매자가 "이 요리는 맛있습니다"라고 말하면, 구매자가 "그럼 이 재료로 요리해 보세요"라고 시켜서 맛을 보는 것입니다.
• 문제점: 시식해 본 요리가 맛있다고 해서, 그 요리사가 나중에 몰래 독약을 넣지 않았다는 보장은 없습니다. 특히 아주 드문 상황에서만 작동하는 '악성 코드'는 시식으로는 절대 잡아낼 수 없습니다.

이 논문은 **"요리 시식"이 아니라 "완전 검증 (Formal Verification)"**을 제안합니다. 즉, "이 레시피가 수학적으로 절대 독이 없음을 증명해 주세요"라고 요구하는 것입니다. 하지만 여기서 또 다른 문제가 생깁니다. "레시피 (설계도) 를 보여주지 않고 어떻게 수학적으로 증명하죠?"

💡 이 논문의 해결책: "ZK-CEC (영지식 증명)"

이 논문은 ZK-CEC라는 새로운 시스템을 제안합니다. 이름 그대로 '영지식 증명 (Zero-Knowledge Proof)' 기술을 칩 검증에 처음 적용한 것입니다.

🎭 핵심 비유: "비밀스러운 마술사의 상자"

이 기술은 마치 마술사 (판매자) 가 관객 (구매자) 앞에서 마술을 보여주는 것과 비슷합니다.

1. 상자 (비밀 설계도): 판매자는 자신의 칩 설계도를 투명하지 않은 상자 안에 넣습니다. 구매자는 상자를 열 수 없습니다.
2. 미션 (공식 요구사항): 구매자는 "이 상자가 들어있는 칩이 'A 라는 기능'을 정확히 수행하는지 확인하고 싶다"고 말합니다. (예: "이 칩이 암호화 기능을 정확히 수행하는지 확인해 줘.")
3. 증명 과정 (ZK-CEC):
   • 판매자는 상자를 열지 않고도, "이 상자가 A 기능을 수행한다는 수학적인 증명"을 만들어냅니다.
   • 이때 중요한 점은, 증명 과정에서 상자의 내용 (설계도) 은 전혀 드러나지 않는다는 것입니다.
   • 오직 **"상자가 A 기능을 수행한다는 사실"**과 **"증명의 길이/크기"**만 구매자에게 알려집니다.

🧩 어떻게 가능한가요? (논리의 마법)

논문의 핵심 아이디어는 "비밀 부분"과 "공개 부분"을 나누어 검증하는 것입니다.

• 공개된 청사진 (Public Spec): 구매자가 원하는 기능 (예: "이 칩은 1+1 을 하면 2 가 나와야 한다") 은 공개되어 있습니다.
• 비밀 레시피 (Secret IP): 판매자의 칩 내부 구조는 비밀입니다.
• 검증의 핵심: 판매자는 "내 비밀 레시피와 공개된 청사진을 합치면, 결국 '모순 (틀린 결과)'이 나올 수 없다"는 것을 증명합니다.
  • 만약 칩에 악성 코드가 있어서 결과가 다르게 나온다면, 수학적으로 '모순'이 발생합니다.
  • 판매자는 이 모순이 절대 발생하지 않음을 증명하면서, 동시에 자신의 레시피는 숨깁니다.

🚀 이 기술의 성과 (실험 결과)

연구팀은 이 시스템을 실제로 구현해 보았습니다.

• 결과: AES 암호화 칩 같은 복잡한 설계도 실제 시간 내에 성공적으로 검증했습니다.
• 속도: 기존 방식보다 약 2.8 배 더 빠르도록 최적화했습니다.
• 의미: 이제 칩을 사기 전에, 설계도를 훔쳐보지 않고도 "이 칩은 해킹당하지 않았고, 내가 원하는 대로 정확히 작동한다"는 것을 수학적으로 100% 확신할 수 있게 되었습니다.

🌟 요약: 왜 이것이 중요한가요?

이 논문은 "비밀을 지키면서도 진실을 증명하는" 방법을 제시했습니다.

• 과거: "내 칩을 보여줘야 안전하다고 믿을 수 있어." (비밀 유출 위험)
• 현재 (이 논문): "내 칩은 절대 보여주지 않지만, 수학적으로 안전하다고 증명해 줄게. 믿어줄래?" (신뢰 구축 + 비밀 보호)

이 기술은 앞으로 반도체 공급망의 신뢰를 회복하고, 더 안전하고 투명한 전자기기를 만드는 데 큰 역할을 할 것입니다. 마치 비밀 레시피를 공개하지 않고도 "이 식당은 위생 기준을 완벽히 지켰다"는 것을 증명하는 마법과 같습니다.

기술 요약

1. 연구 배경 및 문제 정의 (Problem)

• 배경: 현대 집적 회로 (IC) 생태계는 제 3 자 지식재산권 (3PIP) 통합에 크게 의존하고 있습니다. 이로 인해 하드웨어 트로이 목마 (Hardware Trojans), 보안 취약점, 악의적인 로직 버그 등의 위험이 증가하고 있습니다.
• 핵심 문제: IP 벤더와 시스템 통합자 간의 신뢰를 구축해야 하지만, IP 벤더는 설계의 기밀성 (지식재산권 보호) 을 유지해야 하고, 구매자는 설계의 정확성과 안전성을 검증해야 합니다.
• 기존 방법의 한계:
  • 기존 프라이버시 보존 하드웨어 검증 방법 (동형 암호화 기반 시뮬레이션, zkVM 기반 시뮬레이션 등) 은 모두 **시뮬레이션 (Simulation)**에 기반합니다.
  • 시뮬레이션은 특정 입력에 대한 결과만 확인하므로, 드물게 발생하는 조건에서 활성화되는 은밀한 하드웨어 트로이 목마나 엣지 케이스 (Corner cases) 를 포착하지 못합니다.
  • **형식 검증 (Formal Verification)**은 수학적 보장을 제공하지만, 기존 영지식 증명 (ZKP) 프로토콜 (예: ZKUNSAT) 은 공개된 공식을 증명하도록 설계되어 있어, **비밀 공식 (Secret Formula)**을 증명할 때 악의적인 증인 (Prover) 이 위조된 공식을 증명할 수 있어 **정합성 (Soundness)**이 깨지는 문제가 있었습니다.

2. 제안된 방법론 (Methodology)

저자들은 ZK-CEC라는 최초의 프라이버시 보존 하드웨어 형식 검증 프레임워크를 제안합니다. 이 프레임워크는 비밀 IP 와 공개 명세 간의 기능적 동등성을 증명하면서도 설계의 기밀성을 유지합니다.

2.1. 핵심 아이디어: 비밀 공식 속성 검증 청사진 (Blueprint)

기존 ZKUNSAT 프로토콜의 한계를 극복하기 위해 저자들은 다음과 같은 청사진을 제안합니다.

• 공식 분할: 검증 대상 공식을 **비밀 시스템 부분 ($\Phi_{sys}$)**과 **공개 속성 부분 ($\Phi_{prop}$)**으로 분할합니다.
• 검증 목표: 비밀 시스템과 공개 속성 위반 조건의 결합 ($\Phi_{sys} \land \Phi_{prop}$) 이 **불만족 (UNSAT)**임을 증명합니다.
• 정합성 보장 (Soundness) 을 위한 4 가지 조건:
  1. $\Phi_{pub}$의 정확성 및 만족 가능성: 공개된 명세와 미터 (Miter) 회로 구조가 올바르게 정의되고 만족 가능해야 함.
  2. $\Phi_{miter}$의 불만족성: 전체 미터 회로가 모순임을 증명 (UNSAT 증명).
  3. $\Phi_{sec}$의 만족 가능성: 비밀 회로 자체에 모순이 없음을 증명 (SAT 증명).
  4. 변수 격리: 공개 부분과 비밀 부분의 변수가 명시된 인터페이스 (I/O) 를 제외하고 겹치지 않음을 증명.

2.2. 프로토콜 구성 (ZK-CEC)

이 청사진을 기반으로 4 가지 하위 프로토콜을 설계하여 결합합니다.

1. $\Pi_{P1}$ (공개 부분 검증): 공개 명세와 미터 회로의 CNF 공식이 올바르게 인코딩되었는지 확인.
2. $\Pi_{P2}$ (UNSAT 증명): 기존 ZKUNSAT 프로토콜을 기반으로, 비밀 공식을 기반으로 한 반증 (Refutation) 증명 (Resolution proof) 의 유효성을 검증.
3. $\Pi_{P3}$ (SAT 증명): 비밀 공식이 실제로 만족 가능함을 증명 (비밀 할당값을 공개하지 않고).
4. $\Pi_{P4}$ (변수 격리 증명): 비밀 부분과 공개 부분의 변수가 인터페이스를 제외하고 겹치지 않음을 증명.

2.3. 기술적 세부 사항

• 인코딩: CNF 공식과 절 (Clause) 을 다항식 (Univariate Polynomials) 으로 인코딩하여 VOLE (Vector Oblivious Linear Evaluation) 기반 영지식 증명을 수행합니다.
• 암호화: 비밀 리터럴 (Literal) 은 키가 있는 해시 함수 (PRF) 를 사용하여 인코딩하여, 검증자가 리터럴의 극성 (양/부) 을 추론하지 못하도록 합니다.
• 최적화: 반증 증명 (Refutation Proof) 의 크기를 줄이기 위해 학습된 절 (Learned Clauses) 만을 저장하는 절 압축 (Resolvent Compression) 기법을 도입하여 증명 시간을 단축합니다.

3. 주요 기여 (Key Contributions)

1. 프라이버시 보존 형식 검증을 위한 일반화된 청사진: 공식을 비밀/공개 부분으로 분할하고 교차 제약을 부과하여, 숨겨진 로직에 대한 형식 증명을 가능하게 하면서 프로토콜의 정합성을 유지합니다.
2. 최초의 영지식 결합 동등성 검사 (ZK-CEC) 프로토콜: IP 벤더가 비밀 IP 가 공개 명세와 기능적으로 동등함을 증명할 수 있게 하여, 하드웨어 트로이 목마와 설계 오류에 대한 형식적 보장을 제공합니다.
3. 구현 및 성능 평가: EMP-toolkit 을 기반으로 프로토콜을 구현하고, 다양한 회로 (산술 연산자, 암호화 구성 요소 등) 에 대해 통신 및 계산 오버헤드를 분석했습니다.
4. 최적화 및 속도 향상: 증명 내 특정 단계를 병합하는 최적화 기법을 제안하여, 증명 시간을 최대 2.88 배까지 단축했습니다. 이 최적화로 인한 정보 누출이 공식 복원을 가능하게 하지 않음을 하한 분석 (Lower bound analysis) 을 통해 증명했습니다.

4. 실험 결과 (Results)

• 벤치마크: 37 개의 다양한 결합 회로 (Adder, Multiplier, AES S-Box, SM4, FSM 등) 를 사용하여 평가했습니다.
• 성능:
  • AES S-Box와 같은 실제적인 설계도 실용적인 시간 내에 검증이 가능함을 확인했습니다.
  • 전체 실행 시간의 대부분은 **UNSAT 증명 ($\Pi_{P1} + \Pi_{P2}$)**에 소요되었으며, 이는 불만족 문제가 co-NP-complete 문제이기 때문입니다.
  • 최적화 효과: 최적화 기법을 적용했을 때, 회로 크기가 커질수록 속도 향상 폭이 증가했습니다. (예: 6x6 Multiplier 기준 약 2.84 배, AES S-Box 기준 약 2.81 배).
• 확장성: 현재는 큰 회로에 대해 반증 증명 길이가 기하급수적으로 증가하여 메모리 부족 (Out-of-memory) 이나 시간 초과가 발생할 수 있으나, 작은/중간 규모 설계에서는 실용성을 입증했습니다.

5. 의의 및 결론 (Significance)

• 신뢰 구축: IP 벤더와 구매자 간의 신뢰 deadlock 을 해결하며, 설계 기밀성을 유지하면서 하드웨어 공급망의 무결성을 보장합니다.
• 형식 검증의 혁신: 기존 시뮬레이션 기반 검증의 한계를 넘어, 영지식 증명 기술을 통해 수학적 보장을 제공하는 최초의 프라이버시 보존 하드웨어 검증 프레임워크라는 점에서 의의가 큽니다.
• 확장 가능성: 제안된 청사진은 하드웨어뿐만 아니라 소프트웨어 및 사이버 - 물리 시스템의 프라이버시 보존 검증에도 적용 가능한 범용적인 솔루션을 제시합니다.

이 논문은 하드웨어 공급망 보안과 영지식 증명 기술의 융합을 통해, 지식재산권 보호와 보안 검증이라는 상충되는 요구사항을 동시에 해결하는 새로운 패러다임을 제시했습니다.