A Deductive System for Contract Satisfaction Proofs

이 논문은 하드웨어 - 소프트웨어 계약 만족성 증명을 위한 새로운 연역적 증명 시스템을 개발하여, Rocq 증명 도구를 통해 상대적 추적 동등성 문제를 해결하고 두 가지 복잡한 사례에 적용한 결과를 제시합니다.

핵심

이 논문은 **"컴퓨터 칩이 비밀을 지키고 있는지 증명하는 새로운 방법"**에 대해 설명합니다.

기존의 복잡한 수학적 증명 대신, **인터랙티브 증명 도구 (Rocq)**를 사용하여 하드웨어와 소프트웨어가 어떻게 서로 신뢰할 수 있는 관계를 맺는지 논리적으로 증명하는 시스템을 개발했습니다.

이 내용을 일반인이 이해하기 쉽게 요리사와 식자재 검수원, 그리고 스파이 영화에 비유해서 설명해 드리겠습니다.

---

1. 배경: 왜 이 문제가 중요할까요? (스파이 영화의 상황)

상상해 보세요. 여러분은 클라우드 서버라는 거대한 빌딩에서 일하고 있습니다. 하지만 이 빌딩에는 다른 회사 (해커) 의 직원들도 함께 살고 있습니다.

• 문제: 해커는 여러분이 비밀 문서를 읽는다고 직접 볼 수는 없습니다. 하지만 여러분이 문서를 읽을 때 발생하는 미세한 소리 (팬 소음), 전류 소모량, 캐시 메모리 사용량 같은 '부수적인 흔적 (Side-channel)'을 관측하면, 여러분이 무엇을 했는지 추측할 수 있습니다.
• 해결책 (계약): 하드웨어 제조사는 "우리의 CPU 는 이런 식으로만 정보를 흘릴 것이다"라고 **계약서 (Contract)**를 작성합니다. 소프트웨어 개발자는 이 계약서를 믿고 프로그램을 작성합니다.
• 핵심 질문: "이 계약서 (하드웨어가 흘리는 정보의 양) 가 실제 CPU 의 동작보다 더 많거나 적지 않고, 정확히 맞거나 더 많은 정보를 포함하고 있을까?" 즉, 계약서가 실제 하드웨어를 **완벽하게 감싸고 있는지 (Over-approximation)**를 증명해야 합니다.

2. 기존 방법의 한계: "눈으로 확인하기" vs "수학으로 증명하기"

• 기존 방법 (모델 체킹): 컴퓨터가 모든 경우의 수를 일일이 시뮬레이션해 보며 "혹시 비밀이 새나가는 경우가 있나?"를 찾습니다. 하지만 CPU 는 너무 복잡해서 모든 경우를 다 볼 수 없거나, 프로그램이 너무 길어지면 컴퓨터가 멈춰버립니다.
• 종이와 펜: 수학자들이 손으로 증명합니다. 하지만 이 증명서는 너무 길고 복잡해서 (예: 25 페이지 분량) 다른 사람이 검증하기가 매우 어렵습니다.

3. 이 논문의 해결책: "증명 도우미 (Rocq) 와 새로운 증명법"

저자들은 **"증명 도구 (Rocq)"**를 사용하여 이 복잡한 논리를 컴퓨터가 직접 검증할 수 있도록 만들었습니다. 여기서 핵심은 **'상대적 추적 동등성 (Relative Trace Equality)'**이라는 개념입니다.

🍳 비유: 요리사와 식자재 검수원

이 논리의 핵심을 **요리사 (하드웨어)**와 **식자재 검수원 (계약)**에 비유해 볼까요?

1. 상황: 두 명의 요리사 (A 와 B) 가 같은 레시피 (프로그램) 를 가지고 있습니다. 하지만 A 는 **실제 주방 (하드웨어)**에서 요리하고, B 는 **가상 주방 (계약)**에서 요리합니다.
2. 목표: "만약 가상 주방의 요리사 B 가 두 가지 다른 재료를 써도 **같은 냄새 (정보)**만 풍긴다면, 실제 주방의 요리사 A 도 두 가지 재료를 써도 같은 냄새만 풍겨야 한다."는 것을 증명해야 합니다.
3. 난이도:
   • 가상 주방은 항상 똑같은 속도로 요리합니다.
   • 실제 주방은 예측 실패 (Speculation) 나 순서 변경 (Out-of-order) 으로 인해 요리 속도가 들쑥날쑥할 수 있습니다. (예: A 는 먼저 고기를 굽고, B 는 먼저 야채를 자를 수도 있음)
   • 그래서 두 주방의 요리 과정을 동시에 (Lockstep) 비교하는 것은 불가능합니다.

🕵️‍♂️ 새로운 증명법: "상대적 비동기 추적 (Relative Bisimulation)"

저자들은 **"동시 진행이 아니더라도, 결국 같은 결론에 도달하면 된다"**는 논리를 개발했습니다.

• 기존 방식: "A 와 B 가 동시에 한 걸음씩 움직여야 해." (이건 너무 엄격해서 증명하기 어려움)
• 이 논문의 방식: "A 가 3 걸음 뛰고, B 가 1 걸음만 뛰어도, 결국 두 사람의 발자국 패턴 (정보) 이 같다면 OK야."

이것을 증명하기 위해 4 개의 시나리오를 동시에 추적합니다.

1. 가상 주방 A (재료 1)
2. 가상 주방 B (재료 2)
3. 실제 주방 A (재료 1)
4. 실제 주방 B (재료 2)

이 네 가지가 서로 어떻게 움직이든, **"가상 주방의 냄새가 같다면 실제 주방의 냄새도 같아야 한다"**는 것을 논리적으로 쌓아 올리는 증명 시스템을 만들었습니다.

4. 이 시스템의 장점: "조각 puzzle 맞추기"

이 증명 시스템은 마치 레고 블록을 쌓는 것처럼 작동합니다.

• 점진적 증명: 처음부터 완벽한 증명서를 다 만들어야 하는 게 아니라, 작은 단계 (블록) 를 하나씩 쌓아갑니다.
• 유연성: 실제 주방이 가상 주방보다 더 빨리 움직일 때, "잠시 기다려"라고 말하며 논리를 이어갈 수 있습니다.
• 상호작용: 사용자가 "여기서는 이 규칙을 써도 돼"라고 제안하면, 컴퓨터가 "그 규칙이 수학적으로 안전한가?"를 즉시 확인해 줍니다.

5. 실제 적용 사례: "스펙트르 (Spectre) 공격 방어"

이론만 설명하면 어렵기 때문에, 실제 유명한 해킹 기법인 '스펙트르 (Spectre)' 공격을 막는 방법을 증명했습니다.

• 상황: CPU 는 명령을 미리 예측해서 실행합니다. (예: "문서가 열릴 것 같으니 미리 열어둔다") 만약 예측이 틀리면 실행을 취소하지만, **미세한 흔적 (캐시)**은 남습니다.
• 계약서 (Always-Mispredict): "우리는 예측을 항상 틀리게 설정할 거야. 그래서 두 가지 경로 (올바른 경로와 잘못된 경로) 를 모두 실행해. 그러면 실제 하드웨어가 예측을 잘하든 못하든, 우리가 보여주는 정보는 항상 같아."
• 증명: 저자들은 이 "항상 틀리는 예측"이라는 계약서가 실제 CPU 의 복잡한 동작을 완벽하게 감싸고 있음을, 이 새로운 증명 도구로 컴퓨터가 직접 검증했습니다.

6. 요약: 왜 이것이 혁신적인가?

• 기존: "컴퓨터가 다 찾아봐" (자동화되지만 불완전) 또는 "수학자가 손으로 써" (정확하지만 검증 어려움).
• 이 논문: "수학자가 논리를 짜고, 컴퓨터가 그 논리를 검증하는" 완벽한 협력 시스템.
• 결과: 하드웨어 제조사와 소프트웨어 개발자가 서로의 약속을 100% 신뢰할 수 있는 기반을 마련했습니다.

한 줄 요약:

"이 논문은 복잡한 CPU 의 비밀 누출을 막기 위해, '가상의 계약서'가 '실제 기계'를 완벽하게 감싸고 있는지 증명하는 새로운 **'수학적 안경'**을 개발했습니다."

기술 요약

이 논문은 하드웨어 - 소프트웨어 계약 (Hardware-Software Contracts) 의 만족도 (Satisfaction) 를 증명하기 위한 **연역적 증명 시스템 (Deductive System)**을 제안하고, 이를 Rocq 증명 보조기 (Proof Assistant) 에서 형식화하여 검증한 연구입니다. 하드웨어 - 소프트웨어 계약은 CPU 의 누출 (Leakage) 행위를 추상화하여 사이드 채널 공격에 대한 소프트웨어의 보성을 검증할 수 있게 하지만, 실제 하드웨어가 이 계약을 만족하는지 (즉, 계약이 하드웨어의 누출을 상회하는지) 를 증명하는 것은 매우 어렵습니다.

주요 내용은 다음과 같습니다.

1. 문제 정의 (Problem)

• 배경: 클라우드 컴퓨팅 등 공유 하드웨어 환경에서 발생하는 사이드 채널 공격 (Meltdown, Spectre 등) 은 하드웨어의 미세 아키텍처 (캐시, 분기 예측기 등) 에 의존합니다. 이를 방어하기 위해 하드웨어 - 소프트웨어 계약이 도입되었는데, 이는 ISA(명령어 집합 구조) 수준에서 누출을 추상화한 명세입니다.
• 핵심 과제: 계약이 하드웨어의 누출을 올바르게 상회 (Over-approximation) 하는지 증명하는 것 (Contract Satisfaction).
  • 정의: "어떤 프로그램 $P$와 두 입력 $\sigma, \sigma'$에 대해, 계약이 동일한 누출을 예측한다면, 하드웨어 실행에서도 두 실행은 구별 불가능해야 한다."
• 기존 접근법의 한계:
  • 모델 체킹: 자동화되었지만, 불변식 (Invariant) 찾기에 의존하며 알고리즘 오류 가능성이 있음.
  • 펜 - 앤 - 페이퍼 증명: 엄밀하지만 복잡도가 높아 검증이 어려움 (예: 25 페이지 분량의 밀도 높은 증명).
  • 상호작용 증명 보조기 활용의 어려움: 두 개의 다른 의미론 (계약 vs 하드웨어) 에 의해 유도된 실행 트레이스 간의 4-항 (4-ary) 관계적 추론이 필요하며, 비동기적 실행 (계약 1 단계가 하드웨어 여러 단계에 대응되거나 그 반대) 으로 인해 동기화 (Lockstep) 가 어렵습니다.

2. 방법론 (Methodology)

저자들은 계약 만족도 증명을 **"상대적 트레이스 동등성 (Relative Trace Equality)"**의 한 사례로 재정의하고, 이를 해결하기 위한 새로운 증명 기법을 개발했습니다.

• 상대적 트레이스 동등성 (Relative Trace Equality): "트레이스 동등성이 트레이스 동등성을 함의한다"는 형태의 명제를 증명하는 문제 ($\text{Trace}_C(s_1) = \text{Trace}_C(s_2) \implies \text{Trace}_H(h_1) = \text{Trace}_H(h_2)$).
• 상대적 비시뮬레이션 (Relative Bisimulation):
  • 기존의 이항 (Binary) 비시뮬레이션을 4-항 (4-ary) 관계로 확장하여 정의했습니다.
  • 비동기적 처리: 계약 단계와 하드웨어 단계가 서로 다른 속도로 진행될 수 있으므로, 단순한 동시 진행 (Lockstep) 이 아닌 비동기적 (Non-lockstep) 추론을 지원합니다.
  • 고정점 (Fixpoint) 혼합: 계약 단계는 **귀납적 (Inductive)**으로, 하드웨어 단계는 **공귀납적 (Coinductive)**으로 처리하여, 계약의 가정 ($\text{Trace}_C$가 같음) 을 풀어가면서 하드웨어의 동등성을 증명하는 구조를 가집니다. 이는 무한 트레이스에서의 귀납적 증명 불가능 문제를 해결합니다.
• 연역적 증명 시스템 (Deductive System):
  • **파라미터화된 공귀납 (Parameterized Coinduction, Paco)**을 기반으로 합니다.
  • 증명 5-튜플 (Proof Quintuples): 증명 상태를 나타내는 표기법을 도입하여, 불변식 (Invariant) 을 증명 도중 점진적으로 구성할 수 있게 합니다.
  • 핵심 규칙:
    • C-Step: 계약 단계를 건너뛰며 (Contract step), 계약의 누출이 같다는 가정을 활용.
    • H-Step: 하드웨어 단계를 진행하며, 하드웨어 누출이 같음을 증명.
    • Invariant: 증명 과정에서 발견된 관계적 불변식을 가설에 추가하여 재사용.
    • Up-to Techniques: 대칭성 (Symmetry) 과 전이성 (Transitivity) 을 활용하여 증명을 단순화하는 기법들을 시스템에 통합.

3. 주요 기여 (Key Contributions)

1. 상대적 비시뮬레이션의 정의 및 증명: 계약 만족도 문제를 해결하기 위한 4-항 비시뮬레이션 관계를 정의하고, 이것이 상대적 트레이스 동등성과 동치임을 증명했습니다.
2. 형식적 연역 시스템 개발: Rocq 증명 보조기에서 구현된 증명을 위한 규칙 세트를 제시했습니다. 이 시스템은 **건전성 (Soundness)**과 **완전성 (Completeness)**을 갖습니다.
3. 점진적 증명 스타일: 기존 방법론처럼 증명 시작 시 복잡한 시뮬레이션 관계를 미리 제시할 필요가 없으며, 증명 과정에서 불변식을 점진적으로 구성하고 확장할 수 있습니다.
4. Up-to 기법 통합: 대칭성, 전이성, 누출 동등성 등을 활용하여 증명을 간소화하는 기법들을 시스템에 안전하게 통합했습니다.

4. 결과 (Results)

저자들은 제안된 시스템을 Rocq 에서 형식화하고 두 가지 복잡한 사례 연구에 적용하여 성공적으로 검증했습니다.

• 사례 1: 항상 오분기 예측 (Always-Mispredict) 계약:
  • 분기 예측 오작동 (Speculative Execution) 을 모델링하는 계약입니다. 하드웨어가 실제 분기를 예측하는지 여부와 관계없이, 계약은 항상 두 가지 분기 경로를 모두 실행한 후 올바른 경로로 복귀합니다.
  • 하드웨어가 분기를 올바르게 예측하든 잘못 예측하든, 계약이 하드웨어의 누출을 상회함을 증명했습니다. 특히 하드웨어가 분기를 올바르게 예측할 때 발생하는 비동기적 실행 차이를 처리하는 데 시스템이 효과적이었습니다.
• 사례 2: 순차적 (Sequential) 계약:
  • 현대 CPU 의 명령어 비순차적 실행 (Out-of-Order Execution) 을 추상화하여 순차적 실행으로 모델링하는 계약입니다.
  • 하드웨어의 버퍼링 및 명령어 재배열이 계약의 순차적 누출 모델과 일치함을 증명했습니다.

5. 의의 및 의의 (Significance)

• 형식적 검증의 새로운 패러다임: 하드웨어 - 소프트웨어 계약 만족도 증명을 모델 체킹이나 수작업 증명이 아닌, 상호작용 증명 보조기를 통한 자동화된 연역 증명으로 전환하는 토대를 마련했습니다.
• 비동기적 추론의 해결: 서로 다른 의미론을 가진 시스템 간의 비동기적 실행을 처리하는 데 있어, 귀납과 공귀납을 혼합한 4-항 비시뮬레이션 기법은 사이드 채널 보안뿐만 아니라 안전한 컴파일 (Secure Compilation) 등 다른 4-항 관계 증명 문제에도 적용 가능한 일반적인 해결책을 제시합니다.
• 실용성: 복잡한 하드웨어 동작 (예: 분기 예측, 비순차 실행) 을 추상화하는 계약의 정확성을 기계적으로 검증할 수 있게 함으로써, 더 안전한 하드웨어 설계와 소프트웨어 개발을 가능하게 합니다.
• 확장성: 이 시스템은 추후 비결정성 (Nondeterminism) 지원, 중첩된 예측 (Nested Speculation) 처리, 그리고 더 높은 수준의 프로그램 논리로의 확장 가능성을 열어두고 있습니다.

요약하자면, 이 논문은 하드웨어의 보안 속성을 검증하는 데 있어 상호작용 증명 보조기를 활용한 체계적이고 모듈화된 증명 프레임워크를 제시함으로써, 사이드 채널 공격 방어 기술의 신뢰성을 획기적으로 높이는 기여를 했습니다.