Projects

Atmosphere is a full-featured microkernel developed in Rust and verified with Verus. Conceptually Atmosphere is similar to the line of L4 microkernels. Atmosphere pushes most kernel functionality to user-space, e.g., device drivers, network stack, file systems, etc. The microkernel supports a minimal set of mechanisms to implement address spaces, page-tables, coarse-grained memory management, and threads of execution that together with address spaces implement an abstraction of a process. Each process has a page table and a collection of schedulable threads....

Today, the lack of isolation within an operating system kernel is one of the main factors undermining its security. While the core kernel is relatively stable, the number of kernel extensions and device drivers is growing with every hardware generation (a modern Linux kernel contains around 8,867 device drivers, with around 180-130 drivers running on a typical system). Developed by third-party vendors that often have an incomplete understanding of the kernel programming and security idioms, kernel extensions and device drivers are a primary source of vulnerabilities in the kernel....

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....

KSplit, a new framework for isolating device drivers in the Linux kernel. KSplit performs a collection of static analyses on the source code of the kernel and the driver to generate the synchronization code that is required to execute the driver in isolation. Specifically, KSplit identifies the shared state that is accessed by both driver and the kernel computing how this state is accessed on both sides of the isolation boundary and how it should be synchronized on each kernel-driver invocation and when a shared synchronization primitive, e....

Modern operating systems are monolithic. Today, however,lack of isolation is one of the main factors undermining security of the kernel. Inherent complexity of the kernel code and rapid development pace combined with the use of unsafe,low-level programming language results in a steady streamof errors. Even after decades of efforts to make commodity kernels more secure, i.e., development of numerous static and dynamic approaches aimed to prevent exploitation of mostcommon errors, several hundreds of serious kernel vulnerabilities are reported every year....

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. Historically, isolation within the kernel remained prohibitive due to the high cost of hardware isolation primitives. Recent CPUs, however, bring a new set of mechanisms....

A research operating system developed from scratch in Rust, aimed to explore the impact of language safety on operating system organization.

Persistent memory (PM) hardware such as Intel’s Optane DC memory product promises to transform how programs store and manipulate information. Persistent memory provides a mixture of the performance and flexibility of DRAM and the price and persistence of FLASH storage. There has been much exciting work in the systems community to explore how persistent memory enables new more efficient designs of storage systems ranging from file systems that bypass the kernel to key-value storage systems to concurrent DRAM indices to databases....