기술 요약: 클레이니의 제2 재귀 정리(Kleene's Second Recursion Theorem)를 이용한 상호 검증 부트스트래핑

1. 문제 정의

본 논문은 상호 검증(mutual attestation)에서의 **참조 값 부트스트래핑 문제(reference-value bootstrapping problem)**를 다룬다. 노드들이 서로의 무결성을 상호 검증해야 하는(검증자이자 검증 대상인 Attester 및 Verifier 역할을 동시에 수행하는) 분산형 또는 P2P 시스템에서는, 모든 노드가 피어(peer)의 참조 값(기대되는 코드 측정값)을 보유해야 한다.

단순한 해결책인 피어의 참조 값(피어 코드의 해시값)을 노드의 코드 내에 하드코딩하는 방식은 **무한 회귀(infinite regress)**로 인해 실패한다. 만약 노드 A가 노드 B의 참조 값을 내장하고, 노드 B가 노드 A의 참조 값을 내장한다면, 의존 관계가 순환하며 종료되지 않는 체인을 형성하게 된다. 기존의 해결책들은 대개 다음과 같은 방식을 사용한다:

1. 신뢰할 수 있는 제3자(TTP)에 의존하여 참조 값을 배포함.
2. 아키텍처 특화 자격 증명이나 외부 권한 목록을 사용함.
3. 구성을 측정 범위 외부에 배치함.
4. 특정 하드웨어 아키텍처 고유의 측정 메커니즘을 활용함.

저자는 TTP 없이, 외부에서 공급된 참조 값 없이, 또한 아키텍처에 독립적인 방식으로, 오직 기존의 소프트웨어 스택과 검증 메커니즘만을 사용하여 이 문제를 해결하고자 한다.

2. 방법론

저자는 부트스트래핑 문제를 상호 고정점 방정식(mutual fixed-point equations) 체계로 재정의하고, 이를 **클레이니의 제2 재귀 정리(Kleene's Second Recursion Theorem)**를 사용하여 해결한다.

이론적 기초

• 모델: $k$개의 노드로 구성된 그룹을 모델링하며, 각 노드 $i$는 모든 노드(자기 자신을 포함한 전체 노드 집합 $\vec{e} = (e_1, \dots, e_k)$)의 소스 코드에 의존하는 부분 함수 $f_i$를 계산한다.
• 방정식: 목표는 모든 $i$에 대하여, $e_i$에 의해 계산된 함수가 $f_i(\vec{e}, -)$와 동일한 $\vec{e}$ (소스 코드 튜플)를 찾는 것이다.
• 클레이니의 제2 재귀 정리: 본 논문은 이 정리의 동시 형태(Corollary 2.3)를 활용한다. 이 정리는 임의의 계산 가능한 동작 세트 $f_1, \dots, f_k$에 대하여, 상호 의존성을 만족하는 계산 가능한 인덱스(소스 코드) 튜플 $\vec{e}$가 존재함을 보장한다.
• 구성적 접근법(Constructive Approach): 이 정리는 피어의 소스가 자유 변수(free variables)로 취급되는 템플릿으로부터, 이러한 상호 참조 프로그램을 자동으로 생성할 수 있는 **트랜스파일러(transpiler)**의 존재를 시사한다.

구현 전략

본 논문은 타겟 아키텍처가 측정을 수행하는 방식에 따라 두 가지 별도의 구현 방안을 제안한다.

A. 직접 코드 측정 (예: Linux IMA, TPM)

• 메커니즘: 아키텍처가 배포된 원시 코드(예: 파일을 해싱함)를 측정한다.
• 해결책: PyReflect, 파이썬 트랜스파일러.
  • 노드들이 서로의 소스 코드를 참조하는 템플릿을 입력으로 받는다.
  • 전체 소스 코드 제품군을 하나의 공유 데이터 블롭(blob)으로 직렬화하여 모든 노드에 내장한다.
  • 런타임 시, 각 노드는 이 블롭으로부터 피어의 정확한 바이트 단위 소스 코드를 재구성하고 이를 직접 해싱한다.
  • 이를 통해 빌드 단계를 생략할 수 있으며, "측정"은 단순히 재구성된 소스의 해시값이 된다.

B. 빌드 아티팩트 측정 (예: AWS Nitro Enclaves, SGX, Confidential VMs)

• 메커니즘: 아키텍처가 원시 소스가 아닌 빌드 아티팩트(예: 엔클레이브 이미지 파일 또는 컨테이너 이미지)를 측정한다. 이때 측정값은 $\mu(\beta(e))$이며, 여기서 $\beta$는 빌드 절차를 의미한다.
• 과제: 재구성된 소스가 올바른 측정값을 생성하려면 빌드 절차 $\beta$가 결정론적(reproducible)이어야 한다.
• 해결책: NixReflect, Nix 트랜스파일러.
  • 재현 가능한 빌드를 보장하기 위해 Nix 패키지 매니저를 사용한다.
  • 노드는 내장된 데이터를 통해 피어의 Nix 표현식(빌드 정의)을 재구성한다.
  • 그 후, 노드는 자신의 환경 내부에서 피어의 아티팩트(예: Nitro Enclave 이미지 파일)를 재현 가능하게 다시 빌드한다.
  • 재구축된 아티팩트로부터 참조 측정값(예: PCR)을 도출한다.

3. 주요 기여

1. 이론적 재정의: 문제를 상호 고정점 방정식 체계로 표현하고 클레이니의 제2 재귀 정리를 사용하여 해결함으로써, TTP 없이도 자기 완결적인 참조 값을 구축할 수 있음을 증명하였다.
2. PyReflect (직접 측정): 피어의 소스를 재구성하고 이를 직접 해싱할 수 있는 상호 참조 노드를 생성하는 파이썬 트랜스파일러이다. 개념 증명(PoC)을 통해 소프트웨어 TPM(swtpm)을 사용하여 상호 검증을 수행하는 것을 보여주었다.
3. NixReflect (아티팩트 측정): 피어의 아티팩트를 재현 가능하게 재빌드할 수 있는 노드를 생성하는 Nix 트랜스파일러이다. PoC를 통해 두 개의 AWS Nitro Enclave가 내장된 데이터만으로 서로의 엔클레이브 이미지를 재현하고 참조 PCR을 도출하는 것을 입증하였다.
4. 아키텍처 독립성: 본 솔루션은 대상 하드웨어의 SDK, 서명 도구, 로더 또는 검증 스택의 수정 없이도 작동하며, 외부의 '참조 값 제공자' 역할을 로컬의 자기 완결적 도출로 대체한다.

4. 결과 및 성능

• 실현 가능성: 두 PoC 모두 외부 개입 없이 내장된 데이터만으로 피어의 참조 값을 도출할 수 있음을 성공적으로 입증하여 무한 회귀 문제를 해결하였다.
• 오버헤드 분석 (Nitro Enclaves):
  • 논문은 두 가지 변형을 비교한다: 재구성된 소스만 해싱하는 방식(digest)과 아티팩트를 재현 가능하게 다시 빌드하는 방식(rebuild)이다.
  • Digest 변형: 도출 시간은 미미하다 (~0.07초).
  • Rebuild 변형: 도출 시간이 약 100배 느리다 (~6.8초). 이는 아티팩트를 재생성하기 위해 전체 빌드 클로저(closure)를 탐색해야 하기 때문이다.
  • 저자는 복잡한 애플리케이션의 경우 이 재빌드 비용이 더 증가할 것이라고 언급하며, 아티팩트 측정 아키텍처의 경우 런타임 지연을 줄이기 위해 빌드 단계를 배포 전 단계로 오프로딩(attestable builds 사용)하는 것이 필요할 수 있음을 시사한다.
• 코드 크기: 트랜스파일링은 전체 소스 제품군 크기에 비례하여 선형적인 코드 크기 오버헤드를 발생시키지만, 그 증가는 완만하다 (예: 0.9 KB 템플릿이 3.4 KB의 노드로 생성됨).

5. 의의 및 주장

본 논문은 다음과 같은 특성을 가진 최초의 솔루션을 제공한다고 주장한다:

• 아키텍처 독립적: 커스텀 하드웨어 기능 없이도 다양한 TEE 및 측정 유형에서 작동한다.
• TTP-free: 신뢰할 수 있는 제3자나 외부 참조 값 제공자를 필요로 하지 않는다.
• 비침습적: 하드웨어 벤더의 검증 스택이나 SDK를 변경할 필요가 없다.

한계 및 범위:

• 저자는 자신의 기여가 자기 완결적 재구성의 실현 가능성에 국한됨을 명시한다. 본 논문은 하드웨어의 근본적인 보안 보장을 강화한다는 주장을 하지 않는다. 신뢰 모델은 표준적인 단방향 검증(하드웨어 루트 오브 트러스트 및 엔도스먼트 PKI에 의존)과 동일하다.
• 본 솔루션은 표준 위협 모델 외부의 공격(예: 하드웨어 침해)을 방지하지 못한다.
• 운영상의 제약:
  • 완전한 상호 참조 제품군을 업데이트하려면 모든 노드를 재배포해야 한다. 공유 데이터 블롭에 전체 제품군의 소스가 포함되어 있기 때문이다.
  • 아티팩트 측정 시스템의 경우, 재현 가능한 재빌드의 런타임 비용이 상당하다. 다만, 저자는 "검증 가능한 빌드(attestable builds)"를 통해 빌드 단계를 TEE 기반 샌드박스로 오프로딩함으로써, 런타임 비용을 빌드 시점의 TEE에 대한 신뢰와 교환하는 완화 방안을 제시한다.

결론적으로, 본 논문은 재귀 이론을 이용한 소프트웨어 구성을 통해 상호 검증 부트스트래핑이 가능하다는 것을 입증함으로써, 기존에 신뢰할 수 있는 제3자나 아키텍처 특화적인 편법을 필요로 했던 순환 의존성을 제거하였다.