Enrich unit tests with symbolic proofs

[tiferrei]

Hi there,

Over the past few weeks I have been working on making some of the tests for the TCP implementation more powerful. I have been using Kani to be able to prove stronger theorems resembling the unit tests' behavior.

This mostly means proving that the behavior expected by the unit tests is met not only with the specific mocked IPs, sockets, packets, etc. but in general with any such structures, as long as the actually meaningful properties of such structures are met.

I saw that smoltcp makes use of some fuzzing to increase the trust in correctness of the library, and so thought symbolic execution would be a great addition to cover even more scenarios, and unexpected edge cases.

We were hoping to upstream these efforts into smoltcp, to hopefully be able to capture breaking issues in code changes before they're published. We have also configured a CI job that can run the proofs automatically to check they're still being met.

So far the proofs cover the wire parts of TCP, mostly proving that serializing and deserializing are inverse operations (w.r.t most fields being made symbolic), and we have theorems that augment the TCP socket tests for Closed, Listen, and Syn-Received states.

We would love to get some feedback!

[codecov[bot]]

Codecov Report

:exclamation: No coverage uploaded for pull request base (main@edfdb23). Click here to learn what that means. The diff coverage is 100.00%.

@@           Coverage Diff           @@
##             main     #846   +/-   ##
=======================================
  Coverage        ?   79.59%           
=======================================
  Files           ?       78           
  Lines           ?    27838           
  Branches        ?        0           
=======================================
  Hits            ?    22159           
  Misses          ?     5679           
  Partials        ?        0           

Files	Coverage Δ
src/iface/interface/mod.rs	45.63% <ø> (ø)
src/socket/tcp.rs	96.63% <100.00%> (ø)
src/time.rs	86.41% <ø> (ø)
src/wire/ip.rs	77.85% <ø> (ø)
src/wire/ipv4.rs	86.35% <ø> (ø)
src/wire/ipv6.rs	97.51% <ø> (ø)
src/wire/tcp.rs	74.46% <ø> (ø)

:mega: We’re building smart automated test selection to slash your CI/CD build times. Learn more