본 연구는 가상화 시스템을 설계, 구현, 검증하는 것을 목표로 한다. 따라서 본 과제는 설계와 구현을 위한 연구(PI)와 구현된 가상화 시스템을 검증하는 연구(Co-PI)의 협력 통해서 이루어집니다. 본 과제는 Rust 언어를 이용하여 가상화 환경을 구축합니다. 기존 가상화 시스템은 가상화 hardware 지원을 통하여 isolation과 protection을 이루기 때문에 이로 인한 성능 오버해드가 발생하는데, 본 과제에서는 Rust를 활용하여 하드웨어로 인한 오버해드 없이 가상화 환경을 구축합니다. 또한 Rust언어로 시스템을 구축할때 Rust의 unsafe 기능을 사용할 수 밖에 없는 상황이 발생하는데, unsafe의 사용을 최소화하고 unsafe의 안전성을 자동으로 검증하여 버그가 없는 가상화 시스템을 구현하는 것을 최종 목표로 합니다.

본 과제는 크게 두가지 목표를 갖습니다. 첫째는 Rust를 이용한 고성능 가상화 시스템 구축이고 둘째는 시스템을 구축하는데 사용할 수 밖에 없는 unsafe code에 대한 안전성 검증하는 것입니다. 고성능 가상화 시스템을 구축하기 위한 핵심 기술은 별도의 하드웨어 지원이 없이 기존의 하드웨어와 동일한 isolation과 protection을 Rust언어의 safety 특성을 활용하여 통해 구현하는 것입니다. 이를 위하여 가상화 환경에서 사용할 isolation을 위한 abstraction을 설계합니다. 본 과제에서 제안하는 시스템 구조는 다음과 같습니다.

<시스템 구조도>

Coffer라 명명한 이 abstraction은 하나의 게스트 운영체제에 대응되며 코드, 데이터, 스택, 힙을 제공합니다. 본 과제는 여러 coffer abstraction을 동시에 실행할 수 있도록하여 (즉 복수의 게스트 운영체제를 구동) 가상화와 동일 환경을 응용 프로그램에 제공합니다. 각각의 coffer abstraction간에는 Rust를 이용하여 가상머신과 동일한 수준의 isolation이 Rust 언어를 통해 제공합니다
Unsafe code의 안전성 검증을 위한 핵심 기술은 Rust 컴파일러 최적화와 저수준 프로그래밍 기법을 동시에 지원하는 Rust의 실행 의미를 정의, safe code의 타입 안전성 증명, safe code의 타입 안전성에 기반한 unsafe code의 안전성을 검증하는 것입니다.

본 과제는 독창성은 다음과 같습니다. (1) 기존 가상화 시스템의 안정성과 OS container 시스템의 고성능 장점을 둘 다 제공하는 새로운 형태의 가상화 시스템을 제안합니다. (2) 가상화 시스템과 같은 대규모 Rust코드에서 unsafe의 안정성을 자동으로 검증하는 framework을 최초로 제안합니다.

본 과제에 제안하는 가상화 시스템은 별도의 가상화 하드웨어를 지원하지 않는 Embedded과 IoT장치에서도 가상화 환경을 제공해줍니다. 따라서 Edge cloud나 자율 주행 자동자와 같은 차세대 산업에 하드웨어 비용을 절감하여 저비용 고성능의 가상화 기술을 도입할 수 있는 새로운 방향을 제시할 것입니다. 또한 unsafe code에 대한 안정성 보장 기법은 모든 Rust언어를 사용하는 소프트웨어 범용적으로 적용가능하기 때문에 Rust 소프트웨어의 안정성 증진에 큰 기여를 할 것이라고 기대하고 있습니다.