vSECvma：經優化與形式化驗證的 Arm 平台 Linux 核心保護框架

Abstract

隨着單體式核心如 Linux 的規模與複雜度的不斷提升，其不僅造成了巨大的攻擊面，也引發了頻繁的安全性漏洞。雖然基於虛擬化的核心防護機制能透過硬體強制隔離提供強大的安全性，但它往往會帶來顯著的效能開銷，且僅僅是將信任邊界轉移到管理程式 (Hypervisor)。本論文提出 vSECvma，這是首個針對 Arm 架構、具備高效能且經過功能正確性形式化驗證的 Linux 核心防護框架。我們的工作證明了在強安全性、高效能與形式化保證之間能夠同時達成。在既有研究的基礎上，vSECvma 強化了安全性保證，並引入一系列新穎的最佳化技術，以緩解虛擬化方法所造成的效能負擔，從而維持 Linux 的效率與相容性。我們接著對系統核心進行功能正確性的形式化驗證。此驗證透過多重策略得以實現：重用來自SeKVM（經過形式化驗證的 KVM 管理程式）的已驗證元件；運用自動化驗證框架 Spoq；並將系統系統化地重構為更適合驗證的模型。本研究最終實現了首個能同時在 Arm 上提供強安全性與高效能，並具備功能正確性機器檢證證明的 Linux 核心防護框架。

Monolithic kernels such as Linux have grown vastly in complexity, creating a large attack surface with frequent vulnerabilities. While virtualization-based kernel protection offers strong, hardware-enforced isolation, it often incurs significant performance overhead and merely shifts the trust boundary to the hypervisor. This thesis presents vSECvma, the first high-performance Linux kernel protection framework on Arm to be formally verified for functional correctness. Our work demonstrates that it is possible to achieve strong security, high performance, and formal assurance simultaneously. Building on prior work, vSECvma strengthens security guarantees and incorporates a suite of novel optimizations to mitigate the performance overhead of virtualization-based approaches, thereby retaining Linux’s efficiency and compatibility. We then formally prove the functional correctness of its system’s core. Our verification is made tractable through a multi-faceted strategy: reusing verified components from the SeKVM, a formally verified KVM-based hypervisor; leveraging Spoq, an automated verification framework; and systematically restructuring the system into a verification-friendly model. Our work delivers the first framework for Linux on Arm that simultaneously achieves strong security and high performance, backed by a machine-checked proof of functional correctness.