Minesweeper use learning

BGP test learning used by Minesweeper

1, BGP1

1. Import BGP1 network.

init-testrig /home/yahui/Desktop/batfish-abstraction-fixes/test_rigs/smt-examples/BGP1

The path here is the folder where the network configuration file is stored on the computer
The network is very small, with only two routers. It's about this long (I marked the ip address of loopback0 of R2 incorrectly, which should be 69.69.69.1):

After the import is successful, a long message is returned:

2. Test forwarding hops

Next, test the forwarding hops.

get smt-bounded-length finalNodeRegex="R1", finalIfaceRegex="Loopback.*", bound=1, fullModel=True

among

  1. SMT bounded length is the command to test the length,
  2. finalNodeRegex specifies that the end point is R1. (to specify the starting node, use ingressNodeRegex)
  3. finalfaceRegex is the interface that specifies the final traffic entry,
  4. bound specifies the upper limit of path forwarding hops,
  5. fullModel doesn't understand what it is.

The following are the results of the query

I don't understand what the result means.

The following is the statement to test whether the result is correct:

test /home/yahui/Desktop/batfish-abstraction-fixes/tests/java-smt/bgp1-bounded-len.ref get smt-bounded-length finalNodeRegex="R1", finalIfaceRegex="Loopback.*", bound=1, fullModel=True

It can be seen that the final result is Pass, which proves that the result is consistent with the expectation.

2, BGP2

The network of BGP2 is not much different from that of BGP1. (yes, the wrong one is inherited)

R2 has an external interface Serial1 connected to 192.168.43.2 (not shown in the figure).

1. Test forwarding hops

It is specified that the endpoint is R1 and the maximum hops are 1 and 0. We tested them respectively.

get smt-bounded-length finalNodeRegex="R1",bound=1
get smt-bounded-length finalNodeRegex="R1",bound=0


It is found that when the limit hop count is 1, nothing is returned; When it is 0, a packet to 192.168.42.1 is returned. The forwarding path is from the Serial0 interface of R2 to the Serial0 interface of R1 (does the bracket mean direct connection?)

It also specifies that the starting node is R1, and tests the case when the maximum hops are 1 and 0 respectively:

get smt-bounded-length ingressNodeRegex="R1",bound=1
get smt-bounded-length ingressNodeRegex="R1", bound=0



BGP appears here. It seems that this is different from the previous ones. Isn't it a direct connection? I don't know why this happens when the restrictions are different? Shouldn't it be connected in theory?

Specify that the starting node is R1, and specify the final interface. When the maximum hops of the test limit is 1:

get smt-bounded-length ingressNodeRegex="R1", finalIfaceRegex="Serial1.*", bound=1
get smt-bounded-length ingressNodeRegex="R1", finalIfaceRegex="Serial0.*", bound=1


Here, when the interface is the one external to R2, an error will be reported. However, shouldn't it just fail to meet the path forwarding hop limit? How can an error be reported (even the forwarding limit seems not to exist)

3, BGP3

The network of BGP3 is shown in the figure:

Beginners of computer network do not quite understand what it means. Personal feeling:

  • R1 first announced that its BGP network is 42.42.42.0/24
  • R1 declares that it has a neighbor 192.168.42.2 with number 200
  • R1 to 192.168 x. All data of X is forwarded according to ospf protocol
  • R2 is similar. It also announced that the data to 69.69.69.0/24 should be forwarded to the black hole route

Code interpretation of ospf declaration
ospf precise declaration and scope declaration
Black hole routing

1. Test forwarding hops

Specify R1 as the destination node, the destination ip is 42.42.42.0, and the destination interface is Loopback. *, The maximum forwarding times is limited to 1. (there is another parameter, negate. I don't know what it is.)

get smt-bounded-length finalNodeRegex="R1", dstIps=[42.42.42.0], finalIfaceRegex="Loopback.*", bound=1, negate=True
get smt-bounded-length finalNodeRegex="R1", dstIps=[42.42.42.0], finalIfaceRegex="Loopback.*", bound=1

2. Test forwarding

Test whether the route can be forwarded to the destination ip of 42.42.42.0 (that is, serial1 of R2)

get smt-forwarding dstIps=["42.42.42.0"]
get smt-forwarding dstIps=["192.168.42.2"]


Why is there a problem with this? Why is the path from R1 interface 0 to R2 interface 0 wrong?

Setting the destination ip to the ip address of interface 0 of R2 is still not possible. The only difference is that this road has been changed to direct connection. Try the ip address of interface 0 of R1 again, and the result is the same as that above.
I tried different ip addresses, and later found that the counterexample of this discovery is not the counterexample I imagined. This command may require that no traffic can flow into the destination ip. The return counterexample means that there is such a path that can flow into the ip.

3. Test whether it can be forwarded

The Serial0 interfaces of R1 and R2 are selected respectively. The following fullModel does not know what it is

get smt-reachability finalNodeRegex="R1", finalIfaceRegex="Serial0.*", fullModel=True
get smt-reachability finalNodeRegex="R2", finalIfaceRegex="Serial0.*", fullModel=True


As you can see, you can forward it

4. Test?

I don't know what this order means

get smt-routing-loop

4, Question

  • All questions raised above
  • What does the result mean? What do those things behind destport mean?
  • Does the Summary return all counterexamples?
  • According to the Question above, ACCEPT is returned, that is, the traffic passing through. So how to return the discarded traffic?

Keywords: network

Added by weekenthe9 on Tue, 18 Jan 2022 10:06:02 +0200