From 8ce19f47de0b324b15bf514e37f2c2ab2a0234d6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lennard=20G=C3=A4her?= Date: Wed, 17 Jul 2024 18:48:11 +0200 Subject: [PATCH] clean up page table MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Lennard Gäher --- .../core/architecture/riscv/mmu/page_table.rs | 20 +- verification/theories/page_allocator/page.v | 6 +- .../theories/page_allocator/page_allocator.v | 64 ++---- verification/theories/page_table/page_table.v | 190 +++++++++--------- 4 files changed, 122 insertions(+), 158 deletions(-) diff --git a/security-monitor/src/core/architecture/riscv/mmu/page_table.rs b/security-monitor/src/core/architecture/riscv/mmu/page_table.rs index c39f223..7dc35dd 100644 --- a/security-monitor/src/core/architecture/riscv/mmu/page_table.rs +++ b/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(); diff --git a/verification/theories/page_allocator/page.v b/verification/theories/page_allocator/page.v index c30f1d2..cdb2fae 100644 --- a/verification/theories/page_allocator/page.v +++ b/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 diff --git a/verification/theories/page_allocator/page_allocator.v b/verification/theories/page_allocator/page_allocator.v index 12a0362..2d3e804 100644 --- a/verification/theories/page_allocator/page_allocator.v +++ b/verification/theories/page_allocator/page_allocator.v @@ -3,6 +3,7 @@ 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; @@ -10,22 +11,20 @@ Record memory_region := { 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,10 +83,10 @@ 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 *) @@ -118,14 +94,15 @@ Definition page_storage_node_children_wf (parent_base_address : Z) (parent_node_ 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. diff --git a/verification/theories/page_table/page_table.v b/verification/theories/page_table/page_table.v index 8adbd7c..ff78a03 100644 --- a/verification/theories/page_table/page_table.v +++ b/verification/theories/page_table/page_table.v @@ -86,7 +86,7 @@ Definition pte_is_ptr (flags : pte_flags) : bool := (* Check if PTE is valid *) Definition pte_is_invalid (flags : pte_flags) : bool := - (negb flags.(PTEValid)) + (negb flags.(PTEValid)) (* TODO: security monitor does not have to check for it *) || (flags.(PTEWrite) && negb flags.(PTERead)) . @@ -125,7 +125,7 @@ Definition encode_physical_address_to_ppn (addr : Z) : bv pte_ppn_length := (** A valid physical address should fit into 64 bits. The highest 8 bits should replicate the 56th bit. *) Definition is_valid_physical_address (addr : Z) := - ∃ bv_addr, + ∃ bv_addr, Z_to_bv_checked 64 addr = Some bv_addr ∧ Forall (λ x, bv_to_bit (N.to_nat physical_address_length) bv_addr = x) (drop (N.to_nat physical_address_length) (bv_to_bits bv_addr)). @@ -139,61 +139,11 @@ Definition encode_pte $ pte_encode_flags flags (* flags *) . -(* - ∀ guest_physical_address, - memory_isolation_translate (some_hw_config) serialized_page_table guest_phyiscal_address = Some real_address → - real_address belongs to this VM - - - (* TODO: does it suffice to prove a weaker property? *) - - is_byte_level_logical_representation logical physical → - - we also need to require that the hardware actually does an exception if the translation fails. - - - - What is the right way to formalize this? - Probably we need a logical version and a physical version. - - The physical version is used by the semantics, and it requires access to the whole state in order to follow pointers - The logical version should be used in our spec, and correspond to the physical version, in that it translates to the same things. - - - *) - - - -(* Notes: - all of RWX are zero => pointer to next level - otherwise a leaf - - W implies R - - SUM bit determines whether supervisor can access user mode pages - - G exists in all address spaces. - - leaves contain A D U; for non-leafs, they have to be cleared - - - How does the shape of the page table relate between the one for guest translation and supervisor translation? - Sv57x4 is for guest physical to supervisor physical - So does the hypervisor also go through this scheme, or is that using Sv57? - => It's using Sv57. But the hypervisor page table is not managed by the security monitor. - It's setup by the hypervisor boot process. - The security monitor only cares about correctly backing up and restoring the satp config. - - - Steps for formalization: - - convert bit sequence to integer - - stuff to concatenate bit sequences - - *) - +(** Translate an address according to the page table located at [pt_addr] in [σ]. *) Definition translate_address (pt_addr : Z) (σ : state) (addr : Z) : option Z := + (* TODO *) None -. +. (** * Logical representation *) @@ -230,24 +180,6 @@ Definition to_pte_flags (valid : bool) (ptc : page_table_config) (ptp : page_tab PTEDirty := ptc.(pt_is_dirty); |}. -(** - How do we decode things? - Should we take an integer or another type? - Idea: define a bitvector type that at least requires that it's in the given bitwidth. - But I guess this is already given by the integer type itself. - I could represent it as a list of bits, instead. - But encoding/decoding should anyways be reversible. So it wouldn't change much. - decode (encode bits) = Some bits - decode i = Some bits → encode bits = i - - I guess the main advantage is that it's easier to do stuff with masking etc. - - Especially with or-ing stuff. - that will be difficult to do otherwise. - -*) -(*Definition *) - (** The valid PTE flag bits. *) Inductive pte_flags_bits := | PTValid @@ -262,12 +194,19 @@ Inductive pte_flags_bits := (*Definition pte_flags_bits_mask *) +(** Physical page table entries *) +Inductive page_table_entry := + | UnmappedPTE + | NextPTE (l : loc) + | DataPTE (l : loc) +. Record shared_page : Type := { shared_page_hv_address : Z; shared_page_sz : page_size; }. +(** Level of page tables *) Inductive page_table_level := | PTLevel5 | PTLevel4 @@ -289,6 +228,7 @@ Definition page_table_level_lower (pt : page_table_level) : option page_table_le | PTLevel1 => None end. +(** The highest level for this paging system *) Definition paging_system_highest_level (system : paging_system) : page_table_level := match system with | Sv57x4 => PTLevel5 @@ -297,7 +237,7 @@ Definition paging_system_highest_level (system : paging_system) : page_table_lev Definition number_of_page_table_entries (system : paging_system) (level : page_table_level) : nat := if decide (level = paging_system_highest_level system) then 2048%nat else 512%nat. -(* Can we avoid mutual inductives? *) +(** Logical page table entries defined mutually inductively with page table trees *) Inductive logical_page_table_entry : Type := | PointerToNextPageTable (next : page_table_tree) @@ -310,7 +250,7 @@ Inductive logical_page_table_entry : Type := | PageSharedWithHypervisor (sp : shared_page) - (conf : page_table_config) + (conf : page_table_config) (perm : page_table_permission) | NotValid @@ -348,15 +288,22 @@ Definition pt_number_of_entries (pt : page_table_tree) : nat := | PageTableTree system _ _ level => number_of_page_table_entries system level end. -(*Fixpoint page_table_levels_decreasing (p : page_table_tree) :=*) - (*match p with*) - (*| PageTableTree entries level =>*) - (*Forall logical_page_table_entry_levels_decreasing entries ∧*) - (*max_list (fmap *) -(*with logical_page_table_entry_levels_decreasing (pt : logical_page_table_entry) :=*) - (*match pt with*) - (*| PointerToNextPageTable next conf =>*) +(** Asserts that that the level of a logical page table/page table entry is given by [l], and it is properly decreasing for children. *) +Fixpoint page_table_level_is (l : option page_table_level) (p : page_table_tree) {struct p} := + match p with + | PageTableTree sys addr entries level => + Some level = l ∧ + Forall_cb (logical_page_table_entry_level_is (page_table_level_lower level)) entries + end +with logical_page_table_entry_level_is (l : option page_table_level) (pt : logical_page_table_entry) {struct pt} := + match pt with + | PointerToNextPageTable next conf => + page_table_level_is l next + | _ => + True + end. +(** Predicate specifying that this entry/tree has a particular paging system *) Fixpoint page_table_tree_has_system (system : paging_system) (pt : page_table_tree) := match pt with | PageTableTree system' _ entries _ => @@ -367,27 +314,43 @@ with logical_page_table_entry_has_system (system : paging_system) (pte : logical match pte with | PointerToNextPageTable pt _ => page_table_tree_has_system system pt - | _ => + | _ => True end. +(** Well-formedness of page table trees *) (* TODO: maybe make this intrinsic using dependent type *) Definition page_table_wf (pt : page_table_tree) := (* number of page table entries is determined by the level *) number_of_page_table_entries (pt_get_system pt) (pt_get_level pt) = length (pt_get_entries pt) ∧ (* ensure that levels are decreasing *) - (* TODO *) + page_table_level_is (Some $ pt_get_level pt) pt ∧ (* ensure that the system is the same across the whole page table *) page_table_tree_has_system (pt_get_system pt) pt . (* TODO: ensure everything is in confidential memory *) +Definition page_table_is_first_level (pt : page_table_tree) := + pt_get_level pt = paging_system_highest_level (pt_get_system pt). + -Definition make_empty_page_tree (system : paging_system) (level : page_table_level) (loc : Z) := - PageTableTree system loc [] level. +(** Empty page table tree *) +Definition make_empty_page_tree (system : paging_system) (level : page_table_level) (loc : Z) := + PageTableTree system loc (replicate (number_of_page_table_entries system level) NotValid) level. -(** Encoding *) +Lemma make_empty_page_tree_wf system level loc : + page_table_wf (make_empty_page_tree system level loc). +Proof. + split_and!; simpl. + - rewrite replicate_length//. + - split; first done. apply Forall_Forall_cb. + apply Forall_replicate. done. + - split; first done. apply Forall_Forall_cb. + apply Forall_replicate. done. +Qed. + +(** * Encoding of logical page table trees into the physical byte-level representation *) Definition encode_logical_page_table_entry_bv (pte : logical_page_table_entry) : bv 64 := match pte with | PointerToNextPageTable pt ptc => @@ -416,20 +379,54 @@ Definition is_byte_level_representation (pt_logical : page_table_tree) (pt_byte (* We have a 16KiB page for Level 5, and 4KiB pages otherwise *) (if pt_get_level pt_logical is PTLevel5 then pt_byte.(page_sz) = Size16KiB else pt_byte.(page_sz) = Size4KiB) ∧ (* The encoding of the entries matches the physical content of the pages *) - (* NOTE: if the list of entries is [], this should be trivial. *) pt_byte.(page_val) = encode_page_table_entries (pt_get_entries pt_logical) . - (** Operations modifying the page table *) Definition pt_set_entry (pt : page_table_tree) (index : nat) (entry : logical_page_table_entry) : page_table_tree := match pt with | PageTableTree system serialized_addr entries level => PageTableTree system serialized_addr (<[index := entry]> entries) level end. - -(*Lemma pt_set_entry_wf : *) - (*pt_set*) +Lemma pt_set_entry_system pt i en : + pt_get_system (pt_set_entry pt i en) = pt_get_system pt. +Proof. destruct pt; done. Qed. +Lemma pt_set_entry_addr pt i en : + pt_get_serialized_addr (pt_set_entry pt i en) = pt_get_serialized_addr pt. +Proof. destruct pt; done. Qed. +Lemma pt_set_entry_level pt i en : + pt_get_level (pt_set_entry pt i en) = pt_get_level pt. +Proof. destruct pt; done. Qed. +Lemma pt_set_entry_entries pt i en : + pt_get_entries (pt_set_entry pt i en) = <[i := en]> (pt_get_entries pt). +Proof. destruct pt; done. Qed. + +(** Preservation of well-formedness when setting an entry *) +Lemma pt_set_entry_wf pt pt' i en : + pt_set_entry pt i en = pt' → + logical_page_table_entry_level_is (page_table_level_lower $ pt_get_level pt) en → + logical_page_table_entry_has_system (pt_get_system pt) en → + page_table_wf pt → + page_table_wf pt'. +Proof. + intros <- Hlevel Hsystem. + intros (Hlen & Hlv & Hsys). + split_and!. + - rewrite pt_set_entry_system pt_set_entry_level. + rewrite pt_set_entry_entries insert_length//. + - rewrite pt_set_entry_level. + destruct pt; simpl in *. split; first done. + apply Forall_Forall_cb. apply Forall_insert. + { destruct Hlv as [_ Ha]. apply Forall_Forall_cb. done. } + { done. } + - rewrite pt_set_entry_system. + destruct pt; simpl in *. + split; first done. + apply Forall_Forall_cb. + apply Forall_insert. + { destruct Hsys as [_ Hsys]. apply Forall_Forall_cb; done. } + { done. } +Qed. (** ** Using a page table *) (** Translate an address according to the logical page table representation *) @@ -442,15 +439,14 @@ Definition pt_represented_at (σ : state) (pt : page_table_tree) (pt_addr : Z) : False. (** Address translation should be consistent between the logical and physical version *) -Lemma page_table_translate_address_consistent_1 (pt : page_table_tree) addr pt_addr σ translated_addr : +Lemma page_table_translate_address_consistent_1 (pt : page_table_tree) addr pt_addr σ translated_addr : pt_represented_at σ pt pt_addr → page_table_translate_address pt addr = Some translated_addr → - translate_address pt_addr σ addr = Some translated_addr -. + translate_address pt_addr σ addr = Some translated_addr. Proof. Abort. -Lemma page_table_translate_address_consistent_2 pt addr pt_addr σ translated_addr : +Lemma page_table_translate_address_consistent_2 pt addr pt_addr σ translated_addr : pt_represented_at σ pt pt_addr → translate_address pt_addr σ addr = Some translated_addr → page_table_translate_address pt addr = Some translated_addr