RedLeaf: a clean-slate operating system in Rust designed to support formal verification of functional correctness (project web page).

Redshift: a new operating system aimed to support heterogeneous hardware, e.g., FPGAs, GPUs, TPUs, near storage, and near network cores, etc., as first class citizens (project web page).

Horizon: a new secure hypervisor and secure cloud in which users own their data. Horizon is developed in Rust, and relies on novel techniques of hardware and software isolation, and will implement cloud-wide information flow control (project web page).

Operating systems: novel abstractions for structuring operating systems (microkernels, virtualization, language-based kernels, security and verification of the kernel).

Security: operating system and datacenter security (secure cloud architectures, network access control, object capabilities).

Fast datacenter stacks: low-latency system stacks, support for heterogeneou hardware.

Yongzhe Huang, Vikram Narayanan, David Detweiler, Kaiming Huang, Gang Tan, Trent Jaeger, and Anton Burtsev. KSplit: Automating Device Driver Isolation.. In In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI'22), July 2022. [PDF]

Anton Burtsev, Dan Appel, David Detweiler, Tianjiao Huang, Zhaofeng Li, Vikram Narayanan, Gerd Zellweger. Isolation in Rust: What is Missing?. In 11th Workshop on Programming Languages and Operating Systems (PLOS'21), October 2021. [PDF]

Zhaofeng Li, Tianjiao Huang, Vikram Narayanan, Anton Burtsev. Understanding the Overheads of Hardware and Language-Based IPC Mechanisms. In 11th Workshop on Programming Languages and Operating Systems (PLOS'21), October 2021. [PDF]

Vikram Narayanan, Tianjiao Huang, David Detweiler, Dan Appel, Zhaofeng Li, Gerd Zellweger, Anton Burtsev. RedLeaf: Isolation and Communication in a Safe Operating System. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI), November 2020. [PDF]

[Best paper award] Vikram Narayanan, Yongzhe Huang, Gang Tan, Trent Jaeger, and Anton Burtsev Lightweight Kernel Isolation with Virtualization and VM Functions. In 16th ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments (VEE 20), March 2020. [PDF].

Vikram Narayanan, Abhiram Balasubramanian, Charlie Jacobsen, Sarah Spall, Scott Bauer, Michael Quigley, Aftab Hussain, Abdullah Younis, Junjie Shen, Moinak Bhattacharyya, and Anton Burtsev LXDs: Towards Isolation of Kernel Subsystems. In 2019 USENIX Annual Technical Conference (USENIX ATC 19), July 2019. [PDF].

Vikram Narayanan (University of California, Irvine), Marek S. Baranowski (University of Utah), Leonid Ryzhyk (VMware Research), Zvonimir Rakamarić (University of Utah), Anton Burtsev (University of California, Irvine). RedLeaf: Towards An Operating System for Safe and Verified Firmware. In 17th Workshop on Hot Topics in Operating Systems (HotOS), May 2019. [PDF].

Anton Burtsev, David Johnson, Josh Kunz, Eric Eide, Jacobus Van der Merwe. CapNet: Security and Least Authority in a Capability-Enabled Cloud. In 8th ACM Symposium on Cloud Computing (SoCC), September 2017. [PDF].

Abhiram Balasubramanian, Marek S. Baranowski, Anton Burtsev, Aurojit Panda, Zvonimir Rakamaric, Leonid Ryzhyk. System Programming in Rust: Beyond Safety. In 16th Workshop on Hot Topics in Operating Systems (HotOS), May 2017. [PDF].

143A Principles of Operating Systems (Fall 2021, Fall 2020, Fall 2019, Fall 2018, Fall 2017, Winter 2017)

238P Operating Systems (Fall 2021, Spring 2020, Spring 2019, Fall 2018, Winter 2018)

250P Computer Systems Architecture (Fall 2021, Spring 2021, Fall 2019, Winter 2019)

MARS Systems Reading Group (2021-2017)

Low-Level System Reading Group with Ryan Stutsman (Spring 2016 at University of Utah)

cs5460/6460 Operating Systems (Spring 2014 at University of Utah)

RedLeaf: Verified Operating Systems in Rust RedLeaf is a new operating system, and associated formal verification tools for implementing provably secure and reliable systems in the Rust programming language. RedLeaf brings together state-of-the-art results from verification, programming-language, and systems research communities in order to enable unprecedented security and reliability guarantees in low-level systems software. To achieve complete verification of the entire software stack, i.e., operating system and applications, the RedLeaf team will develop a set of new tools, a collection of techniques and engineering disciplines, and a methodology focused on rapid development of verified systems software. The RedLeaf OS will run on an embedded CPU of a medical sensor, implement a network function virtualization framework aimed at line-rate network processing, and provide a general platform for a broad range of verifiably secure systems.

NSF abstract

Redshift: An Operating System for Pervasive Hardware Acceleration In contrast to today's systems centered around general-purpose processors also known as central processing units (CPUs), the next generation of high-performance computers will inherently rely on diverse, heterogeneous hardware ranging from many-core processors like Intel Xeon Phi that contains up to 72 processor cores and graphical processing units (GPUs) to specialized hardware accelerators, like specialized machine-learning chips and field-programmable gate arrays (FPGAs) re-programmed on demand for a specific task. In a hardware-accelerated environment that consists of many diverse execution units, the execution of a program is no longer a conventional thread tied to a single CPU, but a graph of small computations scheduled on a set of hardware accelerators each implementing a part of the program logic. Redshift is a new operating system for developing applications that leverage performance of a heterogeneous hardware-accelerated system. At the core of Redshift is a dataflow programming model that enables execution of commodity programs on a network of heterogeneous hardware execution units with only minimal modifications. Redshift implements programs as collections of asynchronous invocations that transparently move execution between hardware functions. A novel runtime maps computations to execution units, balances load among them, and scales the hardware graph of computation in response to load.

NSF abstract

Horizon: Secure Large-Scale Scientific Cloud Computing Horizon is a novel cloud architecture aimed at providing data and computation security within a scientific cloud. Horizon builds upon three premises: (1) strong isolation on end-hosts, (2) fine-grained isolation in the cloud network, and (3) cloud-wide information flow control. To protect the end-hosts, Horizon develops a new layered hypervisor, and disaggregated virtualization stack with key features of: language safety, software fault isolation, and integrated software verification. To provide secure cloud network environment, Horizon relies on a new network architecture and implements a distributed network firewall, where all network communication and exchange of rights are mediated and controlled by the rules of the object capability system. To protect the cloud data, Horizon develops a set of abstractions and mechanisms to enforce cloud-wide information flow control. In Horizon all data is labeled. The hypervisor mediates all communication of each virtual machine and enforces propagation of labels and security checks for each cloud computation.

NSF abstract

Secure and Oblivious Data Bases with secure computation and SGX We collaborate with crypto and DB teams to develop novel data base architectures that protect sensitive data through novel cryptographic primitives and secure enclaves (Intel SGX).

NSF abstract

LCDs: Disaggregated System Services Through Lightweight Capability Domains. For several decades the operating system community has accepted that the only way of minimizing the trusted computing base, and constructing more secure, least authority systems, is to reimplement monolithic kernel functionality as a set of isolated microkernel servers. Instead of splitting the core functionality of a traditional operating system into multiple servers, we develop a mechanism that can securely isolate individual kernel components right inside the address space of the monolithic operating system kernel. Effectively, we build a capability machine for the Linux kernel.

LCDs source code and documentation

XCap project page

Deker project page

CapNet: Capability-Enabled Networks and Clouds. Building on the principles of capability access control, CapNet represents system resources as a graph of objects connected with edges that represent rights, or capabilities. By controlling the distribution of capabilities, CapNet (i) implements strong, fine-grained isolation of network hosts; (ii) develops mechanisms for decentralized, application-driven dynamic management of connectivity; and (iii) provides a formal foundation for establishing secure collaboration in face of dynamic, mistrusting principals and insecure end-hosts.

CapNet project page

Deker: Decomposing Commodity Kernels for Verification. Deker is a framework for decomposing and verifying commodity operating system kernels. Deker turns a de-facto standard commodity operating system kernel into a collection of strongly isolated subsystems suitable for verification. Despite multiple decades of evolution and improvements in software verification tools, almost none of them made their way into regular industry practice. Deker aims to amend this using a holistic approach unifying modular redesign of legacy components with customized verification techniques. While decomposing the kernel and providing complete isolation of subsystems, Deker remains practical: retains source-level compatibility with the non-decomposed kernel, enables incremental adoption, and remains fast.

Deker project page

XCap: Practical Capabilities and Least Authority for Virtualized Environments. XCap is a secure environment for least-authority execution of applications and system services. Unmodified, untrusted, off-the-shelf applications, running on untrusted operating systems, are isolated by a virtual machine monitor. XCap's default -- a share nothing environment -- is augmented by a capability access control model: a clean and general abstraction, enabling fine-grained delegation of rights in a flexible and manageable way.

XCap project page

XenTT: Deterministic system analysis. XenTT is full-system deterministic replay engine for Xen capable of capturing and replaying execution of Xen VMs. XenTT creates a foundation for a deterministic replay analysis platform aimed at automatic debugging, and analysis of complex software systems. XenTT comes with a powerful virtual machine introspection (VMI) library, and a streaming language, Weir, both of which create a convenient programming environment for monitoring execution of the guest system, accessing its state through convenient symbol names, and implementing reusable analysis algorithms.

XenTT source code and documentation