Device driver isolation aims to protect kernels from faulty/malicious drivers, yet its security guarantees are not fully understood. Compartment Interface Vulnerabilities (CIVs), known in userspace applications, also impact driver isolation, but this area is underexplored. This paper surveys existing driver isolation frameworks, systematizes CIV classifications, and evaluates them in the driver isolation context. Our analysis reveals CIV prevalence under a baseline threat model, with large drivers exhibiting over 100 CIV instances and an average of 33 across the studied drivers. Enforcing additional security properties like CFI reduces average CIVs to approximately 28. This work offers insights into driver isolation security, CIV prevalence, and guidance for future systems.

Recent advances in programming languages and automated formal reasoning have changed the balance between the complexity and practicality of developing formally verified systems. Our work leverages Verus, a new verifier for Rust that combines ideas of linear types, permissioned reasoning, and automated verification based on satisfiability modulo theories (SMT), for the development of a formally verified microkernel, Atmosphere.

Rust-for-Linux (RFL) is a new framework that allows development of Linux kernel extensions in Rust. At first glance, RFL is a huge step forward in terms of improving the security of the kernel: As a safe programming language, Rust can eliminate wide classes of low-level vulnerabilities. Yet, in practice, low-level driver code – complex driver interface, a combination of reference counting and manual memory management, arithmetic pointer and index operations, unsafe type casts, and numerous logical invariants about the data structures exchanged with the kernel might significantly limit the security impact of Rust.This work takes a careful look at how Rust can impact the security of driver code. Specifically, we ask the question: What classes (and what fraction) of vulnerabilities typically found in device driver code can be eliminated by reimplementing device drivers in Rust? We find that Rust can eliminate large classes of safety-related vulnerabilities, but naturally struggles to address protocol violations and semantic errors. Moreover, to be fully eliminated, many classes of flaws require careful programming discipline to avoid memory leaks and runtime panics (e.g., explicit checks for integer overflows and option types), careful implementation of Drop traits, as well as correct implementation of reference counting. Our analysis of 240 driver vulnerabilities that are present in device drivers in the last four years, shows that 82 could be automatically eliminated by Rust, 113 require specific programming idioms and developer’s involvement, and 45 remain unaffected by Rust. We hope that our work can improve the understanding of potential flaws in Rust drivers and result in more secure kernel code.

Trying to address the security challenges of a cloud-centric software deployment paradigm, silicon and cloud vendors are introducing confidential computing – an umbrella term aimed at providing hardware and software mechanisms for protecting cloud workloads from the cloud provider and its software stack. Today, Intel Software Guard Extensions (SGX), AMD secure encrypted virtualization (SEV), Intel trust domain extensions (TDX), etc., provide a way to shield cloud applications from the cloud provider through encryption of the application’s memory below the hardware boundary of the CPU, hence requiring trust only in the CPU vendor. Unfortunately, existing hardware mechanisms do not automatically enable the guarantee that a protected system was not tampered with during configuration and boot time. Such a guarantee relies on a hardware root of trust, i.e., an integrity-protected location that can store measurements in a trustworthy manner, extend them, and authenticate the measurement logs to the user (remote attestation).

Despite decades of innovation, existing hash tables fail to achieve peak performance on modern hardware. Built around a relatively simple computation, i.e., a hash function, which in most cases takes only a handful of CPU cycles, hash tables should only be limited by the throughput of the memory subsystem. Unfortunately, due to the inherently random memory access pattern and the contention across multiple threads, existing hash tables spend most of their time waiting for the memory subsystem to serve cache misses and coherence requests.

Our work explores the challenge of developing secure kernel-driver interfaces designed to protect the kernel from isolated kernel extensions. We first analyze a range of possible attack vectors that exist in current isolation frameworks. Then, we suggest a new approach to building secure isolation boundaries centered around ideas that originate in safe operating systems: isolation of heaps and single ownership.

In contrast to hardware-based isolation solutions, language-based systems support crossing of isolation boundaries with an overhead of a function call. Moreover, the strong type system of a safe language provides support for secure communication in the face of complex, semantically-rich interfaces, i.e., support for fault isolation and end-to-end zero-copy communication through isolation of object spaces and controlled ownership on the shared exchange heap. If historically, safety was prohibitive due to overheads of a managed runtime, today, languages like Rust achieve the performance of unsafe C hence empowering language-based systems to support practical isolation with fine-grained boundaries and frequent communication.

Rust is the first practical programming language that has the potential to provide fine-grained isolation of untrusted computations at the language level. A combination of zero-overhead safety, i.e., safety without a managed runtime and garbage collection, and a unique ownership discipline enable isolation in systems with tight performance budgets, e.g., databases, network processing frameworks, browsers, and even operating system kernels.

A recent surge of security attacks has triggered a renewed interest in hardware support for isolation. Extended page table switching with VMFUNC, memory protection keys (MPK), and memory tagging extensions (MTE) are just a few of the hardware isolation mechanisms that promise support for low-overhead isolation in recent CPUs. Along with the restored interest in lightweight hardware isolation mechanisms, safe programming languages like Rust has made a leap towards practical, zero-overhead safety implemented without garbage collection.

Commodity operating systems execute core kernel subsystems in a single address space along with hundreds of dynamically loaded extensions and device drivers. Lack of isolation within the kernel implies that a vulnerability in any of the kernel subsystems or device drivers opens a way to mount a successful attack on the entire kernel.

RedLeaf is a new operating system being developed from scratch to utilize formal verification for implementing provably secure firmware. RedLeaf is developed in a safe language, Rust, and relies on automated reasoning using satisfiability modulo theories (SMT) solvers for formal verification. RedLeaf builds on two premises: (1) Rust's linear type system enables practical language safety even for systems with tightest performance and resource budgets (e.g., firmware), and (2) a combination of SMT-based reasoning and pointer discipline enforced by linear types provides a unique way to automate and simplify verification effort scaling it to the size of a small OS kernel.