Progress on page allocator verification

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

Author: lgaeher

confidential-vms/linux_vm/Makefile

@@ -14,7 +14,7 @@ LINUX_VM_ROOTFS_SOURCE_DIR			?= $(CONFIDENTIAL_VMS_LINUX_SOURCE_DIR)/hypervisor_
 LINUX_VM_BUILDROOT_SOURCE_DIR		?= $(CONFIDENTIAL_VMS_LINUX_SOURCE_DIR)/../../hypervisor/buildroot
 LINUX_VM_BUILDROOT_WORK_DIR			?= $(CONFIDENTIAL_VMS_LINUX_WORK_DIR)/buildroot
 LINUX_VM_BUILDROOT_ROOTFS			?= $(LINUX_VM_BUILDROOT_WORK_DIR)/images/rootfs.ext2
-LINUX_VM_BUILDROOT_ROOTFS_SIZE		?= "256M"
+LINUX_VM_BUILDROOT_ROOTFS_SIZE		?= "128M"
 LINUX_VM_OVERLAY_SOURCE_DIR			?= $(CONFIDENTIAL_VMS_LINUX_SOURCE_DIR)/overlay
 LINUX_VM_OVERLAY_WORK_DIR			?= $(CONFIDENTIAL_VMS_LINUX_WORK_DIR)/overlay
 LINUX_VM_OVERLAY_WORK_ROOT_DIR		?= $(LINUX_VM_OVERLAY_WORK_DIR)/root

confidential-vms/linux_vm/configurations/qemu_riscv64_virt_defconfig

@@ -34,7 +34,7 @@ BR2_TARGET_ROOTFS_EXT2=y
 BR2_TARGET_ROOTFS_EXT2_2=n
 BR2_TARGET_ROOTFS_EXT2_3=n
 BR2_TARGET_ROOTFS_EXT2_4=y
-BR2_TARGET_ROOTFS_EXT2_SIZE="5G"
+BR2_TARGET_ROOTFS_EXT2_SIZE="1G"
 
 # Kernel
 BR2_LINUX_KERNEL=y

hypervisor/Makefile

@@ -14,7 +14,7 @@ BUILDROOT_SOURCE_DIR				?= $(MAKEFILE_SOURCE_DIR)/buildroot
 HYPERVISOR_BUILDROOT_CONFIG_DIR		?= $(HYPERVISOR_CONFIGURATION_DIR)/qemu_riscv64_virt_defconfig
 HYPERVISOR_LINUX_CONFIG				?= $(HYPERVISOR_CONFIGURATION_DIR)/linux64-defconfig
 HYPERVISOR_BUILDROOT_OVERRIDE_DIR 	?= $(HYPERVISOR_CONFIGURATION_DIR)/package_override.dev
-HYPERVISOR_ROOTFS_SIZE				?= "1G"
+HYPERVISOR_ROOTFS_SIZE				?= "512M"
 HYPERVISOR_OVERLAY_DIR				?= $(HYPERVISOR_WORK_DIR)/overlay
 HYPERVISOR_OVERLAY_ROOT_DIR			?= $(HYPERVISOR_OVERLAY_DIR)/root
 HYPERVISOR_PATCHES_DIR				?= $(MAKEFILE_SOURCE_DIR)/patches

security-monitor/src/core/architecture/riscv/mmu/page_size.rs

@@ -8,6 +8,23 @@
 #[repr(u8)]
 #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
 #[rr::refined_by("page_size")]
+// PEq
+#[rr::derive_instantiate("PEq" := "λ a b, bool_decide (a = b)")]
+// Eq
+#[rr::derive_instantiate("PEq_refl" := #proof "intros ??; solve_goal")]
+#[rr::derive_instantiate("PEq_sym" := #proof "intros ???; solve_goal")]
+#[rr::derive_instantiate("PEq_trans" := #proof "intros ????; solve_goal")]
+// POrd
+#[rr::derive_instantiate("POrd" := "λ a b, Some (page_size_cmp a b)")]
+#[rr::derive_instantiate("POrd_eq_cons" := #proof "intros ? [] []; simpl; done")]
+// Ord
+#[rr::derive_instantiate("Ord" := "page_size_cmp")]
+#[rr::derive_instantiate("Ord_POrd" := #proof "intros ???; solve_goal")]
+#[rr::derive_instantiate("Ord_lt_trans" := #proof "intros ????; solve_goal")]
+#[rr::derive_instantiate("Ord_eq_trans" := #proof "intros ????; solve_goal")]
+#[rr::derive_instantiate("Ord_gt_trans" := #proof "intros ????; solve_goal")]
+#[rr::derive_instantiate("Ord_leibniz" := #proof "intros ? [] []; simpl; done")]
+#[rr::derive_instantiate("Ord_antisym" := #proof "intros ???; solve_goal")]
 pub enum PageSize {
     #[rr::pattern("Size4KiB")]
     Size4KiB,

security-monitor/src/core/memory_layout/confidential_memory_address.rs

@@ -6,7 +6,7 @@ use pointers_utility::{ptr_byte_add_mut, ptr_byte_offset};
 
 /// The wrapper over a raw pointer that is guaranteed to be an address located in the confidential memory region.
 #[repr(transparent)]
-#[derive(Debug, PartialEq)]
+#[derive(Debug, PartialEq, Clone, Copy)]
 /// Model: The memory address is represented by the location in memory.
 #[rr::refined_by("l" : "loc")]
 /// We require the ghost state for the global memory layout to be available.
@@ -70,12 +70,12 @@ impl ConfidentialMemoryAddress {
     /// Precondition: The offset address is in the given range.
     #[rr::requires("self.2 + offset_in_bytes < upper_bound.2")]
     /// Precondition: The maximum (and thus the offset address) is in the confidential memory range.
-    #[rr::requires("upper_bound.2 < MEMORY_CONFIG.(conf_end).2")]
+    #[rr::requires("upper_bound.2 ≤ MEMORY_CONFIG.(conf_end).2")]
     /// Postcondition: The offset pointer is in the confidential memory range.
     #[rr::ensures("ret = self +ₗ offset_in_bytes")]
     pub fn add(&self, offset_in_bytes: usize, upper_bound: *const usize) -> Result<ConfidentialMemoryAddress, Error> {
-        let pointer = ptr_byte_add_mut(self.0, offset_in_bytes, upper_bound).map_err(|_| Error::AddressNotInConfidentialMemory())?;
-        Ok(ConfidentialMemoryAddress(pointer))
+        let pointer = ptr_byte_add_mut(self.0, offset_in_bytes, upper_bound).map_err(#[rr::verify] |_| Error::AddressNotInConfidentialMemory())?;
+        Ok(Self::new(pointer))
     }
 
     /// Reads usize-sized sequence of bytes from the confidential memory region.

security-monitor/src/core/memory_layout/mod.rs

@@ -149,10 +149,10 @@ impl MemoryLayout {
 
     /// Offsets an address in the confidential memory by a given number of bytes. Returns an error if the resulting
     /// address is outside the confidential memory region or exceeds the given upper bound.
-    #[rr::trust_me]
+    #[rr::only_spec]
     #[rr::ok]
     /// Precondition: The offset address is in confidential memory.
-    #[rr::requires("address.2 + offset_in_bytes < self.(conf_end).2")]
+    #[rr::requires("address.2 + offset_in_bytes < upper_bound.2")]
     /// Precondition: The bounds we are checking are within confidential memory.
     #[rr::requires("upper_bound.2 ≤ self.(conf_end).2")]
     /// Postcondition: Then we can correctly offset the address and ensure it is in confidential
@@ -162,7 +162,7 @@ impl MemoryLayout {
         &self, address: &ConfidentialMemoryAddress, offset_in_bytes: usize, upper_bound: *const usize,
     ) -> Result<ConfidentialMemoryAddress, Error> {
         ensure!(upper_bound <= self.confidential_memory_end, Error::AddressNotInConfidentialMemory())?;
-        Ok(self.confidential_address_at_offset(address, offset_in_bytes)?)
+        Ok(address.add(offset_in_bytes, upper_bound).map_err(|_| Error::AddressNotInConfidentialMemory())?)
     }
 
     /// Offsets an address in the non-confidential memory by given number of bytes. Returns an error if the resulting
@@ -199,8 +199,8 @@ impl MemoryLayout {
         // We can safely cast the below offset to usize because the constructor guarantees that the confidential memory
         // range is valid, and so the memory size must be a valid usize
         let memory_size = ptr_byte_offset(self.confidential_memory_end, self.confidential_memory_start) as usize;
-        let usize_alligned_offsets = (0..memory_size).step_by(core::mem::size_of::<usize>());
-        usize_alligned_offsets.for_each(|offset_in_bytes| {
+        let usize_aligned_offsets = (0..memory_size).step_by(core::mem::size_of::<usize>());
+        usize_aligned_offsets.for_each(|offset_in_bytes| {
             let _ = ptr_byte_add_mut(self.confidential_memory_start, offset_in_bytes, self.confidential_memory_end)
                 .and_then(|ptr| Ok(unsafe { ptr.write_volatile(0) }));
         });