Arjun Guha, assistant professor of Computer Science at UMass
Amherst, presents at Jane Street.
Puppet is a configuration management system used by hundreds of organizations to manage thousands of machines. It is designed to automate tasks such as application configuration, service orchestration, VM provisioning, and more. The heart of Puppet is a declarative language that specifies a collection of resources, their desired state, and their inter-dependencies. Although Puppet
performs some static checking, there are many opportunities for errors to occur at runtime. Even if a configuration is bug-free, when a machine is updated to a new configuration, it is easy for the machine state and its configuration to "drift" apart.
This talk presents an automated toolchain for verifying essential properties of Puppet configurations. First, we identify non deterministic behavior as the root cause of several classes of bugs. Second, we present a sound, complete, and scalable algorithm to verify that configurations are deterministic. Our approach
is to encode configurations as logical formulas in an SMT solver and apply partial order reduction and program slicing to achieve scalability. Third, we address the configuration update problem, where a live update can cause a machine to "drift" from its specified configuration. Our approach is to treat deterministic configurations as functions and build a configuration synthesis tool that calculates a safe configuration update. We apply our tools to real-world Puppet configurations gleaned from open-source projects and reproduce
several known bugs and find a few new issues.