Identification of conflict rules in a network intent formal equivalence failure
First Claim
1. A method comprising:
- obtaining, via one or more processors and from one or more network controllers, at least a first model of network intents and a second model of network intents, the first model and the second model describing an operation and communication between one or more network devices in a network based on one or more network policies configured at the one or more network controllers;
calculating, via the one or more processors, a logical exclusive disjunction between the first model of network intents and the second model of network intents, wherein the logical exclusive disjunction is calculated over a space of possible packet conditions and network actions defined by the first and second models, the calculating performed without enumerating all possible packet conditions and network actions;
based on the logical exclusive disjunction, detecting, via the one or more processors, whether the first model and second model are in conflict with respect to at least a first network device of the one or more network devices; and
in response to detecting that the first and second model are in conflict, determining, for one or more given rules of a plurality of rules associated with the first model of network intents, whether the given rule is a conflict rule, wherein the determining comprises calculating the intersection between the given rule and the logical exclusive disjunction such that the given rule is a conflict rule if the calculated intersection is non-zero.
1 Assignment
0 Petitions
Accused Products
Abstract
Systems, methods, and computer-readable media for identifying conflict rules between models of network intents. A first and second model of network intents are obtained, the models describing the operation and communication between one or more network devices in a network. A logical exclusive disjunction between the first and second models is calculated over the space of possible packet conditions and network actions defined by models, without enumerating all possible packet conditions and network actions. It is detected whether the models are in conflict with respect to at least a first network device. If the models are in conflict, it is determined whether a given rule of a plurality of rules associated with the first model is a conflict rule. The determining comprises calculating the intersection between the given rule and the logical exclusive disjunction, wherein the given rule is a conflict rule if the calculated intersection is non-zero.
181 Citations
20 Claims
-
1. A method comprising:
-
obtaining, via one or more processors and from one or more network controllers, at least a first model of network intents and a second model of network intents, the first model and the second model describing an operation and communication between one or more network devices in a network based on one or more network policies configured at the one or more network controllers; calculating, via the one or more processors, a logical exclusive disjunction between the first model of network intents and the second model of network intents, wherein the logical exclusive disjunction is calculated over a space of possible packet conditions and network actions defined by the first and second models, the calculating performed without enumerating all possible packet conditions and network actions; based on the logical exclusive disjunction, detecting, via the one or more processors, whether the first model and second model are in conflict with respect to at least a first network device of the one or more network devices; and in response to detecting that the first and second model are in conflict, determining, for one or more given rules of a plurality of rules associated with the first model of network intents, whether the given rule is a conflict rule, wherein the determining comprises calculating the intersection between the given rule and the logical exclusive disjunction such that the given rule is a conflict rule if the calculated intersection is non-zero. - View Dependent Claims (2, 3, 4, 5, 6, 7)
-
-
8. A system comprising:
-
one or more processors; and at least one computer-readable storage medium having stored therein instructions which, when executed by the one or more processors, cause the system to; obtain, from one or more network controllers, at least a first model of network intents and a second model of network intents, the first model and the second model describing an operation and communication between one or more network devices in a network based on one or more network policies configured at the one or more network controllers; calculate a logical exclusive disjunction between the first model of network intents and the second model of network intents, wherein the logical exclusive disjunction is calculated over a space of possible packet conditions and network actions defined by the first and second models, the calculating performed without enumerating all possible packet conditions and network actions; based on the logical exclusive disjunction, detect whether the first model and second model are in conflict with respect to at least a first network device of the one or more network devices; and in response to detecting that the first and second model are in conflict, determine for one or more given rules of a plurality of rules associated with the first model of network intents whether the given rule is a conflict rule, wherein the determining comprises calculating the intersection between the given rule and the logical exclusive disjunction such that the given rule is a conflict rule if the calculated intersection is non-zero. - View Dependent Claims (9, 10, 11, 12, 13)
-
-
14. A non-transitory computer-readable storage medium comprising:
-
instructions stored therein which, when executed by one or more processors, cause the one or more processors to; obtain, from one or more network controllers, at least a first model of network intents and a second model of network intents, the first model and the second model describing an operation and communication between one or more network devices in a network based on one or more network policies configured at the one or more network controllers; calculate a logical exclusive disjunction between the first model of network intents and the second model of network intents, wherein the logical exclusive disjunction is calculated over a space of possible packet conditions and network actions defined by the first and second models, the calculating performed without enumerating all possible packet conditions and network actions; based on the logical exclusive disjunction, detect whether the first model and second model are in conflict with respect to at least a first network device of the one or more network devices; and in response to detecting that the first and second model are in conflict, determine for one or more given rules of a plurality of rules associated with the first model of network intents whether the given rule is a conflict rule, by calculating an intersection between the given rule and the logical exclusive disjunction such that the given rule is a conflict rule if the calculated intersection is non-zero. - View Dependent Claims (15, 16, 17, 18, 19, 20)
-
Specification