seL4 마이크로커널(microkernel)을 기반으로 리눅스(Linux) 가상 머신(VM)을 위한 새로운 타입 1 하이퍼바이저(Type-1 hypervisor)인 L4H가 공개되었습니다. L4H는 인텔(Intel) VT-x나 AMD-V 같은 하드웨어 가상화 기능을 사용하지 않고도 리눅스 커널을 seL4 유저모드 스레드(usermode threads)로 실행하며, 2020년 이후 인텔 및 AMD CPU에서 프로덕션(production) 준비가 완료되었다고 개발팀은 밝혔습니다. 베어메탈(bare metal) 환경은 물론 KVM 기반 VM 내부에서도 구동 가능합니다.
L4H는 단일 .efi 이미지로 배포되며, seL4 커널과 사전 빌드된 게스트 리눅스 커널, 그리고 여러 시스템 구성 요소 seL4 프로세스들을 포함합니다. 주요 구성 요소로는 VM 생명주기를 관리하는 vmmgr, VM별로 virtio 프로토콜을 구현하는 vmm, 호스트 TPM(신뢰 플랫폼 모듈)을 소유하고 VM 무결성을 증명하는 trustd, 디스크 및 네트워크 장치를 관리하는 blkd와 netd 등이 있습니다. 특히 trustd는 VM 시작 시 측정값을 기록하고, VM은 호스트 TPM에 뿌리를 둔 완전한 신뢰 체인(chain-of-trust)을 통해 원격 증명(remote attestation)을 요청할 수 있어 보안성이 매우 높습니다. 또한, blkd/netd는 IOMMU(입출력 메모리 관리 장치) 보호를 받아 장치 드라이버(device driver)가 침해되더라도 VM에 영향을 미치지 않습니다.
성능 면에서 L4H는 입출력(IO) 집약적인 워크로드(workload)에서 젠(Xen) PV와 동등한 수준이며, gVisor systrap 모드보다 2배에서 20배 빠르다고 합니다. 대부분의 워크로드에서는 베어메탈 대비 5~10%의 성능 손실을 예상할 수 있습니다. 이러한 특성 덕분에 L4H는 높은 보안성과 효율성이 요구되는 클라우드(cloud) 환경이나 엣지 컴퓨팅(edge computing) 장치에 특히 유용할 것으로 보입니다. 하드웨어 가상화에 의존하지 않으면서도 강력한 VM 격리(isolation)와 무결성 검증을 제공하여, 잠재적인 보안 위협으로부터 시스템을 보호하는 새로운 대안이 될 수 있습니다.