XMHF: 확장 가능 및 모듈식 하이퍼바이저 프레임워크
Source
Evernote/Papers/Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework.md
Summary
구글 연구진이 설계한 XMHF(eXtensible and Modular Hypervisor Framework)는 모듈식 확장성, 자동화된 검증, 고성능을 목표로 하는 하이퍼바이저 프레임워크입니다. XMHF는 메모리 무결성(하위 권한 레벨의 소프트웨어에 의한 하이퍼바이저 메모리 수정 방지)을 보장하는 코어와 이를 확장하는 모듈로 구성됩니다. 코어(6018 줄)의 메모리 무결성은 CBMC 모델 체커를 통해 C 코드 5208 줄을 자동 검증하고, 나머지 C 코드(422 줄)와 어셈블리 코드(388 줄)는 수동 감사로 검증했습니다. 실험 결과, 단일 게스트 지원 환경에서 XMHF의 성능은 일반적인 고성능 하이퍼바이저와 유사한 것으로 나타났습니다.
Key Points
- XMHF는 모듈식 확장성, 자동 검증, 고성능을 핵심 목표로 함
- 하이퍼바이저 메모리 무결성 보장을 위한 코어와 확장 모듈 아키텍처
- CBMC 모델 체커를 활용한 C 코드 자동 검증(5208 줄, 약 80 초 소요)
- 변경 가능성이 낮은 코어 코드(C 422 줄, 어셈블리 388 줄)에 대한 수동 감사
- 단일 게스트 환경에서 기존 고성능 하이퍼바이저와 유사한 성능 달성