Explaining Network Configurations Under Failures via Localized Subspecifications
TL;DR
This work explores fault-tolerant subspecifications as a way to bridge the gap between network fault-tolerance verification and operators' guidance on which configuration fields are responsible for correctness or which local edits are safe under the full failure model.
Abstract
Network fault-tolerance verification checks whether configurations satisfy properties such as reachability and isolation under a bounded set of failures, but produces only a global pass/fail result. Operators are left without guidance on which configuration fields are responsible for correctness or which local edits are safe under the full failure model. We explore fault-tolerant subspecifications as a way to bridge this gap: for each configuration location h, a constraint ψ(h) that characterizes the replacement values guaranteed to preserve the global property across all failure scenarios within the budget. Our approach combines per-device SMT encodings with a failure-aware symbolic route; guarded routing branches induce branch-local constraints on h, whose intersection yields the fault-tolerant subspecification. We present the approach, illustrate it on a small BGP example, and discuss preliminary results that demonstrate feasibility and interpretability. We conclude with open problems and directions for future work.