Initial formal verification results

.github/workflows/verify.yml

@@ -44,6 +44,12 @@ jobs:
       run: eval $(opam env) && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/setup-coq.sh
     - name: Install RefinedRust type system
       run: eval $(opam env) && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/install-typesystem.sh
+    - 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
       run: sudo apt -qq -y install wget autoconf automake autotools-dev curl python3 libmpc-dev libmpfr-dev libgmp-dev gawk build-essential bison flex texinfo gperf libtool patchutils bc zlib1g-dev libexpat-dev
     - name: install OpenSBI dependencies
@@ -54,7 +60,5 @@ jobs:
       run: source "$HOME/.cargo/env" && eval $(opam env) && make setup
     - name: make devtools
       run: source "$HOME/.cargo/env" && eval $(opam env) && make devtools
-    - name: Translate specified files using RefinedRust
+    - name: Translate specified files using RefinedRust and check proofs
       run: source "$HOME/.cargo/env" && eval $(opam env) && make verify
-    - name: Check proofs
-      run: eval $(opam env) && cd verification && dune build

Makefile

@@ -82,6 +82,7 @@ tools: setup
 	cp -rf $(TOOLS_SOURCE_DIR)/* $(TOOLS_WORK_DIR)
 
 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
 
 clean:

security-monitor/Makefile

@@ -35,8 +35,11 @@ build: opensbi_bindings fmt
 	cp $(SM_WORK_DIR)/$(CHAIN)/release/$(EXEC_NAME) $(SM_WORK_DIR)/ ; \
 	rm -rf $(OPENSBI_WORK_DIR)/
 
-refinedrust: build
-	RUSTFLAGS='$(RUSTFLAGS)' CARGO_TARGET_DIR=$(SM_WORK_DIR) INSTALL_DIR=$(ACE_DIR) $(CARGO) refinedrust $(RELEASE) $(TARGET) --features verbose
+refinedrust: opensbi_bindings
+	echo "Generating OpenSBI bindings" ;\
+	mkdir -p $(SM_WORK_DIR) ; \
+	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
 	echo "Compiling the security monitor in DEBUG mode" ;\

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

@@ -5,6 +5,13 @@
 #![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")]
+
+
 mod error;
 use core::mem::size_of;
 pub use crate::error::PointerError;
@@ -27,6 +34,11 @@ 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)")]
 pub fn ptr_byte_add_mut(
     pointer: *mut usize, offset_in_bytes: usize, owned_region_end: *const usize,
 ) -> Result<*mut usize, PointerError> {

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

@@ -1,22 +1,39 @@
 // SPDX-FileCopyrightText: 2023 IBM Corporation
 // SPDX-FileContributor: Wojciech Ozga <woz@zurich.ibm.com>, IBM Research - Zurich
 // SPDX-License-Identifier: Apache-2.0
+#![rr::import("ace.theories.page", "page_extra")]
+#![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`.
 #[repr(u8)]
 #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
+#[rr::refined_by("page_size")]
 pub enum PageSize {
+    #[rr::pattern("Size4KiB")]
     Size4KiB,
     /// 16KiB page is used by G-stage root page table in RISC-V
+    #[rr::pattern("Size16KiB")]
     Size16KiB,
+    #[rr::pattern("Size2MiB")]
     Size2MiB,
+    #[rr::pattern("Size1GiB")]
     Size1GiB,
+    #[rr::pattern("Size512GiB")]
     Size512GiB,
+    #[rr::pattern("Size128TiB")]
     Size128TiB,
 }
 
 impl PageSize {
+    // Usually there are 512 pages of size x that can fit in a single page of size y, where y is next page size larger than x (e.g., 2MiB
+    // and 4KiB).
+    pub const TYPICAL_NUMBER_OF_PAGES_INSIDE_LARGER_PAGE: usize = 512;
+
+    #[rr::trust_me]
+    #[rr::params("x")]
+    #[rr::args("#x")]
+    #[rr::returns("page_size_in_bytes_Z x")]
     pub fn in_bytes(&self) -> usize {
         match self {
             PageSize::Size128TiB => 8 * 512 * 512 * 512 * 512 * 256,
@@ -28,6 +45,10 @@ impl PageSize {
         }
     }
 
+    #[rr::trust_me]
+    #[rr::params("x")]
+    #[rr::args("#x")]
+    #[rr::returns("<#>@{option} page_size_smaller x")]
     pub fn smaller(&self) -> Option<PageSize> {
         match self {
             PageSize::Size128TiB => Some(PageSize::Size512GiB),
@@ -39,6 +60,10 @@ impl PageSize {
         }
     }
 
+    #[rr::trust_me]
+    #[rr::params("x")]
+    #[rr::args("#x")]
+    #[rr::returns("<#>@{option} page_size_larger x")]
     pub fn larger(&self) -> Option<PageSize> {
         match self {
             PageSize::Size128TiB => None,
@@ -61,10 +86,12 @@ impl PageSize {
         }
     }
 
+    #[rr::returns("Size128TiB")]
     pub fn largest() -> PageSize {
         PageSize::Size128TiB
     }
 
+    #[rr::returns("Size4KiB")]
     pub fn smallest() -> PageSize {
         PageSize::Size4KiB
     }

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

@@ -1,6 +1,7 @@
 // SPDX-FileCopyrightText: 2023 IBM Corporation
 // SPDX-FileContributor: Wojciech Ozga <woz@zurich.ibm.com>, IBM Research - Zurich
 // SPDX-License-Identifier: Apache-2.0
+#![rr::import("ace.theories.page_table", "page_table")]
 use crate::core::architecture::mmu::page_table_entry::{LogicalPageTableEntry, PageTableEntry};
 use crate::core::architecture::mmu::page_table_level::PageTableLevel;
 use crate::core::architecture::mmu::paging_system::PagingSystem;
@@ -14,6 +15,8 @@ use alloc::boxed::Box;
 use alloc::vec::Vec;
 use sha2::digest::crypto_common::generic_array::GenericArray;
 
+// TODO: rename Page -> PageToken ?
+// Consider: make generic over PageTableLevel
 /// Represents an architectural 2nd level page table that defines the guest physical to real address translation. The security monitor fully
 /// controls these mappings for confidential VMs. These page tables are stored in confidential memory (use `Page<Allocated>`).
 ///
@@ -26,16 +29,30 @@ use sha2::digest::crypto_common::generic_array::GenericArray;
 ///
 /// During the execution of a confidential hart, MMU might traverse the serialized representation. Our changes to this representation must
 /// be atomic, so that MMU always reads a valid configuration.
+#[rr::refined_by("pt_logical" : "page_table_tree")]
+#[rr::exists("pt_byte" : "page")]
+#[rr::invariant("is_byte_level_representation pt_logical p_byte")]
 pub struct PageTable {
+    #[rr::field("pt_get_level pt_logical")]
     level: PageTableLevel,
+    #[rr::field("pt_get_system pt_logical")]
     paging_system: PagingSystem,
     /// Serialized representation stores the architecture-specific, binary representation of the page table configuration that is read by
     /// the MMU.
+    #[rr::field("pt_byte")]
     serialized_representation: Page<Allocated>,
     /// Logical representation stores a strongly typed page table configuration used by security monitor.
+    #[rr::field("<#> (pt_get_entries pt_logical)")]
     logical_representation: Vec<LogicalPageTableEntry>,
 }
 
+// What do we want to prove?
+// - good structure according to hw spec
+// - page table has unique ownership over all "reachable" memory
+// - copy from non-confidential memory only reads from non-confidential memory
+// - if input to copy_.. is not a valid page table, fail correctly
+
+#[rr::skip]
 impl PageTable {
     /// This functions copies recursively page table structure from non-confidential memory to confidential memory. It
     /// allocated a page in confidential memory for every page table. After this function executes, a valid page table
@@ -53,6 +70,45 @@ impl PageTable {
     ///   * all `pointer` page table entries point to another page table belonging to the same page table configuration.
     ///
     /// This is a recursive function, which deepest execution is not larger than the number of paging system levels.
+    // input: page table to copy
+    // output:
+    //
+    // Need to make sure that we only copy from non-confidential memory.
+    //
+    // NOTE: Attestation happens after this function.
+    // - measure in order of guest-physical addresses
+    // - if hypervisor switches around order of guest-physical addresses, attestation will
+    // fail
+    //
+    // NOTE: Does not support COW. The hypervisor cannot map zeroed pages to the same address (this function will create multiple copies and
+    // create a static image). Every entry in the page table will get its own physical page.
+    //
+    // Implicit property of this specification: We do not copy from confidential memory, as we do
+    // not get memory permission for that.
+    // SPEC 1:
+    // For security (not trusting the hypervisor):
+    #[rr::params("l_nonconf", "ps", "level")]
+    #[rr::args("l_nonconf", "ps", "level")]
+    #[rr::requires(#iris "permission_to_read_from_nonconfidential_mem")]
+    // might need atomicity?
+    // TODO: want to prove eventually
+    //#[rr::ensures("value_has_security_level Hypervisor x")]
+    // eventually: promote x from Hypervisor to confidential_vm_{new_id}
+    #[rr::exists("x" : "result page_table_tree core_error_Error")]
+    #[rr::returns("<#>@{result} x")]
+    /* Alternative specification:
+    // We won't need this for security, but if we were to trust the hypervisor, we could
+    // prove this specification.
+    //
+    // SPEC 2:
+    // For functional correctness (trusting the hypervisor):
+    #[rr::params("l_nonconf", "ps", "level" : "nat", "pt" : "page_table_tree")]
+    #[rr::args("l_nonconf", "ps", "level")]
+    #[rr::requires(#iris "address_has_valid_page_table l_nonconf pt")]
+    #[rr::exists("pt'")]
+    #[rr::ensures("related_page_tables pt pt'")]
+    #[rr::returns("#Ok(pt')")]   // TODO or out of memory
+    */
     pub fn copy_from_non_confidential_memory(
         address: NonConfidentialMemoryAddress, paging_system: PagingSystem, level: PageTableLevel,
     ) -> Result<Self, Error> {
@@ -91,6 +147,11 @@ impl PageTable {
 
     /// Creates an empty page table for the given page table level. Returns error if there is not enough memory to allocate this data
     /// structure.
+    #[rr::params("system", "level")]
+    #[rr::args("system", "level")]
+    #[rr::exists("res")]
+    #[rr::returns("<#>@{result} res")]
+    #[rr::returns("if_Ok res (λ tree, tree = make_empty_page_tree system level)")]
     pub fn empty(paging_system: PagingSystem, level: PageTableLevel) -> Result<Self, Error> {
         let serialized_representation = PageAllocator::acquire_page(paging_system.memory_page_size(level))?.zeroize();
         let number_of_entries = serialized_representation.size().in_bytes() / paging_system.entry_size();
@@ -188,6 +249,9 @@ impl PageTable {
     }
 
     /// Returns the physical address in confidential memory of the page table configuration.
+    #[rr::params("pt")]
+    #[rr::args("#pt")]
+    #[rr::returns("pt_get_serialized_loc pt")]
     pub fn address(&self) -> usize {
         self.serialized_representation.start_address()
     }
@@ -197,6 +261,12 @@ impl PageTable {
     }
 
     /// Set a new page table entry at the given index, replacing whatever was there before.
+    // TODO: this requires the representation to be fully initialized, which is not true for empty() page tables.
+    // (or we need to reflect this in pt_number_of_entries accordingly)
+    #[rr::params("pt", "γ", "vpn", "pte")]
+    #[rr::args("(#pt, γ)", "vpn", "pte")]
+    #[rr::requires("vpn < pt_number_of_entries pt")]
+    #[rr::oberve("γ": "pt_set_entry pt vpn pte")]
     fn set_entry(&mut self, virtual_page_number: usize, entry: LogicalPageTableEntry) {
         self.serialized_representation.write(self.paging_system.entry_size() * virtual_page_number, entry.serialize()).unwrap();
         let entry_to_remove = core::mem::replace(&mut self.logical_representation[virtual_page_number], entry);

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

@@ -1,6 +1,7 @@
 // SPDX-FileCopyrightText: 2023 IBM Corporation
 // SPDX-FileContributor: Wojciech Ozga <woz@zurich.ibm.com>, IBM Research - Zurich
 // SPDX-License-Identifier: Apache-2.0
+#![rr::import("ace.theories.page_table", "page_table")]
 use super::specification::*;
 use crate::core::architecture::mmu::page_table::PageTable;
 use crate::core::architecture::SharedPage;
@@ -11,10 +12,18 @@ use alloc::boxed::Box;
 
 /// Logical page table entry contains variants specific to the security monitor architecture. These new variants distinguish among certain
 /// types (e.g., shared page, confidential data page) that are not covered by the general RISC-V specification.
+#[rr::refined_by("page_table_entry")]
 pub(super) enum LogicalPageTableEntry {
+    #[rr::pattern("PointerToNextPageTable" $ "next", "conf")]
+    #[rr::refinement("-[ #(#next); #conf]")]
     PointerToNextPageTable(Box<PageTable>),
+    #[rr::pattern("PageWithConfidentialVmData" $ "p", "conf", "perm")]
+    #[rr::refinement("-[ #(#p); #conf; #perm]")]
     PageWithConfidentialVmData(Box<Page<Allocated>>),
+    #[rr::pattern("PageSharedWithHypervisor" $ "sp", "conf", "perm")]
+    #[rr::refinement("-[ #sp; #conf; #perm]")]
     PageSharedWithHypervisor(SharedPage),
+    #[rr::pattern("UnmappedPage")]
     NotMapped,
 }
 

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

@@ -9,7 +9,9 @@ use crate::core::memory_layout::ConfidentialVmPhysicalAddress;
 // TODO: add more 2nd-level paging systems corresponding to 3 and 4 level page
 // tables.
 #[derive(Debug, Copy, Clone)]
+#[rr::refined_by("paging_system")]
 pub enum PagingSystem {
+    #[rr::pattern("Sv57x4")]
     Sv57x4,
 }
 
@@ -26,6 +28,10 @@ impl PagingSystem {
         }
     }
 
+    #[rr::skip]
+    #[rr::params("system")]
+    #[rr::args("#system")]
+    #[rr::returns("paging_system_highest_level system")]
     pub fn levels(&self) -> PageTableLevel {
         match self {
             PagingSystem::Sv57x4 => PageTableLevel::Level5,