Re: Failed TCP connection reset when processing overlapping data segments

[Lucas Aubard <lucas.aubard@xxxxxxxx>]

Dear Hannes, 

Thank you for your interest in the testing platform! 

I am submitting some work in the next few days, but I'd be happy to test utcp 
afterward.  
I'll certainly need a hand to test it; I get back to you as soon as possible.   

The behavior you describe for processing overlapping data segments makes sense 
to me. 

Best regards,
Lucas 

----- Mail original -----
> De: "Hannes Mehnert" <hannes@xxxxxxxxxxx>
> À: "mirageos-devel" <mirageos-devel@xxxxxxxxxxxxxxxxxxxx>
> Cc: "Johan Mazel" <Johan.Mazel@xxxxxxxxxxx>, "gilles guette" 
> <gilles.guette@xxxxxxxxxxxxxxxxx>, "Pierre Chifflier"
> <Pierre.Chifflier@xxxxxxxxxxx>, "Lucas Aubard" <lucas.aubard@xxxxxxxx>
> Envoyé: Vendredi 11 Avril 2025 12:42:51
> Objet: Re: Failed TCP connection reset when processing overlapping data 
> segments

> 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