diff --git a/CHANGES b/CHANGES
index 00b1dd78d..d75836f35 100644
--- a/CHANGES
+++ b/CHANGES
@@ -9,6 +9,8 @@ changes are added the compatibility information should be updated.
upcoming release BREAKING
+BREAKING CHANGE
+
= Changes =
* Debugging option on x86 for syscall interface to read/write MSRs (this is an, equally dangerous, alternative to
dangerous code injection)
@@ -27,6 +29,17 @@ upcoming release BREAKING
* x86 TSC frequency exported in extended bootinfo header
* `archInfo` is no longer a member of the bootinfo struct. Its only use was for TSC frequency on x86, which
can now be retrieved through the extended bootinfo
+ * Invocations to set thread priority and maximum control priority (MCP) have changed.
+ - For both invocations, users must now provide a TCB capability `auth`
+ - The requested MCP/priority is checked against the MCP of the `auth` capability.
+ - Previous behavior checked against the invoked TCB, which could be subject to the confused deputy
+ problem.
+ * seL4_TCB_Configure no longer takes prio, mcp as an argument. Instead these fields must be set separately
+ with seL4_TCB_SetPriority and seL4_TCB_SetMCPriority.
+
+= Upgrade notes =
+ * seL4_TCB_Configure calls that set priority should be changed to explicitly call seL4_TCB_SetPriority
+ * seL4_TCB_Configure calls that set MCP should be changed to explicitly call seL4_TCB_SetMCPriority
---
8.0.0 2018-01-17
diff --git a/include/api/types.h b/include/api/types.h
index b7be2e8ea..fa9301fb8 100644
--- a/include/api/types.h
+++ b/include/api/types.h
@@ -99,15 +99,6 @@ wordFromMessageInfo(seL4_MessageInfo_t mi)
return mi.words[0];
}
-static inline seL4_PrioProps_t CONST
-prioPropsFromWord(word_t w)
-{
- seL4_PrioProps_t pp;
- pp.words[0] = w;
-
- return pp;
-}
-
#ifdef CONFIG_PRINTING
#ifdef CONFIG_COLOUR_PRINTING
#define ANSI_RESET "\033[0m"
diff --git a/include/object/tcb.h b/include/object/tcb.h
index 617a54043..c8991037e 100644
--- a/include/object/tcb.h
+++ b/include/object/tcb.h
@@ -96,8 +96,8 @@ exception_t decodeReadRegisters(cap_t cap, word_t length, bool_t call,
exception_t decodeWriteRegisters(cap_t cap, word_t length, word_t *buffer);
exception_t decodeTCBConfigure(cap_t cap, word_t length,
cte_t* slot, extra_caps_t rootCaps, word_t *buffer);
-exception_t decodeSetPriority(cap_t cap, word_t length, word_t *buffer);
-exception_t decodeSetMCPriority(cap_t cap, word_t length, word_t *buffer);
+exception_t decodeSetPriority(cap_t cap, word_t length, extra_caps_t excaps, word_t *buffer);
+exception_t decodeSetMCPriority(cap_t cap, word_t length, extra_caps_t excaps, word_t *buffer);
exception_t decodeSetIPCBuffer(cap_t cap, word_t length,
cte_t* slot, extra_caps_t excaps, word_t *buffer);
exception_t decodeSetSpace(cap_t cap, word_t length,
@@ -112,7 +112,6 @@ enum thread_control_flag {
thread_control_update_ipc_buffer = 0x2,
thread_control_update_space = 0x4,
thread_control_update_mcp = 0x8,
- thread_control_update_all = 0xF,
};
typedef word_t thread_control_flag_t;
diff --git a/libsel4/include/interfaces/sel4.xml b/libsel4/include/interfaces/sel4.xml
index d4f051c65..5f7079bcb 100644
--- a/libsel4/include/interfaces/sel4.xml
+++ b/libsel4/include/interfaces/sel4.xml
@@ -125,8 +125,6 @@
-
See
+
@@ -159,6 +159,8 @@
See
+
diff --git a/libsel4/include/sel4/shared_types_32.bf b/libsel4/include/sel4/shared_types_32.bf
index 31e1b34ee..ab4331581 100644
--- a/libsel4/include/sel4/shared_types_32.bf
+++ b/libsel4/include/sel4/shared_types_32.bf
@@ -21,12 +21,6 @@ block seL4_MessageInfo {
field length 7
}
-block seL4_PrioProps {
- padding 16
- field mcp 8
- field prio 8
-}
-
-- Cap rights
block seL4_CapRights {
padding 29
diff --git a/libsel4/include/sel4/shared_types_64.bf b/libsel4/include/sel4/shared_types_64.bf
index 790a43fd3..66bf73aad 100644
--- a/libsel4/include/sel4/shared_types_64.bf
+++ b/libsel4/include/sel4/shared_types_64.bf
@@ -22,13 +22,6 @@ block seL4_MessageInfo {
field length 7
}
-block seL4_PrioProps {
- padding 32
- padding 16
- field mcp 8
- field prio 8
-}
-
block seL4_CapRights {
padding 32
diff --git a/libsel4/tools/syscall_stub_gen.py b/libsel4/tools/syscall_stub_gen.py
index f4580d76d..0397becbd 100644
--- a/libsel4/tools/syscall_stub_gen.py
+++ b/libsel4/tools/syscall_stub_gen.py
@@ -230,7 +230,6 @@ def init_data_types(wordsize):
Type("seL4_Bool", 1, wordsize, native_size_bits=8),
# seL4 Structures
- BitFieldType("seL4_PrioProps_t", wordsize, wordsize),
BitFieldType("seL4_CapRights_t", wordsize, wordsize),
# Object types
diff --git a/manual/parts/threads.tex b/manual/parts/threads.tex
index 411ae9081..fda6f1fe3 100644
--- a/manual/parts/threads.tex
+++ b/manual/parts/threads.tex
@@ -63,10 +63,12 @@ deleted.
seL4 uses a preemptive round-robin scheduler with 256 priority levels.
All threads have a maximum controlled priority (MCP) and a priority, the latter being the effective
priority of the thread.
-When a thread creates or modifies a thread (including itself), it can only set the
-other thread's priority and MCP to be less than or equal to its own MCP. Thread priority and MCP can be
-set with \apifunc{seL4\_TCB\_Configure}{tcb_configure} and
-\apifunc{seL4\_TCB\_SetPriority}{tcb_setpriority}, \apifunc{seL4\_TCB\_SetMCPriority}{tcb_setmcpriority} methods.
+When a thread modifies a another threads priority (including itself) it must provide a
+thread capability from which to use the MCP from. Threads can only set priorities and MCPs
+to be less than or equal to the provided thread's MCP.
+The initial task starts with an MCP and priority as the highest priority in the system (\texttt{seL4\_MaxPrio}).
+Thread priority and MCP can be set with \apifunc{seL4\_TCB\_SetPriority}{tcb_setpriority}
+and \apifunc{seL4\_TCB\_SetMCPriority}{tcb_setmcpriority} methods.
\subsection{Exceptions}
diff --git a/src/object/tcb.c b/src/object/tcb.c
index 6951c4959..c7b2cd4f9 100644
--- a/src/object/tcb.c
+++ b/src/object/tcb.c
@@ -31,11 +31,11 @@
#define NULL_PRIO 0
static exception_t
-checkPrio(prio_t prio)
+checkPrio(prio_t prio, tcb_t *auth)
{
prio_t mcp;
- mcp = NODE_STATE(ksCurThread)->tcbMCP;
+ mcp = auth->tcbMCP;
/* system invariant: existing MCPs are bounded */
assert(mcp <= seL4_MaxPrio);
@@ -698,10 +698,10 @@ decodeTCBInvocation(word_t invLabel, word_t length, cap_t cap,
return decodeTCBConfigure(cap, length, slot, excaps, buffer);
case TCBSetPriority:
- return decodeSetPriority(cap, length, buffer);
+ return decodeSetPriority(cap, length, excaps, buffer);
case TCBSetMCPriority:
- return decodeSetMCPriority(cap, length, buffer);
+ return decodeSetMCPriority(cap, length, excaps, buffer);
case TCBSetIPCBuffer:
return decodeSetIPCBuffer(cap, length, slot, excaps, buffer);
@@ -884,9 +884,8 @@ decodeWriteRegisters(cap_t cap, word_t length, word_t *buffer)
w, transferArch, buffer);
}
-/* SetPriority, SetMCPriority, SetIPCParams and SetSpace are all
+/* SetPriority, SetMCPriority, SetIPCBuffer and SetSpace are all
* specialisations of TCBConfigure. */
-
exception_t
decodeTCBConfigure(cap_t cap, word_t length, cte_t* slot,
extra_caps_t rootCaps, word_t *buffer)
@@ -895,12 +894,9 @@ decodeTCBConfigure(cap_t cap, word_t length, cte_t* slot,
cap_t bufferCap, cRootCap, vRootCap;
deriveCap_ret_t dc_ret;
cptr_t faultEP;
- seL4_PrioProps_t props;
- prio_t prio, mcp;
word_t cRootData, vRootData, bufferAddr;
- exception_t status;
- if (length < 5 || rootCaps.excaprefs[0] == NULL
+ if (length < 4 || rootCaps.excaprefs[0] == NULL
|| rootCaps.excaprefs[1] == NULL
|| rootCaps.excaprefs[2] == NULL) {
userError("TCB Configure: Truncated message.");
@@ -909,10 +905,9 @@ decodeTCBConfigure(cap_t cap, word_t length, cte_t* slot,
}
faultEP = getSyscallArg(0, buffer);
- props = prioPropsFromWord(getSyscallArg(1, buffer));
- cRootData = getSyscallArg(2, buffer);
- vRootData = getSyscallArg(3, buffer);
- bufferAddr = getSyscallArg(4, buffer);
+ cRootData = getSyscallArg(1, buffer);
+ vRootData = getSyscallArg(2, buffer);
+ bufferAddr = getSyscallArg(3, buffer);
cRootSlot = rootCaps.excaprefs[0];
cRootCap = rootCaps.excaprefs[0]->cap;
@@ -921,23 +916,6 @@ decodeTCBConfigure(cap_t cap, word_t length, cte_t* slot,
bufferSlot = rootCaps.excaprefs[2];
bufferCap = rootCaps.excaprefs[2]->cap;
- prio = seL4_PrioProps_get_prio(props);
- mcp = seL4_PrioProps_get_mcp(props);
-
- status = checkPrio(prio);
- if (status != EXCEPTION_NONE) {
- userError("TCB Configure: Requested priority %lu too high (max %lu).",
- (unsigned long) prio, (unsigned long) NODE_STATE(ksCurThread)->tcbMCP);
- return status;
- }
-
- status = checkPrio(mcp);
- if (status != EXCEPTION_NONE) {
- userError("TCB Configure: Requested maximum controlled priority %lu too high (max %lu),",
- (unsigned long) mcp, (unsigned long) NODE_STATE(ksCurThread)->tcbMCP);
- return status;
- }
-
if (bufferAddr == 0) {
bufferSlot = NULL;
} else {
@@ -997,31 +975,38 @@ decodeTCBConfigure(cap_t cap, word_t length, cte_t* slot,
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
return invokeTCB_ThreadControl(
TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)), slot,
- faultEP, mcp, prio,
+ faultEP, NULL_PRIO, NULL_PRIO,
cRootCap, cRootSlot,
vRootCap, vRootSlot,
bufferAddr, bufferCap,
- bufferSlot, thread_control_update_all);
+ bufferSlot, thread_control_update_space |
+ thread_control_update_ipc_buffer);
}
exception_t
-decodeSetPriority(cap_t cap, word_t length, word_t *buffer)
+decodeSetPriority(cap_t cap, word_t length, extra_caps_t excaps, word_t *buffer)
{
- prio_t newPrio;
- exception_t status;
-
- if (length < 1) {
+ if (length < 1 || excaps.excaprefs[0] == NULL) {
userError("TCB SetPriority: Truncated message.");
current_syscall_error.type = seL4_TruncatedMessage;
return EXCEPTION_SYSCALL_ERROR;
}
- newPrio = getSyscallArg(0, buffer);
+ prio_t newPrio = getSyscallArg(0, buffer);
+ cap_t authCap = excaps.excaprefs[0]->cap;
- status = checkPrio(newPrio);
+ if (cap_get_capType(authCap) != cap_thread_cap) {
+ userError("Set priority: authority cap not a TCB.");
+ current_syscall_error.type = seL4_InvalidCapability;
+ current_syscall_error.invalidCapNumber = 1;
+ return EXCEPTION_SYSCALL_ERROR;
+ }
+
+ tcb_t *authTCB = TCB_PTR(cap_thread_cap_get_capTCBPtr(authCap));
+ exception_t status = checkPrio(newPrio, authTCB);
if (status != EXCEPTION_NONE) {
userError("TCB SetPriority: Requested priority %lu too high (max %lu).",
- (unsigned long) newPrio, (unsigned long) NODE_STATE(ksCurThread)->tcbMCP);
+ (unsigned long) newPrio, (unsigned long) authTCB->tcbMCP);
return status;
}
@@ -1036,23 +1021,29 @@ decodeSetPriority(cap_t cap, word_t length, word_t *buffer)
}
exception_t
-decodeSetMCPriority(cap_t cap, word_t length, word_t *buffer)
+decodeSetMCPriority(cap_t cap, word_t length, extra_caps_t excaps, word_t *buffer)
{
- prio_t newMcp;
- exception_t status;
-
- if (length < 1) {
+ if (length < 1 || excaps.excaprefs[0] == NULL) {
userError("TCB SetMCPriority: Truncated message.");
current_syscall_error.type = seL4_TruncatedMessage;
return EXCEPTION_SYSCALL_ERROR;
}
- newMcp = getSyscallArg(0, buffer);
+ prio_t newMcp = getSyscallArg(0, buffer);
+ cap_t authCap = excaps.excaprefs[0]->cap;
- status = checkPrio(newMcp);
+ if (cap_get_capType(authCap) != cap_thread_cap) {
+ userError("TCB SetMCPriority: authority cap not a TCB.");
+ current_syscall_error.type = seL4_InvalidCapability;
+ current_syscall_error.invalidCapNumber = 1;
+ return EXCEPTION_SYSCALL_ERROR;
+ }
+
+ tcb_t *authTCB = TCB_PTR(cap_thread_cap_get_capTCBPtr(authCap));
+ exception_t status = checkPrio(newMcp, authTCB);
if (status != EXCEPTION_NONE) {
userError("TCB SetMCPriority: Requested maximum controlled priority %lu too high (max %lu).",
- (unsigned long) newMcp, (unsigned long) NODE_STATE(ksCurThread)->tcbMCP);
+ (unsigned long) newMcp, (unsigned long) authTCB->tcbMCP);
return status;
}