Arjun Guha: On Verification for System Configurations Languages

Motivation and Context

• System configuration errors, distinct from software bugs, are a leading cause of major outages (e.g., NYSE downtime, military plane crash due to ECU settings, Facebook 2.5-hour outage).
• Puppet is the primary focus of the research, utilized by over 30,000 organizations.
• The core problem addressed is ensuring Puppet manifests are deterministic (produce the same result regardless of resource order) and idempotent (applying the configuration multiple times yields the same result as applying it once).
• Real-world Puppet usage often violates these properties due to implicit dependencies (e.g., installing Go depending on Perl removal) and arbitrary resource ordering.

Tool and Methodology: "Rehearsal"

• The research introduces a verification tool named "Rehearsal" that analyzes Puppet manifests for determinism and idempotency.
• Transformation Pipeline:
  • Step 1: Parses complex Puppet syntax and generates an equivalent Datalog program, modeling the logic as a graph of atomic resources.
  • Step 2: Translates resource graphs into a small, imperative modeling language that simulates low-level file system operations (e.g., mkdir, write, delete).
  • Step 3: Encodes the semantics of these programs as relations between input and output file system states.
• Verification Engine: Uses the Z3 SMT solver to check if a single input state maps to exactly one output state (proving determinism) or if multiple states are reachable.

Technical Challenges and Optimizations

• State Space Explosion: Naive modeling of file systems is intractable due to infinite states and exponential formula sizes (potentially billions of variables).
• Partial Order Reduction: The system prunes the search space by identifying independent resource blocks that commute, avoiding the need to explore every possible interleaving of resources.
• Specialized Commutativity Checks: Standard read/write set checks fail for packages (which may create overlapping directories like /opt). The tool abstracts programs to include directory tree creation to accurately detect interference.
• State Pruning: The model dynamically removes paths that do not interact between resources (e.g., ignoring 7,000 icon files if only Apache's config file is relevant to the specific bug), reducing the state from thousands of files to ~250 critical paths.
• Handling Empty Directories: The model explicitly accounts for tests checking if a directory is empty, as these tests can distinguish between otherwise identical file system states.

Benchmark Results

• The tool successfully verified determinism on real-world manifests scraped from GitHub.
• Benchmarks show that without heuristics, analysis often times out; with optimizations, analysis completes in seconds.
• The tool successfully identified previously unknown non-deterministic bugs in real manifests and generated code fragments to fix them (e.g., adding missing dependency edges).

Future Work and Limitations

• Shell Scripts: Current analysis excludes exec resources containing shell scripts (approx. 50% of manifests), which often break idempotency or determinism (e.g., interactive license agreements).
  • Solution in progress: Using IO examples and S-trace data to learn finite state models of specific shell commands via containerization.
• File Permissions: Current benchmarks do not model file permissions/modes, as they rarely cause determinism bugs, though this is being revisited.
• Automated Bug Fixing: Research is exploring automated generation of configuration updates based on a sequence of manual shell commands executed to debug a failure (e.g., fixing a vimrc typo), effectively shortening the edit-compile-debug loop.