Correctness issue with FaureEvaluation in Containment

[mudbri]

There is a correctness issue in FaureEvaluation when we use it for checking containment. Unit test 10 illustrates this issue. The program P:

\\ Program P
l(x)[And(x > 2, x  < 7)] :- R(x)[And(x > 2, x  < 7)], R(x)[And(x > 0, x  < 10)]

should be minimized as:

\\ Expected P_mininimzed
l(x)[And(x > 2, x  < 7)] :- R(x)[And(x > 2, x  < 7)]

But the actual minimization that our code outputs is:

\\ Actual P_mininimzed
l(x)[And(x > 2, x  < 7)] :-  R(x)[And(x > 0, x  < 10)]

Importance: Although this issue did not appear in any of our unit tests, it will appear when we work with firewalls. We will not be able to minimize ACLs properly if this issue is not fixed.

The root of the problem: We need to use a different valuation function for Faurelog when we are checking for containment. Currently, a Faurelog query q over a c_table T returns tuples that match the pattern matching in q and the conditions imposed by the valuation on the tuple do not contradict. That is, a tuple _ti in T will also be in the result if at least one instance of _ti matches the query. (Note that if there are c_variables in tuple _ti then the tuple represents multiple instances). However, for containment, we need to make sure that a tuple _ti appears in the output only if all possible instances of it match the query. Thus, we need a different valuation function. This is explained in the technical report. The valuation function should have the following rules:

1. Fauré-log variables are assigned to constants or c-variables (by simple substitution)
2. A constant c is assigned to either itself, or to a c- variable 𝑥 ˆ if the condition of 𝑥 ˆ imply the constrain 𝑥 ˆ = c
3. a c-variable 𝑦 ˆ is assigned to either (i) another constant c if the constrain 𝑦 ˆ = c implies the condition of 𝑦 ˆ or (ii) to another c-variable 𝑥 ˆ if the conditions of 𝑥 ˆ imply the conditions of 𝑦 ˆ

Note that we use implication rather than contradiction here to take into account all possible instances of the data table.

[mudbri]

Fix attempted by Fangping in commit d8c71d31784eecdff6a387ed3c6f621d9b4aa593

[mudbri]

I fixed some minor bugs in e0b15ff5d6aaf3433d9facd33c1e9fc3cb23e975. @lanfangping, there are still some correctness issues. Specifically, unit test 12 is failing. The test has two equivalent rules and attempts to perform rule minimization on them. Minimization should remove one of the rules, but none of the rules get removed. This issue seems to only appear with IPs. Can you please look into this?

[lanfangping]

Specifically, unit test 12 is failing. The test has two equivalent rules and attempts to perform rule minimization on them. Minimization should remove one of the rules, but none of the rules get removed. This issue seems to only appear with IPs. Can you please look into this?

@mudbri Hi Mubashir, I have fixed this bug. It was caused by the wrong parsing for the IP prefixes inequality condition for Z3. For example, for condition "D != 216.186.192.0/22", its z3 BitVec format should be "Or( z3.BitVec('D',32) < z3.BitVecVal('3636117504',32),z3.BitVec('D',32) > z3.BitVecVal('3636118527',32) )", but it was parsed to "And( z3.BitVec('D',32) <= z3.BitVecVal('3636117504',32),z3.BitVec('D',32) >= z3.BitVecVal('3636118527',32) )" which is a contradiction. Then it further causes the head containment check fails.

See commit e197fce8593336a0105f1806d89b6398aabdcffb and 3bd4b4f171d4e6845a53a00dbba4f65003b0baca