`make verify-iptables_blacklist` raise `AssertionError: The rule should no longer be in the map`

dslab-epfl / klint

Repository for the "Automated Verification of Network Function Binaries" paper (NSDI'22).

MIT License

8 stars 5 forks source link

`make verify-iptables_blacklist` raise `AssertionError: The rule should no longer be in the map` #7

Closed tharvik closed 1 year ago

tharvik commented 1 year ago

currently, verifying the iptables_blacklist NF doesn't work.

from what I gathered, it is the only spec where a branch is actually "Multivalued!". the assertion is actually sent by the spec, meaning in my understanding that the selected branch can't be taken. but in tool/klint/verif/symbex.py:_symbex, it actually try for a "choice" exception but not for a "bad branching" exception. maybe the constraints are too loose and this path shouldn't happen?

SolalPirelli commented 1 year ago

this is probably because of that heuristic I removed in the commit fixing the verification for others. Oops! We can do the same "remove, write the commit tag in readme for those interested" approach.