clean up page table

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

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

@@ -78,22 +78,12 @@ 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: 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")]
+    /// Precondition: We require the permission to copy from arbitrary non-confidential memory.
+    /// Note that this implicitly specifies that we do not read from confidential memory.
+    /// TODO: might need atomicity?
     #[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}
@@ -264,11 +254,11 @@ 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")]
+    /// Precondition: The vpn is valid for the number of entries of this page table.
     #[rr::requires("vpn < pt_number_of_entries pt")]
+    /// Postcondition: The entry has been set correctly.
     #[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();

verification/theories/page_allocator/page.v

@@ -32,8 +32,8 @@ Proof.
     | 0 => Some Size4KiB
     | 1 => Some Size16KiB
     | 2 => Some Size2MiB
-    | 3 => Some Size1GiB 
-    | 4 => Some Size512GiB 
+    | 3 => Some Size1GiB
+    | 4 => Some Size512GiB
     | 5 => Some Size128TiB
     | _ => None
     end) _).
@@ -77,7 +77,7 @@ Definition page_size_larger (sz : page_size) : option page_size :=
   | Size128TiB => None
   end.
 
-(** Pages should be aligned to the size of the page; 
+(** Pages should be aligned to the size of the page;
   compute the log2 of this page's alignment *)
 Definition page_size_align_log (sz : page_size) : nat :=
   match sz with

verification/theories/page_allocator/page_allocator.v

@@ -3,29 +3,28 @@ From refinedrust Require Import ghost_var_dfrac.
 From ace.theories.page_allocator Require Import page.
 
 (** * Page allocator ghost state *)
+
 Record memory_region := {
   mreg_start : Z;
   mreg_size : nat;
 }.
 Definition mreg_end (mreg : memory_region) : Z :=
   mreg.(mreg_start) + mreg.(mreg_size).
 
-(*Definition memory_region_incl *)
-
 Class memory_regionG Σ := {
   mreg_ghost_var :: ghost_varG Σ memory_region;
 }.
 Section page_allocator.
   Context `{!typeGS Σ}.
   Context `{!memory_regionG Σ}.
-  
+
   Definition has_memory_region_def (γ : gname) (mreg : memory_region) :=
     ghost_var γ DfracDiscarded mreg.
   Definition has_memory_region_aux : seal (@has_memory_region_def). Proof. by eexists. Qed.
   Definition has_memory_region := has_memory_region_aux.(unseal).
   Definition has_memory_region_eq : @has_memory_region = @has_memory_region_def := has_memory_region_aux.(seal_eq).
 
-  Lemma has_memory_region_alloc mreg : 
+  Lemma has_memory_region_alloc mreg :
     ⊢ |==> ∃ γ, has_memory_region γ mreg.
   Proof.
     rewrite has_memory_region_eq.
@@ -49,38 +48,15 @@ Section page_allocator.
   Qed.
 End page_allocator.
 
-(* 
-New reasoning:
-   - we bound the memory region by a constant
-   - the page allocator fully covers that region
-   - so we get the initial precondition of the recursion
-
- *)
-
-
-(*
-(** [m1] is a correct abstraction of [m2] to only specify the number of pages at a given size. *)
-Definition page_allocator_maps_related (m1 : gmap page_size nat) (m2 : gmap page_size (place_rfn (list (place_rfn page)))) : Prop :=
-  ∀ (sz : page_size) num_pages, m1 !! sz = Some num_pages →
-    ∃ list_pages : list page,
-      (* There exists a list of pages at that size *)
-      m2 !! sz = Some (# (<#> list_pages)) ∧
-      (* The length matches up *)
-      length list_pages = num_pages ∧
-      (* The pages have the right size *)
-      Forall (λ pg : page, pg.(page_sz) = sz) list_pages.
-*)
-
 (** * Page allocator invariants *)
 Inductive node_allocation_state :=
-
+  (** This page node is completely allocated *)
   | PageTokenUnavailable
-
+  (** The page token in this node is available *)
   | PageTokenAvailable
-
+  (** The page node is partially available, with a page of the given size being allocable *)
   | PageTokenPartiallyAvailable (allocable_sz : page_size)
 .
-
 Global Instance node_allocation_state_eqdec : EqDecision node_allocation_state.
 Proof. solve_decision. Defined.
 
@@ -107,25 +83,26 @@ Definition child_base_address (parent_base_address : Z) (child_size : page_size)
 *)
 Definition page_storage_node_children_wf (parent_base_address : Z) (parent_node_size : page_size) (children : list page_storage_node) : Prop :=
   (* If there is a smaller child node size *)
-  (∀ child_node_size, 
+  (∀ child_node_size,
     page_size_smaller parent_node_size = Some child_node_size →
     (* Then all children are sorted *)
-    (∀ (i : nat) child, children !! i = Some child → 
+    (∀ (i : nat) child, children !! i = Some child →
       child.(max_node_size) = child_node_size ∧
       child.(base_address) = child_base_address parent_base_address parent_node_size i)) ∧
   (* If there can't be any children, there are no children *)
   (page_size_smaller parent_node_size = None →
     children = [])
 .
 
-Definition page_node_can_allocate (node : page_storage_node) : option page_size := 
+(** Computes the maximum size this page node can allocate *)
+Definition page_node_can_allocate (node : page_storage_node) : option page_size :=
   match node.(allocation_state) with
   | PageTokenUnavailable => None
   | PageTokenAvailable => Some node.(max_node_size)
   | PageTokenPartiallyAvailable allocable => Some allocable
   end.
 
-
+(** The logical invariant on a page node *)
 Definition page_storage_node_invariant
   (node : page_storage_node)
   (max_sz : option page_size) (maybe_page_token : option page) (children : list page_storage_node) :=
@@ -139,8 +116,8 @@ Definition page_storage_node_invariant
   (if node.(children_initialized) then length children = page_size_multiplier node.(max_node_size) else True) ∧
 
   (* invariant depending on the allocation state: *)
-  if decide (node.(allocation_state) = PageTokenUnavailable) 
-  then 
+  if decide (node.(allocation_state) = PageTokenUnavailable)
+  then
       (* No allocation is possible *)
       maybe_page_token = None ∧ max_sz = None ∧
 
@@ -149,7 +126,7 @@ Definition page_storage_node_invariant
       Forall (λ child, child.(allocation_state) = PageTokenUnavailable) children
   else if decide (node.(allocation_state) = PageTokenAvailable)
   then
-      (* This node is completely available *) 
+      (* This node is completely available *)
       ∃ token,
         (* there is some token *)
         maybe_page_token = Some token ∧
@@ -158,25 +135,25 @@ Definition page_storage_node_invariant
         (* the token spans the whole node *)
         token.(page_loc).2 = node.(base_address) ∧
         token.(page_sz) = node.(max_node_size) ∧
-        
+
         (* all children are unavailable *)
         (* TODO: do we need this? *)
         Forall (λ child, child.(allocation_state) = PageTokenUnavailable) children
-  else 
+  else
 
       (* This node is partially available with initialized children *)
       maybe_page_token = None ∧
       (* Some size is available *)
-      ∃ allocable_sz, 
+      ∃ allocable_sz,
       node.(allocation_state) = PageTokenPartiallyAvailable allocable_sz ∧
       max_sz = Some allocable_sz ∧
-      
+
       (* children need to be initialized *)
       node.(children_initialized) = true ∧
 
       (* The maximum size stored in this node needs to be available in one of the children *)
-      ∃ i child, 
-        children !! i = Some child ∧ 
+      ∃ i child,
+        children !! i = Some child ∧
         page_node_can_allocate child = Some allocable_sz
 .
 
@@ -189,6 +166,7 @@ Proof.
   apply Nat2Z.divide. done.
 Qed.
 
+(** States that the page is in the given memory range *)
 (* TODO unify all the memory range stuff *)
 Definition page_within_range (base_address : Z) (sz : page_size) (p : page) : Prop :=
   (base_address ≤ p.(page_loc).2 ∧ p.(page_loc).2 + page_size_in_bytes_Z p.(page_sz) < base_address + page_size_in_bytes_Z sz)%Z.