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.
Conference DayThu 16 JunDisplayed time zone: Tijuana, Baja California change
15:30 - 17:00
|Rehearsal: A Configuration Verification Tool for Puppet|
Rian ShambaughUniversity of Massachusetts Amherst, Aaron WeissUniversity of Massachusetts Amherst, Arjun GuhaUniversity of Massachusetts, AmherstPre-print Media Attached
|Toward Compositional Verification of Interruptible OS Kernels and Device Drivers|
Hao ChenYale University, Xiongnan (Newman) WuYale University, Zhong ShaoYale University, Joshua LockermanYale University, Ronghui GuYale UniversityPre-print Media Attached
|Verified Peephole Optimizations for CompCert|
Eric MullenUniversity of Washington, Daryl ZunigaUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, Dan GrossmanUniversity of Washington, USAPre-print Media Attached