Dear Lucas,
On 27/03/2025 16:03, Lucas Aubard wrote:
I am Lucas Aubard. I am a PhD student in an Inria lab in Rennes, France.
This PhD is supervised by Gilles Guette (IMT Atlantique), Pierre Chifflier
(ANSSI) and Johan Mazel (ANSSI).
During our research work, we analyzed mirage-tcpip 9.0.0 reassembly when
processing overlapping TCP data segments. We noticed something weird for some
of our test cases.
This is excellent work. Since some time we are working on an independent
implementation (https://github.com/robur-coop/utcp) -- it seems you have
a nice test suite/system setup to detect interesting behaviour.
It is based (manually translated to OCaml) on the formal specification
in HOL4 (http://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf /
https://www.cl.cam.ac.uk/~pes20/Netsem/).
Would you mind to use your tests against the utcp stack as well? If you
need a hand on how to get this up and running into an existing
unikernel, please don't hesitate to reach out -- we use it in several
deployments for testing.
For the specific issue, processing overlapping data segments -- the utcp
behaviour is that the older segment data is preserved, and the newer
segment data is filled where needed (i.e. where there's not yet any
data). Does this make sense, or should it be the other way around that
more recent received bytes are preferred?
Best,
Hannes
