Network-wide verification of invariants

A method for network-wide verification of invariants, the method executable by a computer having a processor and memory, the method comprising:

• retrieving from memory, using the processor, a representation of packet-forwarding rules installed in multiple network devices that control the flow of packets through a network;
• retrieving from memory, using the processor, multiple network invariants expected to be upheld in valid network operation as determined by a combined effect of packet-forwarding rules across multiple devices;
• verifying, using the processor, validity of invariants within the representation of the packet-forwarding rules of the network based on the retrieved network invariants, comprising:
• creating a representation of sets of packets that could be sent through the network in a form of multiple equivalence classes, each equivalence class experiencing common forwarding actions within the network;
• executing an equivalence class selection procedure to determine a set of equivalence classes exhibiting behavior that should be verified;
• and
• verifying the invariants of the network only within the selected equivalence classes.

A non-transitory computer-readable storage medium comprising a set of instructions to implement a data plane verification layer for network-wide verification of invariants by a computing device having a processor and memory, the computer readable medium comprising:

• instructions to direct the processor to obtain data comprising routing activity sent to a network controller by multiple network devices of a network;
• instructions to direct the processor to obtain packet-forwarding rules issued by a controller, where the controller is in network communication with the multiple network devices and configured to transmit the packet-forwarding rules to the multiple network devices;
• instructions to direct the processor to monitor packet-forwarding rule modifications in a network, including modifications initiated by the network devices and by the controller;
• instructions to direct the processor to retrieve from the memory network invariants expected to be upheld by valid network operations as determined by a combined effect of packet-forwarding rules across multiple devices;
• and
• instructions to direct the processor to verify the validity of invariants of the network according to the retrieved network invariants, where the verification is executed on parts of the network that take actions capable of being influenced by a new rule modification.