Progress on page allocator verification

Signed-off-by: Lennard Gäher <[email protected]>

Author: lgaeher

.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,