Imagelibrary/seL4
1
0
Fork 1
mirror of https://github.com/seL4/seL4.git synced 2026-03-27 18:39:55 +00:00
Code Issues Packages Projects Releases Wiki Activity

mcs: refactor decodeSchedControl_ConfigureFlags

Browse Source 
Done in order to ensure overflow does not occur. More
specifically, we call usToTicks on an argument only
when it has been checked to be at most MAX_PERIOD_US,
so that we know that overflow does not occur as a
result of the conversion. We also rephrase the check
on extra_refills. Rather than performing an addition,
which may in extreme cases overflow, we perform a
subtraction, which we know does not underflow, as a
result of our invariants.

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
Michael McInerney
2025-05-03 00:18:33 +09:30
committed by Gerwin Klein
parent c55f50b6e5
commit 8d569b8e65
1 changed files with 40 additions and 18 deletions
Download Patch File Download Diff File Expand all files Collapse all files

58
src/object/schedcontrol.c
View File

@@ -92,22 +92,8 @@ static exception_t decodeSchedControl_ConfigureFlags(word_t length, cap_t cap, w
} }
time_t budget_us = mode_parseTimeArg(0, buffer); time_t budget_us = mode_parseTimeArg(0, buffer);
ticks_t budget_ticks = usToTicks(budget_us);
time_t period_us = mode_parseTimeArg(TIME_ARG_SIZE, buffer);
ticks_t period_ticks = usToTicks(period_us);
word_t extra_refills = getSyscallArg(TIME_ARG_SIZE * 2, buffer);
word_t badge = getSyscallArg(TIME_ARG_SIZE * 2 + 1, buffer);
word_t flags = getSyscallArg(TIME_ARG_SIZE * 2 + 2, buffer);
cap_t targetCap = current_extra_caps.excaprefs[0]->cap; if (budget_us > MAX_PERIOD_US) {
if (unlikely(cap_get_capType(targetCap) != cap_sched_context_cap)) {
userError("SchedControl_ConfigureFlags: target cap not a scheduling context cap");
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 1;
return EXCEPTION_SYSCALL_ERROR;
}
if (budget_us > MAX_PERIOD_US || budget_ticks < MIN_BUDGET) {
userError("SchedControl_ConfigureFlags: budget out of range."); userError("SchedControl_ConfigureFlags: budget out of range.");
current_syscall_error.type = seL4_RangeError; current_syscall_error.type = seL4_RangeError;
current_syscall_error.rangeErrorMin = MIN_BUDGET_US; current_syscall_error.rangeErrorMin = MIN_BUDGET_US;
@@ -115,7 +101,29 @@ static exception_t decodeSchedControl_ConfigureFlags(word_t length, cap_t cap, w
return EXCEPTION_SYSCALL_ERROR; return EXCEPTION_SYSCALL_ERROR;
} }
if (period_us > MAX_PERIOD_US || period_ticks < MIN_BUDGET) { ticks_t budget_ticks = usToTicks(budget_us);
time_t period_us = mode_parseTimeArg(TIME_ARG_SIZE, buffer);
if (period_us > MAX_PERIOD_US) {
userError("SchedControl_ConfigureFlags: period out of range.");
current_syscall_error.type = seL4_RangeError;
current_syscall_error.rangeErrorMin = MIN_BUDGET_US;
current_syscall_error.rangeErrorMax = MAX_PERIOD_US;
return EXCEPTION_SYSCALL_ERROR;
}
ticks_t period_ticks = usToTicks(period_us);
if (budget_ticks < MIN_BUDGET) {
userError("SchedControl_ConfigureFlags: budget out of range.");
current_syscall_error.type = seL4_RangeError;
current_syscall_error.rangeErrorMin = MIN_BUDGET_US;
current_syscall_error.rangeErrorMax = MAX_PERIOD_US;
return EXCEPTION_SYSCALL_ERROR;
}
if (period_ticks < MIN_BUDGET) {
userError("SchedControl_ConfigureFlags: period out of range."); userError("SchedControl_ConfigureFlags: period out of range.");
current_syscall_error.type = seL4_RangeError; current_syscall_error.type = seL4_RangeError;
current_syscall_error.rangeErrorMin = MIN_BUDGET_US; current_syscall_error.rangeErrorMin = MIN_BUDGET_US;
@@ -131,16 +139,30 @@ static exception_t decodeSchedControl_ConfigureFlags(word_t length, cap_t cap, w
return EXCEPTION_SYSCALL_ERROR; return EXCEPTION_SYSCALL_ERROR;
} }
if (extra_refills + MIN_REFILLS > refill_absolute_max(targetCap)) { cap_t targetCap = current_extra_caps.excaprefs[0]->cap;
if (unlikely(cap_get_capType(targetCap) != cap_sched_context_cap)) {
userError("SchedControl_ConfigureFlags: target cap not a scheduling context cap");
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 1;
return EXCEPTION_SYSCALL_ERROR;
}
word_t extra_refills = getSyscallArg(TIME_ARG_SIZE * 2, buffer);
word_t max_refills = refill_absolute_max(targetCap);
if (extra_refills > max_refills - MIN_REFILLS) {
current_syscall_error.type = seL4_RangeError; current_syscall_error.type = seL4_RangeError;
current_syscall_error.rangeErrorMin = 0; current_syscall_error.rangeErrorMin = 0;
current_syscall_error.rangeErrorMax = refill_absolute_max(targetCap) - MIN_REFILLS; current_syscall_error.rangeErrorMax = max_refills - MIN_REFILLS;
userError("Max refills invalid, got %lu, max %lu", userError("Max refills invalid, got %lu, max %lu",
extra_refills, extra_refills,
current_syscall_error.rangeErrorMax); current_syscall_error.rangeErrorMax);
return EXCEPTION_SYSCALL_ERROR; return EXCEPTION_SYSCALL_ERROR;
} }
word_t badge = getSyscallArg(TIME_ARG_SIZE * 2 + 1, buffer);
word_t flags = getSyscallArg(TIME_ARG_SIZE * 2 + 2, buffer);
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
return invokeSchedControl_ConfigureFlags(SC_PTR(cap_sched_context_cap_get_capSCPtr(targetCap)), return invokeSchedControl_ConfigureFlags(SC_PTR(cap_sched_context_cap_get_capSCPtr(targetCap)),
cap_sched_control_cap_get_core(cap), cap_sched_control_cap_get_core(cap),