Large-scale modern datacenters and cloud computing have turned system configuration into a challenging and urgent problem. Several widely-publicized outages have been blamed not on software bugs, but on software configuration issues. To cope, thousands of organizations now use system configuration languages to manage their computing infrastructure. Of these languages, Puppet is the most widely used with over 18,000 paying customers and several more open-source users. The heart of Puppet is a declarative domain-specific language that describes the state of a system. Although Puppet performs some basic static checks, there are several opportunities for errors to occur. Furthermore, testing is ineffective because many errors are only triggered under specific machine states that are difficult to predict and reproduce.
This paper presents Rehearsal, a verification tool for Puppet configurations. We first illustrate the kinds of errors that occur in Puppet with several examples. We show that the key issue is that configurations can easily be non-deterministic, thus Rehearsal implements a sound, complete, and scalable determinacy analysis for Puppet. To develop it, we (1) present a formal model for Puppet configurations, (2) use two different program analyses to prune our models to a tractable size, and (3) frame determinism-checking as an SMT problem. Rehearsal then leverages the determinacy analysis to check other important properties, such as idempotency. Finally, we apply Rehearsal to several real-world Puppet configurations.
Thu 16 JunDisplayed time zone: Tijuana, Baja California change
15:30 - 17:00
|Rehearsal: A Configuration Verification Tool for Puppet|
Rian Shambaugh University of Massachusetts Amherst, Aaron Weiss University of Massachusetts Amherst, Arjun Guha University of Massachusetts, AmherstPre-print Media Attached
|Toward Compositional Verification of Interruptible OS Kernels and Device Drivers|
Hao Chen Yale University, Xiongnan (Newman) Wu Yale University, Zhong Shao Yale University, Joshua Lockerman Yale University, Ronghui Gu Yale UniversityPre-print Media Attached
|Verified Peephole Optimizations for CompCert|
Eric Mullen University of Washington, Daryl Zuniga University of Washington, Zachary Tatlock University of Washington, Seattle, Dan Grossman University of Washington, USAPre-print Media Attached