From 4a8b048604ee45dfcdc3e5219161e35b249a1b89 Mon Sep 17 00:00:00 2001 From: Siddharth Priya Date: Sun, 7 Sep 2025 13:36:20 -0400 Subject: [PATCH 1/2] virtio-queue: handle more cases for needs_notification proof This simplifies the logic for the existing need_notification proof and makes it more general accounting for both when notification is needed and when it is not. Signed-off-by: Siddharth Priya --- virtio-queue/src/queue/verification.rs | 62 +++++++++++++------------- 1 file changed, 31 insertions(+), 31 deletions(-) diff --git a/virtio-queue/src/queue/verification.rs b/virtio-queue/src/queue/verification.rs index 1ac9513b..0e000f8e 100644 --- a/virtio-queue/src/queue/verification.rs +++ b/virtio-queue/src/queue/verification.rs @@ -459,6 +459,17 @@ impl kani::Arbitrary for ProofContext { } } +/// Helper function to determine if `point` is in the wrapping range `[start, stop)`. +fn pred_in_wrapping_range(start: Wrapping, stop: Wrapping, point: Wrapping) -> bool { + // Check if point is in the range [start, stop) in a wrapping manner. + if start <= stop { + start <= point && point < stop + } else { + // If start > stop, we wrap around the maximum value of u16. + point >= start || point < stop + } +} + /// # Specification (VirtIO 1.3, Section 2.7.7.2: "Device Requirements: Used Buffer Notification Suppression") /// /// Section 2.7.7.2 deals with device-to-driver notification suppression. It @@ -468,46 +479,35 @@ impl kani::Arbitrary for ProofContext { /// specific number of descriptors has been processed. This is done by the /// driver defining a "used_event" index, which tells the device "please do not /// notify me until used.ring[used_event] has been written to by you". +/// +/// This proof checks: +// - If event_idx is not enabled, a notification is always needed. +// - If event_idx is enabled, a notification is needed if the used_event index +// is in the wrapping range [next_used - num_added, next_used). #[kani::proof] // 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)] -fn verify_device_notification_suppression() { - let ProofContext { - mut queue, - memory: mem, - } = kani::any(); - - let num_added_old = queue.num_added.0; - let needs_notification = queue.needs_notification(&mem); +fn verify_device_to_driver_notification() { + let ProofContext { mut queue, memory } = kani::any(); - // event_idx_enabled equivalent to VIRTIO_F_EVENT_IDX negotiated + // If the event_idx_enabled is false, we always need a notification if !queue.event_idx_enabled { - // The specification here says - // After the device writes a descriptor index into the used ring: - // – If flags is 1, the device SHOULD NOT send a notification. - // – If flags is 0, the device MUST send a notification - // flags is the first field in the avail_ring_address, which we completely ignore. We - // always send a notification, and as there only is a SHOULD NOT, that is okay - assert!(needs_notification.unwrap()); + assert!(queue.needs_notification(&memory).unwrap()); } else { - // next_used - 1 is where the previous descriptor was placed - if Wrapping(queue.used_event(&mem, Ordering::Relaxed).unwrap()) - == std::num::Wrapping(queue.next_used - Wrapping(1)) - && num_added_old > 0 - { - // If the idx field in the used ring (which determined where that descriptor index - // was placed) was equal to used_event, the device MUST send a - // notification. - assert!(needs_notification.unwrap()); - - kani::cover!(); - } - - // The other case is handled by a "SHOULD NOT send a notification" in the spec. - // So we do not care + // If the event_idx_enabled is true, we only need a notification if + // the used_event is in the range of [next_used - num_added, next_used) + let used_event = queue.used_event(&memory, Ordering::Relaxed).unwrap(); + let current_used = queue.next_used; + let old = current_used - queue.num_added; + let should_notify = pred_in_wrapping_range(old, current_used, used_event); + assert_eq!( + queue.needs_notification(&memory).unwrap(), /* actual */ + should_notify, /* expected */ + ); + assert_eq!(queue.num_added.0, 0); } } From 24dc553a8aa0165f0eb78d41a0376f359e13f36e Mon Sep 17 00:00:00 2001 From: Siddharth Priya Date: Sun, 7 Sep 2025 15:44:12 -0400 Subject: [PATCH 2/2] virtio-queue: additional proofs around notification logic 1. Verify enable_notification logic 2. Verify when driver should send notification to device 3. Verify when driver should not send notification to device 4. Verify that set_next_used method actually changes the next_used field in memory Signed-off-by: Siddharth Priya --- virtio-queue/src/queue/verification.rs | 136 +++++++++++++++++++++++++ 1 file changed, 136 insertions(+) diff --git a/virtio-queue/src/queue/verification.rs b/virtio-queue/src/queue/verification.rs index 0e000f8e..138360a9 100644 --- a/virtio-queue/src/queue/verification.rs +++ b/virtio-queue/src/queue/verification.rs @@ -565,3 +565,139 @@ fn verify_add_used() { kani::cover!(); } } + +/// This proof checks that after setting the `next_used` field of the queue +/// using `set_next_used(x)`, reading back the value of `next_used` returns the +/// same value `x`. +#[kani::proof] +#[kani::unwind(0)] +fn verify_used_ring_avail_event() { + let ProofContext { + mut queue, + memory: _, + } = kani::any(); + let x = kani::any(); + queue.set_next_used(x); + assert_eq!(x, queue.next_used.0); +} + +/// # Specification (VirtIO 1.3, Section 2.7.6.1: "Driver Requirements: The Virtqueue Available Ring") +/// +/// This proof checks that: +/// - If there are pending entries in the avail ring (avail_idx != next_avail), +/// `enable_notification` returns true. +/// - If there are no pending entries (avail_idx == next_avail), it returns false. +/// This matches the monotonicity property of the avail ring in VirtIO 1.3 Section 2.7.6.1. +#[kani::proof] +#[kani::unwind(0)] +fn verify_enable_driver_to_device_notification() { + let ProofContext { mut queue, memory } = kani::any(); + + // The enable_notification method sets notification to true and returns + // - true, if there are pending entries in the `idx` field of the + // avail ring + // - false, if there are no pending entries in the `idx` field of the + // avail ring The check for pending entries is done by comparing the + // current `avail_idx` with the `next_avail` field of the queue. If they + // are different, there are pending entries, otherwise there are no + // pending entries. The equality check is a consequence of the + // monotonicity property of `idx` (2.7.6.1) that it cannot be decreased + // by the driver. + if queue.enable_notification(&memory).unwrap() { + assert_ne!( + queue.avail_idx(&memory, Ordering::Relaxed).unwrap(), + queue.next_avail + ); + } else { + assert_eq!( + queue.avail_idx(&memory, Ordering::Relaxed).unwrap(), + queue.next_avail + ); + } +} + +// Helper method that reads `val` from the `avail_event` field of the used ring, using +// the provided ordering. Takes used_ring address and queue size directly. +fn get_avail_event( + used_ring_addr: GuestAddress, + queue_size: u16, + mem: &M, + order: Ordering, +) -> Result { + // This can not overflow an u64 since it is working with relatively small numbers compar + // to u64::MAX. + let avail_event_offset = + VIRTQ_USED_RING_HEADER_SIZE + VIRTQ_USED_ELEMENT_SIZE * u64::from(queue_size); + let addr = used_ring_addr + .checked_add(avail_event_offset) + .ok_or(Error::AddressOverflow)?; + + mem.load::(addr, order).map_err(Error::GuestMemory) +} + +// Get the value of the `flags` field of the used ring, applying the specified ordering. +fn get_used_flags(queue: &Queue, mem: &M, order: Ordering) -> Result { + mem.load::(queue.used_ring, order) + .map(u16::from_le) + .map_err(Error::GuestMemory) +} +/// # Specification (VirtIO 1.3, Section 2.7.7: "Used Buffer Notification Suppression") +/// +/// This proof checks: +/// - If event_idx is not enabled, `set_notification(false)` sets used.flags to 1 (NO_NOTIFY). +/// - If event_idx is enabled, the call is a no-op. +#[kani::proof] +#[kani::unwind(0)] +fn verify_set_notification_true() { + let ProofContext { mut queue, memory } = kani::any(); + if queue + .set_notification(&memory, true /* enable notification */) + .is_ok() + { + if queue.event_idx_enabled { + // Since VIRTIO_F_EVENT_IDX is negotiated, we make sure that set_notification + // has updated the used.avail_event field with the tail position of + // the avail ring. + let used_ring_addr = queue.used_ring; + let queue_size = queue.size(); + kani::cover!(); + assert_eq!( + get_avail_event(used_ring_addr, queue_size, &memory, Ordering::Relaxed).unwrap(), + queue.next_avail.0 + ); + } else { + // If VIRTIO_F_EVENT_IDX is not negotiated, we make sure that the + // used.flags field is set to 0, meaning that the driver should not + // send notifications to the device. + kani::cover!(); + assert_eq!( + get_used_flags(&queue, &memory, Ordering::Relaxed).unwrap(), + 0 + ); + } + } +} + +/// # Specification (VirtIO 1.3, Section 2.7.7: "Used Buffer Notification Suppression") +/// +/// This proof checks: +/// - If event_idx is not enabled, `set_notification(false)` sets used.flags to 1 (NO_NOTIFY). +/// - If event_idx is enabled, the call is a no-op. +#[kani::proof] +#[kani::unwind(0)] +fn verify_set_notification_false() { + let ProofContext { mut queue, memory } = kani::any(); + let result = queue.set_notification(&memory, false /* disable notification */); + if !queue.event_idx_enabled { + // Check for Sec 2.7.10 + assert_eq!( + get_used_flags(&queue, &memory, Ordering::Relaxed).unwrap(), + 1 + ); + // don't check Ok() result since that is a property of the + // underlying mem system and out of scope. E.g., it is stubbed for + // this proof and we always expect it to succeed. + } else { + assert!(result.is_ok()); + } +}