MadSystems Seminar -- Xudong Sun (UW-Madison, UToronto)

Title: Improving Reliability of Modern Cloud Systems with Verification in the Loop

Abstract: 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 Postdoc at the University of Wisconsin-Madison working with Prof. Tej Chajed. He will join the University of Toronto as an assistant professor in July. He obtained his PhD from 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.