Mars Research Group

Mars Research is a systems research group at the University of Utah. Primarily we are interested in a broad range of problems at the very core of the systems stack related to the security, reliability, and performance of operating systems.

Our work explores the challenges related to the design and implementation of operating systems as well as a range of issues on the intersection of systems with architecture, programming languages, security, and formal methods.

Historically, we are always working on at least one clean-slate operating system. Right now its:

Atmostphere, a clean-slate fully-verified operating system

Notable past projects are RedLeaf, a clean slate operating system that uses Rust safety for isolation, and KSplit, a static analysis framework and lightweight runtime for automatic isolation of device drivers in the Linux kernel.

We also built DRAMHiT – the fastest ever hash table.

We’re always looking for motivated students interested in operating systems at all levels from undergraduate to PhD. If you have relevant skills (take a look at our repos to see what we normally do) send me an email.

Active Projects

Atmostphere verified operating system develooped in Rust and Verus: atmo
Formally verified drivers for the Linux kernel VELD
Hardware support for low-overhead, fine grained isolation ipc
Retrofitting isolation in the Linux kernel: kernel-isolation
Hash table designed to work at the speed of DRAM: DRAMHiT
Impact of Rust on the Linux kernel: rfl

Past Projects

Redleaf operating system: redleaf
KSplit framework for decomposing the Linux kernel ksplit
Lightweight VMFUNC Domains LVDs
Lightweight eXecution Domains LXDs

People

Anton Burtsev (Faculty, lead)

Xiandong Chen (PhD, 2026 expected)

Zhaofeng Li (PhD, 2025 expected)

Jerry Zhang (PhD, 2028 expected)

Joshua Tlatelpa-Agustin (BS, expected 2025)

Alumni

Vikram Narayanan (PhD, 2024, now at Palo Alto Networks)

Dan Appel (BS 2021, now at Apple)

Tianjiao Huang (MS 2022, now PhD student at UC Irvine)

Michael Lusher (BS 2021, now at Splunk)

Daman M Kumar (MS 2020, now at Amazon)

Vincent Whizin (BS, 2022)

Ed Younis (BS 2018, now at Berkeley Lab)

Connor Zwick (BS, 2022)

Tirth Jain (Summer Intern, 2022)

David Detweiler (BS 2023, now at Atlassian)

Posts

Setting up Alveo FPGAs on Cloudlab - Part 1

As a systems research team, we build operating systems, low-level software, hack kernels and yet hardware programming always remained on the todo-list of “cool, but haven’t tried yet”. When Cloudlab started introducing FPGA accelerators to their testbed, we got excited and finally decided to give it a try. Cloudlab is one of the publicly available testbeds for research. In all of our projects, we carry out the whole development process on Cloudlab infrastructure....

Debugging QEMU/KVM Setup If Something Goes Wrong (e.g., Support for 1GB Pages)

In our previous projects, we always did all development on real hardware. For example, LXDs and LVDs required baremetal speed of the cache-coherence protocol and support for nested virtualization (both systems use hardware-supported virtualization). So development under QEMU looked unrealistic. Well, maybe we need to explore more. KVM supports nested virtualization, but we needed support for features like extended page table (EPT) switching with VMFUNC. In the end, we were reluctant to take this approach....

Kernel Development with Qemu (Printing "Hello World" On Bare Metal)

If you plan to start working on a new operating system kernel things get hard fast—there is a ton of low-level hardware details you have to understand and a number of design decisions you have to make (after all, why would you build yet another kernel—you have to invent something new, right?). Complexity is intimidating. Nevertheless, if you take it step by step, the basics are simple. And it’s worth trying....

Active Projects#

Past Projects#

People#

Alumni#

Posts#

Active Projects

Past Projects

People

Alumni

Posts