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

vspace: check for stale mapping on all flush types

Browse source 
Frame caps should be checked for stale mapping info before authorising
any operation on them. In this particular case, the mapping may have
become invalid.

See also #1281

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2024-07-01 10:25:36 +10:00
parent 79cee3563f
commit e5d01aa3f2
1 changed files with 18 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/arch/arm/64/kernel/vspace.c
View file

@ -1664,26 +1664,25 @@ static exception_t decodeARMFrameInvocation(word_t invLabel, word_t length,
return EXCEPTION_SYSCALL_ERROR;
}
#else
/* When in EL1, we are using the user page table for flushing and need to make sure
the mapping info in the cap is not stale. */
lookupPTSlot_ret_t lu_ret = lookupPTSlot(find_ret.vspace_root, vaddr);
pte_t pte = *lu_ret.ptSlot;
void *base_ptr = (void *) cap_frame_cap_get_capFBasePtr(cap);
if (unlikely(lu_ret.ptBitsLeft != pageBitsForSize(cap_frame_cap_get_capFSize(cap)) ||
!pte_is_page_type(pte) ||
pte_get_page_base_address(pte) != pptr_to_paddr(base_ptr))) {
userError("Page Flush: Attempting to use cap with stale mapping information.");
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 0;
return EXCEPTION_SYSCALL_ERROR;
}
/* When in EL1, the mapping must be writeable for DC IVAC */
if (invLabel == ARMPageInvalidate_Data) {
lookupPTSlot_ret_t lu_ret = lookupPTSlot(find_ret.vspace_root, vaddr);
pte_t pte = *lu_ret.ptSlot;
void *base_ptr = (void *) cap_frame_cap_get_capFBasePtr(cap);
/* The cap mapping info could be out of date, so we need to check that the page we are
getting is the one the cap provides authority for. */
if (unlikely(lu_ret.ptBitsLeft != pageBitsForSize(cap_frame_cap_get_capFSize(cap)) ||
!pte_is_page_type(pte) ||
pte_get_page_base_address(pte) != pptr_to_paddr(base_ptr))) {
userError("ARMPageInvalidate_Data: Attempting to use cap with stale mapping information.");
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 0;
return EXCEPTION_SYSCALL_ERROR;
}
if (vmRightsFromPTE(pte) != VMReadWrite) {
userError("ARMPageInvalidate_Data: Cannot call on mapping without write rights.");
current_syscall_error.type = seL4_IllegalOperation;
return EXCEPTION_SYSCALL_ERROR;
}
if (invLabel == ARMPageInvalidate_Data && vmRightsFromPTE(pte) != VMReadWrite) {
userError("ARMPageInvalidate_Data: Cannot call on mapping without write rights.");
current_syscall_error.type = seL4_IllegalOperation;
return EXCEPTION_SYSCALL_ERROR;
}
#endif
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);