기술 요약: 인지 워크플로우 실행기를 위한 인증된 순수성

1. 문제: 인지 워크플로우의 순수성 격차

인지 워크플로우 시스템 (AI 추론, 도구 사용, 추론을 조정) 은 점점 더 고위험 분야에서 작동하고 있습니다. 이전 연구 (McCann [2026e]) 는 거버넌스 완전성, 출처 완전성, 그리고 통제되지 않은 효과의 불가능성을 보장하는 3 계층 거버넌스 아키텍처를 확립했습니다. 그러나 이러한 안전성 정리는 순수 모듈 제약이라는 중요한 전제에 의존했습니다. 이 제약은 실행기 모듈이 I/O 효과를 수행할 수 없으며 선언적 지시문만 반환할 수 있어야 함을 요구합니다.

이전 구현에서는 이 제약이 BEAM 가상 머신 (Erlang/OTP) 에서의 정적 모듈 임포트 그래프 분석을 통해 강제되었습니다. 관례 기반 거버넌스보다 강력하지만, 이 메커니즘은 적대적 우회에는 불충분합니다. BEAM 의 동적 기능은 정적 분석이 신뢰성 있게 방지할 수 없는 5 가지 유형의 우회를 허용합니다:

1. 동적 디스패치: :erlang.apply/3 를 사용하여 정적 임포트 없이 임의의 함수를 호출합니다.
2. 코드 평가: Code.eval_string/1 을 사용하여 런타임에 임의의 코드를 실행합니다.
3. 네이티브 구현 함수 (NIFs): 제한 없는 시스템 접근 권한을 가진 공유 라이브러리를 로드합니다.
4. 포트: :erlang.open_port/2 를 통해 외부 프로세스를 생성합니다.
5. 동적 모듈 로드: :code.load_binary/3 를 통해 런타임에 임의의 바이트코드를 로드합니다.

리치 정리 (Rice's Theorem) 에 따라, 모든 가능한 프로그램에 대해 "I/O 효과 없음"이라는 비자명한 의미론적 속성을 결정하는 정적 분석은 존재할 수 없습니다. 건전한 과대포함 (overapproximation) 은 대부분의 합법적인 관용적 Elixir 코드를 거부하게 됩니다. 이로 인해 순수성 격차가 발생합니다: 형식 모델은 순수성을 가정하지만, 강제 메커니즘 (정적 분석) 은 결연한 적대자에 대해 이를 구조적으로 보장할 수 없습니다.

2. 방법론: 탐지에서 구조적 예방으로

본 논문은 순수 모듈 제약을 분석에 의해 강제되는 관례에서 실행 환경에 의해 강제되는 구조적 능력 경계로 전환하는 인증된 순수성 아키텍처를 제안합니다. 이 방법론은 네 가지 핵심 메커니즘에 의존합니다:

A. 제한된 컴파일 대상 (WebAssembly)

실행기는 제한된 WebAssembly (WASM) 대상으로 컴파일됩니다. WASM 능력 모델을 활용하여 모든 5 가지 BEAM 우회 유형을 구조적으로 제거합니다:

• 동적 디스패치 부재: WASM 은 런타임 문자열/원자 이름으로 함수 호출을 해결하는 지시어가 없습니다. 호출은 함수 테이블의 정적 인덱스로 제한됩니다.
• 코드 평가 부재: WASM 은 사전 컴파일된 바이트코드를 실행하며, 런타임에 새 코드를 생성하거나 로드하는 메커니즘이 없습니다.
• NIF/포트 부재: WASM 모듈은 호스트 파일 시스템, 공유 라이브러리, 또는 프로세스 생성에 접근할 수 없는 샌드박스 VM 에서 실행됩니다.
• 동적 로드 부재: 모듈 인스턴스화는 호스트에 의해 완전히 제어되며, 모듈은 다른 모듈을 로드할 수 없습니다.

B. 호스트 함수 화이트리스트 ($W$)

WASM 모듈은 명시적으로 임포트 섹션에 선언된 함수만 호출할 수 있습니다. 이러한 임포트는 유한하고 열거된 **화이트리스트 ($W$)**로 제한됩니다:

• $W_{data}$: 순수 데이터 작업 (메모리 관리, 문자열 조작, 산술, JSON 직렬화, 컨텍스트 읽기).
• $W_{dir}$: 지시문 생성자 (효과를 나타내는 데이터 구조를 구축하는 함수, 예: directive_http_request이지만, 이를 실행하지는 않음).
• 제외: 효과 능력을 부여하는 WASI (WebAssembly System Interface) 임포트는 명시적으로 제외됩니다.

C. 순수성 증명서

순수성 증명서는 실행기 바이너리를 그 순수성 분류에 바인딩하는 암호학적 증명 아티팩트입니다.

• 구조: 실행기 바이너리의 SHA-256 해시, 순수성 증명 (임포트 목록 + 분류) 의 해시, 그리고 이러한 해시들에 대한 Ed25519 서명을 포함합니다.
• 무결성: SHA-256 의 충돌 저항성과 Ed25519 의 위조 불가능성으로 인해, 증명서는 수정된 아티팩트로 이전될 수 없습니다.

D. 런타임 검증 게이트

실행기가 거버넌스 파이프라인에 진입하기 전에 검증 게이트가 다음을 수행합니다:

1. 서명 검증: Ed25519 서명을 유효성 검사합니다.
2. 아티팩트 바인딩: 바이너리 해시가 증명서와 일치하는지 확인합니다.
3. 독립적 증명 유도: WASM 바이너리의 임포트 섹션을 새로이 파싱하여 현재 화이트리스트에 대해 주장된 순수성 증명과 일치하는지 검증합니다.
4. 분류 유효성 검사: 모든 임포트가 순수 것으로 분류되었는지 확인합니다.

이 게이트를 통과한 실행기만 인스턴스화됩니다. 이 게이트는 구조적 전제 조건으로 작용하여, 유효한 순수성 증명서가 없는 실행기는 실행될 수 없음을 보장합니다.

3. 주요 기여

1. 형식적 위협 모델: 5 가지 BEAM 우회 유형과 이 맥락에서 정적 분석의 이론적 한계 (리치 정리) 에 대한 엄밀한 특성화.
2. 구축에 의한 구조적 순수성: 실행기 코드 내용과 무관하게 제한된 WASM 대상으로 컴파일하는 것이 순수 모듈 제약을 충족함을 증명하는 정리 (Theorem 4.5).
3. 우회 제거: 제한된 WASM 환경에서 5 가지 BEAM 우회 유형 각각이 구조적으로 불가능함을 증명하는 형식적 증명 (Theorem 5.5).
4. 암호학적 인증: 소스 코드 접근 없이 실행기 순수성을 이식 가능하고 조직 간에 검증할 수 있게 하는 순수성 증명서 및 원격 인증 기록 체계.
5. 신뢰 컴퓨팅 베이스 (TCB) 정의: 보장 (WASM 런타임, 호스트 함수, 화이트리스트, 검증 게이트, 지시문 해석기) 에 필요한 5 가지 구성 요소에 대한 명시적 정의로, 무제한 실행기 코드에서 제한되고 감사 가능한 집합으로 신뢰 표면을 축소.
6. 단계적 신뢰 계층: 점진적 채택을 허용하는 3 계층 (검증된 순수성, 정적 분석, 실험적) 을 지원하는 구현 아키텍처.

4. 결과 및 평가

이 아키텍처는 Apple M 시리즈 프로세서에서 Wasmtime JIT 백엔드로 실행되는 4 개의 구현된 실행기 (Rust 기반, WASM 으로 컴파일됨) 에서 평가되었습니다.

• 검증 지연 시간: 검증 게이트는 프로덕션 실행기에 대해 39–42 µs(중앙값) 를 소요합니다. 해시 기반 캐싱을 사용하면 반복 호출에 대한 평균 비용은 0 에 수렴합니다.
• 런타임 오버헤드: 전체 계획 주기 (인스턴스화, 실행, 역직렬화) 는 256–398 µs 내에 완료됩니다. 이는 100ms HTTP 요청에서 0.4% 미만의 오버헤드이며, 일반적인 800ms LLM 호출에서는 0.05% 미만입니다.
• 결정론성: 동일한 입력으로 40 회 반복 호출 시 분기 (divergence) 가 전혀 관찰되지 않아 WASM 실행 환경의 결정론적 특성이 확인되었습니다.
• 증명서 크기: 증명서는 작아 (~1.3 KB) 대역폭 예산 내에서 충분히 작동합니다.
• 정확성: 모든 실행기는 예상되는 지시문 형태를 생성했으며, 시스템은 실행 간에 바이트 단위로 동일한 출력을 유지했습니다.

5. 중요성 및 주장

본 논문은 거버넌스 보장의 인식론적 지위에서 근본적인 전환을 주장합니다:

• 탐지에서 예방으로: 이전 접근법은 정적 분석을 통해 알려진 우회 패턴을 탐지하는 데 의존했습니다. 이 아키텍처는 효과 생성 능력을 구조적으로 부재하게 만들어 우회를 예방합니다.
• 기존 정리 강화: McCann [2026e] 의 안전성 정리 (거버넌스 완전성, 출처 완전성, 통제되지 않은 효과 없음) 는 형식적으로 동일하게 유지됩니다. 그러나 그 기초 전제는 가정되는 것이 아니라 기계적으로 소멸됩니다. 이제 보장은 정적 분석기의 한계가 아닌 WASM 능력 모델과 암호학적 원시 (SHA-256, Ed25519) 의 수학적 특성에 기반합니다.
• 이식 가능한 신뢰: 로컬 순수성 증명을 이식 가능한 인증 기록으로 전환함으로써, 이 아키텍처는 조직 간 거버넌스 구성을 가능하게 하여, 조직 A 가 소스 코드 검토 없이도 조직 B 의 실행기 순수성을 암호학적으로 검증할 수 있게 합니다.

본 논문은 이것이 Rocq 또는 Lean 의 의미에서의 자동화 증명 (이는 동반 논문에서 기본 거버넌스 논리에 reserved 됨) 이 아니라, 런타임에 검증되는 구조적 보장임을 명시적으로 지적합니다. 이 기여는 "모든 실행기 코드"에서 작고 명시적으로 정의된 신뢰 컴퓨팅 베이스로 신뢰 표면을 축소하는 것입니다.