MCS: Remove grant right from reply cap

This commit removes the grant right from reply caps on MCS. This is the
second alternative discussed in seL4 RFC-13:

https://sel4.atlassian.net/browse/RFC-13

Grant rights on reply object caps in MCS have limited use, because any
server with sufficient untyped memory can create new reply objects with
full grant rights.

A previous change restricted a server's ability to grant to its clients
by requiring that the server has grant rights on both the reply object
cap and the endpoint cap it used to receive a call. This change removes
grant rights from reply object caps, so that only the grant rights on
the receive endpoint matter.

This second change is motivated by the observation that there is no
clear use for a grant right on reply object caps once the first change
is implemented.

We did consider a hypothetical use case for this grant right. Suppose
there is a server T that is trusted to grant to its clients, but which
may delegate some calls to another server U that is *not* trusted to
grant to its clients. One way to perform the delegation would be for T
to pass the reply object capability to U, so that U can reply directly.
T would need grant rights on its receive endpoint, but would need to be
able to diminish grant rights on any reply object capability before
passing it to U.

However, we concluded that the protocol that would be needed to manage
reply objects between T and U would be more complex and less efficient
than simply proxying the reply via T.

Additionally, it's not even possible to construct such a system in a
non-MCS configuration, because the non-MCS kernel does not provide an
API to diminish the rights on a reply capability, other than using the
grant right on the receiver's endpoint capability.

Signed-off-by: Matthew Brecknell <matt@kry10.com>

CHANGES.md

@@ -27,6 +27,11 @@ description indicates whether it is SOURCE-COMPATIBLE, BINARY-COMPATIBLE, or BRE
 
 * Added `zynqmp` and `rpi4` to the set of verified AArch64 configs.
 
+## MCS
+
+* To grant capabilities when replying to a call in MCS configurations, it is now necessary to have grant rights on
+  the endpoint cap used to receive the call. The grant right on reply caps has been removed.
+
 ### Upgrade Notes
 
 ---

include/object/objecttype.h

@@ -36,7 +36,7 @@ exception_t performInvocation_Endpoint(endpoint_t *ep, word_t badge,
                                        bool_t block, bool_t call, bool_t canDonate);
 exception_t performInvocation_Notification(notification_t *ntfn,
                                            word_t badge);
-exception_t performInvocation_Reply(tcb_t *thread, reply_t *reply, bool_t canGrant);
+exception_t performInvocation_Reply(tcb_t *thread, reply_t *reply);
 #else
 exception_t decodeInvocation(word_t invLabel, word_t length,
                              cptr_t capIndex, cte_t *slot, cap_t cap,

include/object/structures.h

@@ -393,8 +393,13 @@ struct reply {
      * context was passed along the call chain */
     call_stack_t replyNext;
 
-    /* Unused, explicit padding to make struct size the correct power of 2. */
-    word_t padding;
+    /* If replyTCB is non-NULL, then canGrant indicates whether there was a grant right on the
+     * receiver's endpoint cap when the receiver called receiveIPC with a capability to this reply.
+     * This is the case whether replyTCB indicates the receiver waiting for a caller, or a caller
+     * waiting for a reply. The value of canGrant is undefined when replyTCB is NULL. In order to
+     * grant through a reply, the replier must have had a grant right on the endpoint cap used to
+     * receive the call. */
+    bool_t canGrant;
 };
 #endif
 

include/object/structures_32.bf

@@ -51,8 +51,7 @@ block notification_cap {
 block reply_cap {
     field capReplyPtr 32
 
-    padding 27
-    field capReplyCanGrant 1
+    padding 28
     field capType 4
 }
 

include/object/structures_64.bf

@@ -79,8 +79,7 @@ block reply_cap {
     field capReplyPtr 64
 
     field capType 5
-    field capReplyCanGrant 1
-    padding 58
+    padding 59
 }
 
 block call_stack(callStackPtr, isHead) {

manual/parts/ipc.tex

@@ -260,8 +260,11 @@ directly addressed with any CPtr as it is not part of any CSpace.
 A reply capability is invoked in the same way as a normal send on a
 \obj{Endpoint}. A reply capability has implicitly the Write right, so the
 message will always go through. Transferring caps in the reply can only happen
-if the reply capability has the Grant right and is done in exactly the same way
-as in a normal IPC transfer as described in \autoref{sec:cap-transfer}.
+if the receive endpoint capability had the Grant right at the time
+\apifunc{seL4\_Recv} was called, and (in non-MCS configurations) if the Grant
+right on the reply capability has not since been removed. The capability
+transfer is performed as in normal IPC transfer as described in
+\autoref{sec:cap-transfer}.
 
 The main difference with a normal endpoint transfer is that the kernel guarantees
 that invoking a reply capability cannot block: If you own a reply capability,

src/object/endpoint.c

@@ -175,6 +175,7 @@ void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
                 thread_state_ptr_set_replyObject(&thread->tcbState, REPLY_REF(replyPtr));
                 if (replyPtr) {
                     replyPtr->replyTCB = thread;
+                    replyPtr->canGrant = cap_endpoint_cap_get_capCanGrant(cap);
                 }
 #else
                 thread_state_ptr_set_blockingIPCCanGrant(
@@ -248,6 +249,7 @@ void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
                 if ((canGrant || canGrantReply) && replyPtr != NULL) {
                     bool_t canDonate = sender->tcbSchedContext != NULL
                                        && seL4_Fault_get_seL4_FaultType(sender->tcbFault) != seL4_Fault_Timeout;
+                    replyPtr->canGrant = cap_endpoint_cap_get_capCanGrant(cap);
                     reply_push(sender, thread, replyPtr, canDonate);
                 } else {
                     setThreadState(sender, ThreadState_Inactive);

src/object/objecttype.c

@@ -459,6 +459,7 @@ cap_t CONST maskCapRights(seL4_CapRights_t cap_rights, cap_t cap)
 #ifdef CONFIG_KERNEL_MCS
     case cap_sched_context_cap:
     case cap_sched_control_cap:
+    case cap_reply_cap:
 #endif
         return cap;
 
@@ -493,6 +494,8 @@ cap_t CONST maskCapRights(seL4_CapRights_t cap_rights, cap_t cap)
 
         return new_cap;
     }
+
+#ifndef CONFIG_KERNEL_MCS
     case cap_reply_cap: {
         cap_t new_cap;
 
@@ -501,7 +504,7 @@ cap_t CONST maskCapRights(seL4_CapRights_t cap_rights, cap_t cap)
                       seL4_CapRights_get_capAllowGrant(cap_rights));
         return new_cap;
     }
-
+#endif
 
     default:
         fail("Invalid cap type"); /* Sentinel for invalid enums */
@@ -587,7 +590,7 @@ cap_t createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceM
 
     case seL4_ReplyObject:
         /** AUXUPD: "(True, ptr_retyp (Ptr (ptr_val \<acute>regionBase) :: reply_C ptr))" */
-        return cap_reply_cap_new(REPLY_REF(regionBase), true);
+        return cap_reply_cap_new(REPLY_REF(regionBase));
 #endif
 
     default:
@@ -698,8 +701,7 @@ exception_t decodeInvocation(word_t invLabel, word_t length,
         setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
         return performInvocation_Reply(
                    NODE_STATE(ksCurThread),
-                   REPLY_PTR(cap_reply_cap_get_capReplyPtr(cap)),
-                   cap_reply_cap_get_capReplyCanGrant(cap));
+                   REPLY_PTR(cap_reply_cap_get_capReplyPtr(cap)));
 #else
     case cap_reply_cap:
         if (unlikely(cap_reply_cap_get_capReplyMaster(cap))) {
@@ -812,9 +814,9 @@ exception_t performInvocation_Notification(notification_t *ntfn, word_t badge)
 }
 
 #ifdef CONFIG_KERNEL_MCS
-exception_t performInvocation_Reply(tcb_t *thread, reply_t *reply, bool_t canGrant)
+exception_t performInvocation_Reply(tcb_t *thread, reply_t *reply)
 {
-    doReplyTransfer(thread, reply, canGrant);
+    doReplyTransfer(thread, reply, reply->canGrant);
     return EXCEPTION_NONE;
 }
 #else

src/object/reply.c

@@ -27,6 +27,10 @@ void reply_push(tcb_t *tcb_caller, tcb_t *tcb_callee, reply_t *reply, bool_t can
 
     /* link caller and reply */
     reply->replyTCB = tcb_caller;
+
+    /* canGrant should have already been set according to the grant
+       right on the receiver's endpoint capability. */
+
     thread_state_ptr_set_replyObject(&tcb_caller->tcbState, REPLY_REF(reply));
     setThreadState(tcb_caller, ThreadState_BlockedOnReply);