Add kani in ci + kani proof for conformance to 2.7.7.2 section #338

priyasiddharth · 2025-06-03T17:35:22Z

Enable Kani in the CI and add the verify_spec_2_7_7_2() proof to verify that the implementation of queue satisfies 2.7.7.2 requirement. The proof relies on whether the EVENT_IDX feature has been negotiated. Conversely with test_needs_notification() test, this proof tests for all possible values of the queue structure.

Summary of the PR

This is review-ready version of #324 and #339.
First, we add Kani to the CI pipeline with a timeout of 20 minutes. The timeout is essential because Kani converts a rust program to a SAT problem which is NP-complete and may not return in a reasonable time.

Second, we add a kani proof to meet the requirements outlined in 2.7.7.2 of the virtio specification regarding the notification suppression mechanism. We have sketched this proof from the same proof defined for the queue implemented in firecraker. This commit adds the verify_spec_2_7_7_2() proof to verify that the implementation of queue meets 2.7.7.2 requirement. The proof relies on whether the EVENT_IDX feature has been negotiated. Conversely with test_needs_notification() test, this proof tests for all possible values of queue. To run the proof, you can run:

cargo kani

The proof currently passes with kani v0.62.0:

SUMMARY:
 ** 0 of 4880 failed (379 unreachable)

 ** 1 of 1 cover properties satisfied


VERIFICATION:- SUCCESSFUL
Verification Time: 82.47572s

Manual Harness Summary:
Complete - 1 successfully verified harnesses, 0 failures, 1 total.

Requirements

Before submitting your PR, please make sure you addressed the following
requirements:

All commits in this PR have Signed-Off-By trailers (with
git commit -s), and the commit message has max 60 characters for the
summary and max 75 characters for each description line.
All added/changed functionality has a corresponding unit/integration
test.
All added/changed public-facing functionality has entries in the "Upcoming
Release" section of CHANGELOG.md (if no such section exists, please create one).
Any newly added unsafe code is properly documented.

virtio-queue/src/queue.rs

virtio-queue/Cargo.toml

virtio-queue/src/queue.rs

virtio-queue/Cargo.toml

stefano-garzarella · 2025-06-10T10:21:19Z

@priyasiddharth thanks for this PR. IIUC you are re-working a patch initially developed from @MatiasVara, so I think you should add also your S-o-b in the patch.

priyasiddharth · 2025-06-10T14:14:02Z

Thank you @stefano-garzarella for the taking on the review. I have added a sign-off tag.

virtio-queue/Cargo.toml

priyasiddharth · 2025-06-12T16:17:00Z

@stefano-garzarella PTAL

stefano-garzarella · 2025-06-13T08:43:52Z

@priyasiddharth please mention big changes (e.g. you included patch from #339) and the reason after a push. I think that should also be mentioned in the PR description/title.

Also we usually squash new changes in commit, so all the "fix(comment)..." commit, should be squashed in the first commit (you can remove my Co-authored-by, it was just a suggestion while reviewing. As a general rule, a commit in a PR should not change/fix code added in the same PR.

Maybe we can also change the order of the patches, first enable the CI, then add the first test.

Run kani as a part of the CI pipeline. In particular, run the proofs for virtio-queue. In some cases, kani may not finish so set a twenty minutes timeout. Signed-off-by: Matias Ezequiel Vara Larsen <mvaralar@redhat.com> Signed-off-by: Siddharth Priya <s2priya@uwaterloo.ca>

priyasiddharth · 2025-06-13T14:38:16Z

@priyasiddharth please mention big changes (e.g. you included patch from #339) and the reason after a push. I think that should also be mentioned in the PR description/title.

Mentioned Run kani as part of the CI pipeline #339 and reason
Added kani note in PR description/title

Also we usually squash new changes in commit, so all the "fix(comment)..." commit, should be squashed in the first commit (you can remove my Co-authored-by, it was just a suggestion while reviewing. As a general rule, a commit in a PR should not change/fix code added in the same PR.

squashed changes
Followed rule

Maybe we can also change the order of the patches, first enable the CI, then add the first test.

done
@MatiasVara PTAL

stefano-garzarella

LGTM, just very minimal comments! Thanks!

virtio-queue/Cargo.toml

virtio-queue/src/queue.rs

stefano-garzarella

LGTM for the project POV, but I have no experience with kani, so I cced @roypat that may have comments on the direction!

virtio-queue/src/queue.rs

roypat · 2025-06-18T07:57:25Z

.buildkite/custom-tests.json

+      "test_name": "prove-virtio-queue",
+      "command": "cargo kani --package virtio-queue",
+      "platform": ["x86_64", "aarch64"],
+      "timeout_in_minutes": 20


nit: currently it finishes in just 2 minutes, so maybe we can leave the default timeout for now?

I would prefer to let this be in this PR and change once this goes in.

It makes more sense to only have override the timeout if it's needed, I agree with @roypat

priyasiddharth · 2025-06-24T11:23:54Z

@roypat PTAL

stefano-garzarella · 2025-07-03T11:26:43Z

@alexandruag @andreeaflorescu @jiangliu @slp @stsquad @epilys any thought on this?

virtio-queue/src/queue.rs

epilys · 2025-07-03T15:15:58Z

virtio-queue/src/queue.rs

+    #[kani::unwind(0)] // There are no loops anywhere, but kani really enjoys getting stuck in std::ptr::drop_in_place.
+                       // This is a compiler intrinsic that has a "dummy" implementation in stdlib that just
+                       // recursively calls itself. Kani will generally unwind this recursion infinitely


Suggested change

#[kani::unwind(0)] // There are no loops anywhere, but kani really enjoys getting stuck in std::ptr::drop_in_place.

// This is a compiler intrinsic that has a "dummy" implementation in stdlib that just

// recursively calls itself. Kani will generally unwind this recursion infinitely

// There are no loops anywhere, but kani really enjoys getting stuck in std::ptr::drop_in_place.

// This is a compiler intrinsic that has a "dummy" implementation in stdlib that just

// recursively calls itself. Kani will generally unwind this recursion infinitely

#[kani::unwind(0)]

andreeaflorescu · 2025-07-03T15:11:44Z

virtio-queue/src/queue.rs

@@ -269,6 +269,284 @@ impl Queue {
    }
 }

+#[cfg(kani)]
+#[allow(dead_code)]


Why do we need this allow(dead_code)?

andreeaflorescu · 2025-07-03T15:15:39Z

virtio-queue/src/queue.rs

@@ -269,6 +269,284 @@ impl Queue {
    }
 }

+#[cfg(kani)]
+#[allow(dead_code)]
+mod verification {


So far we've been keeping the tests related modules at the end of files. We shouldn't interleave this code with the functionality of the queue.

Is there anything stopping us from having a separate file for the kani related tests and functionality? It looks like it's adding quite a lot of code to a file that's already pretty large.

Currently the unit proofs rely on internal queue state like queue.num_added and internal predicates likeneeds_notification.
IIUC either these need to made public piecewise or the whole module needs to be made public.

andreeaflorescu · 2025-07-03T15:17:39Z

virtio-queue/src/queue.rs

+    /// speeds up all queue proofs, because it eliminates the only loop contained herein,
+    /// meaning we can use `kani::unwind(0)` instead of `kani::unwind(2)`. Functionally,
+    /// it works identically to `GuestMemoryMmap` with only a single contained region.
+    pub struct ProofGuestMemory {


nit: might be better to name this for what it does instead of what it is used for as we might end up needing different kinds of "GuestMemory" for other proofs.

andreeaflorescu · 2025-07-03T15:19:58Z

virtio-queue/src/queue.rs

+        }
+    }
+
+    pub struct ProofContext(pub Queue, pub ProofGuestMemory);


Can you make these named fields instead? We've been using tuples like these when it's obvious what the tuple items represent (i.e. a Point(x, y)).

andreeaflorescu · 2025-07-03T15:25:14Z

virtio-queue/src/queue.rs

+        }
+    }
+
+    // can't implement kani::Arbitrary for the relevant types due to orphan rules


Is the "orhphan" here the kani vector that provides the baking memory for GuestMemory? If yes, could we have the baking memory part of the ProofGuestMemory and implement any on that?

Add the verify_spec_2_7_7_2() proof to verify that the implementation of queue satisfies 2.7.7.2 requirement. The proof relies on whether the EVENT_IDX feature has been negotiated. Conversely with `test_needs_notification()` test, this proof `tests` for all possible values of the queue structure. Signed-off-by: Matias Ezequiel Vara Larsen <mvaralar@redhat.com> Signed-off-by: Siddharth Priya <s2priya@uwaterloo.ca>

priyasiddharth · 2025-07-08T15:40:36Z

@andreeaflorescu @epilys PTAL

priyasiddharth requested review from alexandruag, andreeaflorescu, jiangliu, slp, stsquad, epilys and stefano-garzarella as code owners June 3, 2025 17:35