Bump Rust + RefinedRust versions

.github/workflows/verify.yml

@@ -22,8 +22,6 @@ jobs:
       run: opam init -y
     - name: Setup opam switch
       run: opam switch create refinedrust-ace --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda
-    - name: Install coq
-      run: eval $(opam env) && opam update && opam pin add coq 8.17.1 -y
     - name: ls
       run: ls -la .
     - name: Install openssl dependency
@@ -44,8 +42,6 @@ jobs:
       run: cargo --version 
     - name: Install RefinedRust stdlib
       run: eval $(opam env) && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/install-stdlib.sh
-    - name: Generate stdlib metadata
-      run: eval $(opam env) && make -C verification/refinedrust/stdlib generate_stdlib
     - name: Exclude RefinedRust from dune build
       run: echo "(dirs :standard \ generated_code.bak refinedrust)" > verification/dune
     - name: install build dependencies
@@ -59,4 +55,4 @@ 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) && make verify
+      run: source "$HOME/.cargo/env" && eval $(opam env) && DUNEFLAGS="-j 1" make verify

.gitignore

@@ -3,10 +3,9 @@
 /target/
 build/*
 target/*
+**/target
 
-tools/cove_tap_tool/target
 qemu/
-security-monitor/target
 
 configurations/overlay/root/harness/baremetal
 confidential-vms/linux_vm/configurations/package_override.dev
@@ -23,4 +22,4 @@ Cargo.lock
 *.ko
 
 # skip log files
-*.log
+*.log

Makefile

@@ -26,7 +26,7 @@ export LINUX_IMAGE						?= $(HYPERVISOR_WORK_DIR)/buildroot/images/Image
 export TOOLS_SOURCE_DIR					?= $(MAKEFILE_SOURCE_DIR)/tools
 export TOOLS_WORK_DIR					?= $(ACE_DIR)/tools
 
-export CROSS_COMPILE					= riscv64-unknown-linux-gnu-
+export CROSS_COMPILE					?= riscv64-unknown-linux-gnu-
 export PLATFORM_RISCV_XLEN				= 64
 export PLATFORM_RISCV_ISA				= rv64gc
 export PLATFORM_RISCV_ABI				= lp64d

rust-toolchain.toml

@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2023-09-15"
-targets = [ "riscv64gc-unknown-none-elf" ]
+channel = "nightly-2025-09-12"
+targets = [ "riscv64gc-unknown-none-elf" ]

security-monitor/Makefile

@@ -38,7 +38,7 @@ build: opensbi_bindings fmt
 refinedrust: opensbi_bindings
 	echo "Generating RefinedRust translation" ;\
 	mkdir -p $(SM_WORK_DIR) ; \
-	RUSTFLAGS='$(RUSTFLAGS)' CARGO_TARGET_DIR=$(SM_WORK_DIR) INSTALL_DIR=$(ACE_DIR) $(CARGO) refinedrust $(RELEASE) $(TARGET) --features verbose ; \
+	RUSTFLAGS='$(RUSTFLAGS)' CARGO_TARGET_DIR=$(SM_WORK_DIR) INSTALL_DIR=$(ACE_DIR) $(CARGO) refinedrust -- $(RELEASE) $(TARGET) --features verbose; \
 	rm -rf $(OPENSBI_WORK_DIR)/
 
 debug: opensbi_bindings

security-monitor/rust-crates/pointers_utility/src/lib.rs

@@ -3,22 +3,25 @@
 // SPDX-License-Identifier: Apache-2.0
 #![no_std]
 #![no_main]
-#![feature(pointer_byte_offsets)]
 
 // used for RefinedRust annotations
 #![feature(register_tool)]
 #![register_tool(rr)]
 #![feature(custom_inner_attributes)]
 #![rr::coq_prefix("ace_ptr")]
+#![rr::include("stdlib")]
 
 
 mod error;
 use core::mem::size_of;
 pub use crate::error::PointerError;
 
 /// Calculates the offset in bytes between two pointers. 
+#[rr::only_spec]
+#[rr::returns("wrap_to_it (pointer1.2 - pointer2.2) isize")]
 pub fn ptr_byte_offset(pointer1: *const usize, pointer2: *const usize) -> isize {
-    (pointer1 as isize) - (pointer2 as isize)
+    // TODO: we should use wrapping arithmetic here, as it might overflow
+    (pointer1.addr() as isize) - (pointer2.addr() as isize)
 }
 
 /// Aligns the pointer to specific size while making sure that the aligned pointer
@@ -34,11 +37,9 @@ pub fn ptr_align(pointer: *mut usize, align_in_bytes: usize, owned_region_end: *
 /// the one-past-the-end address. The returned pointer is guaranteed to be valid for accesses
 /// of size one, if the original pointer is valid. Additional checks are required for making
 /// larger memory accesses.
-#[rr::skip]
-#[rr::params("l", "off", "lmax")]
-#[rr::args("l", "off", "lmax")]
-#[rr::requires("⌜l.2 + off < lmax.2⌝")]
-#[rr::returns("Ok(l +ₗ off)")]
+#[rr::ok]
+#[rr::requires("pointer.2 + offset_in_bytes < owned_region_end.2")]
+#[rr::ensures("ret = (pointer +ₗ offset_in_bytes)")]
 pub fn ptr_byte_add_mut(
     pointer: *mut usize, offset_in_bytes: usize, owned_region_end: *const usize,
 ) -> Result<*mut usize, PointerError> {
@@ -59,6 +60,9 @@ pub fn ptr_byte_add_mut(
 /// the one-past-the-end address. The returned pointer is guaranteed to be valid for accesses
 /// of size one, if the original pointer is valid. Additional checks are required for making
 /// larger memory accesses.
+#[rr::ok]
+#[rr::requires("pointer.2 + offset_in_bytes < owned_region_end.2")]
+#[rr::ensures("ret = (pointer +ₗ offset_in_bytes)")]
 pub fn ptr_byte_add(
     pointer: *const usize, offset_in_bytes: usize, owned_region_end: *const usize,
 ) -> Result<*const usize, PointerError> {

security-monitor/src/confidential_flow/finite_state_machine.rs

@@ -315,23 +315,23 @@ impl<'a> ConfidentialFlow<'a> {
         self
     }
 
-    pub fn confidential_vm_id(&'a self) -> ConfidentialVmId {
+    pub fn confidential_vm_id(&self) -> ConfidentialVmId {
         self.confidential_hart().confidential_vm_id().expect(Self::DUMMY_HART_ERROR_MSG)
     }
 
-    fn confidential_hart_id(&'a self) -> usize {
+    fn confidential_hart_id(&self) -> usize {
         self.confidential_hart().confidential_hart_id()
     }
 
     fn confidential_hart_mut(&mut self) -> &mut ConfidentialHart {
         self.hardware_hart.confidential_hart_mut()
     }
 
-    fn confidential_hart(&'a self) -> &ConfidentialHart {
+    fn confidential_hart(&self) -> &ConfidentialHart {
         self.hardware_hart.confidential_hart()
     }
 
-    fn hypervisor_hart(&'a self) -> &HypervisorHart {
+    fn hypervisor_hart(&self) -> &HypervisorHart {
         &self.hardware_hart.hypervisor_hart()
     }
 }

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

@@ -2,7 +2,6 @@
 // SPDX-FileContributor: Wojciech Ozga <woz@zurich.ibm.com>, IBM Research - Zurich
 // SPDX-License-Identifier: Apache-2.0
 #![rr::import("ace.theories.page_allocator", "page")]
-#![rr::include("option")]
 
 // The order of page size in this enum must follow the increasing sizes of page to guarantee that the Ord/PartialOrd are correctly derived
 // for the `PageSize`.
@@ -30,10 +29,9 @@ impl PageSize {
     // and 4KiB).
     pub const TYPICAL_NUMBER_OF_PAGES_INSIDE_LARGER_PAGE: usize = 512;
 
+    // TODO: need performance optimizations for verifying this
     #[rr::trust_me]
-    #[rr::params("x")]
-    #[rr::args("#x")]
-    #[rr::returns("page_size_in_bytes_Z x")]
+    #[rr::returns("page_size_in_bytes_Z self")]
     pub fn in_bytes(&self) -> usize {
         match self {
             PageSize::Size128TiB => 8 * 512 * 512 * 512 * 512 * 256,
@@ -45,10 +43,7 @@ impl PageSize {
         }
     }
 
-    #[rr::trust_me]
-    #[rr::params("x")]
-    #[rr::args("#x")]
-    #[rr::returns("<#>@{option} page_size_smaller x")]
+    #[rr::returns("page_size_smaller self")]
     pub fn smaller(&self) -> Option<PageSize> {
         match self {
             PageSize::Size128TiB => Some(PageSize::Size512GiB),
@@ -60,10 +55,7 @@ impl PageSize {
         }
     }
 
-    #[rr::trust_me]
-    #[rr::params("x")]
-    #[rr::args("#x")]
-    #[rr::returns("<#>@{option} page_size_larger x")]
+    #[rr::returns("page_size_larger self")]
     pub fn larger(&self) -> Option<PageSize> {
         match self {
             PageSize::Size128TiB => None,
@@ -75,10 +67,7 @@ impl PageSize {
         }
     }
 
-    #[rr::trust_me]
-    #[rr::params("x")]
-    #[rr::args("#x")]
-    #[rr::returns("page_size_multiplier x")]
+    #[rr::returns("number_of_smaller_pages self")]
     pub fn number_of_smaller_pages(&self) -> usize {
         match self {
             PageSize::Size128TiB => 256,

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

@@ -20,10 +20,7 @@ pub enum PageTableLevel {
 }
 
 impl PageTableLevel {
-    #[rr::trust_me]
-    #[rr::params("x")]
-    #[rr::args("#x")]
-    #[rr::returns("<#>@{option} (page_table_level_lower x)")]
+    #[rr::returns("page_table_level_lower self")]
     pub fn lower(&self) -> Option<Self> {
         match self {
             Self::Level5 => Some(Self::Level4),

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

@@ -11,8 +11,9 @@ use crate::core::memory_layout::ConfidentialVmPhysicalAddress;
 #[derive(Debug, Copy, Clone)]
 #[rr::refined_by("paging_system")]
 pub enum PagingSystem {
+    #[rr::pattern("Sv48")]
     Sv48x4,
-    #[rr::pattern("Sv57x4")]
+    #[rr::pattern("Sv57")]
     Sv57x4,
 }
 
@@ -31,10 +32,7 @@ impl PagingSystem {
         }
     }
 
-    #[rr::skip]
-    #[rr::params("system")]
-    #[rr::args("#system")]
-    #[rr::returns("paging_system_highest_level system")]
+    #[rr::returns("paging_system_highest_level self")]
     pub fn levels(&self) -> PageTableLevel {
         match self {
             PagingSystem::Sv48x4 => PageTableLevel::Level4,

security-monitor/src/core/heap_allocator/allocator.rs

@@ -22,7 +22,7 @@ impl<A> Locked<A> {
         Locked { inner: spin::Mutex::new(inner) }
     }
 
-    pub fn lock(&self) -> spin::MutexGuard<A> {
+    pub fn lock(&self) -> spin::MutexGuard<'_, A> {
         self.inner.lock()
     }
 }

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

@@ -8,7 +8,7 @@ mod allocator;
 
 /// global allocator allocates memory on the security monitor's heap.
 #[global_allocator]
-static mut HEAP_ALLOCATOR: Locked<LinkedListAllocator> = Locked::new(LinkedListAllocator::new());
+static HEAP_ALLOCATOR: Locked<LinkedListAllocator> = Locked::new(LinkedListAllocator::new());
 
 pub(super) fn init_heap(start_address: ConfidentialMemoryAddress, heap_size: usize) {
     debug!("Heap {:x}-{:x}", start_address.as_usize(), start_address.as_usize() + heap_size);

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

@@ -21,49 +21,36 @@ pub struct ConfidentialMemoryAddress(#[rr::field("l")] *mut usize);
 /// Verification: We require the ghost state for the global memory layout to be available.
 #[rr::context("onceG Σ memory_layout")]
 impl ConfidentialMemoryAddress {
-    #[rr::params("l", "MEMORY_CONFIG")]
-    #[rr::args("l")]
+    #[rr::params("MEMORY_CONFIG")]
     /// Precondition: The global memory layout is initialized.
     #[rr::requires(#iris "once_status \"MEMORY_LAYOUT\" (Some MEMORY_CONFIG)")]
     /// Precondition: The address is in the confidential region of the global memory layout.
-    #[rr::requires("(MEMORY_CONFIG.(conf_start).2 ≤ l.2 < MEMORY_CONFIG.(conf_end).2)%Z")]
-    #[rr::returns("l")]
+    #[rr::requires("(MEMORY_CONFIG.(conf_start).2 ≤ address.2 < MEMORY_CONFIG.(conf_end).2)%Z")]
+    #[rr::returns("address")]
+    // TODO this should be unsafe
     pub(super) fn new(address: *mut usize) -> Self {
         Self(address)
     }
 
-    #[rr::params("l")]
-    #[rr::args("#l")]
-    #[rr::returns("l")]
-    pub unsafe fn to_ptr(&self) -> *const u8 {
+    #[rr::returns("self")]
+    pub fn to_ptr(&self) -> *const u8 {
         self.0 as *const u8
     }
 
-    #[rr::only_spec]
-    #[rr::params("l")]
-    #[rr::args("#l")]
-    #[rr::returns("l.2")]
+    #[rr::returns("self.2")]
     pub fn as_usize(&self) -> usize {
-        // TODO: check if we need to expose the pointer.
-        // If not, use addr() instead.
-        // self.0.addr()
-        self.0 as usize
+        self.0.addr()
     }
 
     #[rr::only_spec]
-    #[rr::params("l", "align")]
-    #[rr::args("#l", "align")]
     /// Postcondition: Verifies that the pointer is aligned to the given alignment.
-    #[rr::returns("bool_decide (l `aligned_to` (Z.to_nat align))")]
+    #[rr::returns("bool_decide (self `aligned_to` (Z.to_nat align))")]
     pub fn is_aligned_to(&self, align: usize) -> bool {
         self.0.is_aligned_to(align)
     }
 
-    #[rr::only_spec]
-    #[rr::params("this", "other")]
-    #[rr::args("#this", "other")]
     /// Postcondition: Compute the offset.
-    #[rr::returns("other.2 - this.2")]
+    #[rr::returns("wrap_to_it (pointer.2 - self.2) isize")]
     pub fn offset_from(&self, pointer: *const usize) -> isize {
         ptr_byte_offset(pointer, self.0)
     }
@@ -76,17 +63,17 @@ impl ConfidentialMemoryAddress {
     /// The caller must ensure that the address at given offset is still within the confidential memory region.
     // TODO: can we require the offset to be a multiple of usize? (woz: yes we can)
     #[rr::only_spec]
-    #[rr::params("l", "off", "lmax", "MEMORY_CONFIG")]
-    #[rr::args("#l", "off", "lmax")]
-    /// Precondition: The offset address is in the given range.
-    #[rr::requires("l.2 + off < lmax.2")]
+    #[rr::params("MEMORY_CONFIG")]
     /// Precondition: The global memory layout is initialized.
     #[rr::requires(#iris "once_status \"MEMORY_LAYOUT\" (Some MEMORY_CONFIG)")]
+    #[rr::ok]
+    /// 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("lmax.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::returns("Ok(#(l +ₗ off))")]
-    pub unsafe fn add(&self, offset_in_bytes: usize, upper_bound: *const usize) -> Result<ConfidentialMemoryAddress, Error> {
+    #[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))
     }
@@ -96,12 +83,9 @@ impl ConfidentialMemoryAddress {
     ///
     /// Caller must ensure that the pointer is not used by two threads simultaneously and that it is correctly aligned for usize.
     /// See `ptr::read_volatile` for safety concerns
-    // TODO: currently only_spec because shim registration for read_volatile doesn't work
-    // TODO require that lifetime [lft_el] is actually alive
-    #[rr::only_spec]
-    #[rr::params("l", "z", "lft_el")]
-    #[rr::args("#l")]
-    #[rr::requires(#iris "l ◁ₗ[π, Shared lft_el] #z @ ◁ int usize_t")]
+    #[rr::params("z", "lft_el")]
+    #[rr::unsafe_elctx("[ϝ ⊑ₑ lft_el]")]
+    #[rr::requires(#iris "self ◁ₗ[π, Shared lft_el] #z @ ◁ int usize")]
     #[rr::returns("z")]
     pub unsafe fn read_volatile<'a>(&'a self) -> usize {
         self.0.read_volatile()
@@ -112,12 +96,9 @@ impl ConfidentialMemoryAddress {
     ///
     /// Caller must ensure that the pointer is not used by two threads simultaneously and that it is correctly aligned for usize.
     /// See `ptr::write_volatile` for safety concerns
-    // TODO: currently only_spec because shim registration for write_volatile doesn't work
-    #[rr::only_spec]
-    #[rr::params("l", "z", "x")]
-    #[rr::args("#l", "x")]
-    #[rr::requires(#type "l" : "z" @ "int usize_t")]
-    #[rr::ensures(#type "l" : "x" @ "int usize_t")]
+    #[rr::params("z")]
+    #[rr::requires(#type "self" : "z" @ "int usize")]
+    #[rr::ensures(#type "self" : "value" @ "int usize")]
     pub unsafe fn write_volatile(&self, value: usize) {
         self.0.write_volatile(value);
     }