From aa0dca977b3e723b29d5db9b20775818a75c8f75 Mon Sep 17 00:00:00 2001 From: Babis Chalios Date: Tue, 1 Oct 2024 14:52:12 +0200 Subject: [PATCH] iovec: fix kani proof for write_volatile_at IoVecBufferMut type now uses IovDeque as its backing memory. IovDeque is performing a custom memory allocation, using memfd_create() and a combination of mmap() calls in order to provide a memory layout where the iovec objects stored in the IovDeque will always be in consecutive memory. kani doesn't really get along with these system calls, which breaks our proof for IoVecBufferMut::write_volatile_at. Substitute memory allocation and deallocation with plain calls to std::alloc::(de)alloc when we run kani proofs. Also provide a stub for IovDeque::push_back to provide the same memory layout invariants. Co-authored-by: Babis Chalios Signed-off-by: Egor Lazarchuk --- src/vmm/src/devices/virtio/iov_deque.rs | 6 +-- src/vmm/src/devices/virtio/iovec.rs | 66 ++++++++++++++++++++++++- 2 files changed, 68 insertions(+), 4 deletions(-) diff --git a/src/vmm/src/devices/virtio/iov_deque.rs b/src/vmm/src/devices/virtio/iov_deque.rs index 03b8c8778b4..3dff1e04d71 100644 --- a/src/vmm/src/devices/virtio/iov_deque.rs +++ b/src/vmm/src/devices/virtio/iov_deque.rs @@ -71,9 +71,9 @@ pub enum IovDequeError { // so making a slice out of them does not require any copies. #[derive(Debug)] pub struct IovDeque { - iov: *mut libc::iovec, - start: u16, - len: u16, + pub iov: *mut libc::iovec, + pub start: u16, + pub len: u16, } // SAFETY: This is `Send`. We hold sole ownership of the underlying buffer. diff --git a/src/vmm/src/devices/virtio/iovec.rs b/src/vmm/src/devices/virtio/iovec.rs index 0e2bf76525c..064660a4b54 100644 --- a/src/vmm/src/devices/virtio/iovec.rs +++ b/src/vmm/src/devices/virtio/iovec.rs @@ -796,6 +796,7 @@ mod tests { } #[cfg(kani)] +#[allow(dead_code)] // Avoid warning when using stubs mod verification { use std::mem::ManuallyDrop; @@ -804,7 +805,9 @@ mod verification { use vm_memory::VolatileSlice; use super::{IoVecBuffer, IoVecBufferMut}; + use crate::arch::PAGE_SIZE; use crate::devices::virtio::iov_deque::IovDeque; + use crate::devices::virtio::queue::FIRECRACKER_MAX_QUEUE_SIZE; // Maximum memory size to use for our buffers. For the time being 1KB. const GUEST_MEMORY_SIZE: usize = 1 << 10; @@ -816,6 +819,50 @@ mod verification { // >= 1. const MAX_DESC_LENGTH: usize = 4; + mod stubs { + use super::*; + + /// This is a stub for the `IovDeque::push_back` method. + /// + /// `IovDeque` relies on a special allocation of two pages of virtual memory, where both of + /// these point to the same underlying physical page. This way, the contents of the first + /// page of virtual memory are automatically mirrored in the second virtual page. We do + /// that in order to always have the elements that are currently in the ring buffer in + /// consecutive (virtual) memory. + /// + /// To build this particular memory layout we create a new `memfd` object, allocate memory + /// with `mmap` and call `mmap` again to make sure both pages point to the page allocated + /// via the `memfd` object. These ffi calls make kani complain, so here we mock the + /// `IovDeque` object memory with a normal memory allocation of two pages worth of data. + /// + /// This stub helps imitate the effect of mirroring without all the elaborate memory + /// allocation trick. + pub fn push_back(deque: &mut IovDeque, iov: iovec) { + // This should NEVER happen, since our ring buffer is as big as the maximum queue size. + // We also check for the sanity of the VirtIO queues, in queue.rs, which means that if + // we ever try to add something in a full ring buffer, there is an internal + // bug in the device emulation logic. Panic here because the device is + // hopelessly broken. + assert!( + !deque.is_full(), + "The number of `iovec` objects is bigger than the available space" + ); + + let offset = (deque.start + deque.len) as usize; + let mirror = if offset >= FIRECRACKER_MAX_QUEUE_SIZE as usize { + offset - FIRECRACKER_MAX_QUEUE_SIZE as usize + } else { + offset + FIRECRACKER_MAX_QUEUE_SIZE as usize + }; + + // SAFETY: self.iov is a valid pointer and `self.start + self.len` is within range (we + // asserted before that the buffer is not full). + unsafe { deque.iov.add(offset).write_volatile(iov) }; + unsafe { deque.iov.add(mirror).write_volatile(iov) }; + deque.len += 1; + } + } + fn create_iovecs(mem: *mut u8, size: usize, nr_descs: usize) -> (Vec, u32) { let mut vecs: Vec = Vec::with_capacity(nr_descs); let mut len = 0u32; @@ -846,8 +893,23 @@ mod verification { } } + fn create_iov_deque() -> IovDeque { + // SAFETY: safe because the layout has non-zero size + let mem = unsafe { + std::alloc::alloc(std::alloc::Layout::from_size_align_unchecked( + 2 * PAGE_SIZE, + PAGE_SIZE, + )) + }; + IovDeque { + iov: mem.cast(), + start: kani::any_where(|&start| start < FIRECRACKER_MAX_QUEUE_SIZE), + len: 0, + } + } + fn create_iovecs_mut(mem: *mut u8, size: usize, nr_descs: usize) -> (IovDeque, u32) { - let mut vecs = IovDeque::new().unwrap(); + let mut vecs = create_iov_deque(); let mut len = 0u32; for _ in 0..nr_descs { // The `IoVecBufferMut` constructors ensure that the memory region described by every @@ -956,6 +1018,7 @@ mod verification { #[kani::proof] #[kani::unwind(5)] #[kani::solver(cadical)] + #[kani::stub(IovDeque::push_back, stubs::push_back)] fn verify_write_to_iovec() { for nr_descs in 0..MAX_DESC_LENGTH { let mut iov_mut = IoVecBufferMut::any_of_length(nr_descs); @@ -984,6 +1047,7 @@ mod verification { .unwrap(), buf.len().min(iov_mut.len().saturating_sub(offset) as usize) ); + std::mem::forget(iov_mut.vecs); } } }