IP Library › Granted Patent US 12,395,418
Granted Patent B2
US 12,395,418 · App. 18/017,654 · Granted Aug 19, 2025

Network verification systems and methods

Inventors: Ryan Andrew Beckett (Redmond, WA); Karthick Jayaraman (Kirkland, WA); Neha Milind Raje (Redmond, WA); Jitendra Padhye (Redmond, WA); Christopher Scott Johnston (Redmond, WA); Steven Jeffrey Benaloh (Seattle, WA); Nikolaj Bjorner (Woodinville, WA); Andrey Aleksandrovic Rybalchenko (Cambridge, GB); Nuno Cerqueira Afonso (Cambridge, GB); Nuno Claudino Pereira Lopes (Cambridge, GB); Sharad Agarwal (Seattle, WA); Hang Kwong Lee (Issaquah, WA); Aniruddha Parkhi (Bothell, WA); Maik Riechert (Cambridge, GB)
Assignee: Microsoft Technology Licensing, LLC
H04L43/50H04L41/145H04L43/06
View Patent ↗
Loading inventors, assignments & file history…
Monitor This Case
Get email alerts when status or documents change.
Order Certified Copies
Most orders are placed with the USPTO same day — all within 24 business hours.
Order via The Patent Place →
Pre-filled with this patent's details
Quick Facts
Patent No.
US 12,395,418
App. No.
18/017,654
Granted
Aug 19, 2025
Kind
B2
Abstract

A network verification system uses general-purpose programming language to create network verification tests. A test orchestrator builds a model of the network only using data from the network verification test. An optimization testing manager creates symbolic packets for verification tests using assertions based on a packet library embedded into the testing manager and the general-purpose programming language.

Claims (44)

1. A method, comprising:

identifying a network change to be implemented on a network, the network change affecting transfer of data packets through the network, the network being implemented on a cloud computing network;

receiving a network verification test including test parameters determined to correlate to network elements affected by the network change, the network verification test including one or more invariants, wherein the one or more invariants include a condition for the transfer of the data packets through the network, and wherein the network verification test tests the transfer of the data packets through the network;

retrieving network data from the network elements identified by the test parameters;

building a representation of the network from the network data on which to run the network verification test, the representation of the network including representations of the network elements identified by the test parameters, the representation of the network being configured to transfer simulated data packets across the network elements; and

applying the network verification test to the representation of the network data to determine whether the condition included in the one or more invariants is satisfied.

2. The method of claim 1 , wherein the network data includes at least one of network topology, device metadata, IP addressing information, routing tables, or device configurations.

3. The method of claim 2 , wherein applying the network verification test includes testing at least one element of the network data.

4. The method of claim 1 , wherein building the representation of the network includes building the representation of the network only from the network data received from the network elements.

5. The method of claim 1 , wherein the network verification test is written in a general-purpose programming language.

6. The method of claim 1 , wherein the network verification test is separate from the representation of the network.

7. The method of claim 1 , further comprising preparing a test report including results of the network verification test.

8. The method of claim 7 , wherein the test report includes results from each of multiple elements of the network verification test.

9. The method of claim 1 , wherein receiving the network verification test includes identifying the test parameters from the network verification test.

10. The method of claim 1 , wherein building the representation of the network includes generating a network graph of the network.

11. A system, comprising:

one or more processors;

a memory in electronic communication with the one or more processors; and

instructions stored in the memory, the instructions being executable by the one or more processors to:

receive a network change to be implemented on a network, the network change affecting transfer of data packets through the network, the network being implemented on a cloud computing network;

receive a network verification test;

identify test parameters from the network verification test that correlate to specific network elements that will be affected by the network change, the test parameters including one or more invariants, wherein the one or more invariants include a condition for the transfer of data packets through the network, and wherein the network verification test tests the transfer of data packets and identifies network elements relevant to the transfer of the data packets through the network;

retrieve network data from the network elements identified by the test parameters;

build a representation of the network from the network data on which to run the network verification test, the representation of the network including representations of the network elements identified by the test parameters, the representation of the network being configured to transfer simulated data packets across the network elements;

generate a symbolic packet based on an equivalence class for a plurality of data packets, the equivalence class correlating the plurality of data packets based on a similar data packet trait used to test the condition of the one or more invariants; and

apply the network verification test to the symbolic packet to determine whether the condition included in the one or more invariants is satisfied.

12. The system of claim 11 , wherein the network verification test is written in a general-purpose programming language.

13. The system of claim 11 , wherein the network verification test is separate from the representation of the network.

14. The system claim 11 , wherein generating the symbolic packet includes:

creating an abstract syntax tree based on a packet assertion in the network verification test; and

analyzing the abstract syntax tree with a binary decision diagram.

15. The system claim 11 , wherein generating the symbolic packet includes:

creating an abstract syntax tree based on a packet assertion in the network verification test; and

analyzing the abstract syntax tree with a binary decision diagram.

16. A method, comprising:

identifying a network change to be implemented on a network, the network change affecting transfer of data packets through the network, the network being implemented on a virtual network;

receiving a network verification test including test parameters determined to correlate to network elements affected by the network change, the network verification test including one or more invariants, wherein the one or more invariants include a condition for the transfer of the data packets through the network, and wherein the network verification test tests the transfer of the data packets through the network;

retrieving network data from the network elements identified by the test parameters;

building a representation of the network from the network data on which to run the network verification test, the representation of the network including representations of the network elements identified by the test parameters, the representation of the network being configured to transfer simulated data packets across the network elements; and

applying the network verification test to the representation of the network data to determine whether the condition included in the one or more invariants is satisfied.

17. The method of claim 16 , wherein the network data includes at least one of network topology, device metadata, IP addressing information, routing tables, or device configurations.

18. The method of claim 17 , wherein applying the network verification test includes testing at least one element of the network data.

19. The method of claim 16 , wherein building the representation of the network includes building the representation of the network only from the network data received from the network elements.

20. The method of claim 16 , wherein the network verification test is written in a general-purpose programming language.

Assignments (1)
ASSIGNMENT OF ASSIGNOR'S INTEREST Recorded Jan 24, 2023
From: BECKETT, RYAN ANDREW; JAYARAMAN, KARTHICK; RAJE, NEHA MILIND; PADHYE, JITENDRA; JOHNSTON, CHRISTOPHER SCOTT; BENALOH, STEVEN JEFFREY; BJORNER, NIKOLAJ; RYBALCHENKO, ANDREY ALEKSANDROVIC; CERQUEIRA AFONSO, NUNO; CLAUDINO PEREIRA LOPES, NUNO; AGARWAL, SHARAD; LEE, HANG KWONG; PARKHI, ANIRUDDHA; RIECHERT, MAIK
To: MICROSOFT TECHNOLOGY LICENSING, LLC
Reel/Frame 062477/0911 →
Continuity (3)
Continuation In Part 17115379 · Dec 8, 2020
Provisional Application 63055812 · Jul 23, 2020
Related Publication 20230300053A1 · Sep 21, 2023
References Cited (61)
US 7342897B1 · Nader et al. · 2008 [cited by applicant]
US 7978601B1 · Croak et al. · 2011 [cited by applicant]
US 8611219B2 · Golic · 2013 [cited by applicant]
US 9929915B2 · Erickson et al. · 2018 [cited by applicant]
US 10686671B1 · Mozumdar · 2020 [cited by examiner]
US 20140026123A1 · Dhanapal · 2014 [cited by examiner]
US 20160373334A1 · Gintis et al. · 2016 [cited by applicant]
US 20170155569A1 · Chinnaswamy et al. · 2017 [cited by applicant]
US 20180375730A1 · Anand et al. · 2018 [cited by applicant]
US 20190044790A1 · Dickens · 2019 [cited by examiner]
US 20190334807A1 · Clark et al. · 2019 [cited by applicant]
US 20200067788A1 · Thakkar · 2020 [cited by examiner]
US 20200106676A1 · Duda et al. · 2020 [cited by applicant]
Communication Pursuant to Rule 71 (3) Received for European Application No. 21727654.2, mailed on Nov. 17, 2023, 09 pages. [cited by applicant]
European Decision to Grant for European Application No. 21727654.2, dated Mar. 21, 2024, 2 pages. [cited by applicant]
“Notice of Allowance Issued in U.S. Appl. No. 17/115,379”, Mailed Date: May 13, 2021, 10 Pages. [cited by applicant]
Anderson, et al., “NetKat: Semantic Foundations for Networks”, In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan. 22, 2014, pp. 113-126. [cited by applicant]
Armstrong, et al., “Challenges in the Automatic Parallelization of Large-scale Computational Applications”, In Commercial Applications for High-Performance Computing, Jul. 27, 2001, 11 Pages. [cited by applicant]
Beckett, et al., “A General Approach to Network Configuration Verification”, In Proceedings of the Conference of the ACM Special Interest Group on Data Communication, Aug. 21, 2017, pp. 155-168. [cited by applicant]
Beckett, et al., “Don't Mind the Gap: Bridging Network-wide Objectives and Device-level Configurations”, In Proceedings of the ACM SIGCOMM Conference, Aug. 22, 2016, pp. 328-341. [cited by applicant]
Beckett, et al., “Network Configuration Synthesis with Abstract Topologies”, In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun. 18, 2017, pp. 437-451. [cited by applicant]
Beckett, et al., “Putting Network Verification to Good Use”, In Proceedings of the 18th ACM Workshop on Hot Topics in Networks, Nov. 13, 2019, pp. 77-84. [cited by applicant]
Bjørner, et al., “ddNF: An Efficient Data Structure for Header Spaces”, In Haifa Verification Conference, Nov. 14, 2016, 16 Pages. [cited by applicant]
Brace, et al., “Efficient Implementation of a BDD Package”, In Proceedings of 27th ACM/IEEE Design Automation Conference, Jun. 24, 1990, pp. 40-45. [cited by applicant]
Bryant, Randal E., “Chain Reduction for Binary and Zero-suppressed Decision Diagrams”, In Repository of arXiv:1710.06500v1, Oct. 17, 2017, pp. 1-21. [cited by applicant]
Canini, et al., “A Nice Way to Test OpenFlow Applications”, In Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation, Apr. 25, 2012, 14 Pages. [cited by applicant]
Dobrescu, et al., “Software Dataplane Verification”, In Proceedings of 11th USENIX Symposium on Networked Systems Design and Implementation, Apr. 2, 2014, pp. 101-114. [cited by applicant]
El-Hassany, et al., “NetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion”, In Proceedings of 15th USENIX Symposium on Networked Systems Design and Implementation, Apr. 9, 2018, pp. 579-594. [cited by applicant]
El-Hassany, et al., “Network-Wide Configuration Synthesis”, In Repository of arXiv:1611.02537v1, Nov. 8, 2016, pp. 1-30. [cited by applicant]
Fayaz, et al., “Efficient Network Reachability Analysis Using a Succinct Control Plane Representation”, In Proceedings of 12th USENIX Symposium on Operating Systems Design and Implementation, Nov. 2, 2016, pp. 217-232. [cited by applicant]
Fogel, et al., “A General Approach to Network Configuration Analysis”, In Proceedings of the 12th USENIX Symposium on Networked Systems Design and Implementation, May 4, 2015, pp. 469-483. [cited by applicant]
Gember-Jacobson, et al., “Fast Control Plane Analysis Using an Abstract Representation”, In Proceedings of the ACM SIGCOMM Conference, Aug. 22, 2016, pp. 300-313. [cited by applicant]
Gomes, et al., “Vericonn: A Tool to Generate Efficient Interconnection Networks for Post-silicon Debug”, In Proceedings of 16th Latin-American Test Symposium, Mar. 25, 2015, 6 Pages. [cited by applicant]
Hardcastle, Jessica Lyons, “VMware Buys Veriflow for Network Monitoring, Verification”, Retrieved from: https://www.sdxcentral.com/articles/news/vmware-buys-veriflow-for-network-monitoring-verification/2019/08/, Aug. 16… [cited by applicant]
Horn, et al., “Delta-net: Real-time Network Verification using Atoms”, In Proceedings of 14th USENIX Symposium on Networked Systems Design and Implementation, Mar. 27, 2017, pp. 735-749. [cited by applicant]
Jayaraman, et al., “Validating Datacenters at Scale”, In Proceedings of the ACM Special Interest Group on Data Communication, Aug. 19, 2019, pp. 200-213. [cited by applicant]
Kazemian, et al., “Header Space Analysis: Static Checking for Networks”, In Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation, vol. 12, Apr. 25, 2012, 14 Pages. [cited by applicant]
Kazemian, et al., “Real Time Network Policy Checking Using Header Space Analysis”, In Proceedings of the 10th USENIX Conference on Networked Systems Design and Implementation, Apr. 2, 2013, 13 Pages. [cited by applicant]
Khurshid, et al., “VeriFlow: Verifying Network-wide Invariants in Real Time”, In Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation, Apr. 2, 2013, pp. 15-27. [cited by applicant]
Liu, et al., “p4v: Practical Verification for Programmable Data Planes”, In Proceedings of the Conference of the ACM Special Interest Group on Data Communication, Aug. 20, 2018, pp. 490-503. [cited by applicant]
Long, David E., “The Design of a Cache-Friendly BDD Library”, In Proceedings of the IEEE/ACM International Conference on Computer-aided Design, Nov. 1, 1998, pp. 639-645. [cited by applicant]
Lopes, et al., “Checking Beliefs in Dynamic Networks”, In Proceedings of 12th USENIX Symposium on Networked Systems Design and Implementation, May 4, 2015, pp. 499-512. [cited by applicant]
Lunden, Ingrid, “Forward Networks Raises $35M to Help Enterprises Map, Track and Predict their Networks' Behavior”, Retrieved from: https://techcrunch.com/2019/10/08/forward-networks-raises-35m-to-help-enterprises-map-t… [cited by applicant]
Mai, et al., “Debugging the Data Plane with Anteater”, In Proceedings of the ACM SIGCOMM Conference, Aug. 15, 2011, pp. 290-301. [cited by applicant]
Panda, et al., “Verifying Reachability in Networks with Mutable Datapaths”, In Proceedings of the 14th USENIX Symposium on Networked Systems Design and Implementation, Mar. 27, 2017, pp. 699-718. [cited by applicant]
Zhu, et al., “Packet-Level Telemetry in Large Datacenter Networks”, In Proceedings of the ACM Conference on Special Interest Group on Data Communication, Aug. 17, 2015, pp. 479-491. [cited by applicant]
Scudder, et al., “BGP Monitoring Protocol (BMP)”, Retrieved from: https://www.rfc-editor.org/rfc/rfc7854.html, Jun. 2016, 27 Pages. [cited by applicant]
Soulé, et al., “Merlin: A Language for Provisioning Network Resources”, In Proceedings of the 10th ACM International on Conference on Emerging Networking Experiments and Technologies, Dec. 2, 2014, pp. 213-225. [cited by applicant]
Stoenescu, et al., “Debugging P4 Programs with Vera”, In Proceedings of the Conference of the ACM Special Interest Group on Data Communication, Aug. 20, 2018, pp. 518-532. [cited by applicant]
Sung, et al., “Robotron: Top-down Network Management at Facebook Scale”, In Proceedings of the ACM SIGCOMM Conference, Aug. 22, 2016, pp. 426-439. [cited by applicant]
Xie, et al., “On Static Reachability Analysis of IP Networks”, In Proceedings IEEE 24th Annual Joint Conference of the IEEE Computer and Communications Societies, vol. 3, Mar. 13, 2005, pp. 1-15. [cited by applicant]
Yang, et al., “Real-time Verification of Network Properties using Atomic Predicates”, In Journal of IEEE/ACM Transactions on Networking, vol. 24, Issue 2, Apr. 2016, pp. 887-900. [cited by applicant]
Zeng, et al., “Automatic Test Packet Generation”, In Proceedings of the 8th International Conference on Emerging Networking Experiments and Technologies, Dec. 10, 2012, pp. 241-252. [cited by applicant]
Zeng, et al., “Libra: Divide and Conquer to Verify Forwarding Tables in Huge Networks”, In Proceedings of 11th USENIX Symposium on Networked Systems Design and Implementation, Apr. 2, 2014, pp. 87-99. [cited by applicant]
U.S. Appl. No. 17/115,379, filed Dec. 8, 2020. [cited by applicant]
Li, et al., “A Survey on Network Verification and Testing With Formal Methods: Approaches and Challenges”, In Journal of IEEE Communications Surveys & Tutorials, vol. 21, Issue 1, Feb. 22, 2019, pp. 940-969. [cited by applicant]
Liu, et al., “CrystalNet: Faithfully Emulating Large Production Networks”, In Proceedings of the 26th Symposium on Operating Systems Principle, Oct. 28, 2017, pp. 599-613. [cited by applicant]
Marchetto, et al., “A Framework for Verification-Oriented User-Friendly Network Function Modeling”, In Journal of IEEE Access, vol. 7, Aug. 7, 2019, pp. 99349-99359. [cited by applicant]
“International Search Report & Written Opinion Issued in PCT Application No. PCT/US21/030028”, Mailed Date: Jul. 2, 2021, 11 Pages. [cited by applicant]
Song, Jaeseung, “SymbexNet: Checking Network Protocol Implementations using Symbolic Execution”, In Thesis of Imperial College London, Feb. 2013, 150 Pages. [cited by applicant]
Yuan, et al., “NetSMC: A Custom Symbolic Model Checker for Stateful Network Verification”, In Proceedings of 17th USENIX Symposium on Networked Systems Design and Implementation, Feb. 25, 2020, 20 Pages. [cited by applicant]