Bug with the iptables overlay and transit

[jkhourybbn]

Related to #462

Hi Ari/Ratul,

I am attaching a very simple test rig which has 2 zones

z1-host1 <--> z1-firewall <--> r1 <--> r2  <--> z2-firewall <--> z2-host1

The following query and output is anomalous. Even though I am fixing the dstIp in the query (verified it against the NoD program), z3 returns an answer that effectively ignores the dstIp constraints. This seems to happen only with transit.

batfish> get reachability notIngressNodeRegex="z1-.*", dstIps=["10.0.3.20"], notTransitNodes=["z1-firewall"]
Status: SUCCESS
Question: reachability actions=[ACCEPT] | dstIps=[10.0.3.20] | notIngressNodeRegex=z1-.* | notTransitNodes=[z1-firewall]

Flow: ingress:z2-firewall vrf:default 0.0.0.0->10.0.1.10 ICMP icmpType:255 icmpCode:255 packetLength:0 state:NEW
  environment:BASE
    ACCEPTED

Flow: ingress:z2-host1 vrf:default 10.0.4.0->10.0.4.1 UDP sport:0 dport:0 packetLength:0 state:NEW
  environment:BASE
    Hop 1: z2-host1:eth0 -> z2-firewall:Ethernet1 --- [ConnectedRoute<10.0.4.0/24,nhip:AUTO/NONE(-1l),nhint:eth0>_fnhip:null]
    ACCEPTED

I spent a couple hours chasing the potential problem in z3 but I am slow at z3 still. Can you take a look? We can add this unit test once we figure out the problem.

[jkhourybbn]

Here is an even simpler version of the unit test where the problem persists (for easier debugging)

z1-host1 <--> z1-firewall <-->  z2-firewall <--> z2-host1

updated the test rig (there was a small glitch in it)
testrigvs.tar.gz

[jkhourybbn]

It looks like the iptables rules are not being converted correctly, I will open a separate ticket for it

[jkhourybbn]

resuming the discussion on #464

[arifogel]

Since #464 is closed, is this bug fixed too? Can we close?

[jkhourybbn]

Ari, lets keep this open and use it to discuss the NoD anomalies I am seeing. Ill see if I can recreate those now that iptables is fixed.

[dhalperi]

Related to #317 ?

[dhalperi]

@jkhourybbn – any more information to provide here?

[jkhourybbn]

@dhalperi I will work on this tomorrow. I will either provide an example by Thursday or close this out. Tx

[jkhourybbn]

@arifogel Here is a detailed account of the NoD inconsistency (or likely something I am missing)

Consider the following testrig.zip

See the diagram, this is a very simple network that is partitioned, on purpose. I basically removed the link between the firewalls.

Now if you run a simple transit query on the network

get reachability notIngressNodeRegex="z1-.*", dstIps=["10.0.3.20"], notTransitNodes=["z1-firewall"], actions=["ACCEPT"]

NoD here returns a result that doesn't match the query, see how the dstIP is different than the one in the query. This query should return no results instead because the flow did not transit through z1-firewall. Looking at the NoD query it seems fine, but I guess there must be some inconsistency in the program somewhere when the link is removed

Flow: ingress:z2-firewall vrf:default 0.0.0.0->10.0.4.1 ICMP icmpType:255 icmpCode:255 packetLength:0 state:NEW

Thoughts?

[ratulm]

@arifogel, can you follow up here?

[arifogel]

On my queue..

[arifogel]

Appears to be a bug with z3.
I filed Z3Prover/z3#1452 as a minimized version of one of the queries formed by your reachability question.

[arifogel]

Closed via #853
Note that you may have to reinstall Z3 using the appropriate script from the tools folder. A full rebuild should follow to ensure the Java API jar for z3 is updated.

[jkhoury]

tx folks