Lecture, Conference Presentation, Presentation
Arjun Guha: On Verification for System Configurations Languages
- Predicts that configuration bugs, rather than software bugs, are the primary cause of major system outages in recent years, citing incidents such as the New York Stock Exchange outage, a military plane crash due to incorrect ECU settings, and a two-and-a-half-hour Facebook outage.
- Plans to extend current Puppet-based analysis techniques to other system configuration languages like Chef and Ansible, though notes that unique challenges in these domains require specific discussion.
- Anticipates exponential growth in possible resource installation orders for well-structured manifests, leading to state space explosion that makes exhaustive testing intractable, with specific benchmarks noting up to a billion variables and on the order of two to the power of 10 interleavings for ten non-conflicting packages.
- Develops heuristics to prune the state space, reducing the number of files to reason about from approximately 1,500 to 250, which allows manifests to be analyzed in roughly 1.5 seconds instead of timing out, while warning that naive file system representations can produce unsound results.
- Notes that current modeling covers 25 common resource types but excludes macOS and Windows-specific resources, and does not deeply model file contents or permissions to maintain speed, though these are relevant for debugging.
- Foresees that installing large packages like
lxde-icon-themecan generate around 7,000 files, necessitating precise tracking of paths rather than just contents to distinguish between programs checking for empty versus non-empty directories. - Identifies that about half of Puppet manifests on GitHub use embedded shell scripts, which often cause failures in non-interactive environments, such as the Oracle Java installer failing due to an interactive license screen.
- Plans to learn finite state models of shell scripts by executing them in containers to capture IO traces, aiming to automatically calculate updated configurations to resolve errors in the typical development loop.
- Warns that while the system can suggest corrections to make manifests deterministic, these fixes may not always be semantically correct, and proposes presenting multiple possible updates to the user when several valid configuration changes exist.
- Expects that specialized commutativity checks will allow the system to consider only one ordering for non-interfering packages rather than checking all permutations, improving efficiency in analyzing resource graphs.
- States that resource graph translation naively produces exponentially large formulas, making SAT solvers intractable for large instances, but that the proposed approach models resources as small imperative programs to better analyze interactions.
- Notes that dependency issues, such as those arising from Perl requirements in the Go compiler under Ubuntu Trustee or cycles in dependency graphs caused by conflicting module orders, can cause systems to flip between states or become non-co-installable.