From 999f81ded16170d3b092a419bbedeed9a51ea0f5 Mon Sep 17 00:00:00 2001 From: June Rousseau Date: Wed, 7 Jan 2026 14:33:50 +0100 Subject: [PATCH] Frame contains bounds of the stack capability instead of arbitrary word --- theories/logrel/call_stack.v | 7 +++-- theories/logrel/logrel.v | 14 ++++------ theories/logrel/monotone.v | 5 +--- theories/switcher/interp_switcher_call.v | 6 ++-- theories/switcher/interp_switcher_return.v | 9 ------ theories/switcher/switcher_preamble.v | 32 ++++++++++------------ theories/switcher/switcher_spec_call.v | 12 ++++---- theories/switcher/switcher_spec_return.v | 14 +--------- 8 files changed, 39 insertions(+), 60 deletions(-) diff --git a/theories/logrel/call_stack.v b/theories/logrel/call_stack.v index c5f9720..64129f7 100644 --- a/theories/logrel/call_stack.v +++ b/theories/logrel/call_stack.v @@ -8,10 +8,11 @@ From cap_machine Require Import cap_lang. kept track by the switcher. - [wret] records the value of [cra], the return pointer of the caller - - [wstk] records the value of [csp], the (compartment) stack frame of the caller - [wcgp] records the value of [cgp], the global data (compartment's memory) of the caller - [wcs0] records the value of [cs0], general purpose register - [wcs1] records the value of [cs1], general purpose register + - [b_stk], [a_stk] and [e_stk] records the bounds of the stack capability [csp], + the (compartment) stack frame of the caller TODO: reformulate the following. In addition, it records whether the caller of the topmost frame @@ -23,10 +24,12 @@ From cap_machine Require Import cap_lang. **) Record cframe := MkCFrame { wret : Word; - wstk : Word; wcgp : Word; wcs0 : Word; wcs1 : Word; + b_stk : Addr; + a_stk : Addr; + e_stk : Addr; is_untrusted_caller : bool; }. diff --git a/theories/logrel/logrel.v b/theories/logrel/logrel.v index 1e91a4c..87bdd39 100644 --- a/theories/logrel/logrel.v +++ b/theories/logrel/logrel.v @@ -302,13 +302,16 @@ Section logrel. := (λne (cstk : CSTK) (W : WORLD) (C : CmptName) (frm : cframe) , - ∀ wca0 wca1 regs a_stk e_stk stk_mem_l stk_mem_h, + ∀ wca0 wca1 regs stk_mem_l stk_mem_h, + let b_stk := frm.(b_stk) in + let a_stk := frm.(a_stk) in + let e_stk := frm.(e_stk) in let astk4 := (a_stk ^+4)%a in let callee_stk_region := finz.seq_between (if frm.(is_untrusted_caller) then a_stk else astk4) e_stk in let callee_stk_mem := if frm.(is_untrusted_caller) then stk_mem_l++stk_mem_h else stk_mem_h in ( PC ↦ᵣ updatePcPerm frm.(wret) ∗ cra ↦ᵣ frm.(wret) - ∗ csp ↦ᵣ frm.(wstk) + ∗ csp ↦ᵣ (WCap RWL Local b_stk e_stk a_stk) (* cgp, cs0 and cs1 are callee-saved registers *) ∗ cgp ↦ᵣ frm.(wcgp) ∗ cs0 ↦ᵣ frm.(wcs0) @@ -320,8 +323,6 @@ Section logrel. ∗ ⌜dom regs = all_registers_s ∖ {[PC; cra ; cgp; csp; cs0; cs1 ; ca0; ca1]}⌝ ∗ ( [∗ map] r↦w ∈ regs, r ↦ᵣ w ∗ ⌜ w = WInt 0 ⌝ ) (* points-to predicate of the stack region *) - ∗ ⌜ get_a frm.(wstk) = Some a_stk ⌝ - ∗ ⌜ get_e frm.(wstk) = Some e_stk ⌝ ∗ [[ a_stk , astk4 ]] ↦ₐ [[ stk_mem_l ]] ∗ [[ astk4 , e_stk ]] ↦ₐ [[ stk_mem_h ]] (* World interpretation *) @@ -388,7 +389,7 @@ Section logrel. (* Continuation for the rest of the call-stack *) interp_cont_aux interp cstk' Ws' Cs' (* The callee stack frame must be safe, because we use the old copy of the stack to clear the stack *) - ∗ interp_callee_part_of_the_stack interp Wt Ct frm.(wstk) frm.(is_untrusted_caller) + ∗ interp_callee_part_of_the_stack interp Wt Ct (WCap RWL Local frm.(b_stk) frm.(e_stk) frm.(a_stk)) frm.(is_untrusted_caller) (* The continuation when matching the switcher's state at return-to-caller *) ∗ (∀ W', ⌜related_sts_pub_world Wt W'⌝ -∗ interp_cont_exec interp (interp_cont_aux interp cstk' Ws' Cs') cstk' W' Ct frm)))%I @@ -408,9 +409,6 @@ Section logrel. f_equiv. f_equiv;[apply IHy|]. f_equiv;[| repeat (f_equiv; auto)]. - rewrite /interp_callee_part_of_the_stack. - destruct wstk; auto. - destruct sb ; auto. apply Heq. Qed. diff --git a/theories/logrel/monotone.v b/theories/logrel/monotone.v index a67a5a8..4a20378 100644 --- a/theories/logrel/monotone.v +++ b/theories/logrel/monotone.v @@ -601,10 +601,7 @@ Proof. iNext. iSplitL "Hic";[|iSplitL "Hcallee"]. - iFrame. - - rewrite /interp_callee_part_of_the_stack /=. - case_match=>//. - case_match=>//. - iApply (interp_monotone with "[//] [$]"). + - iApply (interp_monotone with "[//] [$]"). - iIntros (W'' Hrel'). iApply "Hcont". iPureIntro. eapply related_sts_pub_trans_world;eauto. diff --git a/theories/switcher/interp_switcher_call.v b/theories/switcher/interp_switcher_call.v index 98b4497..8d350c1 100644 --- a/theories/switcher/interp_switcher_call.v +++ b/theories/switcher/interp_switcher_call.v @@ -964,10 +964,12 @@ Section fundamental. eset (frame := {| wret := WInt 0; - wstk := (WCap RWL Local b e a); wcgp := WInt 0; wcs0 := WInt 0; wcs1 := WInt 0; + b_stk := b ; + a_stk := a ; + e_stk := e ; is_untrusted_caller := true |}). @@ -993,7 +995,7 @@ Section fundamental. { iFrame. iNext. simpl. iSplit. - iApply (interp_weakening with "IH Hspv");auto;solve_addr. - - iIntros (W' HW' ???????) "(HPC & _)". + - iIntros (W' HW' ?????) "(HPC & _)". rewrite /interp_conf. wp_instr. iApply (wp_notCorrectPC with "[$]"). diff --git a/theories/switcher/interp_switcher_return.v b/theories/switcher/interp_switcher_return.v index 060b9a6..384316f 100644 --- a/theories/switcher/interp_switcher_return.v +++ b/theories/switcher/interp_switcher_return.v @@ -223,15 +223,6 @@ Section fundamental. rewrite /cframe_interp. iEval (cbn) in "Hcframe_interp". iDestruct "Hcframe_interp" as (wtstk4) "[Ha_tstk Hcframe_interp]". - destruct wstk; try done. - destruct sb; try done. - destruct p; try done. - destruct rx; try done. - destruct w; try done. - destruct dl; try done. - destruct dro; try done. - destruct g; try done. - rename a into a_stk; rename b into b_stk; rename e into e_stk. iDestruct "Hcframe_interp" as "(%HWF & -> & Hcframe_interp)". destruct HWF as (Hb_a4 & He_a1 & [a_stk4 Ha_stk4]). simpl in Hfreq. destruct Hfreq as (Hfrelated & <- & Hfreq). diff --git a/theories/switcher/switcher_preamble.v b/theories/switcher/switcher_preamble.v index 378cc59..453c8c4 100644 --- a/theories/switcher/switcher_preamble.v +++ b/theories/switcher/switcher_preamble.v @@ -101,11 +101,11 @@ Section Switcher_preamble. with the stack pointer of the callee. See [execute_entry_point] to understand how they are related. *) - Definition csp_sync (cstk : CSTK) (a_stk e_stk : Addr) := + Definition csp_sync (cstk : CSTK) (a_stk' e_stk' : Addr) := match cstk with | frm::_ => - get_a frm.(wstk) = Some a_stk - ∧ get_e frm.(wstk) = Some e_stk + frm.(a_stk) = a_stk' + ∧ frm.(e_stk) = e_stk' | _ => True end . @@ -244,22 +244,20 @@ Section Switcher_preamble. and the content should match the words of the call-frame. *) Definition cframe_interp (frm : cframe) (a_tstk : Addr) : iProp Σ := + let b_stk := frm.(b_stk) in + let a_stk := frm.(a_stk) in + let e_stk := frm.(e_stk) in ∃ (wtstk4 : Word), a_tstk ↦ₐ wtstk4 ∗ - match frm.(wstk) with - | WCap RWL Local b_stk e_stk a_stk => - (⌜ (b_stk <= a_stk)%a ∧ (a_stk ^+ 3 < e_stk)%a ∧ is_Some (a_stk + 4)%a ⌝ - ∗ ⌜ wtstk4 = WCap RWL Local b_stk e_stk (a_stk ^+ 4)%a ⌝ - ∗ if frm.(is_untrusted_caller) - then True - else - a_stk ↦ₐ frm.(wcs0) - ∗ (a_stk ^+ 1)%a ↦ₐ frm.(wcs1) - ∗ (a_stk ^+ 2)%a ↦ₐ frm.(wret) - ∗ (a_stk ^+ 3)%a ↦ₐ frm.(wcgp))%I - (* Constraints WFness of the register save area *) - | _ => False - end. + (⌜ (b_stk <= a_stk)%a ∧ (a_stk ^+ 3 < e_stk)%a ∧ is_Some (a_stk + 4)%a ⌝ + ∗ ⌜ wtstk4 = WCap RWL Local b_stk e_stk (a_stk ^+ 4)%a ⌝ + ∗ if frm.(is_untrusted_caller) + then True + else + a_stk ↦ₐ frm.(wcs0) + ∗ (a_stk ^+ 1)%a ↦ₐ frm.(wcs1) + ∗ (a_stk ^+ 2)%a ↦ₐ frm.(wret) + ∗ (a_stk ^+ 3)%a ↦ₐ frm.(wcgp))%I. (** [cstack_interp] interprets a call-stack. It simply interpret the topmost stack frame, diff --git a/theories/switcher/switcher_spec_call.v b/theories/switcher/switcher_spec_call.v index 22c17b2..b7ccf47 100644 --- a/theories/switcher/switcher_spec_call.v +++ b/theories/switcher/switcher_spec_call.v @@ -802,10 +802,12 @@ Section Switcher. set (frame := {| wret := wcra_caller; - wstk := (WCap RWL Local b_stk e_stk a_stk); wcgp := wcgp_caller; wcs0 := wcs0_caller; wcs1 := wcs1_caller; + b_stk := b_stk; + a_stk := a_stk; + e_stk := e_stk; is_untrusted_caller := false |}). @@ -881,7 +883,7 @@ Section Switcher. iSplit;[auto|]. iFrame "Htstk Hstk_interp". iSplit;[iPureIntro;solve_addr|]. iSplit;[iPureIntro;solve_addr|]. - iFrame. + iFrame; cbn. replace (a_stk ^+ 1)%a with a_stk1 by solve_addr+Hastk1. replace (a_stk ^+ 2)%a with a_stk2 by solve_addr+Hastk1 Hastk2. replace (a_stk ^+ 3)%a with a_stk3 by solve_addr+Hastk1 Hastk2 Hastk3. @@ -917,10 +919,10 @@ Section Switcher. iEval (cbn). replace (a_stk ^+ 4)%a with a_stk4 by solve_addr. iSplitR. { iNext. iFrame "Hstk4v". } - iIntros "!>" (W' HW' ???????) "(HPC & Hcra & Hcsp & Hgp & Hcs0 & Hcs1 & Ha0 & #Hv - & Hca1 & #Hv' & % & Hregs & % & % & Hstk & Hstk' & Hr & Hcls & Hsts & Hcont & Hcstk & Own)". + iIntros "!>" (W' HW' ?????) "(HPC & Hcra & Hcsp & Hgp & Hcs0 & Hcs1 & Ha0 & #Hv + & Hca1 & #Hv' & % & Hregs & Hstk & Hstk' & Hr & Hcls & Hsts & Hcont & Hcstk & Own)". iApply "Hpost";iLeft. simplify_eq. - replace (a_stk0 ^+ 4)%a with a_stk4 by solve_addr. + replace (a_stk ^+ 4)%a with a_stk4 by solve_addr. iFrame "∗#%". iSplit. { diff --git a/theories/switcher/switcher_spec_return.v b/theories/switcher/switcher_spec_return.v index 9fa6b59..74205e7 100644 --- a/theories/switcher/switcher_spec_return.v +++ b/theories/switcher/switcher_spec_return.v @@ -171,15 +171,6 @@ Section Switcher. rewrite /cframe_interp. iEval (cbn) in "Hcframe_interp". iDestruct "Hcframe_interp" as (wtstk4) "[Ha_tstk Hcframe_interp]". - destruct wstk; try done. - destruct sb; try done. - destruct p; try done. - destruct rx; try done. - destruct w; try done. - destruct dl; try done. - destruct dro; try done. - destruct g; try done. - rename a into a_stk; rename b into b_stk; rename e into e_stk. iDestruct "Hcframe_interp" as "(%HWF & -> & Hcframe_interp)". destruct HWF as (Hb_a4 & He_a1 & [a_stk4 Ha_stk4]). cbn in Hcsp_sync; destruct Hcsp_sync as [ Ha He ]; simplify_eq. @@ -802,10 +793,7 @@ Section Switcher. iApply ("Hexec_topmost_frm" with "[] [$HPC $Hcra $Hcsp $Hcgp $Hcs0 $Hcs1 $Hca0 $Hca1 $Hinterp_Wfixed_wca0 $Hinterp_Wfixed_wca1 $Hrmap $Hr $Hstk $Hstk' $Hsts $Hres $Hcont_K $Hcstk_frag $Hna]"); first done. - - iSplitR. - { iPureIntro;rewrite Harg_rmap'; set_solver. } - iSplit; done. + iPureIntro;rewrite Harg_rmap'; set_solver. - (* Case where caller is untrusted, we use the IH *)