Add OOPSLA paper to README.

.github/workflows/build.yml

@@ -10,7 +10,7 @@ jobs:
   build:
     runs-on: ubuntu-24.04
     steps:
-    - uses: actions/checkout@v5
+    - uses: actions/checkout@v7
       with:
         submodules: 'true'
     - name: install build dependencies

.github/workflows/verify.yml

@@ -10,7 +10,7 @@ jobs:
     runs-on: ubuntu-latest  # container actions require GNU/Linux
     steps:
     - name: Checkout repository
-      uses: actions/checkout@v5
+      uses: actions/checkout@v7
       with:
         persist-credentials: false
         submodules: 'true'

README.md

@@ -163,33 +163,31 @@ Integrating local attestation with dm-crypt/LUKS is work in progress. When finis
 A script in initrd will then retrieve the decryption key from TAP and decrypt the rootfs.
 
 # License
-This repository is distributed under the terms of the Apache 2.0 License, see [LICENSE](LICENSE).
-
-**This is an active research project, without warranties of any kind.**
+This repository is distributed under the terms of the Apache 2.0 License, see [LICENSE](LICENSE). This is an active research project, without warranties of any kind.
 
 # Citation
-**Our newest full paper on ACE:**
+**Full paper on ACE:**
 ```
 @misc{ozga2025ace,
     author = {Ozga, Wojciech and Hunt, Guerney D. H. and Le, Michael V. and Gaeher Lennard and Shinnar, Avraham and Palmer, Elaine R. and Jamjoom, Hani and Dragone, Silvio},
-    title = {ACE: Confidential Computing for Embedded RISC-V Systems},
+    title = {ACE: Towards A High-Assurance Isolated Virtualization Environment for RISC-V},
     year = 2025,
     howpublished = {\url{https://arxiv.org/pdf/2505.12995}}
 }
 ```
 
-**Our workshop paper on ACE:**
+**Paper on formal verification of page allocator:**
 ```
-@inproceedings{ozga2023riscvtee,
-    title={Towards a Formally Verified Security Monitor for VM-based Confidential Computing},
-    author={Ozga, Wojciech and Hunt, Guerney D. H. and Le, Michael V. and Palmer, Elaine R. and Shinnar, Avraham},
-    booktitle = {Proceedings of the 12th International Workshop on Hardware and Architectural Support for Security and Privacy},
-    series = {HASP2023},
-    year={2023}
+@inproceedings{gaher2026rr,
+    author = {Gäher, Lennard and Lafeychine, Vincent and Kehrli, Sascha and Shinnar, Avraham and Ozga, Wojciech and Hunt, Guerney D. H. and Dreyer, Derek},
+    title = {Bringing Foundational Verification to Real-World Rust Code},
+    booktitle = {Proceedings of the ACM on Programming Languages},
+    series = {OOPSLA 2026},
+    year = 2026
 }
 ```
 
-**Our paper on context switch validation:**
+**Paper on context switch validation:**
 ```
 @misc{kalani2025sailor,
     author = {Kalani, Neelu and Bourgeat, Thomas and Hunt, Guerney D.H. and Ozga, Wojciech},
@@ -199,3 +197,15 @@ This repository is distributed under the terms of the Apache 2.0 License, see [L
     year = 2025
 }
 ```
+
+**Workshop paper on ACE:**
+```
+@inproceedings{ozga2023riscvtee,
+    title={Towards a Formally Verified Security Monitor for VM-based Confidential Computing},
+    author={Ozga, Wojciech and Hunt, Guerney D. H. and Le, Michael V. and Palmer, Elaine R. and Shinnar, Avraham},
+    booktitle = {Proceedings of the 12th International Workshop on Hardware and Architectural Support for Security and Privacy},
+    series = {HASP2023},
+    year={2023}
+}
+```
+

security-monitor/Cargo.toml

@@ -25,7 +25,7 @@ pointers_utility = {path = "rust-crates/pointers_utility"}
 riscv-decode = "0.2"
 
 # The `spin` crate provides synchronization primitives (Mutexes etc) using spinlocks
-spin = {version="0.10", default-features = false, features = ["once", "rwlock", "spin_mutex"]}
+spin = {version="0.12", default-features = false, features = ["once", "rwlock", "spin_mutex"]}
 
 # This crates provides functionality to parse TVM attestation payload (TAP).
 riscv_cove_tap = {path = "rust-crates/riscv_cove_tap", features = ["parser"]}

security-monitor/rust-crates/riscv_cove_tap/Cargo.toml

@@ -6,7 +6,7 @@ description = "Library to parse the RISC-V CoVE's TEE attestation payload"
 edition = "2024"
 
 [dependencies]
-rand = {version = "0.8.5", optional=true}
+rand = {version = "0.8.6", optional=true}
 
 hybrid-array = "0.2.3"
 ml-kem = {version = "0.3.0-pre", default-features=false, features = [] }

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

@@ -1,9 +1,9 @@
 // SPDX-FileCopyrightText: 2023 IBM Corporation
 // SPDX-FileContributor: Wojciech Ozga <woz@zurich.ibm.com>, IBM Research - Zurich
 // SPDX-License-Identifier: Apache-2.0
+use super::MemoryLayout;
 use crate::error::Error;
 use pointers_utility::{ptr_byte_add_mut, ptr_byte_offset};
-use super::MemoryLayout;
 
 /// The wrapper over a raw pointer that is guaranteed to be an address located in the confidential memory region.
 #[repr(transparent)]
@@ -38,7 +38,6 @@ impl ConfidentialMemoryAddress {
         self.0 as *const u8
     }
 
-
     #[rr::returns("self.(loc_a)")]
     pub fn as_usize(&self) -> usize {
         self.0.addr()

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

@@ -58,7 +58,10 @@ impl NonConfidentialMemoryAddress {
     pub unsafe fn add(&self, offset_in_bytes: usize, upper_bound: *const usize) -> Result<NonConfidentialMemoryAddress, Error> {
         let memory_layout = MemoryLayout::read();
         ensure!(upper_bound <= memory_layout.non_confidential_memory_end, Error::AddressNotInNonConfidentialMemory())?;
-        let pointer = ptr_byte_add_mut(self.0, offset_in_bytes, upper_bound).map_err(#[rr::verify] |_| Error::AddressNotInNonConfidentialMemory())?;
+        let pointer = ptr_byte_add_mut(self.0, offset_in_bytes, upper_bound).map_err(
+            #[rr::verify]
+            |_| Error::AddressNotInNonConfidentialMemory(),
+        )?;
         Ok(NonConfidentialMemoryAddress(pointer))
     }
 

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

@@ -269,10 +269,11 @@ impl PageAllocator {
             #[rr::ok]
             #[rr::ensures("if_Ok ret (λ tok, tok.(page_sz) = {page_size_to_allocate})")]
             |page_allocator| {
-            let base_address = page_allocator.base_address;
-            let page_size = page_allocator.page_size;
-            Ok(page_allocator.root.acquire_page_token(base_address, page_size, page_size_to_allocate))
-        })?
+                let base_address = page_allocator.base_address;
+                let page_size = page_allocator.page_size;
+                Ok(page_allocator.root.acquire_page_token(base_address, page_size, page_size_to_allocate))
+            },
+        )?
     }
 
     /// Consumes the page tokens given by the caller, allowing for their further acquisition. This is equivalent to deallocation of the
@@ -288,23 +289,25 @@ impl PageAllocator {
             #[rr::requires(#iris "once_initialized π \"MEMORY_LAYOUT\" (Some MEMORY_CONFIG)")]
             #[rr::returns("Ok tt")]
             |page_allocator| {
-            let base_address = page_allocator.base_address;
-            let page_size = page_allocator.page_size;
-            let root_node = &mut page_allocator.root;
-            for page_token in released_pages {
-                #[rr::params("γ")]
-                #[rr::inv_vars("root_node")]
-                #[rr::inv("root_node.ghost = γ")]
-                #[rr::inv("root_node.cur.(max_node_size) = Size128TiB")]
-                #[rr::inv("root_node.cur.(base_address) = 0%Z")]
-                #[rr::ignore]
-                #[allow(unused)]
-                || {};
-
-                root_node.store_page_token(base_address, page_size, page_token);
-            }
-            Ok(())
-        }).unwrap();
+                let base_address = page_allocator.base_address;
+                let page_size = page_allocator.page_size;
+                let root_node = &mut page_allocator.root;
+                for page_token in released_pages {
+                    #[rr::params("γ")]
+                    #[rr::inv_vars("root_node")]
+                    #[rr::inv("root_node.ghost = γ")]
+                    #[rr::inv("root_node.cur.(max_node_size) = Size128TiB")]
+                    #[rr::inv("root_node.cur.(base_address) = 0%Z")]
+                    #[rr::ignore]
+                    #[allow(unused)]
+                    || {};
+
+                    root_node.store_page_token(base_address, page_size, page_token);
+                }
+                Ok(())
+            },
+        )
+        .unwrap();
         //.inspect_err(|_| debug!("Memory leak: failed to store released pages in the page allocator"));
     }
 
@@ -507,7 +510,6 @@ impl PageStorageTreeNode {
 
     /// Creates children for the given node because the node gets created with an empty list of children, expecting that children will be
     /// created lazily with this function.
-    ///
     #[rr::params("smaller_sz")]
     /// Precondition: the page size argument has to match the node's logical state.
     #[rr::requires("this_node_page_size = self.cur.(max_node_size)")]
@@ -601,7 +603,6 @@ impl PageStorageTreeNode {
 
     /// Merges page tokens owned by children.
     /// Safety: Requires that all children have been initialized.
-    ///
     #[rr::params("smaller_sz")]
     /// Precondition: The children are initialized.
     #[rr::requires("Hchild_init" : "self.cur.(children_initialized)")]

security-monitor/src/debug.rs

@@ -88,7 +88,8 @@ macro_rules! debug {
     ($fmt:expr, $($args:tt)+) => {{}};
 }
 
-pub(crate) use {_debug, debug};
+pub(crate) use _debug;
+pub(crate) use debug;
 
 pub struct Console {}
 

security-monitor/src/lib.rs

@@ -63,5 +63,4 @@ mod rr_wrappers {
     pub fn vec_iter_mut<T>(x: &mut Vec<T>) -> core::slice::IterMut<'_, T> {
         x.iter_mut()
     }
-
 }