Seminar • Systems and Networking • Improving Reliability of Modern Cloud Systems with Verification in the Loop

Please note: This seminar will take place online.

Xudong Sun, PhD candidate
University of Illinois Urbana-Champaign

Reliability of modern cloud systems is paramount but notoriously challenging. Formal verification is a powerful technique to guarantee system reliability, but it is currently not in the loop of building and evolving software systems. Instead, testing is the common practice to improve system reliability, but it cannot provide any formal guarantee. The goal of my research is to bring verification in the loop by gradually verifying practical system implementations and replacing existing, unverified systems with verified ones.

In this talk, I will focus on my recent work, Anvil, a framework for building formally verified cluster management controllers (Kubernetes controllers). I will introduce Eventually Stable Reconciliation (ESR), a liveness property for controller correctness, and a general proof strategy for proving liveness of controllers. I will present the practical Kubernetes controllers that we have built and verified against ESR using Anvil. I will also briefly talk about my work on testing controllers. To conclude, I will outline future research directions on broadening the scope of systems verification and addressing reliability challenges in emerging domains.

Bio: Xudong Sun is a PhD candidate in Computer Science at the University of Illinois Urbana-Champaign (UIUC), advised by Prof. Tianyin Xu. His research primarily focuses on computer systems, with a special interest in improving reliability of modern cloud systems using formal verification and testing techniques.

His work on formal verification for modern cluster managers was recognized with a Jay Lepreau Best Paper Award at OSDI 2024. He was a recipient of the Mavis Future Faculty Fellowship in 2024 and the Yunni & Maxine Pao Memorial Fellowship in 2022.

Attend this seminar virtually on Zoom.