On Verification for System Configurations Languages
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.
- Presented by:
Arjun Guha is an assistant professor of Computer Science at UMass Amherst. He enjoys tackling problems in systems using the tools and principles of programming languages. Arjun is an avid functional programmer, despite conducting research on system configurations, software-defined networking, and web security. He received a PhD in Computer Science from Brown University in 2012 and a BA in Computer Science from Grinnell College in 2006.
Monday, March 6th
Snacks will be served.
Would you like to find out about future talks?