Arjun Guha on Verifying System Configurations

I am Arjun Guha, a computer science professor at UMass Amherst. My group brings programming-language and verification techniques to messy systems problems. Today I will focus on Puppet and the properties we might want from system configurations.

Setting up one web server involves installing software, editing configuration, restarting services and testing. Repeating those steps across many machines is difficult, especially when systems play different roles or run different operating systems. Configuration errors have also caused serious outages.

Configuration-management languages address this problem. Puppet uses a client-server architecture: configurations on a master are applied to machines running agents. I will focus on its configuration language rather than the deployment architecture.

A small manifest can create an authorized-keys file and specify ownership, permissions, parent-directory behavior and whether existing content is replaced or backed up. Puppet also offers a specialized SSH authorized-key resource. These resources describe desired machine state while hiding many low-level operations.

Puppet is often called declarative: it describes what to achieve rather than every step of how. I prefer to ask which properties we can reason about. Two desirable properties are determinism and idempotence, and neither removes the need to test the configuration.

Determinism means that the same initial state should lead to the same outcome despite choices in resource ordering. Idempotence means applying a configuration again does not change the resulting state. Puppet documentation promotes these ideas, but individual manifests can violate them.

Consider a manifest that creates a user, a vimrc file in that user’s home directory and the Vim package. Unless the dependency is specified, the file may be created before the user and fail. Puppet has ordering rules, but composition can expose different orders; relying on a particular incidental order is fragile.

A second example installs Go and removes Perl. On the Ubuntu release in the example, the Go compiler depends on Perl. Depending on the order, installation and removal can undo one another; repeating the manifest can make the system alternate between states.

Why not impose one global order? Even if a fixed order produces a reproducible error, it does not fix conflicting intent. It can also harm modularity: two independently written modules that choose opposite orders for shared resources can create a dependency cycle and cannot be installed together.

A simple non-idempotent manifest copies file two to file one and then deletes file two. It works the first time but fails the second because its input was removed. We want tools that can identify such failures rather than assuming a declarative language guarantees the properties.

Analysis is difficult because Puppet has many built-in and custom resource types, and their effects on system state can interact. The language also has complex features. Our first step translates Puppet through Datalog into a graph of atomic resources and dependencies, separating language-specific details from later reasoning.

Trying every possible installation order on real machines or containers quickly becomes intractable. Even with a fixed manifest, composing it with other modules can expose exponentially many valid orders. We therefore turn to static analysis.

The next step maps each resource into a small imperative modeling language with file-system tests and updates. A file resource may remove and recreate a file; with replace disabled it may leave an existing file alone. These are models of resource behavior, not analyses of the underlying Ruby implementation.

For packages, the system runs tools such as repoquery or apt-file in containers to obtain the files a package creates, then models those effects. The abstraction can produce false positives, and it does not cover post-install scripts. At the time of the talk the team modeled roughly 25 common resource types, primarily for Linux.

A modeled resource is a function from an input file system to an output state or an error. A partially ordered resource graph may have several possible outputs for one input. Determinism requires the set of outcomes for each input to have exactly one member; that member can be an error.

We encode the modeled semantics in Z3. A counterexample consists of one input state and two allowed executions with different outcomes. If the solver cannot find such a witness, the result establishes determinism relative to the model and the supported features.

The naïve formulation is enormous: possible file systems are effectively infinite, each state can be large, and encoding all resource interactions can produce an exponentially large formula. The problem needs reductions before it can be practical.

Partial-order reduction exploits commutativity. If two actions always produce the same result in either order, we need consider only one order. A conventional read/write-set check is too conservative for packages because many may create the same parent directories.

A domain-specific check also tracks directories that resources create. It can prove that some operations do not interfere despite their common directory setup. The tool uses this information while constructing the formula, avoiding the exponential object rather than building it and pruning afterward.

The analysis presented here does not model permissions and modes; the benchmark results therefore depend on that abstraction. The speaker notes that permissions may matter for other problems and can make reasoning slower when included.

A second challenge is the size of each state. A package may create hundreds or thousands of files, but most do not interact with other resources. We can remove portions of the model that commute with everything relevant to the nondeterminism question.

For example, installing Apache and separately creating its configuration can conflict if a dependency is missing. The analyzer retains the interacting configuration path while pruning unrelated package files. Similarly, when a manifest creates two users but only one user’s home file is involved, unrelated paths can be removed.

This is not merely a rule that globally discards every path touched once. The analysis reasons about fragments of resources and whether they can be commuted to the end of the relevant executions without changing the comparison. Paths used only by removable fragments need not appear in that model.

The finite-state abstraction has a subtle edge case around empty directories. Looking only at paths explicitly mentioned in a manifest can miss a distinction: an unmentioned child can make a directory nonempty. The model must include additional representative paths to preserve the distinction.

In a web demo, the tool Rehearsal analyzes the user-and-vimrc example and reports that it may be nondeterministic. It offers a Puppet dependency fragment; adding it makes this example deterministic and idempotent. A suggested correction still needs human review because making a configuration deterministic is not the same as making it correct.

The resource interpretations are written in the team’s modeling language. Containers are used to obtain package file listings, not to execute every modeled resource during verification. Results can be cached, with a new package query triggered when needed.

Benchmarks on manifests collected from GitHub show why the reductions matter. Some cases time out with naïve models but finish in roughly a second and a half with the optimizations. In one example the relevant modeled file count falls from about 1,500 to about 250.

The model tracks file equality, directories and empty directories, but does not inspect arbitrary file contents in detail. Copying a file can be modeled precisely, whereas a script that reads and transforms portions of its contents is outside that precision. Permissions and modes are also omitted from this analysis.

Once determinism is established, a manifest can be treated as a function from input to output file systems under the model. That makes other checks easier: idempotence asks whether applying the function twice equals applying it once, and users can also express preconditions or postconditions.

The team is exploring how to handle shell scripts embedded in manifests. One example is an installer that requires a noninteractive license-acceptance step. The current abstraction does not generally analyze such scripts, and the speaker estimates that many public manifests use them.

The proposed approach learns finite-state models from input-output examples by running a script in containers and perturbing its inputs. Modeling a command with the specific arguments used in a manifest is a narrower problem than modeling a general utility for every possible invocation. This is work in progress.

Another research direction is configuration repair. A user might deploy a vimrc with an incorrect setting, fix the live machine through shell commands and then need to apply the same correction back to the manifest. The team is exploring how to synthesize an updated configuration from the original and the observed edits.

Several configuration updates may be consistent with the same edits, so choosing and presenting alternatives is part of the problem. The aim is to shorten the edit, deploy and debug cycle while keeping the configuration aligned with the repaired system.