MCS: Remove grant right from reply cap #808

corlewis · 2024-08-02T03:34:28Z

This commit is the corresponding specification and proof updates for seL4/seL4#945, the second alternative described in https://github.com/seL4/rfcs/blob/main/src/active/0130-mcs-grant-reply.md.

The updates to the specifications, abstract invariants and refine proofs are complete. As crefine for MCS is still in progress, I have only updated it as needed to maintain its current state. In particular, this means that I have not proven refinement to the C code for the changes made to receiveIPC, since that would require first updating that proof for all of the other unrelated MCS content. receiveIPC is a relatively complicated function, so this could be a significant amount of work and should probably be done separately.

Test with: seL4/seL4#945

proof/refine/RISCV64/KHeap_R.thy

Xaphiosis · 2024-08-08T01:18:12Z

proof/refine/RISCV64/KHeap_R.thy

+    apply (clarsimp simp: obj_at'_def)
+   apply wpsimp
+  apply wpsimp
+  apply (clarsimp simp: obj_at'_def)


this pattern is a bit long-winded, any way to shorten it? I guess passing obj_at'_def to wpsimp is probably going to not go where we want, but as this is terminal, maybe a (wpsimp | ...)+?

I ended up going with apply (wpsimp | normalise_obj_at' | erule obj_at'_weakenE)+, as an attempt to make it less likely to go down unintended paths if anything changes.

proof/refine/RISCV64/Ipc_R.thy

proof/invariant-abstract/KHeap_AI.thy

Xaphiosis

Well done getting this done so quickly, it's been pending for a long while, good to have it cleared. Apologies review took so long.
Apart from small nitpicks (rt proofs seem to have more verbosity in places, maybe it's the general vibe on that branch), I have one extra concern: I'm seeing changes to the manual in the corresponding seL4 PR, and some of those descriptions look to originally have been copied from our Haskell spec comments. However, this PR does not change any Haskell or abstract comments, which seems suspicious. Either we never added/changed them for MCS (also not great), or it feels like something should get updated. Thoughts?

corlewis · 2024-08-08T05:10:00Z

I'm seeing changes to the manual in the corresponding seL4 PR, and some of those descriptions look to originally have been copied from our Haskell spec comments. However, this PR does not change any Haskell or abstract comments, which seems suspicious. Either we never added/changed them for MCS (also not great), or it feels like something should get updated. Thoughts?

Hmm, I haven't done an exhaustive search but I can't see any equivalent comments in the specifications.

proof/refine/RISCV64/Invariants_H.thy

lsf37

Excellent, and as Raf said this went much quicker than I thought it would. Good work.

I don't think this interferes with anything @michaelmcinerney has in flight, so we should be able to merge after squashing.

In MCS configurations, a server's ability to grant capabilities when replying to a call were previously determined entirely by the grant right on the reply capability the server supplied when calling `receiveIPC`. If the server had sufficient untyped memory, it could create arbitrary reply capabilities, giving itself the ability to grant to its clients. Consequently, the only way to restrict a server's ability to grant to its clients was to avoid giving it untyped memory. This would break the expected authority confinement property. Contrast this with non-MCS configurations, where the grant rights on a server's receive endpoint control the server's ability to grant capabilities when replying to calls. This makes it much easier to restrict a server's ability to grant when replying. This commit makes MCS configurations behave more like non-MCS configurations: In order to grant capabilities when replying to a call, a server must have a grant right on the receive endpoint capability when it calls `receiveIPC`. This commit also removes the grant right from reply caps, as following the previous change this right has no clear use case. Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

michaelmcinerney

I still don't know enough about caps to really comment on the design choices, but the proofs look good. Just some idle musings and nitpicks from me.

michaelmcinerney · 2025-06-20T05:01:48Z

spec/abstract/Structures_A.thy

-  reply_sc     :: "obj_ref option"
+  reply_tcb       :: "obj_ref option"
+  reply_sc        :: "obj_ref option"
+  reply_can_grant :: "bool"


Nitpick: the quotation marks can be removed from the bool

michaelmcinerney · 2025-06-20T05:03:37Z

spec/abstract/KHeap_A.thy

+where
+  "update_reply ptr f  \<equiv> do
+     obj \<leftarrow> get_object ptr;
+     case obj of Reply reply \<Rightarrow> set_object ptr (Reply (f reply)) | _ \<Rightarrow> fail


I haven't looked into the details in a while, but did we want to use set_object, or do we prefer set_simple_ko? I was thinking of making a similar "update" function for the endpoints and notifications, so maybe we should decide on the right pattern for this.

michaelmcinerney · 2025-06-20T05:04:55Z

proof/crefine/RISCV64/SR_lemmas_C.thy

  apply fastforce
  done

+lemma obj_at_cslift_reply:


I think Nick ended up adding this when he did the rules for replyUnlink_ccorres and cancelIPC_ccorres. So this is duplicated now, though I'm not sure where his rule ended up.

michaelmcinerney · 2025-06-20T05:07:08Z

proof/invariant-abstract/AInvs.thy

  "check_budget_restart \<lbrace>\<lambda>s. schact_is_rct s \<longrightarrow> ct_in_state activatable s\<rbrace>"
  by (wpsimp simp: check_budget_restart_def)

+lemma update_reply_schact_is_rct_imp_ct_activatable[wp]:


update_reply won't touch the scheduler action or the TCB heap, so with the right rules, this should be crunchable, and we won't need to unfold low-level things like set_object and get_object.

michaelmcinerney · 2025-06-20T05:07:52Z

proof/invariant-abstract/ARM/ArchCSpace_AI.thy

  "is_zombie cap = (\<exists>r b n. cap = cap.Zombie r b n)"
  "is_arch_cap cap = (\<exists>a. cap = cap.ArchObjectCap a)"
-  "is_reply_cap cap = (\<exists>x R. cap = cap.ReplyCap x R)"
+  "is_reply_cap cap = (\<exists>x. cap = cap.ReplyCap x)"


While we're here, would a more informative name for the green variable x be nicer?

michaelmcinerney · 2025-06-20T05:15:36Z

proof/invariant-abstract/KHeap_AI.thy

+  "update_reply ptr f \<lbrace>cur_tcb\<rbrace>"
+  by (wpsimp simp: update_reply_def set_object_def get_object_def cur_tcb_def tcb_at_def get_tcb_def)
+
+lemma update_reply_cur_sc_tcb[wp]:


I wonder if we have crunches and things for update_sched_context for some of these easy invariants, in which case maybe we can just add update_reply to the list of functions which we crunch. Again thinking about this in case I/we add an update_endpoint or update_ntfn

michaelmcinerney · 2025-06-20T05:16:16Z

proof/refine/RISCV64/ADT_H.thy

-     apply (case_tac x; clarsimp)
+      apply (case_tac "x", simp_all)
+     apply (rule set_eqI, clarsimp)
+     apply (case_tac "x", simp_all add: word_bits_def)


Nitpick: unnecessary quotation marks

michaelmcinerney · 2025-06-20T05:19:57Z

proof/refine/RISCV64/Ipc_R.thy

  apply (fastforce simp: pred_map_def map_project_def opt_map_def tcbs_of_kh_def)
  done

+lemma update_reply_in_correct_ready_q[wp]:


Maybe there was a lifting rule for in_correct_ready_q that can be used here, but I'm not sure

michaelmcinerney · 2025-06-20T05:21:04Z

proof/refine/RISCV64/Ipc_R.thy

+                                    apply (rule corres_split[OF replyCanGrant_update_corres replyPush_corres])
+                                       apply simp
+                                      apply (clarsimp simp: fault_rel_optionation_def split: option.splits)
+                                     prefer 5 \<comment> \<open> defer wp until corres complete \<close>


Could this prefer be done instead with a match of some kind? match premisses or whatever it is?

michaelmcinerney · 2025-06-20T05:23:10Z

proof/refine/RISCV64/Reply_R.thy

+  apply (wpsimp wp: updateReply_valid_objs' updateReply_iflive' updateReply_valid_replies' updateReply_list_refs_of_replies')
+  apply (clarsimp simp: valid_replies'_def2 valid_reply'_def live_reply'_def
+                  dest: pspace_alignedD' pspace_distinctD')
+  apply (erule delta_sym_refs)


I wonder if you could rewrite the sym_refs for list_refs_of_reply' into the sym_heap version we have, and then get this for free.

corlewis added MCS related to `rt` branch and mixed-criticality systems seL4-PR requires merging a corresponding seL4 pull request labels Aug 2, 2024

corlewis requested review from Xaphiosis, lsf37, mbrcknl and michaelmcinerney August 2, 2024 03:34

corlewis force-pushed the corlewis/mcs-grant-via-reply branch from 675db24 to ab4e713 Compare August 2, 2024 05:50

Xaphiosis reviewed Aug 8, 2024

View reviewed changes

proof/refine/RISCV64/KHeap_R.thy Outdated Show resolved Hide resolved

Xaphiosis reviewed Aug 8, 2024

View reviewed changes

proof/refine/RISCV64/Ipc_R.thy Outdated Show resolved Hide resolved

Xaphiosis reviewed Aug 8, 2024

View reviewed changes

proof/refine/RISCV64/Ipc_R.thy Outdated Show resolved Hide resolved

Xaphiosis reviewed Aug 8, 2024

View reviewed changes

proof/invariant-abstract/KHeap_AI.thy Outdated Show resolved Hide resolved

Xaphiosis approved these changes Aug 8, 2024

View reviewed changes

corlewis force-pushed the corlewis/mcs-grant-via-reply branch from ab4e713 to eda3dfe Compare August 9, 2024 04:26

lsf37 reviewed Aug 9, 2024

View reviewed changes

proof/refine/RISCV64/Invariants_H.thy Outdated Show resolved Hide resolved

lsf37 approved these changes Aug 9, 2024

View reviewed changes

corlewis force-pushed the corlewis/mcs-grant-via-reply branch from eda3dfe to 870da47 Compare August 12, 2024 08:36

michaelmcinerney approved these changes Jun 20, 2025

View reviewed changes

MCS: Remove grant right from reply cap #808

Are you sure you want to change the base?

MCS: Remove grant right from reply cap #808

Uh oh!

Conversation

corlewis commented Aug 2, 2024

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Xaphiosis left a comment

Choose a reason for hiding this comment

Uh oh!

corlewis commented Aug 8, 2024

Uh oh!

Uh oh!

lsf37 left a comment

Choose a reason for hiding this comment

Uh oh!

michaelmcinerney left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants