On Verification for System Configuration Languages

Speaker Name: 
Arjun Guha
Speaker Title: 
Assistant Professor
Speaker Organization: 
UMass Amherst
Start Time: 
Wednesday, December 5, 2018 - 1:20pm
End Time: 
Wednesday, December 5, 2018 - 2:25pm
Location: 
Engineering 2, Room 280
Organizer: 
Lindsey Kuper

Abstract:

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 our work on verification and repair of Puppet configurations. On verification, we develop a Puppet static analysis to verify key properties of configurations, such as determinism and idempotence. We apply our analysis to real-world configurations gleaned from open-source projects and are able to reproduce several known bugs and find new issues. On repair, we develop an interactive configuration repair tool that allows users to use Puppet and the shell in harmony. Using our tool, a user can fix a machine using a conventional shell and the tool suggests updates to the Puppet configuration that are consistent with the changes made from the shell. We apply our technique to a suite of repair scenarios and find that its top-ranked repair is the best repair 76% of the time.

https://plasma.cs.umass.edu/rehearsal

Bio:

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. He works on Web security, network programming languages, and system configuration languages. He received a PhD in Computer Science from Brown University in 2012 and a BA in Computer Science from Grinnell College in 2006.