Nitro Isolation Engine 뒤에 있는 증명 보조기 Isabelle/HOL

AWS는 re:Invent 2025에서 **Nitro Isolation Engine(NIE)**를 공개했고, 이 모듈의 보안과 정당성을 Isabelle/HOL로 형식 검증했다고 밝혔다. NIE는 세계 최초의 형식 검증 클라우드 하이퍼바이저로 소개되며, 클라우드 보안의 기준을 새로 세웠다.

Isabelle/HOL이 선택된 이유는 표현력, 자동화, 증명 가독성, 확장성의 균형이 뛰어나기 때문이다. 저자는 수학적 논리의 수준을 Boolean logic에서 first-order logic, higher-order logic, 그리고 dependent-type theories까지 차례로 설명하며, 표현력이 커질수록 자동 증명은 어려워지지만 증명 보조기가 그 간극을 메운다고 정리한다.

NIE 검증에서는 약 25만 줄에 이르는 형식 증명이 사용됐고, 그 안에는 Graviton-5 아키텍처 명세, 하이퍼콜을 구현한 Rust 코드의 기능적 정당성, 그리고 보안 속성 증명이 포함됐다. 이 작업을 위해 Isabelle/HOL 위에 separation logic을 구현했고, 내장 자동화와 자체 증명 자동화를 함께 활용했다. 그 결과 이 거대한 증명은 일반 노트북에서 약 30분 만에 실행될 정도로 견고하고 효율적으로 동작했다.

Isabelle/HOL의 강점으로는 다음이 꼽힌다.

• 사용자 설정 파서: Rust의 상당 부분을 명세에 임베드 가능
• type classes: 숫자형뿐 아니라 머신 워드 등에도 자연스러운 오버로딩 제공
• locales: 명세 계층을 유연하게 구성하는 경량 모듈 시스템
• built-in automation: simplification, backchaining proof search
• Sledgehammer: 외부 자동 증명 도구와의 원클릭 연동
• counterexample-finding tools: 잘못된 명제를 빠르게 발견
• code generation: 실행 가능한 고차 논리 명세에서 코드 생성 및 테스트 활용

대표적 선행 사례로는 seL4 마이크로커널 검증이 언급된다. 또 WebAssembly 의미론 형식화, Cogent 검증 프레임워크, 분산 편집에 쓰이는 CRDT 알고리즘 검증, 암호 프로토콜 검증, 수학 정리 형식화 등에서도 Isabelle이 사용됐다. Isabelle은 무료 오픈소스이며 주요 운영체제에서 실행된다.