Zoom: https://illinois.zoom.us/j/82500426065?pwd=AbbjRFAvm6P95mM0FtJ8g4w4kNfWa4.1
Refreshments provided.
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.
My insight is that testing can help verification fit in the loop. My research approach can be summarized as first testing and then specifying and verifying systems. My research starts by building systematic and automatic testing techniques for widely-used cloud systems. Testing not only finds many new bugs but also helps develop a deep understanding of the existing system implementation. With findings from testing results, I develop formal specifications and verification techniques for modern cloud systems and use these techniques to formally verify their implementations.
In this talk, I will focus on my research on testing and verifying cluster managers, e.g., Kubernetes. I will discuss how my work on testing cluster managers reveals that liveness violations are a dominating failure pattern of these systems. I will then introduce Eventually Stable Reconciliation (ESR), a liveness property for controller correctness, and Anvil, a framework for verifying liveness and safety of cluster managers. I will present the practical Kubernetes controllers that we have built and verified against ESR using Anvil. 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.