Partially verify page allocator

.github/workflows/prune_dune_modules.py

@@ -0,0 +1,26 @@
+#!/usr/bin/env python3
+import re
+import sys
+
+if len(sys.argv) < 3:
+    print("usage: prune_dune_modules.py <dune-file> <module1> [module2 ...]")
+    sys.exit(1)
+
+path = sys.argv[1]
+remove = set(sys.argv[2:])
+
+with open(path) as f:
+    text = f.read()
+
+# Matches: (modules ... )
+pattern = re.compile(r'\(modules\b([^)]*)\)')
+
+def prune(match):
+    modules = match.group(1).split()
+    kept = [m for m in modules if m not in remove]
+    return "(modules " + " ".join(kept) + ")"
+
+new_text = pattern.sub(prune, text)
+
+with open(path, "w") as f:
+    f.write(new_text)

.github/workflows/verify.yml

@@ -39,7 +39,7 @@ jobs:
     - name: Install RefinedRust type system
       run: eval $(opam env) && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/install-typesystem.sh
     - name: Check cargo version
-      run: cargo --version 
+      run: cargo --version
     - name: Install RefinedRust stdlib
       run: eval $(opam env) && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/install-stdlib.sh
     - name: Exclude RefinedRust from dune build
@@ -55,4 +55,32 @@ jobs:
     - name: make devtools
       run: source "$HOME/.cargo/env" && eval $(opam env) && make devtools
     - name: Translate specified files using RefinedRust and check proofs
-      run: source "$HOME/.cargo/env" && eval $(opam env) && DUNEFLAGS="-j 1" make verify
+      run: |
+        set -o pipefail
+          (source "$HOME/.cargo/env" && eval $(opam env) && make generate_refinedrust_translation) 2>&1 | tee full-build.log
+    - name: Patch dune modules to exclude big proofs from CI
+      run: |
+          python3 .github/workflows/prune_dune_modules.py verification/rust_proofs/ace/proofs/dune \
+            proof_core_page_allocator_allocator_PageAllocator_add_memory_region \
+            proof_core_page_allocator_allocator_PageStorageTreeNode_store_page_token \
+            proof_core_page_allocator_allocator_PageStorageTreeNode_divide_page_token_if_necessary \
+            proof_core_page_allocator_allocator_PageAllocator_find_largest_page_size \
+            proof_core_page_allocator_page_Page_T_write \
+            proof_core_page_allocator_page_Page_core_page_allocator_page_Allocated_read \
+            proof_core_page_allocator_allocator_PageStorageTreeNode_store_page_token \
+            proof_core_page_allocator_page_Page_core_page_allocator_page_UnAllocated_divide
+    - name: Compile Rocq proofs
+      run: |
+          (
+            set -o pipefail
+            source "$HOME/.cargo/env"
+            eval "$(opam env)"
+            cd verification
+            DUNEFLAGS="-j 1 --display verbose" dune build
+          ) 2>&1 | tee full-build.log
+    - name: Upload full build log
+      if: always()
+      uses: actions/upload-artifact@v4
+      with:
+        name: full-build-log
+        path: full-build.log

Makefile

@@ -96,6 +96,9 @@ tools: setup
 verify:
 	rm -rf $(ACE_DIR)/security_monitor/verify/
 	PATH="$(RISCV_GNU_TOOLCHAIN_WORK_DIR)/bin:$(PATH)" ACE_DIR=$(ACE_DIR) LINUX_IMAGE=$(LINUX_IMAGE) CROSS_COMPILE=$(CROSS_COMPILE) PLATFORM_RISCV_XLEN=$(PLATFORM_RISCV_XLEN) PLATFORM_RISCV_ISA=$(PLATFORM_RISCV_ISA) PLATFORM_RISCV_ABI=$(PLATFORM_RISCV_ABI) $(MAKE) -C verification verify
+generate_refinedrust_translation:
+	rm -rf $(ACE_DIR)/security_monitor/verify/
+	PATH="$(RISCV_GNU_TOOLCHAIN_WORK_DIR)/bin:$(PATH)" ACE_DIR=$(ACE_DIR) LINUX_IMAGE=$(LINUX_IMAGE) CROSS_COMPILE=$(CROSS_COMPILE) PLATFORM_RISCV_XLEN=$(PLATFORM_RISCV_XLEN) PLATFORM_RISCV_ISA=$(PLATFORM_RISCV_ISA) PLATFORM_RISCV_ABI=$(PLATFORM_RISCV_ABI) $(MAKE) -C verification generate
 
 clean:
 	rm -rf $(ACE_DIR)

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/confidential_flow/handlers/shutdown/shutdown_vm.rs

@@ -14,6 +14,7 @@ use crate::core::control_data::{ConfidentialHart, ConfidentialHartRemoteCommand,
 /// shutdown (lifecycle state `Shutdown`). To do so, we send `Shutdown IPI` to all confidential harts. The last
 /// confidential hart that shutdowns itself, will remove the entire confidential VM from the control data.
 #[derive(Clone, PartialEq)]
+#[rr::skip]
 pub struct ShutdownRequest {
     calling_hart_id: usize,
 }

security-monitor/src/confidential_flow/handlers/symmetrical_multiprocessing/fence_i.rs

@@ -10,6 +10,7 @@ use crate::core::control_data::{
 
 /// Handles a request from one confidential hart to execute fence.i instruction on remote confidential harts.
 #[derive(Clone, PartialEq)]
+#[rr::skip]
 pub struct RemoteFenceI {
     ipi: Ipi,
 }

security-monitor/src/confidential_flow/handlers/symmetrical_multiprocessing/hfence_gvma_vmid.rs

@@ -8,6 +8,7 @@ use crate::core::memory_layout::ConfidentialVmPhysicalAddress;
 
 /// An inter hart request sent by the security monitor to clear G-stage level cached address translations.
 #[derive(Clone, PartialEq)]
+#[rr::skip]
 pub struct RemoteHfenceGvmaVmid {
     ipi: Ipi,
     _start_address: Option<ConfidentialVmPhysicalAddress>,

security-monitor/src/confidential_flow/handlers/symmetrical_multiprocessing/ipi.rs

@@ -10,6 +10,7 @@ use crate::core::control_data::{
 
 /// Handles a request from one confidential hart to execute IPI on other confidential harts.
 #[derive(PartialEq, Debug, Clone)]
+#[rr::skip]
 pub struct Ipi {
     hart_mask: usize,
     hart_mask_base: usize,

security-monitor/src/confidential_flow/handlers/symmetrical_multiprocessing/sfence_vma.rs

@@ -11,6 +11,7 @@ use crate::core::control_data::{
 
 /// Handles a request from one confidential hart to execute sfence.vma instruction on remote confidential harts.
 #[derive(Clone, PartialEq)]
+#[rr::skip]
 pub struct RemoteSfenceVma {
     ipi: Ipi,
     _start_address: usize,

security-monitor/src/confidential_flow/handlers/symmetrical_multiprocessing/sfence_vma_asid.rs

@@ -12,6 +12,7 @@ use crate::core::control_data::{
 /// Handles a request from one confidential hart to execute sfence.vma instruction on remote confidential harts. It represents an inter hart
 /// request.
 #[derive(Clone, PartialEq)]
+#[rr::skip]
 pub struct RemoteSfenceVmaAsid {
     ipi: Ipi,
     _start_address: usize,

security-monitor/src/core/architecture/riscv/control_status_registers.rs

@@ -314,6 +314,7 @@ pub const CSR: &ControlStatusRegister = &ControlStatusRegister {
 };
 
 #[derive(Copy, Clone)]
+#[rr::skip]
 pub struct ReadWriteRiscvCsr<const V: u16>(usize);
 
 impl<const V: u16> ReadWriteRiscvCsr<V> {

security-monitor/src/core/architecture/riscv/general_purpose_registers.rs

@@ -40,6 +40,7 @@ impl GeneralPurposeRegisters {
 #[allow(unused)]
 #[allow(non_camel_case_types)]
 #[repr(usize)]
+#[rr::skip]
 pub enum GeneralPurposeRegister {
     zero = 0,
     ra,

security-monitor/src/core/architecture/riscv/hart_lifecycle_state.rs

@@ -9,6 +9,7 @@
 /// additional lifecycle state `Shutdown` that represents a final state of the confidential hart that has been shutdown
 /// as part of the `VM shutdown` procedure.
 #[derive(PartialEq, Clone)]
+#[rr::skip]
 pub enum HartLifecycleState {
     Started,
     Stopped,

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/control_data/confidential_hart_remote_command.rs

@@ -14,6 +14,7 @@ use crate::core::control_data::ConfidentialHart;
 /// the receiver hart is running, it is interrupted (IPI) and executes the command. If the hart is not running, the command is buffered and
 /// executed on the next time the receiver is scheduled to run.
 #[derive(Clone, PartialEq)]
+#[rr::skip]
 pub enum ConfidentialHartRemoteCommand {
     Ipi(Ipi),
     RemoteFenceI(RemoteFenceI),

security-monitor/src/core/control_data/confidential_vm_measurement.rs

@@ -47,6 +47,7 @@ impl StaticMeasurements {
     }
 }
 
+#[rr::skip]
 impl core::fmt::Debug for StaticMeasurements {
     fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
         self.0.iter().enumerate().for_each(|(id, value)| {

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) }));
         });