Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Enrich unit tests with symbolic proofs #846

Open
wants to merge 39 commits into
base: main
Choose a base branch
from

Conversation

tiferrei
Copy link

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!

@tiferrei tiferrei changed the title Feat/verification Enrich unit tests with symbolic proofs Sep 29, 2023
@codecov
Copy link

codecov bot commented Sep 29, 2023

Codecov Report

❗ 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% <ø> (ø)

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

Successfully merging this pull request may close these issues.

1 participant