EC2의 형식 검증된 ‘격리 엔진’, 가상 머신 격리를 수학적으로 보장
출처: 아마존 사이언스
오늘 우리는 Amazon Web Services(AWS)의 Elastic Compute Cloud(EC2)에서 새로운 M9g 및 M9gd 인스턴스의 일반 제공을 발표했습니다. 이는 최신 세대 범용 CPU인 Graviton5로 구동되는 최초의 인스턴스 유형이며, 이전 세대보다 코어 수가 96개에서 192개로 두 배가 되었습니다.
또한 이 인스턴스들은 새로운 Nitro Isolation Engine을 사용하는 최초의 인스턴스 유형이기도 합니다. Nitro Isolation Engine은 Nitro Hypervisor의 구성 요소로, 가상 머신(VM) 간 격리를 전담합니다. 이 글에서는 Isabelle/HOL(고차 논리) 증명 보조기 — 논리 법칙에 따라 추론 단계를 기계적으로 검증하는 소프트웨어 — 를 사용해 Nitro Isolation Engine이 올바르게 동작하고 가상 머신 간 격리를 보장한다는 것을 어떻게 증명했는지 설명합니다. Nitro Isolation Engine은 상업용 클라우드 환경에 배포된 최초의 형식 검증 하이퍼바이저의 핵심 구성 요소입니다.
우리의 Isabelle/HOL 모델과 증명은 330,000줄에 달하는 기계 검증 수학으로 구성되어 있습니다. 이는 현실적인 운영 체제 검증이 가능함을 최초로 입증한 획기적인 프로젝트인 seL4와 규모가 비슷합니다. 그러나 seL4와 달리 Nitro Isolation Engine은 상업용 클라우드 환경을 위해 설계되었으며, Graviton5 사용자를 위한 항상 켜져 있는 기능으로 실제 하드웨어에 탑재됩니다.
우리의 발표는 Amazon 2025 re:Invent 컨퍼런스에서 형식 검증 방법론을 소개합니다. 이 블로그 포스트는 우리의 형식 검증 작업 주요 측면과 그들이 어떻게 서로 맞물리는지를 비공식적으로 개요합니다.
분리 커널이란?
John Rushby는 1981년에 “분리 커널(separation kernel)”이라는 용어를 만들어 시스템을 격리된 구획으로 나누는 최소한의 OS 구성 요소를 설명했습니다. 핵심 아이디어는 정책을 구현 메커니즘과 분리하는 것입니다. 분리 커널은 무엇을 격리할지, 자원을 어떻게 할당할지, 어떤 VM을 스케줄링할지 등을 결정하지 않으며, 이러한 결정은 다른 곳에서 이루어집니다. 대신 격리 enforcement에만 집중하므로, 목적이 명확해 전체 OS 커널보다 구현이 훨씬 단순합니다.
2017년 도입된 이후 Nitro Hypervisor는 EC2에서 격리를 담당해 왔지만, 동시에 비즈니스 로직, 디바이스 드라이버, AWS 전용 기능도 처리했습니다. 이러한 복잡성은 정확성을 증명하기 어렵게 만들었습니다. 게다가 Nitro Hypervisor는 처음부터 검증을 염두에 두고 설계되지 않았습니다.
핵심 격리 로직을 최소 구성 요소인 Nitro Isolation Engine으로 추출함으로써, 검증 및 감사를 수행할 수 있을 만큼 충분히 작게 만들었으며, 고객에게 격리가 어떻게 적용되는지 전례 없는 가시성을 제공합니다. 또한 우리는 Nitro Isolation Engine을 Rust로 작성했으며, Rust는 형식 검증에 보다 자연스럽게 어울리는 언어입니다.
Nitro Hypervisor는 여전히 정책—VM 생성, 자원 할당, 마이그레이션, 스케줄링—을 담당하지만, 이제 권한이 제한되어 게스트 상태에 영향을 주는 모든 작업을 Nitro Isolation Engine에 요청해야 합니다. Nitro Isolation Engine은 모든 요청을 검증한 뒤에야 동작합니다.
System architecture of a Nitro-Isolation-Engine-enabled server.
사양 및 증명
우리 작업의 두 핵심 부분은 사양(specifications)과 증명(proofs)입니다. 형식 사양은 시스템이 기대되는 동작을 정확히 포착하고, 증명은 구현이 그 사양을 만족함을 입증합니다.
Nitro Isolation Engine에 대한 우리의 정리는 네 가지 유형의 속성을 다룹니다:
- 기밀성 및 무결성. 허가된 정보 흐름만 발생합니다. 예를 들어, 게스트 메모리 할당은 재사용 전에 항상 스크럽됩니다.
- 기능적 정확성. 구현이 사양대로 정확히 동작합니다.
- 런타임 오류 부재. Rust에서
None옵션 값을 언랩하는 등 프로그램 실행을 중단시키는 오류가 없습니다. - 메모리 안전성. 버퍼 오버플로우나 NULL 포인터 역참조와 같은 문제가 없습니다.
실제로 우리는 첫 세 속성을 하나의 기능 검증 결과로 다루고, 기밀성·무결성은 별도로 다룹니다. 이는 각각 다른 증명 기법을 사용하기 때문입니다.
기능 검증
기능 검증을 위해 핵심적인 세 부분이 있습니다:
- Rust 언어의 핵심 부분을 형식화한 μRust(“마이크로 Rust”);
- 사양을 정확히 포착하기 위한 Separation Logic 기반의 표현력 있는 사양 언어;
- Weakest-precondition calculus와 맞춤형 증명 자동화 도구를 이용한, 프로그램이 사양에 대해 올바른지를 증명하는 검증 기법.
이 모든 요소는 2025년에 오픈소스로 공개한 **AutoCorrode 라이브러리**의 일반 목적 증명 인프라의 일부입니다.
구체적으로 μRust는 Nitro Isolation Engine을 구현하기에 충분히 표현력이 있으면서도, 트레이트와 동적 디스패치 같은 고급 Rust 기능을 의도적으로 배제해 형식적 추론이 가능하도록 만든 제한된 서브셋입니다. μRust의 형식 의미론은 Isabelle/HOL 안에서 shallow embedding(얕은 삽입) 방식으로 정의되며, 이는 μRust의 의미가 Isabelle/HOL의 고차 논리, 즉 “호스트 언어”에 의해 정의된다는 뜻입니다.
μRust 프로그램에 대한 사양은 **전제(precondition)**와 **후조건(postcondition)**을 포함하는 계약(contract) 형태로 정의됩니다. 계약은 “전체 정확성(total correctness)”을 명시하는데, 이는 전제가 만족되는 모든 상태에서 프로그램이 반드시 종료하고, 종료 후 상태가 후조건을 만족함을 의미합니다. 전체 정확성은 메모리 안전성과 런타임 오류 부재를 동시에 보장합니다. 우리의 사양은 저수준 포인터 조작 프로그램을 다루기 위해 설계된 Separation Logic를 사용해 작성되었습니다.
분리 커널 자체는 비교적 단순하지만, Nitro Isolation Engine을 검증하는 과정은 여전히 형식 검증이 가능한 한계의 최전선에서 진행되고 있으며, 사양과 증명 모두 매우 방대합니다. 예를 들어, 실행 중인 게스트 가상 CPU가 자신을 켜려는(잘못된 요청) 상황을 다루는 사양은 다음과 같습니다:
Specification of PSCI_CPU_ON, a power state function for turning on a target CPU.
위 사양은 복잡해 보이지만 직관적으로는 간단합니다. 이 경우 Nitro Isolation Engine은 호출자가 이미 켜져 있어야 한다는 점을 확인하고, 정의된 오류 코드 AlreadyOn을 반환합니다. 시스템 상태의 다른 부분은 변하지 않습니다. 사양의 복잡성은 우리의 모델링 깊이와, 여러 다른 오류 검사가 이미 수행된 뒤에야 이 지점에 도달한다는 사실을 반영합니다.
μRust 프로그램이 사양에 대해 올바른지를 증명하기 위해 우리는 표준 weakest-precondition calculus를 사용합니다. weakest-precondition calculus는 특정 연산 후 프로그램 상태가 지정된 범위를 벗어나지 않도록 보장하는 최소한의 제약을 체계적으로 도출하는 방법입니다. 예를 들어, 표현식 “x + y”의