netarch / neo

A network testing tool combining formal model checking and container-based emulation that covers in-network non-determinism
Other
8 stars 4 forks source link

Assertion failure in Emulation::rewind() [dynamic port problem] #15

Closed kyechou closed 2 years ago

kyechou commented 2 years ago
./examples/04-squid/run.sh

Output: https://hastebin.com/viwuqaneja

The issue is somewhat similar to #12. During the rewind, new connections spawned by the middleboxes will have L4 source port numbers different from the ones in the packet history and the spin state.

The solution may be to intentionally leave out the source port numbers when the packets are received from the middleboxes (and hence also the destination port numbers when the packets are sent to the middleboxes), by fixing them to a concrete, constant value. We may similarly save the offsets within class Emulation, and update them accordingly.