CURSOR: Configuration Update Synthesis Using Order Rules

Network configuration updates are frequent nowadays to adapt to the rapid evolution of networks. To ensure the safety of the configuration update, network verification can be used to verify that network properties hold for the new configuration. However, configuration updates typically involve multiple routers changing their configurations. Changes on these routers cannot be applied simultaneously. This leads to intermediate configurations, which might violate network properties such as reachability. Configuration updates synthesis aims to find an order of applying changes on routers such that network properties hold for all intermediate configurations.Existing approaches synthesize a safe update order by traversing the update order space, which is time-consuming and does not scale to a large number of configuration updates. This paper proposes CURSOR, a configuration update synthesis that extracts rules that update orders should follow. We implement CURSOR and evaluate its performance with real-world configuration update scenarios. The experimental results show that we can accelerate the synthesis by an order of magnitude on large-scale configuration updates.