FMitF: Track I: Synthesizing Semantic Checkers for Runtime Verification of Production Distributed Systems

Regents Of The University Of Michigan - Ann Arbor, Ann Arbor MI

Investigators

Abstract

As users increasingly depend on distributed systems to provide various services, it is critical to ensure that these systems function properly. However, software bugs and hardware faults can cause production distributed systems to violate semantic guarantees without demonstrating any explicit errors. These "silent failures" can have serious consequences and are difficult to detect using existing methods. One promising approach to this problem involves continuous verification of system behavior using runtime checkers that can detect semantic violations. Unfortunately, few production distributed systems have adopted runtime verification due to the associated difficulty and cost of creating robust and efficient checkers. This project aims to bridge this fundamental gap by designing new, end-to-end methods that automatically synthesize high-quality semantic checkers for modern distributed systems. The project will result in a framework that leverages the many existing tests developers have already written for particular system inputs by analyzing the test code and generating semantic checkers that perform correctly under new inputs. The project will further establish a new language and corresponding runtime verifier to generate more expressive and efficient checkers and to refine the checkers as the system evolves. Distributed systems are the backbone of vital services in our society. Silent failures have led to significant losses and disruptions. This project will make large-scale distributed systems resilient to silent semantic failures and reduce their impact on users and society. Furthermore, it will increase awareness and understanding of runtime verification for distributed systems and provide practical toolchains that facilitate its widespread adoption. The project includes education and outreach activities that include student mentoring, curriculum development, release of software (and related) artifacts, and dissemination of results through a variety of academic and industry venues. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.