Securing the safety of a kernel is primitive but extremely important in protecting operating systems from
security threats. To enforce the kernel safety, various methods, $\textit{e.g.}$ fuzzing, static analysis, and formal
verifications, are proposed, but limited by incompleteness, low precision, and high cost. To overcome
the limitations, one suggested writing a kernel in a type-safe language. However, it is difficult to write
a kernel in a safe language, since it requires unsafe low-level controls for performance and management
of peripheral devices.
In this paper, we propose $\textit{Type-Guided Refactoring (TGR)}$, a method to refactor legacy kernels
to a type-safe programming language Rust, preserving kernel developers’ intent. We present the safe
abstractions of core kernel components in types obtained from the method. Finally we inspect that TGR
is systematic and efficient by applying TGR on an existing kernel, Hafnium.
커널의 안전성을 지키는 것은 보안 위협에서 운영 체제를 보호하기 위해 기본적이면서도 극히 중요하다.
안전한 커널을 만들기 위해, 퍼징(fuzzing), 정적 분석(static analysis), 형식 검증(formal verification) 등이
제시되었으나, 이들은 불완전성, 낮은 정확도, 높은 비용 등의 한계가 있다. 이 한계를 극복하기 위하여, 타입
안전한 언어를 이용하여 커널을 작성하는 방법이 제시된 바 있다. 그러나 커널을 안전한 언어로 작성하는
것에는 어려움이 따르는데, 그것은 커널이 주변 장치 관리와 성능을 위하여 안전하지 않은 저 수준 조작을
필요로 하기 때문이다.
본 논문에서는 기존에 존재하던 커널을 러스트라는 타입 안전한 시스템 프로그래밍 언어로 리팩토링
하여, 커널 개발자의 의도를 해치지 않으면서도 커널의 안전성을 높일 수 있는 방법, $\textit{타입 기반 리팩토링
(Type-Guided Refactoring)}$을 제시한다. 또한, 해당 방법에 따라, 우리는 커널의 핵심 구성 요소들에 대한
안전한 추상화를 타입으로 나타내어 보였다. 마지막으로 우리는 이를 기존 커널인 Hafnium 에 적용하여
타입 기반 리팩토링이 체계적이고 효율적임을 실험을 통해 확인하였다.
