portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

SELFOUR-6: Add GrantReply to the rights system.

Browse source 
GrantReply is a new access right added to endpoint capabilities, which
allows seL4_Call to be used on those capabilities (specifically, it
allows reply caps *only* to be granted across endpoints).

Prior to the addition of GrantReply, endpoint capabilities required the
Grant access right, which allowed any arbitrary capabilitiy to be
transferred over an endpoint. Using GrantReply, systems can now be
constructed where threads using seL4_Call over an endpoint do not need to be in the same
security subsystem.
This commit is contained in:
Thibaut Perami 2018-04-23 15:21:08 +10:00 committed by Anna Lyons
parent fbec286d97
commit 3df00ea4d7
24 changed files with 258 additions and 138 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
CHANGES
View file

@ -8,10 +8,18 @@ The upcoming release notes should indicate whether it is a SOURCE COMPATIBLE, BI
changes are added the compatibility information should be updated.
---
Upcoming release: BINARY COMPATIBLE
Upcoming release: BREAKING
## Changes
* GrantReply right was added to the right system (`seL4_CapRights`)
- `seL4_CapRights_new` now takes 4 parameters
- The endpoint capabilities now have 4 rights with the GrantReply reply right. Calling can be done with either
Grant or GrantReply, However with only GrantReply and not Grant, capabilities other than the Reply
capability will not be transferred.
- Reply capabilities now have a Grant right. This right is set depending according to the Grant right of the
endpoint capability on which `seL4_Recv` is performed when a call is received. In the case where the caller
has Grant to the receiver but the latter doesn't have it towards the former, this is an ABI breaking change.
## Upgrade Notes
---

2
include/api/types.h
View file

@ -54,7 +54,7 @@ rightsFromWord(word_t w)
static inline word_t CONST
wordFromRights(seL4_CapRights_t seL4_CapRights)
{
return seL4_CapRights.words[0] & MASK(3);
return seL4_CapRights.words[0] & MASK(4);
}
static inline cap_transfer_t PURE

9
include/fastpath/fastpath.h
View file

@ -73,15 +73,16 @@ thread_state_ptr_mset_blockingObject_tsType(thread_state_t *ts_ptr,
}
static inline void
cap_reply_cap_ptr_new_np(cap_t *cap_ptr, word_t capReplyMaster,
word_t capTCBPtr)
cap_reply_cap_ptr_new_np(cap_t *cap_ptr, word_t capReplyCanGrant,
word_t capReplyMaster, word_t capTCBPtr)
{
#ifdef __KERNEL_64__
cap_ptr->words[1] = (word_t)capTCBPtr;
cap_ptr->words[0] = (capReplyMaster) | ((word_t)cap_reply_cap << 59);
cap_ptr->words[0] = (capReplyMaster) | (capReplyCanGrant << 1) |
((word_t)cap_reply_cap << 59);
#else
cap_ptr->words[0] = TCB_REF(capTCBPtr) | (capReplyMaster << 4) |
cap_reply_cap ;
(capReplyCanGrant << 5) | cap_reply_cap ;
#endif
}

2
include/kernel/thread.h
View file

@ -93,7 +93,7 @@ void suspend(tcb_t *target);
void restart(tcb_t *target);
void doIPCTransfer(tcb_t *sender, endpoint_t *endpoint,
word_t badge, bool_t grant, tcb_t *receiver);
void doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot);
void doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot, bool_t grant);
void doNormalTransfer(tcb_t *sender, word_t *sendBuffer, endpoint_t *endpoint,
word_t badge, bool_t canGrant, tcb_t *receiver,
word_t *receiveBuffer);

3
include/object/endpoint.h
View file

@ -15,7 +15,8 @@
#include <object/structures.h>
void sendIPC(bool_t blocking, bool_t do_call, word_t badge,
bool_t canGrant, tcb_t *thread, endpoint_t *epptr);
bool_t canGrant, bool_t canGrantReply, tcb_t *thread,
endpoint_t *epptr);
void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking);
void cancelIPC(tcb_t *tptr);
void cancelAllIPC(endpoint_t *epptr);

6
include/object/objecttype.h
View file

@ -35,11 +35,11 @@ exception_t decodeInvocation(word_t invLabel, word_t length,
extra_caps_t excaps, bool_t block, bool_t call,
word_t *buffer);
exception_t performInvocation_Endpoint(endpoint_t *ep, word_t badge,
bool_t canGrant, bool_t block,
bool_t call);
bool_t canGrant, bool_t canGrantReply,
bool_t block, bool_t call);
exception_t performInvocation_Notification(notification_t *ntfn,
word_t badge);
exception_t performInvocation_Reply(tcb_t *thread, cte_t *slot);
exception_t performInvocation_Reply(tcb_t *thread, cte_t *slot, bool_t canGrant);
word_t getObjectSize(word_t t, word_t userObjSize);
static inline void

19
include/object/structures_32.bf
View file

@ -29,10 +29,10 @@ block untyped_cap {
field capType 4
}
block endpoint_cap(capEPBadge, capCanGrant, capCanSend, capCanReceive,
capEPPtr, capType) {
block endpoint_cap(capEPBadge, capCanGrantReply, capCanGrant, capCanSend,
capCanReceive, capEPPtr, capType) {
field_high capEPPtr 28
padding 1
field capCanGrantReply 1
field capCanGrant 1
field capCanReceive 1
field capCanSend 1
@ -51,10 +51,11 @@ block notification_cap {
field capType 4
}
block reply_cap(capReplyMaster, capTCBPtr, capType) {
block reply_cap(capReplyCanGrant, capReplyMaster, capTCBPtr, capType) {
padding 32
field_high capTCBPtr 27
field_high capTCBPtr 26
field capReplyCanGrant 1
field capReplyMaster 1
field capType 4
}
@ -157,9 +158,11 @@ block mdb_node {
-- * Inactive
-- * BlockedOnReceive
-- - Endpoint
-- - CanGrant
-- * BlockedOnSend
-- - Endpoint
-- - CanGrant
-- - CanGrantReply
-- - IsCall
-- - IPCBadge
-- - Fault
@ -270,13 +273,15 @@ block DebugException {
#endif
-- Thread state: size = 12 bytes
block thread_state(blockingIPCBadge, blockingIPCCanGrant, blockingIPCIsCall,
block thread_state(blockingIPCBadge, blockingIPCCanGrant,
blockingIPCCanGrantReply, blockingIPCIsCall,
tcbQueued, blockingObject,
tsType) {
field blockingIPCBadge 28
field blockingIPCCanGrant 1
field blockingIPCCanGrantReply 1
field blockingIPCIsCall 1
padding 2
padding 1
-- this is fastpath-specific. it is useful to be able to write
-- tsType and without changing tcbQueued

28
include/object/structures_64.bf
View file

@ -28,15 +28,16 @@ block untyped_cap {
field_high capPtr 48
}
block endpoint_cap(capEPBadge, capType, capCanGrant, capCanSend, capCanReceive,
capEPPtr) {
block endpoint_cap(capEPBadge, capCanGrantReply, capCanGrant, capCanSend,
capCanReceive, capEPPtr, capType) {
field capEPBadge 64
field capType 5
field capCanGrantReply 1
field capCanGrant 1
field capCanReceive 1
field capCanSend 1
padding 8
padding 7
field_high capEPPtr 48
}
@ -51,17 +52,18 @@ block notification_cap {
field_high capNtfnPtr 48
}
block reply_cap(capReplyMaster, capTCBPtr, capType) {
block reply_cap(capReplyCanGrant, capReplyMaster, capTCBPtr, capType) {
field capTCBPtr 64
field capType 5
padding 58
padding 57
field capReplyCanGrant 1
field capReplyMaster 1
}
-- The user-visible format of the data word is defined by cnode_capdata, below.
block cnode_cap(capCNodeRadix, capCNodeGuardSize, capCNodeGuard,
capType, capCNodePtr) {
capCNodePtr, capType) {
field capCNodeGuard 64
field capType 5
@ -151,11 +153,12 @@ block mdb_node {
-- * Restart
-- * Inactive
-- * BlockedOnReceive
-- - DiminishCaps
-- - Endpoint
-- - CanGrant
-- * BlockedOnSend
-- - Endpoint
-- - CanGrant
-- - CanGrantReply
-- - IsCall
-- - IPCBadge
-- - Fault
@ -278,16 +281,17 @@ block DebugException {
}
#endif
-- Thread state: size = 8 bytes
block thread_state(blockingIPCBadge, blockingIPCCanGrant, blockingIPCIsCall,
tcbQueued, blockingIPCDiminishCaps, tsType,
blockingObject) {
-- Thread state: size = 24 bytes
block thread_state(blockingIPCBadge, blockingIPCCanGrant,
blockingIPCCanGrantReply, blockingIPCIsCall,
tcbQueued, blockingObject,
tsType) {
field blockingIPCBadge 64
padding 60
field blockingIPCCanGrant 1
field blockingIPCCanGrantReply 1
field blockingIPCIsCall 1
field blockingIPCDiminishCaps 1
field tcbQueued 1
padding 16

2
include/object/tcb.h
View file

@ -81,7 +81,7 @@ void remoteTCBStall(tcb_t *tcb);
tcb_queue_t tcbEPAppend(tcb_t *tcb, tcb_queue_t queue);
tcb_queue_t tcbEPDequeue(tcb_t *tcb, tcb_queue_t queue);
void setupCallerCap(tcb_t *sender, tcb_t *receiver);
void setupCallerCap(tcb_t *sender, tcb_t *receiver, bool_t canGrant);
void deleteCallerCap(tcb_t *receiver);
word_t copyMRs(tcb_t *sender, word_t *sendBuf, tcb_t *receiver,

17
libsel4/include/sel4/shared_types.h
View file

@ -37,13 +37,14 @@ enum {
SEL4_FORCE_LONG_ENUM(seL4_CapFault_Msg),
} seL4_CapFault_Msg;
#define seL4_ReadWrite seL4_CapRights_new(0, 1, 1)
#define seL4_AllRights seL4_CapRights_new(1, 1, 1)
#define seL4_CanRead seL4_CapRights_new(0, 1, 0)
#define seL4_CanWrite seL4_CapRights_new(0, 0, 1)
#define seL4_CanGrant seL4_CapRights_new(1, 0, 0)
#define seL4_NoWrite seL4_CapRights_new(1, 1, 0)
#define seL4_NoRead seL4_CapRights_new(1, 0, 1)
#define seL4_NoRights seL4_CapRights_new(0, 0, 0)
#define seL4_ReadWrite seL4_CapRights_new(0, 0, 1, 1)
#define seL4_AllRights seL4_CapRights_new(1, 1, 1, 1)
#define seL4_CanRead seL4_CapRights_new(0, 0, 1, 0)
#define seL4_CanWrite seL4_CapRights_new(0, 0, 0, 1)
#define seL4_CanGrant seL4_CapRights_new(0, 1, 0, 0)
#define seL4_CanGrantReply seL4_CapRights_new(1, 0, 0, 0)
#define seL4_NoWrite seL4_CapRights_new(1, 1, 1, 0)
#define seL4_NoRead seL4_CapRights_new(1, 1, 0, 1)
#define seL4_NoRights seL4_CapRights_new(0, 0, 0, 0)
#endif

3
libsel4/include/sel4/shared_types_32.bf
View file

@ -23,7 +23,8 @@ block seL4_MessageInfo {
-- Cap rights
block seL4_CapRights {
padding 29
padding 28
field capAllowGrantReply 1
field capAllowGrant 1
field capAllowRead 1
field capAllowWrite 1

3
libsel4/include/sel4/shared_types_64.bf
View file

@ -24,7 +24,8 @@ block seL4_MessageInfo {
block seL4_CapRights {
padding 32
padding 29
padding 28
field capAllowGrantReply 1
field capAllowGrant 1
field capAllowRead 1
field capAllowWrite 1

29
manual/parts/cspace.tex
View file

@ -142,10 +142,13 @@ As mentioned previously, some capability types have \emph{access
rights} associated with them. Currently, access rights are
associated with capabilities for \obj{Endpoint}s (see
\autoref{ch:ipc}), \obj{Notification}s (see
\autoref{ch:notifications}) and \obj{Page}s (see \autoref{ch:vspace}). The
\autoref{ch:notifications}), \obj{Page}s (see \autoref{ch:vspace}) and
\obj{Reply}ing (see \autoref{ch:ipc}). The
access rights associated with a capability determine the methods that
can be invoked. seL4 supports three orthogonal access rights, which
are Read, Write and Grant. The meaning of each right is interpreted
can be invoked. seL4 supports four access rights, which
are Read, Write, Grant and GrantReply. Read, Write and Grant are orthogonal to
each other. GrantReply is a less powerful form of Grant e.g. if you already have
Grant, having GrantReply or not is irrelevant. The meaning of each right is interpreted
relative to the various object types, as detailed
in~\autoref{tab:rights}.
@ -158,17 +161,23 @@ rights than the source capability is specified for the destination
capability in either of these invocations, the destination rights are
silently downgraded to those of the source.
%TODO it looks ugly now
\begin{table}[htb]
\begin{tabularx}{\textwidth}{p{0.15\textwidth}XXX}
\renewcommand{\arraystretch}{1.5}
\begin{tabularx}{\textwidth}{p{0.15\textwidth}XXXX}
\toprule
Type & Read & Write & Grant \\
Type & Read & Write & Grant & GrantReply \\
\midrule
\obj{Endpoint} & Required to receive. & Required to send. & Required to send capabilities (including reply capabilities).\\
\obj{Notification} & Required to wait. & Required to signal. & N/A \\
\obj{Page} & Required to map the page readable. & Required to map the page writable. & N/A \\
\obj{Endpoint} & Receiving & Sending & Sending any
capabilities & Sending reply
capabilities \\
\obj{Notification} & Waiting & Signaling & N/A & N/A \\
\obj{Page} & Mapping the page readable. & Mapping the page writable. & N/A & N/A \\
\obj{Reply} & N/A & N/A & Sending any capabilities in reply message & N/A \\
\bottomrule
\end{tabularx}
\caption{\label{tab:rights}seL4 access rights.}
\caption{\label{tab:rights}seL4 access rights: What a specific right entitles a
capability to do}
\end{table}
\subsection{Capability Derivation Tree}
@ -227,7 +236,7 @@ capabilities. Further copies of these derived capabilities will
create siblings, in this case remaining on level 5. There is an
exception to this scheme for \obj{Endpoint} and \obj{Notification} capabilities --- they support an
additional layer of depth though \emph{badging}.
The original \obj{Endpoint} or \emph{Notification} capability will be unbadged. Using
The original \obj{Endpoint} or \obj{Notification} capability will be unbadged. Using
the mint method, a copy of the capability with a specific \emph{badge} can be
created (see \autoref{s:ep-badge}, \autoref{s:notif-badge}). This new, badged capability to the same object is treated as
an original capability (the ``original badged endpoint capability'')

73
manual/parts/ipc.tex
View file

@ -114,6 +114,14 @@ no sender is ready, threads performing the \apifunc{seL4\_Recv}{sel4_recv}
system call or the second half of \apifunc{seL4\_ReplyRecv}{sel4_replyrecv}
will wait for the first available sender.
Trying to Send or Call without the Write right will fail and return an error. In
the case of Send the error is ignored (The kernel isn't allowed to reply). Thus
there is no way of knowing that a send has failed because of missing right.
On the other hand calling \apifunc{seL4\_Recv}{sel4_recv} with a endpoint capability that
does not have the Read right will raise a fault, see \autoref{sec:faults}. This
because otherwise the error message would be indistinguishable from a normal
message received from another thread via the endpoint.
\subsection{Endpoint Badges\label{s:ep-badge}}
\label{sec:ep-badges}
@ -152,11 +160,6 @@ These fields specify the root CNode, capability address and number of bits to re
the slot in which to put the capability. Capability
addressing is described in \autoref{sec:cap_addressing}.
A received capability has the same rights as the original, except if
the \emph{receiving} endpoint capability lacks the Write right.
In this case, the rights on the sent capability are \emph{diminished}, by
stripping the Write right from the received copy of the capability.
Note that receiving threads may specify only one receive slot, whereas a
sending thread may include multiple capabilities in the message. Messages
containing more than one capability may be interpreted by kernel objects. They
@ -220,3 +223,63 @@ buffer is set to the number of capabilities transferred up to failure.
No error message will be returned to the receiving thread in any of the
above cases.
\subsection{Calling and Replying}
\label{sec:ep-cal}
As explained in \autoref{sec:sys_call}, when the user calls
\apifunc{seL4\_Call}{sel4_call} on an endpoint capability,
some specific actions are taken. First a call will do exactly the same action as
a normal \apifunc{seL4\_Send}{sel4_send}. Then after the rendezvous and all the
normal IPC procedure happened, instead of returning directly to the caller,
\apifunc{seL4\_Call}{sel4_call} will check if either Grant or GrantReply are
present on the invoked endpoint capability:
\begin{itemize}
\item If this is not the case, the caller thread is suspended as if
\apifunc{seL4\_TCB\_Suspend}{tcb_suspend} was called on it. The send part of
the call would still have been performed as usual.
\item If this is the case. A reply capability is set in a specific slot of the
receiver TCB. The Grant right of that reply capability is set by copying the Grant
right of the endpoint capability invoked by the receiver in
\apifunc{seL4\_Recv}{sel4_recv}.
Then, the caller thread is blocked waiting for the reply.
\end{itemize}
A reply capability points directly to the caller thread and once the call has
been performed is completely unrelated to the original \obj{Endpoint}. Even if
the latter was destroyed, the reply capability would still exist and point to
the caller who would still be waiting for a reply.
The generated reply capability can then be either invoked in place (in the
specific TCB slot) with the \apifunc{seL4\_Reply}{sel4_reply} or saved to an
addressable slot using \apifunc{seL4\_CNode\_SaveCaller}{cnode_savecaller} to be
invoked later with \apifunc{seL4\_Send}{sel4_send}. The specific slot cannot be
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}.
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,
then the thread it points to is waiting for a reply. However a reply capability
is a non-owning reference, contrary to all the other capabilities. That means that
if the caller thread is destroyed or modified in any way that would render
a reply impossible (for example being suspended with
\apifunc{seL4\_TCB\_Suspend}{tcb_suspend}), the kernel would immediately destroy
the reply capability.
Once the reply capability has been invoked, the caller receives the message as if
it has been performing a \apifunc{seL4\_Recv}{sel4_recv} and just received the
message. In particular, it starts running again.
The \apifunc{seL4\_Call}{sel4_call} operation exists not only for
efficiency reasons (combining two operations into a single system
call). It differs from
\apifunc{seL4\_Send}{sel4_send} immediately followed by
\apifunc{seL4\_Recv}{sel4_recv} in ways that allow certain system setup to work
much more efficiently with much less setup that with a traditional setup.
In particular, it is guaranteed that the reply received by the caller comes from
the thread that received the call without having to check any kind of badge.

90
manual/parts/objects.tex
View file

@ -109,21 +109,28 @@ number of data words and possibly some capabilities. The structure and encoding
of these messages are described in detail in \autoref{ch:ipc}.
Threads send messages by invoking capabilities within their capability space.
When an endpoint capability is invoked in this way, the message will be
transferred through the kernel to another thread. When capabilities to kernel
objects are invoked, the message will be interpreted as a method invocation in a
manner specific to the type of kernel object. For example, invoking a thread
control block (TCB) capability with a correctly formatted message will suspend
the target thread.
When an endpoint, notification or reply capability is invoked in this way, the
message will be transferred through the kernel to another thread.
When other capabilities to kernel objects are invoked, the message will be
interpreted as a method invocation in a manner specific to the type of kernel
object. For example, invoking a thread control block (TCB) capability with a
correctly formatted message will suspend the target thread.
Logically, the kernel provides three system calls, \emph{Send},
\emph{Receive} and \emph{Yield}. However, there are also combinations
and variants of the basic \emph{Send} and \emph{Receive} calls, e.g.\
the \emph{Call} operation, which consists of a send followed by a
\emph{Receive} from the same object. Methods on kernel objects other
than endpoints and notifications are all mapped to \emph{Send} or
\emph{Call}, depending on whether or not the method returns a
result. The \emph{Yield} system call is not associated with any kernel
and variants of the basic \emph{Send} and \emph{Receive} calls. An
important variant is the \emph{Call} operation, which consists of a standard
\emph{Send} operation atomically followed by a variant of \emph{Receive} which is waiting
for a \emph{Reply}. Replying is
always targeted at a specific thread instead of going through standard IPC mechanics.
Invoking Methods on kernel object other than endpoints and notifications
is done with \emph{Send} or \emph{Call},
depending on whether or not the invoker wants a reply from the kernel.
By using functions provided by the libsel4 API you are guaranteed to always use the most
appropriate one.
The \emph{Yield} system call is not associated with any kernel
object and is the only operation that does not invoke a capability.
The complete set of system calls is:
@ -144,53 +151,38 @@ The complete set of system calls is:
\apifunc{seL4\_Send}{sel4_send}, no error code or response will be returned.
\item[\apifunc{seL4\_Call}{sel4_call}] combines \apifunc{seL4\_Send}{sel4_send}
and \apifunc{seL4\_Recv}{sel4_recv}. The call
blocks the sending thread until its message is delivered and a reply message is received. When the
sent message is delivered to another thread (via an
\obj{Endpoint}), the kernel adds an
additional `\emph{reply}' capability to the message that is delivered
to the receiver, giving the latter the right to reply to the original sender. The reply
capability is deposited in a dedicated slot in the receiver's
\obj{TCB}, and is a single-use right, meaning that the kernel
invalidates it as soon as it has been invoked.
and \apifunc{seL4\_Recv}{sel4_recv} with some important differences. The call
blocks the sending thread until its message is delivered and a reply
message is received.
The \apifunc{seL4\_Call}{sel4_call} operation exists not only for
efficiency reasons (combining two operations into a single system
call). It differs from
\apifunc{seL4\_Send}{sel4_send} immediately followed by
\apifunc{seL4\_Recv}{sel4_recv} in two ways:
\begin{enumerate}
\item the single-use reply capability is created to establish a
reply channel with minimal trust;
\item the transition from send to recv phase is atomic, meaning it
cannot be preempted, and the receiver can reply without any risk
of blocking.
\end{enumerate}
When invoking capabilities to kernel services other than endpoints, using
\apifunc{seL4\_Call}{sel4_call} allows the kernel to return an error code
or other response through the reply message.
When invoking capabilities to kernel services, using
\apifunc{seL4\_Call}{sel4_call} allows the kernel to return an error code
or other response through the reply message.
When the sent message is delivered to another thread (via an
\obj{Endpoint}), the kernel does the same operation as
\apifunc{seL4\_Send}{sel4_send}, then deposits a \emph{reply} capability
in a dedicated slot in the receiver's \obj{TCB}. A \emph{reply} capability
is a single-use right to send a reply message and wake up the caller,
meaning that the kernel invalidates it as soon as it has been invoked.
The calling thread is blocked until the reply capability is invoked.
For more information, see \autoref{sec:ep-cal}.
\item[\apifunc{seL4\_Recv}{sel4_recv}] is used by a thread to receive
messages through endpoints or notifications. If no sender or
notification is pending, the caller
will block until a message or notification can be delivered. This system call works only on
\obj{Endpoint} or \obj{Notification} capabilities, raising a fault (see section \ref{sec:faults}) when
\obj{Endpoint} or \obj{Notification} capabilities, raising a fault
(see section \ref{sec:faults}) when
attempted with other capability types.
\item[\apifunc{seL4\_Reply}{sel4_reply}] is used to respond to a
\apifunc{seL4\_Call}{sel4_call}, using the reply capability generated by the
\apifunc{seL4\_Call}{sel4_call} system call and stored in the replying
thread's TCB. It delivers the message to the thread that invoked
the \apifunc{seL4\_Call}{sel4_call}, waking it in
the process.
There is space for only one reply capability in each thread's TCB, so the
\apifunc{seL4\_Reply}{sel4_reply} syscall can be used to reply to the most
recent caller only. The \apifunc{seL4\_CNode\_SaveCaller}{cnode_savecaller}
method that will be described later can be used to save the reply
capability into regular capability space, where it can be used with
\apifunc{seL4\_Send}{sel4_send}.
\apifunc{seL4\_Call}{sel4_call}, by invoking the reply capability
generated by the \apifunc{seL4\_Call}{sel4_call} system call and
stored in a dedicated slot in the replying thread's TCB. It has exactly the
same behavior as invoking the reply cap with
\apifunc{seL4\_Send}{sel4_send} which is described in
\autoref{sec:ep-cal}.
\item[\apifunc{seL4\_ReplyRecv}{sel4_replyrecv}] combines \apifunc{seL4\_Reply}{sel4_reply} and
\apifunc{seL4\_Recv}{sel4_recv}. It exists mostly for efficiency reasons: the common case of

9
manual/parts/threads.tex
View file

@ -114,12 +114,15 @@ The register contents are transferred via the IPC buffer.
A thread's actions may result in a fault. Faults are delivered to the
thread's exception handler so that it can take the appropriate action.
The fault type is specified in the message label and is one of:
seL4\_Fault\_CapFault, seL4\_Fault\_VMFault, seL4\_Fault\_UnknownSyscall, seL4\_Fault\_UserException, seL4\_Fault\_DebugException,
or seL4\_Fault\_NullFault (indicating no fault occurred and this is a normal IPC message).
\texttt{seL4\_Fault\_CapFault}, \texttt{seL4\_Fault\_VMFault},
\texttt{seL4\_Fault\_UnknownSyscall}, \texttt{seL4\_Fault\_UserException},
\texttt{seL4\_Fault\_DebugException}, or \texttt{seL4\_Fault\_NullFault}
(indicating no fault occurred and this is a normal IPC message).
Fault are delivered in such a way as to imitate a Call from the faulting
thread. This means that to send a fault message the fault endpoint
must have both write and grant permissions.
must have Write and either Grant or GrantReply permissions. If this is not the
case, a double fault happens (generally the thread is simply suspended).
\subsection{Capability Faults}

3
src/api/syscall.c
View file

@ -352,7 +352,8 @@ handleReply(void)
/* Haskell error:
* "handleReply: caller must not be the current thread" */
assert(caller != NODE_STATE(ksCurThread));
doReplyTransfer(NODE_STATE(ksCurThread), caller, callerSlot);
doReplyTransfer(NODE_STATE(ksCurThread), caller, callerSlot,
cap_reply_cap_get_capReplyCanGrant(callerCap));
return;
}

12
src/fastpath/fastpath.c
View file

@ -34,6 +34,7 @@ fastpath_call(word_t cptr, word_t msgInfo)
pde_t stored_hw_asid;
word_t fault_type;
dom_t dom;
word_t replyCanGrant;
/* Get message info, length, and fault type. */
info = messageInfoFromWord_raw(msgInfo);
@ -113,9 +114,10 @@ fastpath_call(word_t cptr, word_t msgInfo)
slowpath(SysCall);
}
/* Ensure that the endpoint has has grant rights so that we can
/* Ensure that the endpoint has has grant or grant-reply rights so that we can
* create the reply cap */
if (unlikely(!cap_endpoint_cap_get_capCanGrant(ep_cap))) {
if (unlikely(!cap_endpoint_cap_get_capCanGrant(ep_cap) &&
!cap_endpoint_cap_get_capCanGrantReply(ep_cap))) {
slowpath(SysCall);
}
@ -168,7 +170,9 @@ fastpath_call(word_t cptr, word_t msgInfo)
callerSlot = TCB_PTR_CTE_PTR(dest, tcbCaller);
/* Insert reply cap */
cap_reply_cap_ptr_new_np(&callerSlot->cap, 0, TCB_REF(NODE_STATE(ksCurThread)));
replyCanGrant = thread_state_ptr_get_blockingIPCCanGrant(&dest->tcbState);;
cap_reply_cap_ptr_new_np(&callerSlot->cap, replyCanGrant, 0,
TCB_REF(NODE_STATE(ksCurThread)));
mdb_node_ptr_set_mdbPrev_np(&callerSlot->cteMDBNode, CTE_REF(replySlot));
mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged(
&replySlot->cteMDBNode, CTE_REF(callerSlot), 1, 1);
@ -330,6 +334,8 @@ fastpath_reply_recv(word_t cptr, word_t msgInfo)
/* Set thread state to BlockedOnReceive */
thread_state_ptr_mset_blockingObject_tsType(
&NODE_STATE(ksCurThread)->tcbState, (word_t)ep_ptr, ThreadState_BlockedOnReceive);
thread_state_ptr_set_blockingIPCCanGrant(&NODE_STATE(ksCurThread)->tcbState,
cap_endpoint_cap_get_capCanGrant(ep_cap));;
/* Place the thread in the endpoint queue */
endpointTail = endpoint_ptr_get_epQueue_tail_fp(ep_ptr);

7
src/kernel/faulthandler.c
View file

@ -47,14 +47,15 @@ sendFaultIPC(tcb_t *tptr)
if (cap_get_capType(handlerCap) == cap_endpoint_cap &&
cap_endpoint_cap_get_capCanSend(handlerCap) &&
cap_endpoint_cap_get_capCanGrant(handlerCap)) {
(cap_endpoint_cap_get_capCanGrant(handlerCap) ||
cap_endpoint_cap_get_capCanGrantReply(handlerCap))) {
tptr->tcbFault = current_fault;
if (seL4_Fault_get_seL4_FaultType(current_fault) == seL4_Fault_CapFault) {
tptr->tcbLookupFailure = original_lookup_fault;
}
sendIPC(true, false,
sendIPC(true, true,
cap_endpoint_cap_get_capEPBadge(handlerCap),
true, tptr,
cap_endpoint_cap_get_capCanGrant(handlerCap), true, tptr,
EP_PTR(cap_endpoint_cap_get_capEPPtr(handlerCap)));
return EXCEPTION_NONE;

4
src/kernel/thread.c
View file

@ -116,13 +116,13 @@ doIPCTransfer(tcb_t *sender, endpoint_t *endpoint, word_t badge,
}
void
doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot)
doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot, bool_t grant)
{
assert(thread_state_get_tsType(receiver->tcbState) ==
ThreadState_BlockedOnReply);
if (likely(seL4_Fault_get_seL4_FaultType(receiver->tcbFault) == seL4_Fault_NullFault)) {
doIPCTransfer(sender, NULL, 0, true, receiver);
doIPCTransfer(sender, NULL, 0, grant, receiver);
/** GHOSTUPD: "(True, gs_set_assn cteDeleteOne_'proc (ucast cap_reply_cap))" */
cteDeleteOne(slot);
setThreadState(receiver, ThreadState_Running);

2
src/object/cnode.c
View file

@ -780,7 +780,7 @@ setupReplyMaster(tcb_t *thread)
if (cap_get_capType(slot->cap) == cap_null_cap) {
/* Haskell asserts that no reply caps exist for this thread here. This
* cannot be translated. */
slot->cap = cap_reply_cap_new(true, TCB_REF(thread));
slot->cap = cap_reply_cap_new(true, true, TCB_REF(thread));
slot->cteMDBNode = nullMDBNode;
mdb_node_ptr_set_mdbRevocable(&slot->cteMDBNode, true);
mdb_node_ptr_set_mdbFirstBadged(&slot->cteMDBNode, true);

26
src/object/endpoint.c
View file

@ -38,7 +38,7 @@ ep_ptr_set_queue(endpoint_t *epptr, tcb_queue_t queue)
void
sendIPC(bool_t blocking, bool_t do_call, word_t badge,
bool_t canGrant, tcb_t *thread, endpoint_t *epptr)
bool_t canGrant, bool_t canGrantReply, tcb_t *thread, endpoint_t *epptr)
{
switch (endpoint_ptr_get_state(epptr)) {
case EPState_Idle:
@ -55,6 +55,8 @@ sendIPC(bool_t blocking, bool_t do_call, word_t badge,
&thread->tcbState, badge);
thread_state_ptr_set_blockingIPCCanGrant(
&thread->tcbState, canGrant);
thread_state_ptr_set_blockingIPCCanGrantReply(
&thread->tcbState, canGrantReply);
thread_state_ptr_set_blockingIPCIsCall(
&thread->tcbState, do_call);
@ -71,6 +73,7 @@ sendIPC(bool_t blocking, bool_t do_call, word_t badge,
case EPState_Recv: {
tcb_queue_t queue;
tcb_t *dest;
bool_t replyCanGrant;
/* Get the head of the endpoint queue. */
queue = ep_ptr_get_queue(epptr);
@ -90,13 +93,14 @@ sendIPC(bool_t blocking, bool_t do_call, word_t badge,
/* Do the transfer */
doIPCTransfer(thread, epptr, badge, canGrant, dest);
replyCanGrant = thread_state_ptr_get_blockingIPCCanGrant(&dest->tcbState);;
setThreadState(dest, ThreadState_Running);
possibleSwitchTo(dest);
if (do_call ||
seL4_Fault_ptr_get_seL4_FaultType(&thread->tcbFault) != seL4_Fault_NullFault) {
if (canGrant) {
setupCallerCap(thread, dest);
if (do_call) {
if (canGrant || canGrantReply) {
setupCallerCap(thread, dest, replyCanGrant);
} else {
setThreadState(thread, ThreadState_Inactive);
}
@ -134,6 +138,8 @@ receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
ThreadState_BlockedOnReceive);
thread_state_ptr_set_blockingObject(
&thread->tcbState, EP_REF(epptr));
thread_state_ptr_set_blockingIPCCanGrant(
&thread->tcbState, cap_endpoint_cap_get_capCanGrant(cap));
scheduleTCB(thread);
@ -153,6 +159,7 @@ receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
tcb_t *sender;
word_t badge;
bool_t canGrant;
bool_t canGrantReply;
bool_t do_call;
/* Get the head of the endpoint queue. */
@ -174,6 +181,8 @@ receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
badge = thread_state_ptr_get_blockingIPCBadge(&sender->tcbState);
canGrant =
thread_state_ptr_get_blockingIPCCanGrant(&sender->tcbState);
canGrantReply =
thread_state_ptr_get_blockingIPCCanGrantReply(&sender->tcbState);
/* Do the transfer */
doIPCTransfer(sender, epptr, badge,
@ -181,10 +190,9 @@ receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
do_call = thread_state_ptr_get_blockingIPCIsCall(&sender->tcbState);
if (do_call ||
seL4_Fault_get_seL4_FaultType(sender->tcbFault) != seL4_Fault_NullFault) {
if (canGrant) {
setupCallerCap(sender, thread);
if (do_call) {
if (canGrant || canGrantReply) {
setupCallerCap(sender, thread, cap_endpoint_cap_get_capCanGrant(cap));
} else {
setThreadState(sender, ThreadState_Inactive);
}

32
src/object/objecttype.c
View file

@ -208,6 +208,7 @@ hasCancelSendRights(cap_t cap)
case cap_endpoint_cap:
return cap_endpoint_cap_get_capCanSend(cap) &&
cap_endpoint_cap_get_capCanReceive(cap) &&
cap_endpoint_cap_get_capCanGrantReply(cap) &&
cap_endpoint_cap_get_capCanGrant(cap);
default:
@ -376,7 +377,6 @@ maskCapRights(seL4_CapRights_t cap_rights, cap_t cap)
case cap_domain_cap:
case cap_cnode_cap:
case cap_untyped_cap:
case cap_reply_cap:
case cap_irq_control_cap:
case cap_irq_handler_cap:
case cap_zombie_cap:
@ -395,6 +395,9 @@ maskCapRights(seL4_CapRights_t cap_rights, cap_t cap)
new_cap = cap_endpoint_cap_set_capCanGrant(
new_cap, cap_endpoint_cap_get_capCanGrant(cap) &
seL4_CapRights_get_capAllowGrant(cap_rights));
new_cap = cap_endpoint_cap_set_capCanGrantReply(
new_cap, cap_endpoint_cap_get_capCanGrantReply(cap) &
seL4_CapRights_get_capAllowGrantReply(cap_rights));
return new_cap;
}
@ -411,6 +414,15 @@ maskCapRights(seL4_CapRights_t cap_rights, cap_t cap)
return new_cap;
}
case cap_reply_cap: {
cap_t new_cap;
new_cap = cap_reply_cap_set_capReplyCanGrant(
cap, cap_reply_cap_get_capReplyCanGrant(cap) &
seL4_CapRights_get_capAllowGrant(cap_rights));
return new_cap;
}
default:
fail("Invalid cap type"); /* Sentinel for invalid enums */
@ -456,7 +468,7 @@ createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceMemory)
case seL4_EndpointObject:
/** AUXUPD: "(True, ptr_retyp
(Ptr (ptr_val \<acute>regionBase) :: endpoint_C ptr))" */
return cap_endpoint_cap_new(0, true, true, true,
return cap_endpoint_cap_new(0, true, true, true, true,
EP_REF(regionBase));
case seL4_NotificationObject:
@ -551,7 +563,8 @@ decodeInvocation(word_t invLabel, word_t length,
return performInvocation_Endpoint(
EP_PTR(cap_endpoint_cap_get_capEPPtr(cap)),
cap_endpoint_cap_get_capEPBadge(cap),
cap_endpoint_cap_get_capCanGrant(cap), block, call);
cap_endpoint_cap_get_capCanGrant(cap),
cap_endpoint_cap_get_capCanGrantReply(cap), block, call);
case cap_notification_cap: {
if (unlikely(!cap_notification_cap_get_capNtfnCanSend(cap))) {
@ -579,7 +592,8 @@ decodeInvocation(word_t invLabel, word_t length,
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
return performInvocation_Reply(
TCB_PTR(cap_reply_cap_get_capTCBPtr(cap)), slot);
TCB_PTR(cap_reply_cap_get_capTCBPtr(cap)), slot,
cap_reply_cap_get_capReplyCanGrant(cap));
case cap_thread_cap:
return decodeTCBInvocation(invLabel, length, cap,
@ -610,10 +624,10 @@ decodeInvocation(word_t invLabel, word_t length,
exception_t
performInvocation_Endpoint(endpoint_t *ep, word_t badge,
bool_t canGrant, bool_t block,
bool_t call)
bool_t canGrant, bool_t canGrantReply,
bool_t block, bool_t call)
{
sendIPC(block, call, badge, canGrant, NODE_STATE(ksCurThread), ep);
sendIPC(block, call, badge, canGrant, canGrantReply, NODE_STATE(ksCurThread), ep);
return EXCEPTION_NONE;
}
@ -627,8 +641,8 @@ performInvocation_Notification(notification_t *ntfn, word_t badge)
}
exception_t
performInvocation_Reply(tcb_t *thread, cte_t *slot)
performInvocation_Reply(tcb_t *thread, cte_t *slot, bool_t canGrant)
{
doReplyTransfer(NODE_STATE(ksCurThread), thread, slot);
doReplyTransfer(NODE_STATE(ksCurThread), thread, slot, canGrant);
return EXCEPTION_NONE;
}

5
src/object/tcb.c
View file

@ -263,7 +263,7 @@ setExtraBadge(word_t *bufferPtr, word_t badge,
}
void
setupCallerCap(tcb_t *sender, tcb_t *receiver)
setupCallerCap(tcb_t *sender, tcb_t *receiver, bool_t canGrant)
{
cte_t *replySlot, *callerSlot;
cap_t masterCap UNUSED, callerCap UNUSED;
@ -274,12 +274,13 @@ setupCallerCap(tcb_t *sender, tcb_t *receiver)
/* Haskell error: "Sender must have a valid master reply cap" */
assert(cap_get_capType(masterCap) == cap_reply_cap);
assert(cap_reply_cap_get_capReplyMaster(masterCap));
assert(cap_reply_cap_get_capReplyCanGrant(masterCap));
assert(TCB_PTR(cap_reply_cap_get_capTCBPtr(masterCap)) == sender);
callerSlot = TCB_PTR_CTE_PTR(receiver, tcbCaller);
callerCap = callerSlot->cap;
/* Haskell error: "Caller cap must not already exist" */
assert(cap_get_capType(callerCap) == cap_null_cap);
cteInsert(cap_reply_cap_new(false, TCB_REF(sender)),
cteInsert(cap_reply_cap_new(canGrant, false, TCB_REF(sender)),
replySlot, callerSlot);
}