CRONUS: Counterexample-Guided Constraint Learning for Network Update Synthesis

Network reconfiguration has emerged as a critical task in the face of evolving and dynamic network systems, posing potential risks to the security and reliability of the network service. Current network reconfiguration frameworks focus on security requirements, using brute-force methods to search for update sequences or employing Boolean expressions to generate updates. However, these approaches consider the simulator as a black box and fall short in fine-grained control and management of the reconfiguration process that induces operator-defined priority constraints.To solve the problem, we augment security specifications with priority specifications and propose CRONUS, CounteRexample-guided cOnstraint learning for Network Update Synthesis, the first framework that efficiently synthesizes network configuration updates while meeting both security and priority requirements. Our key contribution lies in the design of learning temporal constraints from counterexamples and automatic translation of priority specifications and learned constraints into a Verilog circuit model, enabling the use of a hardware model checker to efficiently generate the update sequence.We implemented and evaluated CRONUS on real-world and synthesized topologies. The results show that CRONUS achieves a 35× speedup in synthesis time on average compared to SOTA as the specification complexity increases and solves 96% of the reconfiguration tasks in 2 minutes.