AWS, 이제 VM 격리를 수학적으로 증명
출처: The New Stack
수요일에 AWS는 Graviton5 프로세서가 일반 제공(General Availability) 상태가 되었으며 두 개의 새로운 Amazon EC2 인스턴스를 구동한다는 소식을 발표했습니다. M9g는 일반 목적 워크로드용이고, M9gd는 고속 로컬 스토리지가 필요한 워크로드용입니다. 이는 AWS가 re:Invent 2025에서 칩을 미리 공개한 이후 처음 선보이는 Graviton5 인스턴스입니다.
새로운 칩은 코어 수를 96개에서 192개로 두 배로 늘렸으며, AWS는 이번 인스턴스가 이전 세대 대비 최대 25% 더 나은 컴퓨팅 성능을 제공한다고 밝혔습니다.
AWS는 새로운 인스턴스가 이전 세대 대비 최대 25% 더 나은 컴퓨팅 성능을 제공한다고 밝혔습니다.
하지만 더 흥미로운 점은, 이번 인스턴스가 여섯 번째 세대 Nitro 시스템 위에서 동작한다는 것입니다. 이 시스템에는 새로운 Nitro Isolation Engine(NIE) 이 포함되어 있는데, AWS는 이를 “가상 머신을 서로 격리하는 일만을 담당하는 분리 커널(separation kernel)”이라고 설명합니다.
격리만을 담당하는 커널
분리 커널(separation kernel)이라는 개념은 오래전부터 존재했습니다. John Rushby가 1981년에 이 용어를 만들었습니다. 그의 핵심 아이디어는 당시 표준 OS 커널조차도 형식 검증(Formal verification)을 수행하기엔 너무 커졌다는 것이었습니다. 반면, 규모가 작고 특화된 분리 커널은 복잡도가 제한적이기 때문에 형식 검증이 가능하다는 것이었습니다.
AWS는 2017년에 Nitro 시스템 및 하이퍼바이저를 출시했으며, 그때부터 EC2에서 격리를 구현해 왔습니다. 하지만 Nitro는 비즈니스 로직을 많이 담당하고 디바이스 드라이버와 기타 AWS 전용 기능을 관리하기 때문에 처음부터 형식 검증을 염두에 두고 설계된 것은 아니었습니다.
새 시스템에서는 Nitro 하이퍼바이저가 여전히 정책(VM 생성, 자원 할당, 마이그레이션, 스케줄링 등)을 담당하지만, 이제는 어느 정도 권한이 축소되어 게스트 상태에 접근하는 모든 작업을 Nitro Isolation Engine(NIE) 에 요청해야 합니다. Isolation Engine은 모든 요청을 검사한 뒤에야 동작합니다.
“하이퍼바이저의 보안 핵심 격리 로직을 최소 컴포넌트인 NIE로 추출함으로써, 이를 충분히 작게 만들어 검증과 감사를 가능하게 했습니다. 이를 통해 고객은 격리가 어떻게 구현되는지 전례 없는 투명성을 얻을 수 있습니다.” — AWS의 Dominic Mulligan과 Nathan Chong이 설명합니다. “또한 우리는 NIE를 Rust로 작성했으며, Rust는 형식 검증에 보다 자연스럽게 어울리는 언어입니다.”
우리가 여기까지 온 배경
이 분야의 초기 작업 중 하나는 컬럼비아 대학의 SeKVM 프로젝트이며, 2021년에 최초로 형식 검증된 상용급 하이퍼바이저를 선보였습니다. 다만 이 프로젝트는 주로 연구용으로 진행됐으며 실제 상용 클라우드에서는 사용되지 않은 것으로 보입니다.
AWS는 OS 검증이 가능하다는 것을 입증한 seL4 프로젝트에 큰 영감을 받았다고 밝히고 있습니다.
커널이 올바르게 동작함을 증명하기 위해 AWS는 Isabelle/HOL 증명 도우미를 사용했습니다. AWS에 따르면 모델과 증명은 “330,000줄에 달하는 기계 검증 수학”으로 구성되어 있으며, 이는 seL4 프로젝트와 비슷한 규모라고 합니다. “하지만 seL4와 달리, NIE는 상용 클라우드 환경을 위해 설계되었으며 Graviton5 사용자를 위한 항상 켜져 있는 기능으로 생산 하드웨어에 탑재됩니다.”라고 AWS는 발표문에 적었습니다.
192코어: 대대적인 재설계
칩 자체도 크게 재설계되었습니다. Graviton5는 TSMC 4nm 공정에서 3nm 공정으로 이동했으며, Graviton4가 96개의 코어를 하나의 칩렛에 모두 배치하고 PCIe와 DDR 컨트롤러를 별도 칩렛에 두었던 것과 달리, Graviton5는 192개의 코어를 네 개의 칩렛에 나누어 배치하고 각각에 컨트롤러를 탑재했습니다. 이렇게 하면 메모리 컨트롤러가 코어에 더 가깝게 위치하게 됩니다.
AWS는 더 빠른 메모리 칩과 결합된 이번 설계 덕분에 웹 애플리케이션이 최대 35% 더 빠르게, 머신러닝 추론도 최대 35% 더 빠르게 실행될 수 있다고 주장합니다.
Graviton과 에이전트 AI
AWS는 Graviton5를 에이전트 AI 전용으로 설계했다고 내세우고 있습니다. 구글이 ARM 프로세서를 홍보할 때와 크게 다르지 않은 접근 방식이지만, 효과가 있는 듯합니다. Meta는 4월에 수십억 달러 규모의 계약을 체결해 에이전트 AI 작업을 위해 수천만 개의 Graviton 코어를 배치했으며, Snowflake는 5월에 5년간 60억 달러를 투자해 기업용 에이전트 AI 도입을 가속화하겠다고 발표했습니다. AWS는 Uber도 에이전트 워크로드에 Graviton을 활용하고 있다고 전했습니다.
전체적으로 AWS에 따르면