Thu 16 Jun 2016 15:30 - 16:00 at Grand Ballroom Santa Ynez - Verifying Systems Chair(s): Santosh Nagarakatte

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 Jun

Displayed time zone: Tijuana, Baja California change

15:30 - 17:00
Verifying SystemsResearch Papers at Grand Ballroom Santa Ynez
Chair(s): Santosh Nagarakatte Rutgers University
15:30
30m
Talk
Rehearsal: A Configuration Verification Tool for Puppet
Research Papers
Rian Shambaugh University of Massachusetts Amherst, Aaron Weiss University of Massachusetts Amherst, Arjun Guha University of Massachusetts, Amherst
Pre-print Media Attached
16:00
30m
Talk
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
Research Papers
Hao Chen Yale University, Xiongnan (Newman) Wu Yale University, Zhong Shao Yale University, Joshua Lockerman Yale University, Ronghui Gu Yale University
Pre-print Media Attached
16:30
30m
Talk
Verified Peephole Optimizations for CompCert
Research Papers
Eric Mullen University of Washington, Daryl Zuniga University of Washington, Zachary Tatlock University of Washington, Seattle, Dan Grossman University of Washington, USA
Pre-print Media Attached