보안 암호화 가상화 (Secure Encrypted Virtualization)의 형식 검증 (Formal Verification)

신뢰 실행 환경 (Trusted execution environments, TEEs)은 사용 중인 데이터와 코드에 대해 보안 환경을 제공하며, 기밀성 (confidentiality)과 무결성 (integrity) 측면에서 보호되도록 보장합니다. 가상 머신 (Virtual machine, VM) 기반 TEE는 가상화 기술을 활용하여 전체 운영 체제 또는 특정 애플리케이션을 지원할 수 있는 격리된 실행 공간을 생성합니다. AMD SEV (AMD secure encrypted virtualization)는 클라우드 기밀 컴퓨팅 (confidential computing)에서 사용되는 핵심 기술로, VM 내의 민감한 데이터를 보호하기 위해 하드웨어 기반 메모리 암호화 (memory encryption)를 가능하게 합니다. 그러나 AMD SEV는 보안 보장에 대한 형식적 확신 (formal assurances) 없이 작동하는 경우가 많습니다. 본 연구는 AMD SEV 기밀 VM (confidential VMs)을 표현하고 검증하기 위한 형식적 프레임워크 (formal framework)를 소개합니다. 구체적으로, 우리는 AMD SEV 사양 (specification)에 대해 설계 수준 (design-level) 및 속성 수준 (property-level) 추상화 (abstraction)를 수행하고, 기밀성 (confidentiality), 무결성 (integrity) 및 가용성 (availability)을 보장하기 위해 모델에 대한 속성 검사 (property checking)를 수행합니다. 이 접근 방식은 실행 환경을 보호하기 위한 핵심 보안 속성 (security attributes)을 정의하고 검증하는 엄격한 토대를 제공합니다.