This is a network verification tool based on the DyNetKAT language which provides a reasoning method on reachability and waypointing properties for dynamic networks. DyNetiKAT utilizes Maude rewriting system and NetKAT decision procedure in the background.
Python (>= 3.7) including the package NumPy
NetKAT tool (netkat-idd or netkat-automata)
python dnk.py <path_to_maude> <path_to_netkat_tool> <input_file>
Options:
-h, --help show this help message and exit
-t NUM_THREADS, --threads=NUM_THREADS
number of threads (Default: the number of available cores in the system)
-p, --preprocessed pass this option if the given input file is already preprocessed
-v NETKAT_VERSION, --netkat-version=NETKAT_VERSION
the version of the netkat tool: netkat-idd or netkat-automata (Default: netkat-idd)
-s --time-stats reports the timing information.
For netkat-idd
tool, the path should be as follows: path_to_netkat_idd_build_dir/install/default/bin/katbv
.
For netkat-automata
tool, the path should be as follows: path_to_netkat_automata_build_dir/src/Decide_Repl.native
.
In the following we describe how the operators of NetKAT and DyNetKAT can be represented in in the tool. DyNetKAT operators are encoded as follows:
- The dummy policyis encoded as
bot
- The sequential composition operator is encoded as
arg1 ; arg2
. Here,arg1
can either be a NetKAT policy or a communication term andarg2
is always required to be a DyNetKAT term. - The communication terms sending and receiving are encoded as
arg1 ! arg2
andarg1 ? arg2
. Here,arg1
is a channel name andarg2
is a NetKAT policy. - The parallel composition of DyNetKAT policies is encoded as
arg1 || arg2
. - Non-deterministic choice of DyNetKAT policies is encoded as
arg1 o+ arg2
- The constant which pinpoints a communication step is encoded as
rcfg(arg1, arg2)
. Here,arg1
is a channel name andarg2
is a NetKAT policy. - Recursive variables are explicitly defined in the file that is given as input to the tool.
The NetKAT operators are encoded as follows:
- The predicate for dropping a packet is encoded as
zero
- The predicate which passes on a packet without any modification is encoded as
one
- The predicate which checks if the field
arg1
of a packet has the valuearg2
is encoded asarg1 = arg2
- The negation operator is encoded as
~ arg1
- The modification operator which assigns the value
arg2
into the fieldarg1
in the current packet is encoded asarg1 <- arg2
- The union (and disjunction) operator + is encoded as
arg1 + arg2
- The sequential composition (and conjunction) operator is encoded as
arg1 . arg2
- The iteration operator is encoded as
arg1 *
Two types of properties can be checked with DyNetiKAT: reachability and waypointing. Our procedure for checking such properties builds upon the methods introduced in NetKAT for checking reachability and waypointing properties. In NetKAT, these properties are defined with respect to an ingress point , an egress point , a switch policy , a topology and, a waypoint for waypointing properties. The following NetKAT equivalences characterize reachability and waypointing properties:
If the equivalence in (1) holds then this implies that the egress point is reachable from the ingress point. Analogously, if the equivalence in (2) holds then this implies that the egress point is not reachable from the ingress point. If the equivalence in (3) holds then this implies that all the packets from the ingress point to the egress point travel through the waypoint. DyNetKAT provides a mechanism that enables checking such properties in a dynamic setting. This entails utilizing the operators head(D)
and tail(D, R)
where D
is a DyNetKAT term and R
is a set of terms of shape rcfg(X, N).
Intuitively, the operator head(D)
returns a NetKAT policy which represents the current configuration in the input D
. The operator tail(D, R)
returns a DyNetKAT policy which is the sum of DyNetKAT policies inside D
that appear after the synchronization events in R
. Please see here for more details on the head
and tail
operators.
For a given DyNetKAT term D
we first apply our equational reasoning framework to unfold the expression and rewrite it into the normal form. This is achieved by utilizing the projection operator . Note that the number of unfoldings (i.e. the value n
inside the projection operator) is a fixed value specified by the user. We then apply the restriction operator on the resulting expression and eliminate the terms of shape X!Z
and X?Z
. That is, we compute the term where H is the set of all terms of shape X!Z
and X?Z
that appear in D
. Then, we extract the desired configurations by using the head and tail operators. After this step, the resulting expression is a purely NetKAT term and we utilize the NetKAT decision procedure for checking the desired properties.
In our tool a property is defined as a 4-tuple containing the following elements:
- The first element describes the type of property and can be either
r
orw
wherer
denotes a reachability property andw
denotes a waypointing property. - The second element is the property itself. The constructs that can be used to define a property are as follows:
head(@Program)
,tail(@Program, R)
. Here,@Program
is a special construct that refers to DyNetKAT program that is given as input, andR
is a set containing elements of shapercfg(X,N)
. - For reachability properties, the third element can be either
!0
or=0
where!0
denotes that the associated egress point should be reachable from the associated ingress point, whereas=0
denotes that the associated egress should be unreachable from the associated ingress point. For waypointing properties, the third element is a predicate which denotes the waypoint. - The fourth element denotes the maximum number of unfoldings to perform in the projection operator.
For an example, (r, head(@Program), !0, 100)
encodes a reachability property and (w, head(@Program), sw = 1, 100)
encodes a waypointing property. Furthermore, every property is associated with an ingress point and an egress point.
The input to DyNetiKAT is a .json file which contains the following data:
- in_packets: A dictionary with predicates describing the ingress points, e.g.:
{"first_packet": "sw = 1 . pt = 1", "second_packet": "sw = 2 . pt = 2"}
Note that every element in this dictionary must have a corresponding element in out_packets with the same key.
- out_packets: A dictionary with predicates describing the egress points, e.g.:
{"first_packet": "sw = 2 . pt = 2", "second_packet": "sw = 1 . pt = 1"}
As aforementioned, every element in this dictionary must have a corresponding element in in_packets with the same key.
- recursive_variables: Names and definitions of recursive variables that appear in the program, e.g.:
{"Switch": "\"(pt = 1 . pt <- 2)\" ; Switch o+ (secConReq ? \"one\") ; SwitchPrime"}
Note that the NetKAT terms inside the definitions must be enclosed with double quotes.
-
channels: A list containing the names of the channels that appear in the program.
-
program: The program to execute.
-
module_name: The name of the program. The output files will be based on this name.
-
properties: A dictionary which contains a list of properties. All the properties are associated with an ingress and egress point from the in_packets and out_packets. For example, consider the following encoding:
{ "first_packet": [["r", "head(@Program)", "!0", 100], ["w", "head(@Program)", "sw = 1", 100]], "second_packet": [[ "r", "head(@Program)", "!0", 100]] }
The above encoding defines a reachability property and a waypointing property for the
first_packet
and a reachability property for thesecond_packet
.
Sample input files can be found under the folder benchmarks
.
The FatTree topologies and the associated properties that are described here (Section 5) can be generated using the script fattree.py
under the folder benchmarks
. This script requires Python 3 and the package NetworkX.
We observed that in certain cases the netkat-idd
tool raises the following error: (Invalid_argument "union: not right-associative!")
. You may want to use the netkat-automata
tool in these cases.