virtio-queue: add verify_add_used and stub memory region #346

priyasiddharth · 2025-06-18T18:42:23Z

Summary of the PR

virtio-queue: add verification for add_used operation

Kani proofs like verify_add_used do not finish in practical time if we use the production memory region. So we implement a stub region with a simple vector backing it. This will help subsequent proofs work and also enable stateful proofs.

Note that unsafe code is added only for StubRegion that will run in Kani.
Kani verifies all unsafe accesses do not cause undefined behaviour (in the context of unit proof execution).

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/src/queue/verification.rs

MatiasVara · 2025-08-06T08:48:02Z

LGTM!

virtio-queue/src/queue/verification.rs

stefano-garzarella

Please for the commit description, follow the style of other commits, using the crate as prefix, something like this:

virtio-queue: add unit proof for add_used method (sec 2.8.22)

virtio-queue/src/queue/verification.rs

stefano-garzarella · 2025-08-06T09:05:40Z

virtio-queue/src/queue/verification.rs

@@ -14,11 +290,11 @@ use super::*;
 /// 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 SingleRegionGuestMemory {
-    the_region: vm_memory::GuestRegionMmap,
+    the_region: StubRegion,


I'd split this patch in 2 patches, one where you introduce StubRegion (explaining why we need to do that) using it in the existing proofs and another patch where you add the new proof.

I can add that we needed to rely on a StubRegion otherwise Kani won't finish if GuestRegionMmap is used. I agree that this needs to be explained.

@priyasiddharth I meant 2 patches in this PR, why removing the other changes from this PR?

MatiasVara · 2025-08-06T09:36:57Z

virtio-queue/src/queue/verification.rs

+
+/// Kani proof harness for verifying the behavior of the `add_used` method of the `Queue`.
+///
+/// # Specification (VirtIO 1.3, Section 2.8.22: "Receiving Used Buffers From The Device")


I think section 2.8 is for packed virtqueues whereas here we are only dealing with split virtqueues. I think the section should be 2.7.14 (see https://docs.oasis-open.org/virtio/virtio/v1.3/csd01/virtio-v1.3-csd01.html#x1-7100014)

Also, I could not find what the spec says about using a descriptor id that is out of bonds. I think that the spec may let the implementation decide that.

I think what we try to enforce here is 2.7.8.2 Device Requirements: The Virtqueue Used Ring. I think we may need a comment like in firecraker in which we state all the things we do not verify, e.g., the order in which the used-ring indexes are updated.

We are not enforcing any of the following in the current proof therefore I don't think 2.7.8.2 applies:

The device MUST set len prior to updating the used idx.

The device MUST write at least len bytes to descriptor, beginning at the first device-writable buffer, prior to updating the used idx.

The device MAY write more than len bytes to descriptor. Note: There are potential error cases where a device might not know what parts of the buffers have been written. This is why len is permitted to be an underestimate: that’s preferable to the driver believing that uninitialized memory has been overwritten when it has not.

MatiasVara · 2025-08-07T08:05:28Z

virtio-queue/src/queue/verification.rs

+/// When the device has finished processing a buffer, it must add an element to the used ring,
+/// indicating which descriptor chain was used and how many bytes were written. The device must
+/// increment the used index after writing the element. If the descriptor index is out of bounds,
+/// the operation must fail and the used index must not be incremented.


I think this last sentence is not part of the specification. There is no requirement about what to do when the index in the descriptor is out of bonds. I think it is a decision of the implementation what to do in this case.

closing as not relevant to this PR

@priyasiddharth this means that we will lose all the comments of that code, so we need to review again the same changes. Why you removed that changes completely from this PR?

Maybe I was unclear, but I meant just to split the changes in multiple patches but still in the same PR.

Ok I will add it back. I interpreted the word patch to mean different PRs but perhaps you meant commit: #346 (comment)

@priyasiddharth sorry, just to be clear, in my mind commit = patch + description.
PR (or series) is a set of commits/patches.

I clarified in the function doc

MatiasVara · 2025-08-07T09:55:40Z

virtio-queue/src/queue/verification.rs

+        assert_eq!(queue.next_used, used_idx);
+        assert!(used_desc_table_index >= queue.size());
+        // The old value should still be the same as before the add_used call.
+        assert_eq!(old_val, get_used_idx(&queue, &memory).unwrap());


I think different that the proof in firecraker (see https://sourcegraph.com/github.com/firecracker-microvm/firecracker/-/blob/src/vmm/src/devices/virtio/queue.rs?L982) we are checking that the memory values has not changed, right?

I don't understand the link. But to answer your question, firecracker proof does not check guestmemory (because of path explosion), we add this extra check cause kani seems to be able to handle it.

Kani proofs do not finish in practical time if we use the production memory region. So we implement a stub region with a simple vector backing it. This will help subsequent proofs work and also enable stateful proofs. Signed-off-by: Siddharth Priya <[email protected]>

Signed-off-by: Siddharth Priya <[email protected]>

This comment was marked as outdated.

Sign in to view

priyasiddharth force-pushed the verify_add_used branch from 959d811 to 7113f45 Compare June 19, 2025 00:21

priyasiddharth commented Jun 19, 2025

View reviewed changes

virtio-queue/src/queue.rs Outdated Show resolved Hide resolved

virtio-queue/src/queue.rs Outdated Show resolved Hide resolved

virtio-queue/src/queue.rs Outdated Show resolved Hide resolved

MatiasVara reviewed Jun 26, 2025

View reviewed changes

virtio-queue/src/queue.rs Outdated Show resolved Hide resolved

priyasiddharth force-pushed the verify_add_used branch 4 times, most recently from 96d3228 to 89e9614 Compare July 29, 2025 15:15

MatiasVara reviewed Jul 31, 2025

View reviewed changes

virtio-queue/src/queue/verification.rs Outdated Show resolved Hide resolved

priyasiddharth force-pushed the verify_add_used branch from 89e9614 to 7f83b55 Compare August 5, 2025 15:18

priyasiddharth changed the title ~~verify add_used operation using guestmemory stubs~~ unit proof for add_used operation Aug 5, 2025

priyasiddharth force-pushed the verify_add_used branch from 7f83b55 to f8c3526 Compare August 5, 2025 15:24

priyasiddharth marked this pull request as ready for review August 5, 2025 15:24

priyasiddharth requested review from alexandruag, andreeaflorescu, jiangliu, slp, stsquad, epilys and stefano-garzarella as code owners August 5, 2025 15:24

priyasiddharth requested review from MatiasVara and roypat August 5, 2025 16:07

MatiasVara reviewed Aug 6, 2025

View reviewed changes

virtio-queue/src/queue/verification.rs Outdated Show resolved Hide resolved

MatiasVara reviewed Aug 6, 2025

View reviewed changes

virtio-queue/src/queue/verification.rs Show resolved Hide resolved

stefano-garzarella reviewed Aug 6, 2025

View reviewed changes

MatiasVara reviewed Aug 6, 2025

View reviewed changes

MatiasVara reviewed Aug 7, 2025

View reviewed changes

priyasiddharth closed this Aug 7, 2025

priyasiddharth force-pushed the verify_add_used branch from f8c3526 to 433129f Compare August 7, 2025 19:35

priyasiddharth reopened this Aug 7, 2025

priyasiddharth changed the title ~~unit proof for add_used operation~~ virtio-queue: add stub memory region for kani proofs Aug 7, 2025

priyasiddharth added 2 commits August 8, 2025 13:17

virtio-queue: add doc for unit proof verify_2_7_7_2

841de4b

Signed-off-by: Siddharth Priya <[email protected]>

virtio-queue: verify add_used method of the queue

db34f4d

Signed-off-by: Siddharth Priya <[email protected]>

priyasiddharth changed the title ~~virtio-queue: add stub memory region for kani proofs~~ virtio-queue: add verify_add_used and stub memory region Aug 8, 2025

virtio-queue: add verify_add_used and stub memory region #346

Are you sure you want to change the base?

virtio-queue: add verify_add_used and stub memory region #346

Uh oh!

Conversation

priyasiddharth commented Jun 18, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary of the PR

Requirements

Uh oh!

This comment was marked as outdated.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

MatiasVara commented Aug 6, 2025

Uh oh!

Uh oh!

stefano-garzarella left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MatiasVara Aug 6, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MatiasVara Aug 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

priyasiddharth commented Jun 18, 2025 •

edited

Loading

MatiasVara Aug 6, 2025 •

edited

Loading

MatiasVara Aug 7, 2025 •

edited

Loading