ENCODING AND VERIFYING NETWORK INTENTS FOR STATEFUL NETWORKS

• US 20200136917A1
• Filed: 10/31/2018
• Published: 04/30/2020
• Est. Priority Date: 10/31/2018
• Status: Active Grant

• Current Assignee: Hewlett Packard Enterprise Development LP (Hewlett-Packard Enterprise Company)
• Original Assignee: Hewlett Packard Enterprise Development LP (Hewlett-Packard Enterprise Company)
• Inventors: Kang, Joon-Myung, Wang, Huazhe, Sharma, Puneet
• Granted Patent: US 10,771,342 B2
• Time in Patent Office: Days
• CPC Class Codes: H04L 41/12 Discovery or management of network topologies
• CPC Class Codes: H04L 43/0817 by checking functioning
• CPC Class Codes: H04L 61/2514 between local and global IP addresses
• CPC Class Codes: H04L 61/2567 for reachability, e.g. inquiring the address of a correspondent behind a NAT server
• CPC Class Codes: H04L 61/2571 for identification, e.g. for authentication or billing charging arrangements H04L12/14
• CPC Class Codes: H04L 61/2575 using address mapping retrieval, e.g. simple traversal of user datagram protocol through session traversal utilities for NAT [STUN]
• CPC Class Codes: H04L 63/0254 Stateful filtering
• CPC Class Codes: H04L 63/0281 Proxies

Abstract

Example method includes: identifying three relationships about a network function in an intent-based stateful network—(1) the network function forwarding a network packet implies that at least one previous network packet was received by the network function in the same direction prior to the network packet is forwarded, (2) an established state in the network function implies that at least one previous network packet was received at the network function, (3) the network function receiving the network packet as a downward network function implies the network packet was previously sent by a second network function acting as an upward network function; encoding the network function using a combination of at least one of the three identified relationships; and verifying a plurality of network intents in the intent-based stateful network based at least in part on the encoding of the network function.

Claims

1. A method comprising:

identifying, by a computing device, three causal precedent relationships about a network function in an intent-based stateful network,

wherein a first causal precedent relationship indicates that the network function forwarding a network packet implies that at least one previous network packet was received by the network function in the same direction prior to the network packet is forwarded,

wherein a second causal precedent relationship indicates that an established state in the network function implies that at least one previous network packet was received at the network function,

wherein a third causal precedent relationship indicates that the network function receiving the network packet as a downward network function implies the network packet was previously sent by a second network function acting as an upward network function;

encoding, by the computing device, the network function using a combination of at least one of the three identified relationships; and

verifying, by the computing device, a plurality of network intents in the intent-based stateful network based at least in part on the encoding of the network function.

2. The method of claim 1, further comprising:

receiving a network topology comprising a plurality of endpoints, stateful middleboxes, and stateless devices;

extracting a network graph from the received network topology.

3. The method of claim 2, wherein extracting the network graph further comprising:

removing the plurality of stateless devices from the received network topology;

determining a plurality of feasible paths of network packets between at least two endpoints in the intent-based stateful network.

4. The method of claim 2, wherein verifying the plurality of network intents further comprising:

identifying a plurality of candidate paths in the network graph for the plurality of network intents; and

determining whether at least one path between the at least two endpoints exists that satisfy the plurality of network intents.

5. The method of claim 4, wherein determining whether the at least one path between the at least two endpoints exists further comprises:

determining a reachability between the at least two endpoints along each identified path;

using the encoding of the network function to determine how the network function along the each identified path processes network packets; and

using a satisfiability modulo theories (SMT) solver to determine whether the at least one path between the at least two endpoints exists.

6. The method of claim 1, further comprising:

constructing a model comprising a network graph and a plurality of encodings, wherein each encoding represents functionality of a particular type of network function acting as a middlebox.

7. The method of claim 6, wherein the middlebox comprises at least one of a stateful firewall, a network address translator, a load balancer, and a reverse proxy.

8. The method of claim 6, further comprising:

decomposing the model and a preconfigured set of network policies into two stages for verification of intent-based stateful network.

9. The method of claim 8, wherein decomposing the model and the preconfigured set of network policies comprises:

splitting a path into a plurality of sub-paths;

verifying reachability along each sub-path independently to produce a plurality of sub-path verification results;

combining the plurality of sub-path verification results at least based in part on states of the network function.

10. A computing device comprising at least:

a memory;

a processor executing instructions in the memory to;

identify three causal precedent relationships about a network function in an intent-based stateful network,

wherein a first causal precedent relationship indicates that the network function forwarding a network packet implies that at least one previous network packet was received by the network function in the same direction prior to the network packet is forwarded,

wherein a second causal precedent relationship indicates that an established state in the network function implies that at least one previous network packet was received at the network function,

wherein a third causal precedent relationship indicates that the network function receiving the network packet as a downward network function implies the network packet was previously sent by a second network function acting as an upward network function;

encode the network function using a combination of at least one of the three identified relationships; and

verify a plurality of network intents in the intent-based stateful network based at least in part on the encoding of the network function.

11. The computing device of claim 10, wherein the processor further executes the instructions in the memory to:

receive a network topology comprising a plurality of endpoints, stateful middleboxes, and stateless devices;

extract a network graph from the received network topology.

12. The computing device of claim 11, wherein while extracting the network graph, the processor further executes the instructions in the memory to:

remove the plurality of stateless devices from the received network topology; and

determine a plurality of feasible paths of network packets between at least two endpoints in the intent-based stateful network.

13. The computing device of claim 11, wherein while verifying the plurality of network intents, the processor further executes the instructions in the memory to:

identify a plurality of candidate paths in the network graph for the plurality of network intents; and

determine whether at least one path between the at least two endpoints exists that satisfy the plurality of network intents.

14. The computing device of claim 13, wherein while determining whether the at least one path between the at least two endpoints exists, the processor further executes the instructions in the memory to:

determine a reachability between the at least two endpoints along each identified path;

use the encoding of the network function to determine how the network function along the each identified path processes network packets; and

use a satisfiability modulo theories (SMT) solver to determine whether the at least one path between the at least two endpoints exists.

15. The computing device of claim 10, wherein the processor further executes the instructions in the memory to:

construct a model comprising a network graph and a plurality of encodings, wherein each encoding represents functionality of a particular type of network function acting as a middlebox.

16. The computing device of claim 15, wherein the middlebox comprises at least one of a stateful firewall, a network address translator, a load balancer, and a reverse proxy.

17. The computing device of claim 16, wherein the processor further executes the instructions in the memory to:

decompose the model and a preconfigured set of network policies into two stages for verification of intent-based stateful network.

18. The computing device of claim 17, wherein while decomposing the model and the preconfigured set of network policies, the processor further executes the instructions in the memory to:

split a path into a plurality of sub-paths;

verify reachability along each sub-path independently to produce a plurality of sub-path verification results;

combine the plurality of sub-path verification results at least based in part on states of the network function.

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 three causal precedent relationships about a network function in an intent-based stateful network,

wherein a first causal precedent relationship indicates that the network function forwarding a network packet implies that at least one previous network packet was received by the network function in the same direction prior to the network packet is forwarded,

wherein a second causal precedent relationship indicates that an established state in the network function implies that at least one previous network packet was received at the network function,

wherein a third causal precedent relationship indicates that the network function receiving the network packet as a downward network function implies the network packet was previously sent by a second network function acting as an upward network function;

encode the network function using a combination of at least one of the three identified relationships; and

verify a plurality of network intents in the intent-based stateful network based at least in part on the encoding of the network function.

20. The non-transitory machine-readable storage medium of claim 19, further comprising instructions to:

receive a network topology comprising a plurality of endpoints, stateful middleboxes, and stateless devices;

extract a network graph from the received network topology;

identify a plurality of candidate paths in the network graph for the plurality of network intents; and

determine whether at least one path between the at least two endpoints exist that satisfy the plurality of network intents.