hcantunc / dynetikat Goto Github PK

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

Maude (>= 3.0)

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 and arg2 is always required to be a DyNetKAT term.
• The communication terms sending and receiving are encoded as arg1 ! arg2 and arg1 ? arg2. Here, arg1 is a channel name and arg2 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 and arg2 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 value arg2 is encoded as arg1 = arg2
• The negation operator is encoded as ~ arg1
• The modification operator which assigns the value arg2 into the field arg1 in the current packet is encoded as arg1 <- 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:

1. 
2. 
3. +

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:

1. The first element describes the type of property and can be either r or w where r denotes a reachability property and w denotes a waypointing property.
2. 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, and R is a set containing elements of shape rcfg(X,N).
3. 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.
4. 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.