I am an Assistant Adjunct Professor at the Department of Computer Science, University of California Irvine. I design, and build novel operating systems. My work spans a broad variety of topics from novel low-latency datacenters to secure and verified kernels.
Group's reading group.
I am looking for students interested in operating systems at all levels from undergraduate to PhD, if you have relevant skills send me an email.
We are building three new operatings systems
RedLeaf: a clean-slate operating system in Rust designed to support formal verification of functional correctness.
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..
Horizon: a new secure hypervisor and secure cloud in which users own their data (Horizon will be built in Rust, will rely on novel techniques of hardware and software isolation, and will implement cloud-wide information flow control).
Operating systems: novel abstractions for structuring operating systems, microkernels, virtualization, decomposed and library kernels, security and verification of the kernel stack.
Security and access control: capability access control, practical least authority for virtualized environments and commodity operating systems, access control in datacenter and enterprise networks, access control in cloud.
Operating system support for datacenter environments: low-latency system stacks, library operating systems, fast inter-process communication, software stacks for non-uniform high-density memory machines.
Systems Reading Group (Fall 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.
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.
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.
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).
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.
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.
Fast cross-core communicaiton for non-uniform memory access (NUMA) architectures We work on designing a new efficient communication mechanisms aimed at providing efficient communication on modern NUMA machines.
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.
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.
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.
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].
Anton Burtsev, David Johnson, Mike Hibler, Eric Eide, John Regehr. Abstractions for Practical Virtual Machine Replay.. In Proceedings of the 12th ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments (VEE'16), April 2016. [PDF].
Charles Jacobsen, Muktesh Khole, Sarah Spall, Scotty Bauer, and Anton Burtsev. Lightweight Capability Domains: Towards Decomposing the Linux Kernel.. In Proceedings of the 8th Workshop on Programming Languages and Operating Systems (PLOS 2015), October 2015. [PDF].
Anton Burtsev, Nikhil Mishrikoti, Eric Eide, and Robert Ricci. Weir: A Streaming Language for Performance Analysis. In Proceedings of the 7th Workshop on Programming Languages and Operating Systems (PLOS 2013), November 2013. [PDF].
Anton Burtsev, Kiran Srinivasan, Prashanth Radhakrishnan, Lakshmi N. Bairavasundaram, Kaladhar Voruganti, and Garth R. Goodson. Fido: Fast Inter-Virtual-Machine Communication for Enterprise Appliances. In Proceedings of the 2009 USENIX Annual Technical Conference, San Diego, June 2009 [PDF] (Slides [PDF]).
Anton Burtsev, Prashanth Radhakrishnan, Mike Hibler, and Jay Lepreau. Transparent Checkpoints of Closed Distributed Systems in Emulab. In Proceedings of the Fourth ACM SIGOPS/EuroSys European Conference on Computer Systems, Nuremberg, Germany, April 2009 [PDF] (Slides [PDF]).
Skiing, tennis, biking, taking pictures, travel, music, time with family (a long list).
Updated: August, 2016