Reply Capabilities

Summary

Reply capabilities are tokens that a thread may possess that gives it the right to reply to another thread with an IPC.

Motivation

As security sensitive threads may be required to perform IPC calls to untrusted threads, reply capabilities have been introduced to protect security sensitive threads from interference by untrusted threads. Reply capabilities prevent untrusted threads from identifying security sensitive threads whilst enabling them to reply to IPC calls made by the security sensitive server threads. Reply capabilities also prevent untrusted threads from performing kernel operations on security sensitive threads though this is prevented by kernel security checks.

Properties

Reply capabilities may only be used for replying to a previously-received IPC. A reply capability is only valid for single use and expires after the reply IPC is sent.

Usage

The from field returned on the receive phase of IPC no longer contains the global thread id of the IPC caller. It will instead contain an "IPC reply capability". Reply capabilities are limited to certain operations.

It should be noted that the C type of a reply capability is still L4_ThreadId_t, which avoids refactoring of code where unnecessary.

Situations where a thread waits for incoming IPCs, processes the IPC and returns the results by replying to the IPC, are not affected by reply capabilities. Thus, the existing IPC code does not need to be modified.

It should be noted that reply capabilities are only recognized by the kernel if the following conditions are satisfied:

• The capability is used as an L4_ThreadId_t argument during an IPC operation.

• The capability is only used for the send phase of the IPC.
• The thread that the capability refers to is already blocked on the receive phase on an IPC operation.
• The thread that the capability refers to is specifically blocked on the thread using the handle. That is, the callee thread must already be waiting for an IPC from the caller, not an open wait for any thread.

In practice, these conditions will be guaranteed when thread A makes an L4_Call() to thread B. Thread B will receive a reply capability for A, which will remain valid until B replies to A, unless the A's IPC receive phase is aborted.

Reply capabilities may not be used for asynchronous IPC.

Examples

1. Reply capabilities can be used in a server-loop design.

   1 /*
   2  * 'server' should be set up before thread_client is executed,
   3  * see next section on thread identification
   4  */
   5 static L4_ThreadId_t server;
   6 
   7 void thread_client (void)
   8 {
   9     /* IPC to the server, and wait for the reply from the server */
  10     L4_Call(server);
  11     printf("Returned from the server call\n");
  12 }
  13 
  14 void thread_server (void)
  15 {
  16     /* client will always be a reply cap */
  17     L4_ThreadId_t client;
  18 
  19     L4_Wait(&client);
  20 
  21     while (true)
  22     {
  23         /* Do work for incoming IPC */
  24 
  25         /* Reply to the client */
  26         L4_ReplyWait(&client);
  27     }
  28 }

2. The following example will not work, because B may have replied the IPC back to A before A calls L4_Receive(). So technically, B is not replying to the original IPC sent from A. In addition, B may only perform an IPC send phase with a_cap, not an IPC receive phase. Therefore L4_Call() will always fail on the receive phase.

   1 /*
   2  * 'b' should be set up before they are executed,
   3  * see next section on thread identification
   4  */
   5 static L4_ThreadId_t b;
   6 
   7 void thread_a (void)
   8 {
   9     /* Do some work */
  10     
  11     /* Put some payload into IPC, send to b */
  12     L4_Send(b);
  13     
  14     /* Continue with other work */
  15     
  16     /* Wait for b to finish */
  17     L4_Receive(b);
  18 }
  19 
  20 void thread_b (void)
  21 {
  22     L4_ThreadId_t a_cap;
  23 
  24     /* Wait for incoming IPCs */
  25     L4_Wait(&a_cap);
  26 
  27     /* Do some work */
  28 
  29     /* Respond */
  30     L4_Call(a_cap); /* This will fail because L4_Call() includes a receive phase */
  31 }

3. The following example will not work. Reply caps may not be transferred.

   1 /*
   2  * The following are shared variables used to communicate
   3  * thread ids between threads.  However what ends up in the
   4  * variables will be reply caps, which are non-transferrable.
   5  */
   6 static L4_ThreadId_t a_cap;
   7 
   8 /*
   9  * The following are thread ids set up before threads are executed.
  10  */
  11 static L4_ThreadId_t server;
  12 
  13 void thread_a (void)
  14 {
  15     L4_ThreadId_t should_be_b;
  16 
  17     /* Give the server a reply cap to myself */
  18     L4_Call(server);
  19 
  20     /* Wait for an IPC, hopefully from thread 'b' */
  21     L4_Wait(&should_be_b);
  22 
  23     /* 'a' will never receive an IPC from 'b' */
  24 }
  25 
  26 void thread_b (void)
  27 {
  28     L4_MsgTag_t tag;
  29 
  30     /* Make sure a_cap is initialised before executing */
  31 
  32     /* Make an IPC to 'a' */
  33     tag = L4_Send(a_cap);
  34     
  35     /* The IPC will fail, because reply caps are non-transferrable */
  36     if (L4_IpcFailed(tag))
  37     {
  38         /* The following will return IPC_SND_ERROR, ERR_IPC_NOPARTNER */
  39         printf("IPC failed, error code %d\n", L4_ErrorCode());
  40     }
  41 }
  42 
  43 void thread_server (void)
  44 {
  45     L4_ThreadId_t should_be_a;
  46 
  47     L4_Wait(&should_be_a);
  48     a_cap = should_be_a;
  49     
  50     /* 'b' may now execute */
  51 }
  52 

Thread Identification

Reply capabilities may break existing user code that assumes the from field contains a global thread identifier. This is because in OKL4 2.1, recipients of IPC messages are not automatically handed the sender's global thread identifier.

One way of upgrading existing code to work with OKL4 2.1 is to ensure the IPC sender transfers it's own global thread identifier to a recipient via a message register. Options for doing so are presented in PortingConstantL4Myself.