EC2의 정식 검증된 '격리 엔진', 가상 머신 격리에 대한 수학적 보장 제공

AWS는 Graviton5 기반의 새로운 M9g 및 M9gd 인스턴스를 출시하며, 가상 머신(VM) 간 격리를 보장하는 Nitro Isolation Engine을 함께 선보였다. 이 엔진은 Nitro Hypervisor의 핵심 구성 요소로, 상용 클라우드 환경에 배포된 최초의 **정식 검증(Formally Verified)**된 하이퍼바이저이다.

이번 검증은 Isabelle/HOL 증명 보조 도구를 사용하여 수행되었으며, 약 330,000라인의 기계 검증된 수학적 증명을 포함한다. 이는 운영체제 검증의 이정표인 seL4 프로젝트와 유사한 규모다. AWS는 격리 로직을 최소화한 '분리 커널(Separation Kernel)' 개념을 적용하여, 복잡한 Nitro Hypervisor에서 핵심 격리 로직만을 추출해 검증 가능성을 높였다.

검증 과정의 주요 특징은 다음과 같다:

• Rust 언어를 사용하여 구현함으로써 정식 검증에 최적화된 구조를 갖춤
• μRust(Rust의 핵심 부분집합)에 대한 정식화 수행
• Separation Logic 및 AutoCorrode 라이브러리 활용
• 기밀성 및 무결성, 기능적 정확성, 런타임 오류 부재, 메모리 안전성 등 4가지 핵심 속성 검증

Nitro Isolation Engine은 Graviton5 사용자에게 항상 켜져 있는(always-on) 기능으로 제공되며, 고객에게 격리 메커니즘에 대한 전례 없는 투명성을 제공한다.