Incremental intent checking for stateful networks
View Patent ↗An example method including identifying an intent-based stateful network having a first endpoint, a second endpoint, and one or more devices performing stateful network functions between the first endpoint and the second endpoint. Further, constructing a causality graph of the network, the causality graph having a plurality of nodes for each of the one or more devices performing stateful network functions, wherein the connecting comprises connecting the first endpoint, the second endpoint, and the one or more devices performing stateful network functions to show causal relationships between the first endpoint and the second endpoint and the one or more devices performing stateful network functions. Also, determining whether the connections between the first endpoint, the second endpoint, and the one or more devices performing stateful network functions provide a path from the first endpoint and the second endpoint, and updating, incrementally, the causality graph as a change to the network occurs.
1. A method of incremental intent checking with a computing device, the method comprising:
identifying an intent-based stateful network having a first endpoint, a second endpoint, and one or more devices performing stateful network functions between the first endpoint and the second endpoint;
constructing a causality graph of the network, the causality graph comprising a plurality of nodes for each of the one or more devices performing stateful network functions, each node representing a respective packet sending event or a respective packet receiving event associated with a corresponding device performing a stateful network function, wherein the constructing comprises connecting the first endpoint, the second endpoint, and the one or more devices performing stateful network functions to show causal relationships between the first endpoint and the second endpoint and the one or more devices performing stateful network functions;
determining whether the connections between the first endpoint, the second endpoint, and the one or more devices performing stateful network functions provide a path from the first endpoint and the second endpoint; and
updating, incrementally, the causality graph as a change to the intent-based stateful network occurs.
2. The method of claim 1 , wherein the updating, incrementally, comprises at least one of adding and removing an edge between at least two nodes from the causality graph.
3. The method of claim 1 , wherein the determining comprises determining whether the path between the first and the second endpoints satisfies a network intent.
4. The method of claim 1 , wherein the network function performed by the one or more devices comprises at least one of a stateful firewall, a network address translator, and a load balancer.
5. The method of claim 1 , further comprising adding a rule to identify a set of intents that is affected by the change and updating the causality graph based on an effect the rule has on the network.
6. The method of claim 5 , wherein the updating the causality graph comprises at least one of adding an edge, adding an additional node, removing an edge, and removing an additional node.
7. The method of claim 1 , further comprising removing an edge from the causality graph when a loop is introduced by the change.
8. The method of claim 1 , wherein the path defines a reachability between the first endpoint and the second endpoint.
9. The method of claim 1 , further comprising using a Satisfiability Modulo Theories solver to determine whether the path between the first endpoint and the second endpoint exists.
10. The method of claim 1 , further comprising saving the updated causality graph for use in a subsequent network check.
11. The method of claim 1 , further comprising updating, automatically, the causality graph when a change to the network occurs.
12. A computing device comprising at least:
a memory; and
a processor executing instructions in the memory to:
identify an intent-based stateful network having a first endpoint, a second endpoint, and one or more devices performing stateful network functions between the first endpoint and the second endpoint;
construct a causality graph of the network, the causality graph comprising a plurality of nodes for each of the one or more devices performing stateful network functions, each node representing a respective packet sending event or a respective packet receiving event associated with a corresponding device performing a stateful network function, wherein the construction of the causality graph comprises connecting the first endpoint, the second endpoint, and the one or more devices performing stateful network functions to provide a path from the first endpoint and the second endpoint;
determine whether the connections between the first endpoint, the second endpoint, and the one or more devices performing stateful network functions provide a path from the first endpoint and the second endpoint; and
update, incrementally, the causality graph as a change to the intent-based stateful network occurs.
13. The computing device of claim 12 , wherein the processor further executes the instructions in the memory to add a rule to identify a set of intents that is affected by the change and updating the causality graph based on an effect the rule has on the network.
14. The computing device of claim 12 , wherein the processor further executes the instructions in the memory to remove an edge from the causality graph when a loop is introduced by the change.
15. The computing device of claim 12 , wherein the processor further executes the instructions in the memory to add an edge to the causality group when a new path in the network is established.
16. The computing device of claim 12 , wherein the processor further executes the instructions in the memory to use a satisfiability modulo theories solver to determine whether the path between the first endpoint and the second endpoint exists.
17. The computing device of claim 12 , wherein the processor further executes the instructions in the memory to identify a set of intents that are affected by the change and update the causality graph based on the set of intents that are affected by the change.
18. The computing device of claim 12 wherein the processor further executes the instructions in the memory to automatically update the causality graph when a change to the network occurs.
19. A non-transitory machine-readable storage medium encoded with instructions executable by a processor of a computing device, the non-transitory machine-readable storage medium comprising instructions to:
identify an intent-based stateful network having a first endpoint, a second endpoint, and one or more devices performing stateful network functions between the first endpoint and the second endpoint;
construct a causality graph of the network, the causality graph comprising a plurality of nodes for each of the one or more devices performing stateful network functions, each node representing a respective packet sending event or a respective packet receiving event associated with a corresponding device performing a stateful network function, wherein the construction of the causality graph comprises connecting the first endpoint, the second endpoint, and the one or more devices performing stateful network functions to provide a path from the first endpoint and the second endpoint;
determine whether the connections between the first endpoint, the second endpoint, and the one or more devices performing stateful network functions provide a path from the first endpoint and the second endpoint; and
update, incrementally, the causality graph as a change to the intent-based stateful network occurs.
20. The non-transitory machine-readable storage medium of claim 14 , further comprising instructions to identify a set of intents that are affected by the change and update the causality graph based on the set of intents that are affected by the change.