Enrich unit tests with symbolic proofs #846
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
added 30 commits
August 7, 2023 14:28
# Conflicts: # src/iface/interface/mod.rs # src/socket/tcp.rs
Codecov Report
@@ Coverage Diff @@
## main #846 +/- ##
=======================================
Coverage ? 79.59%
=======================================
Files ? 78
Lines ? 27838
Branches ? 0
=======================================
Hits ? 22159
Misses ? 5679
Partials ? 0
📣 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
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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!