From 46109de60f9ef79582bd3db67c7acef99be474cd Mon Sep 17 00:00:00 2001 From: Wojciech Ozga Date: Mon, 10 Aug 2026 06:26:29 +0000 Subject: [PATCH] Add OOPSLA paper, update dependencies Signed-off-by: Wojciech Ozga --- .github/workflows/build.yml | 2 +- .github/workflows/verify.yml | 2 +- README.md | 36 +++++++++----- security-monitor/Cargo.lock | 4 +- security-monitor/Cargo.toml | 2 +- .../rust-crates/riscv_cove_tap/Cargo.toml | 2 +- .../confidential_memory_address.rs | 3 +- .../non_confidential_memory_address.rs | 5 +- .../src/core/page_allocator/allocator.rs | 47 ++++++++++--------- security-monitor/src/debug.rs | 3 +- security-monitor/src/lib.rs | 1 - tools/cove_tap_tool/Cargo.lock | 4 +- 12 files changed, 62 insertions(+), 49 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 381b7dc4..cdd7011d 100644 --- a/.github/workflows/build.yml +++ b/.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 diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 4e8b10b3..5cb17259 100644 --- a/.github/workflows/verify.yml +++ b/.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' diff --git a/README.md b/README.md index fae71717..22fcaa78 100644 --- a/README.md +++ b/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} +} +``` + diff --git a/security-monitor/Cargo.lock b/security-monitor/Cargo.lock index 5850a31c..601f9ab7 100644 --- a/security-monitor/Cargo.lock +++ b/security-monitor/Cargo.lock @@ -588,9 +588,9 @@ checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" [[package]] name = "spin" -version = "0.10.0" +version = "0.12.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d5fe4ccb98d9c292d56fec89a5e07da7fc4cf0dc11e156b41793132775d3e591" +checksum = "8abadc99fd9c7bbb7d0ca2b31d72a067d0c0dcd7aad25ab8cac71ba91417694b" [[package]] name = "static_assertions" diff --git a/security-monitor/Cargo.toml b/security-monitor/Cargo.toml index 95fb9344..e764fdd6 100644 --- a/security-monitor/Cargo.toml +++ b/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"]} diff --git a/security-monitor/rust-crates/riscv_cove_tap/Cargo.toml b/security-monitor/rust-crates/riscv_cove_tap/Cargo.toml index ec7da892..6833c23e 100644 --- a/security-monitor/rust-crates/riscv_cove_tap/Cargo.toml +++ b/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 = [] } diff --git a/security-monitor/src/core/memory_layout/confidential_memory_address.rs b/security-monitor/src/core/memory_layout/confidential_memory_address.rs index c74a4dcf..dafbfe31 100644 --- a/security-monitor/src/core/memory_layout/confidential_memory_address.rs +++ b/security-monitor/src/core/memory_layout/confidential_memory_address.rs @@ -1,9 +1,9 @@ // SPDX-FileCopyrightText: 2023 IBM Corporation // SPDX-FileContributor: Wojciech Ozga , 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() diff --git a/security-monitor/src/core/memory_layout/non_confidential_memory_address.rs b/security-monitor/src/core/memory_layout/non_confidential_memory_address.rs index a8fa77ef..0e93b05d 100644 --- a/security-monitor/src/core/memory_layout/non_confidential_memory_address.rs +++ b/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 { 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)) } diff --git a/security-monitor/src/core/page_allocator/allocator.rs b/security-monitor/src/core/page_allocator/allocator.rs index 928f7348..d80dd5b8 100644 --- a/security-monitor/src/core/page_allocator/allocator.rs +++ b/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)")] diff --git a/security-monitor/src/debug.rs b/security-monitor/src/debug.rs index 160dc909..cb7c53ff 100644 --- a/security-monitor/src/debug.rs +++ b/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 {} diff --git a/security-monitor/src/lib.rs b/security-monitor/src/lib.rs index bc02078d..ea209ad5 100644 --- a/security-monitor/src/lib.rs +++ b/security-monitor/src/lib.rs @@ -63,5 +63,4 @@ mod rr_wrappers { pub fn vec_iter_mut(x: &mut Vec) -> core::slice::IterMut<'_, T> { x.iter_mut() } - } diff --git a/tools/cove_tap_tool/Cargo.lock b/tools/cove_tap_tool/Cargo.lock index 9fef3d02..a1a99f52 100644 --- a/tools/cove_tap_tool/Cargo.lock +++ b/tools/cove_tap_tool/Cargo.lock @@ -420,9 +420,9 @@ dependencies = [ [[package]] name = "rand" -version = "0.8.5" +version = "0.8.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404" +checksum = "22f6172bdec972074665ed81ed53b71da00bfc44b65a753cfde883ec4c702a1a" dependencies = [ "libc", "rand_chacha",