# US 10,771,342 B2 · Encoding and verifying network intents for stateful networks > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 10,771,342 B2 - Document ID: US10771342B2 - Status: Granted - Kind: B2 - Application number: 16/176,905 - Filed: 2018-10-31 - Published: 2020-04-30 - Granted: 2020-09-08 - Earliest claimed: 2018-10-31 - Assignees: Hewlett Packard Enterprises Development LP - Applicants: Hewlett Packard Enterprise Development LP - Inventors: Joon-Myung Kang; Huazhe Wang; Puneet Sharma - Web page: https://patentgrep.com/patent/US10771342B2 ## CPC - H04L 63/0254: {Stateful filtering} - H04L 43/0817: by checking functioning - H04L 61/2567: for reachability, e.g. inquiring the address of a correspondent behind a NAT server - H04L 61/2575: using address mapping retrieval, e.g. simple traversal of user datagram protocol through session traversal utilities for NAT [STUN] - H04L 61/2591: {Identification of devices behind NAT devices} - H04L 63/0281: {Proxies} - H04L 61/2514: between local and global IP addresses - H04L: TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION (arrangements common to telegraphic and telephonic communication H04M) ## 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 ### Claim 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. ### Claim 2 (depends on 1) 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. ### Claim 3 (depends on 2) 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. ### Claim 4 (depends on 2) 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. ### Claim 5 (depends on 4) 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. ### Claim 6 (depends on 1) 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. ### Claim 7 (depends on 6) 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. ### Claim 8 (depends on 6) 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. ### Claim 9 (depends on 8) 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. ### Claim 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. ### Claim 11 (depends on 10) 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. ### Claim 12 (depends on 11) 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. ### Claim 13 (depends on 11) 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. ### Claim 14 (depends on 13) 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. ### Claim 15 (depends on 10) 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. ### Claim 16 (depends on 15) 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. ### Claim 17 (depends on 16) 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. ### Claim 18 (depends on 17) 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. ### Claim 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. ### Claim 20 (depends on 19) 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.