Introduce verified PT code for x86.

.gitmodules

@@ -1,4 +1,7 @@
 [submodule "lib/node-replication"]
 	path = lib/node-replication
-	url = git@github.com:vmware/node-replication.git
+	url = https://github.com/vmware/node-replication.git
 	branch = mut_scan_vec
+[submodule "lib/verified-nrkernel"]
+	path = lib/verified-nrkernel
+	url = [email protected]:utaal/verified-nrkernel.git

Cargo.toml

@@ -10,6 +10,7 @@ members = [
     "lib/lineup",
     "lib/node-replication/cnr",
     "lib/node-replication/nr",
+    "lib/verified-nrkernel",
     "lib/rpc",
     "lib/vibrio",
     "lib/vmxnet3",
@@ -21,7 +22,7 @@ members = [
     #"lib/rust-topology",
     #"lib/rust-driverkit",
     #"lib/rust-x86",
-    #"lib/rawtime",    
+    #"lib/rawtime",
     #"lib/rust-klogger",
     #"lib/rexpect",
 ]

kernel/Cargo.toml

@@ -22,6 +22,7 @@ rpc = { path = "../lib/rpc", optional = true }
 vmxnet3 = { path = "../lib/vmxnet3" }
 bootloader_shared = { path = "../lib/bootloader_shared" }
 x86 = { version = "0.51", features = ["unstable"] }
+verified-pt = { path = "../lib/verified-nrkernel" }
 klogger = "0.0.14"
 driverkit = "0.20"
 spin = "0.9.1"
@@ -85,7 +86,9 @@ which = "4"
 cc = "1.0"
 
 [features]
-default = ["addr2line", "serde", "serde_cbor"]
+default = ["addr2line", "serde", "serde_cbor", "verified-code"]
+# Use formally verified code in some places
+verified-code = []
 # Enable Ethernet based networking.
 ethernet = ["smoltcp"]
 # Enable shared memory based communication.

kernel/src/arch/x86_64/acpi.rs

@@ -211,16 +211,24 @@ pub extern "C" fn AcpiOsMapMemory(location: ACPI_PHYSICAL_ADDRESS, len: ACPI_SIZ
     let p = PAddr::from(location);
     let adjusted_len = (p - p.align_down_to_base_page().as_usize()) + len;
 
-    use crate::round_up;
+    //use crate::round_up;
     let mut vspace = super::vspace::INITIAL_VSPACE.lock();
-    vspace
-        .map_identity_with_offset(
-            PAddr::from(super::memory::KERNEL_BASE),
-            p.align_down_to_base_page(),
-            round_up!(adjusted_len.as_usize(), x86::bits64::paging::BASE_PAGE_SIZE),
-            MapAction::ReadWriteKernel,
-        )
-        .expect("Can't map ACPI memory");
+    for idx in (0..adjusted_len.as_usize()).step_by(4096) {
+        vspace
+            .map_identity_with_offset(
+                PAddr::from(super::memory::KERNEL_BASE),
+                p.align_down_to_base_page() + idx,
+                x86::current::paging::BASE_PAGE_SIZE,
+                MapAction::ReadWriteKernel,
+            )
+            .expect("Can't map ACPI memory");
+    }
+    trace!(
+        "AcpiOsMapMemory(loc = {:#x}, len = {}) = {:#x}",
+        location,
+        len,
+        p
+    );
 
     let vaddr = paddr_to_kernel_vaddr(p);
     vaddr.as_mut_ptr::<c_void>()

kernel/src/arch/x86_64/mod.rs

@@ -254,9 +254,6 @@ fn _start(argc: isize, _argv: *const *const u8) -> isize {
     // Initialize kernel arguments as global
     crate::KERNEL_ARGS.call_once(move || kernel_args);
 
-    // Needs to be done before we switch address space
-    lazy_static::initialize(&vspace::INITIAL_VSPACE);
-
     klogger::init(
         crate::CMDLINE.get().map(|c| c.log_filter).unwrap_or("info"),
         debug::SERIAL_PRINT_PORT.load(Ordering::Relaxed),
@@ -294,7 +291,7 @@ fn _start(argc: isize, _argv: *const *const u8) -> isize {
     let mut dyn_mem = PerCoreMemory::new(emanager, 0);
     // Make `dyn_mem` a static reference:
     let static_dyn_mem =
-        // Safety: 
+        // Safety:
         // - The initial stack of the core will never get deallocated (hence
         //   'static is fine)
         // - TODO(safety): aliasing rules is broken here (we have mut dyn_mem
@@ -305,7 +302,7 @@ fn _start(argc: isize, _argv: *const *const u8) -> isize {
     let mut arch = kcb::Arch86Kcb::new(static_dyn_mem);
     // Make `arch` a static reference:
     let static_kcb =
-        // Safety: 
+        // Safety:
         // - The initial stack of the core will never get deallocated (hence
         //   'static is fine)
         // - TODO(safety): aliasing rules is broken here (we have mut dyn_mem
@@ -317,6 +314,9 @@ fn _start(argc: isize, _argv: *const *const u8) -> isize {
     // return from _start.
     core::mem::forget(arch);
 
+    // Needs to be done before we switch address space
+    lazy_static::initialize(&vspace::INITIAL_VSPACE);
+
     serial::init();
     irq::init_apic();
     // For testing only:
@@ -363,7 +363,7 @@ fn _start(argc: isize, _argv: *const *const u8) -> isize {
     // `global_memory` to every core) that's fine since it is allocated on our
     // BSP init stack (which isn't reclaimed):
     let global_memory_static =
-        // Safety: 
+        // Safety:
         // -'static: Lives on init stack (not deallocated)
         // - No mut alias to it
         unsafe { core::mem::transmute::<&GlobalMemory, &'static GlobalMemory>(&global_memory) };

kernel/src/arch/x86_64/process.rs

@@ -1188,17 +1188,12 @@ impl Process for Ring3Process {
             e.load(self)?;
         }
 
-        // Install the kernel mappings
-        // TODO(efficiency): These should probably be global mappings
-        // TODO(broken): Big (>= 2 MiB) allocations should be inserted here too
-        // TODO(ugly): Find a better way to express this mess
-        let kvspace = super::vspace::INITIAL_VSPACE.lock();
-        for i in 128..=135 {
-            let kernel_pml_entry = kvspace.pml4[i];
-            trace!("Patched in kernel mappings at {:?}", kernel_pml_entry);
-            self.vspace.page_table.pml4[i] = kernel_pml_entry;
+        let mut kvspace = super::vspace::INITIAL_VSPACE.lock();
+        self.vspace.page_table.patch_kernel_mappings(&*kvspace);
+        #[cfg(feature = "verified-code")]
+        {
+            kvspace.inner.memory.ptr = crate::memory::KERNEL_BASE as *mut u64;
         }
-
         Ok(())
     }
 

kernel/src/arch/x86_64/vspace/debug.rs

@@ -23,11 +23,11 @@ impl PageTable {
 
     fn parse_nodes_edges<'a>(
         &'a self,
+        pml4_table: Pin<&'a [PML4Entry; 512]>,
     ) -> Result<(dot::Nodes<'a, Nd<'a>>, dot::Edges<'a, Ed<'a>>), KError> {
         let mut nodes = Vec::try_with_capacity(PageTable::INITIAL_NODES_CAPACITY)?;
         let mut edges = Vec::try_with_capacity(PageTable::INITIAL_EDGES_CAPACITY)?;
 
-        let pml4_table = self.pml4.as_ref();
         nodes.try_push(Nd::PML4(pml4_table, None))?;
 
         unsafe {
@@ -371,13 +371,17 @@ impl<'a> dot::GraphWalk<'a> for PageTable {
     type Edge = Ed<'a>;
     fn nodes(&self) -> dot::Nodes<'a, Nd> {
         // Failure ok this is only used for debugging
-        let (nodes, _) = self.parse_nodes_edges().expect("Can't parse nodes");
+        let (nodes, _) = self
+            .parse_nodes_edges(self.pml4())
+            .expect("Can't parse nodes");
         nodes.into()
     }
 
     fn edges(&'a self) -> dot::Edges<'a, Ed> {
         // Failure ok this is only used for debugging
-        let (_, edges) = self.parse_nodes_edges().expect("Can't parse edges");
+        let (_, edges) = self
+            .parse_nodes_edges(self.pml4())
+            .expect("Can't parse edges");
         edges.into()
     }
 

kernel/src/arch/x86_64/vspace/mod.rs

@@ -1,7 +1,6 @@
 // Copyright © 2021 VMware, Inc. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use alloc::boxed::Box;
 use core::ops::Bound::*;
 
 use fallible_collections::btree::BTreeMap;
@@ -10,7 +9,18 @@ use spin::Mutex;
 use x86::current::paging::{PDFlags, PDPTFlags, PTFlags};
 
 mod debug;
+
+#[cfg(not(feature = "verified-code"))]
 pub mod page_table; /* TODO(encapsulation): This should be a private module but we break encapsulation in a few places */
+
+#[cfg(feature = "verified-code")]
+#[path = "verified_page_table.rs"]
+pub mod page_table;
+
+#[cfg(feature = "verified-code")]
+#[path = "page_table.rs"]
+pub mod unverified_page_table;
+
 #[cfg(test)]
 mod test;
 
@@ -42,7 +52,6 @@ lazy_static! {
         unsafe fn find_current_ptable() -> PageTable {
             use x86::controlregs;
             use x86::current::paging::PML4;
-            use crate::memory::paddr_to_kernel_vaddr;
 
             // The cr3 register holds a physical address
             let pml4: PAddr = PAddr::from(controlregs::cr3());
@@ -51,9 +60,9 @@ lazy_static! {
             // - We know we can access this at kernel vaddr and it's a correctly
             // aligned+initialized PML4 pointer because of the informal contract
             // we have with the bootloader
-            let pml4_table = core::mem::transmute::<VAddr, *mut PML4>(paddr_to_kernel_vaddr(pml4));
+            let pml4_table = core::mem::transmute::<PAddr, *mut PML4>(pml4);
 
-            // Safety `Box::from_raw`:
+            // Safety `from_pml4`:
             // - This is a bit tricky since it technically got allocated by the
             //   bootloader
             // - However it should never get dropped anyways since we don't
@@ -68,10 +77,7 @@ lazy_static! {
             //   (free bits) which won't exist because this memory was never
             //   allocated with slabmalloc (maybe we can have a no_drop variant
             //   of PageTable?)
-            PageTable {
-                pml4: Box::into_pin(Box::from_raw(pml4_table)),
-                da: None,
-            }
+            PageTable::from_pml4(pml4_table)
         }
 
         // Safety `find_current_ptable`:

kernel/src/arch/x86_64/vspace/page_table.rs

@@ -1,6 +1,8 @@
 // Copyright © 2021 VMware, Inc. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+#![allow(warnings, dead_code)]
+
 use alloc::boxed::Box;
 use core::alloc::Layout;
 use core::mem::transmute;
@@ -17,14 +19,14 @@ use crate::memory::vspace::*;
 use crate::memory::{kernel_vaddr_to_paddr, paddr_to_kernel_vaddr, Frame, PAddr, VAddr};
 
 /// Describes a potential modification operation on existing page tables.
-const PT_LAYOUT: Layout =
+pub(super) const PT_LAYOUT: Layout =
     unsafe { Layout::from_size_align_unchecked(BASE_PAGE_SIZE, BASE_PAGE_SIZE) };
 // Safety (size not overflowing when rounding up is given with size == align):
 static_assertions::const_assert!(BASE_PAGE_SIZE > 0); // align must not be zero
 static_assertions::const_assert!(BASE_PAGE_SIZE.is_power_of_two()); // align must be a power of two
 
 /// A modification operation on the PageTable.
-enum Modify {
+pub(super) enum Modify {
     /// Change rights of mapping to new MapAction.
     UpdateRights(MapAction),
     /// Remove frame from page-table.
@@ -184,11 +186,46 @@ impl PageTable {
         })
     }
 
+    /// Create a new address space given a raw pointer to a PML4 table.
+    ///
+    /// # Safety
+    /// - tldr: never use this function (use [`PageTable::new`] instead), except
+    ///   for where we construct a `PageTable` from the initial cr3 value that
+    ///   the bootloader gave us.
+    /// - Pretty unsafe needs to be unaliased and valid PML4 table (including
+    ///   everything the table points to).
+    /// - THe `pml4_table` is converted to a Box using [`Box::from_raw`] so
+    ///   either should make sure that the `Self` lives forever or the PML4 came
+    ///   from a [q`Box::into_raw`] call).
+    pub(super) unsafe fn from_pml4(pml4_table: *mut PML4) -> Self {
+        Self {
+            pml4: Box::into_pin(Box::from_raw(pml4_table)),
+            da: None,
+        }
+    }
+
     pub(crate) fn pml4_address(&self) -> PAddr {
         let pml4_vaddr = VAddr::from(&*self.pml4 as *const _ as u64);
         kernel_vaddr_to_paddr(pml4_vaddr)
     }
 
+    pub(crate) fn pml4(&self) -> Pin<&PML4> {
+        self.pml4.as_ref()
+    }
+
+    pub(crate) fn patch_kernel_mappings(&mut self, kvspace: &Self) {
+        // Install the kernel mappings
+        // TODO(efficiency): These should probably be global mappings
+        // TODO(broken): Big (>= 2 MiB) allocations should be inserted here too
+        // TODO(ugly): Find a better way to express this mess
+
+        for i in 128..=135 {
+            let kernel_pml_entry = kvspace.pml4[i];
+            trace!("Patched in kernel mappings at {:?}", kernel_pml_entry);
+            self.pml4[i] = kernel_pml_entry;
+        }
+    }
+
     /// Constructs an identity map but with an offset added to the region.
     ///
     /// This can be useful for example to map physical memory above `KERNEL_BASE`.

kernel/src/arch/x86_64/vspace/test.rs

@@ -61,7 +61,7 @@ fn map_rights() -> impl Strategy<Value = MapAction> {
 }
 
 fn page_sizes() -> impl Strategy<Value = usize> {
-    prop::sample::select(vec![BASE_PAGE_SIZE, LARGE_PAGE_SIZE])
+    prop::sample::select(vec![BASE_PAGE_SIZE]) //, LARGE_PAGE_SIZE])
 }
 
 prop_compose! {
@@ -95,7 +95,7 @@ proptest! {
         use TestAction::*;
         use crate::memory::detmem::DA;
 
-        let mut totest = VSpace::new(DA::new().expect("Unable to create DA")).expect("Unable to create vspace");;
+        let mut totest = VSpace::new(DA::new().expect("Unable to create DA")).expect("Unable to create vspace");
         let mut model: ModelAddressSpace = Default::default();
 
         for action in ops {