Microsoft Technology Licensing, LLC

Karthick Jayaraman

Nikolaj Skallerud Bjorner

Ryan Andrew Beckett

Jitendra Dattatraya Padhye

Neha Milind Raje

Christopher Scott Johnston

Steven Jeffrey Benaloh

Sharad Agarwal

Geoffrey Hugh Outhred

Rachee Singh

Nuno Claudino Pereira Lopes

Hang Kwong Lee

Wei Bai

Maik Riechert

Andrey Aleksandrovic Rybalchenko

Nuno Cerqueira Afonso

Aniruddha Parkhi

Sarah Elisabeth McClure

Charles W Kaufman

Sarah Elisabeth Mcclure

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.

Network verification systems and methods

Ghost routing is a network verification technique that uses a portion of a production network itself to verify the impact of potential network changes. Ghost routing logically partitions the production network into a main network and a ghost network. The main network handles live traffic while the ghost network handles traffic generated for diagnostic purposes. The ghost network may have a network topology identical to the production network and may use the same hardware and software as the production network. An operator may implement a network configuration change on the ghost network and then use verification tools to verify that the network configuration change on the ghost network does not result in bugs. Verifying on the ghost network may not affect the main network. If the network operator verifies the network configuration change on the ghost network, the network operator may implement the network configuration change on the main network.

Ghost routing

Techniques of network configuration verification are disclosed herein. One example process includes, upon receiving a query to determine whether a packet from a first endpoint is reachable to a second endpoint in a virtual network, identifying a network path between the first endpoint to the second endpoint in a network graph. The network graph has nodes representing corresponding enforcement points of network policies in the virtual network and edges connecting pairs of the nodes. The example process can also include generating compound function representing conjoined individual constraints of the network policies at each of the nodes in the network graph along the identified network path, compiling the generated compound function into a Boolean formula, and solving the compiled Boolean formula to determine whether an assignment of values to packet fields of the packet exists such that all the conjoined individual constraints of the compound function can be satisfied.

Network configuration verification in computing systems

A system performed by a computing device for validating routing tables of routing devices is provided. The routing tables map destination addresses to a next hops of the routing device. The system accesses one or more contracts that specify the desired behavior of a routing table of a routing device by specifying destination addresses and permissible next hops. For each routing device, the system generates a violation predicate for each contract that is applicable to the routing device. When a violation predicate is evaluated for a target destination address and a target next hop of the routing device, the violation predicate indicates whether the routing table violates the contract. The system then solves the violation predicates for all possible combinations of a target destination address and target next hops to determine whether any routing table violates the desired behavior of its routing device as specified by a contract.

Validating routing tables of routing devices

A system is described that analyzes and validates network security policies associated with network devices. The system includes a compiler and a security policy analysis and validation tool. The compiler encodes a security policy associated with a network device into a predicate expressed in bit-vector logic and generates a bit-vector formula based on the predicate. The tool receives the bit-vector formula and applies a Satisfiability Modulo Theories (SMT) solver thereto to identify and enumerate solutions to the bit-vector formula. The enumerated solutions provide information about the validity of the first security policy. The solutions may be compactly enumerated in a as product of intervals or a product of unions of intervals.

System and method for compact form exhaustive analysis of security policies

Growing community of inventors

Kirkland, WA, United States of America

Karthick Jayaraman