diff --git a/CHANGES b/CHANGES index 800a22b1bd3..a61289276d1 100644 --- a/CHANGES +++ b/CHANGES @@ -44,6 +44,8 @@ Upcoming release: BREAKING This change is reflected in the definition of the seL4_UserTop constant that holds the largest user virtual address. * aarch32 VM fault messages now deliver original (untranslated) faulting IP in a hypervisor context, matching aarch64 behaviour. +* Added CONFIG_PHYS_ADDR_SPACE_BITS (KernelPhysAddressSpaceBits), from this CONFIG_PHYS_ADDR_TOP (KernelPhysAddrTop) + gets derived in the generic CMake files. PADDR_USER_DEVICE_TOP (KernelPaddrUserTop) is kept as an alias. ## Upgrade Notes --- diff --git a/config.cmake b/config.cmake index 40bf2663852..46440d5440d 100644 --- a/config.cmake +++ b/config.cmake @@ -202,7 +202,7 @@ if(DEFINED KernelDTSList AND (NOT "${KernelDTSList}" STREQUAL "")) --compat-strings-out "${compatibility_outfile}" --c-header --header-out "${device_dest}" --hardware-config "${config_file}" --hardware-schema "${config_schema}" --yaml --yaml-out "${platform_yaml}" --sel4arch - "${KernelSel4Arch}" --addrspace-max "${KernelPaddrUserTop}" + "${KernelSel4Arch}" --phys-addr-space-bits "${KernelPhysAddressSpaceBits}" RESULT_VARIABLE error ) if(error) @@ -224,7 +224,13 @@ endif() # Enshrine common variables in the config config_set(KernelHaveFPU HAVE_FPU "${KernelHaveFPU}") -config_set(KernelPaddrUserTop PADDR_USER_DEVICE_TOP "${KernelPaddrUserTop}") + +config_set(KernelPhysAddressSpaceBits PHYS_ADDR_SPACE_BITS "${KernelPhysAddressSpaceBits}") +# Calculate the highest address that this still in the physical address space +# here in CMake, so we derive integers that are inside the target's C inter +# range. +math(EXPR KernelPhysAddrTop "(1 << ${KernelPhysAddressSpaceBits}) - 1") +config_set(KernelPhysAddrTop PHYS_ADDR_TOP "SEL4_WORD_CONST(${KernelPhysAddrTop})") # System parameters config_string( diff --git a/include/arch/arm/arch/64/mode/hardware.h b/include/arch/arm/arch/64/mode/hardware.h index cf99d6e6540..f4bff675156 100644 --- a/include/arch/arm/arch/64/mode/hardware.h +++ b/include/arch/arm/arch/64/mode/hardware.h @@ -215,8 +215,8 @@ asserts check that the kernel config won't lead to UTs being created that aren't representable. */ #ifndef __ASSEMBLER__ -compile_assert(ut_max_less_than_cannonical, CONFIG_PADDR_USER_DEVICE_TOP <= BIT(47)); +compile_assert(ut_max_less_than_cannonical, CONFIG_PHYS_ADDR_SPACE_BITS <= 47); #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT -compile_assert(ut_max_is_cannonical, (PPTR_BASE + CONFIG_PADDR_USER_DEVICE_TOP) <= BIT(48)); +compile_assert(ut_max_is_cannonical, PPTR_BASE + CONFIG_PHYS_ADDR_TOP <= BIT(48)); #endif #endif diff --git a/include/config.h b/include/config.h index d3418b8ad0a..c7e7d944b05 100644 --- a/include/config.h +++ b/include/config.h @@ -13,8 +13,17 @@ #define ENABLE_SMP_SUPPORT #endif +/* keep some names for legacy compatibility */ +#ifdef CONFIG_ARCH_ARM +#if (CONFIG_PHYS_ADDR_SPACE_BITS == 40) +#define CONFIG_ARM_PA_SIZE_BITS_40 1 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT -#ifdef CONFIG_ARM_PA_SIZE_BITS_40 -#define AARCH64_VSPACE_S2_START_L1 -#endif -#endif +#define AARCH64_VSPACE_S2_START_L1 CONFIG_AARCH64_VSPACE_S2_START_L1 +#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ +#elif (CONFIG_PHYS_ADDR_SPACE_BITS == 44) +#define CONFIG_ARM_PA_SIZE_BITS_44 1 +#endif /* PHYS_ADDR_SPACE_BITS */ +#endif /* CONFIG_ARCH_ARM */ + +/* CONFIG_PADDR_USER_DEVICE_TOP is no longer set by the CMake configuration. */ +#define CONFIG_PADDR_USER_DEVICE_TOP CONFIG_PHYS_ADDR_TOP diff --git a/src/arch/arm/config.cmake b/src/arch/arm/config.cmake index 32d9619b09a..42133c105dd 100644 --- a/src/arch/arm/config.cmake +++ b/src/arch/arm/config.cmake @@ -10,39 +10,75 @@ if(KernelArchARM) set_property(TARGET kernel_config_target APPEND PROPERTY TOPLEVELTYPES pde_C) endif() -set(KernelArmPASizeBits40 OFF) -set(KernelArmPASizeBits44 OFF) -if(KernelArmCortexA35) +if(KernelArmCortexA7) + # nothing special +elseif(KernelArmCortexA8) + # nothing special +elseif(KernelArmCortexA9) + # nothing special +elseif(KernelArmCortexA15) + # supports a 40-bit physical address space via LPAE +elseif(KernelArmCortexA17) + # supports a 40-bit physical address space via LPAE +elseif(KernelArmCortexA35) set(KernelArmICacheVIPT ON) - set(KernelArmPASizeBits40 ON) - math(EXPR KernelPaddrUserTop "(1 << 40)") + set(KernelPhysAddressSpaceBits 40) elseif(KernelArmCortexA53) set(KernelArmICacheVIPT ON) - set(KernelArmPASizeBits40 ON) - math(EXPR KernelPaddrUserTop "(1 << 40)") + set(KernelPhysAddressSpaceBits 40) elseif(KernelArmCortexA55) set(KernelArmICacheVIPT ON) - set(KernelArmPASizeBits40 ON) - math(EXPR KernelPaddrUserTop "(1 << 40)") + set(KernelPhysAddressSpaceBits 40) elseif(KernelArmCortexA57) - set(KernelArmPASizeBits44 ON) - math(EXPR KernelPaddrUserTop "(1 << 44)") + set(KernelPhysAddressSpaceBits 44) +#elseif(KernelArmCortexA65) +# set(KernelPhysAddressSpaceBits 44) elseif(KernelArmCortexA72) - # For Cortex-A72 in AArch64 state, the physical address range is 44 bits - # (https://developer.arm.com/documentation/100095/0001/memory-management-unit/about-the-mmu) - set(KernelArmPASizeBits44 ON) - math(EXPR KernelPaddrUserTop "(1 << 44)") + # https://developer.arm.com/documentation/100095/0003/Memory-Management-Unit/About-the-MMU + set(KernelPhysAddressSpaceBits 44) +#elseif(KernelArmCortexA73) +# set(KernelPhysAddressSpaceBits 40) +#elseif(KernelArmCortexA75) +# set(KernelPhysAddressSpaceBits 44) +#elseif(KernelArmCortexA76) +# set(KernelPhysAddressSpaceBits 40) +#elseif(KernelArmCortexA77) +# set(KernelPhysAddressSpaceBits 40) +#elseif(KernelArmCortexA78) +# set(KernelPhysAddressSpaceBits 40) +#elseif(KernelArmCortexA78AE) +# set(KernelPhysAddressSpaceBits 48) +#elseif(KernelArmCortexA510) +# set(KernelPhysAddressSpaceBits 40) +#elseif(KernelArmCortexA710) +# set(KernelPhysAddressSpaceBits 40) +else() + # In ARMv8, ID_AA64MMFR0_EL1.PARange gives the physical address space size, + # values are: + # 0: 32 bits (4 GB) + # 1: 36 bits (64 GB) + # 2: 40 bits (1 TB) + # 3: 42 bits (4 TB) + # 4: 44 bits (16 TB) + # 5: 48 bits (256 TB) + # 6: 52 bits (4 PB, added in Armv8.2-A, implies FEAT_LPA) + # 7-15: reserved + # A general comparison table for can be found at + # https://developer.arm.com/-/media/Arm%20Developer%20Community/PDF/Cortex-A%20R%20M%20datasheets/Arm%20Cortex-A%20Comparison%20Table_v4.ashx + message(FATAL_ERROR "unsupported ARM core") endif() -config_set(KernelArmPASizeBits40 ARM_PA_SIZE_BITS_40 "${KernelArmPASizeBits40}") -config_set(KernelArmPASizeBits44 ARM_PA_SIZE_BITS_44 "${KernelArmPASizeBits44}") + config_set(KernelArmICacheVIPT ARM_ICACHE_VIPT "${KernelArmICacheVIPT}") +# In 32-bit mode (AARCH32) seL4 can handle a maximum physical address space of +# 32 bits, even if the core supports LPAE that technically allows mapping pages +# from larger addresses. if(KernelSel4ArchAarch32) - # 64-bit targets may be building in 32-bit mode, - # so make sure maximum paddr is 32-bit. - math(EXPR KernelPaddrUserTop "(1 << 32) - 1") + set(KernelPhysAddressSpaceBits 32) endif() +config_set(KernelArmICacheVIPT ARM_ICACHE_VIPT "${KernelArmICacheVIPT}") + include(src/arch/arm/armv/armv7-a/config.cmake) include(src/arch/arm/armv/armv8-a/config.cmake) @@ -91,7 +127,7 @@ config_option( config_option(KernelArmGicV3 ARM_GIC_V3_SUPPORT "Build support for GICv3" DEFAULT OFF) -if(KernelArmPASizeBits40 AND ARM_HYPERVISOR_SUPPORT) +if((KernelPhysAddressSpaceBits EQUAL 40) AND ARM_HYPERVISOR_SUPPORT) config_set(KernelAarch64VspaceS2StartL1 AARCH64_VSPACE_S2_START_L1 "ON") else() config_set(KernelAarch64VspaceS2StartL1 AARCH64_VSPACE_S2_START_L1 "OFF") diff --git a/src/arch/riscv/config.cmake b/src/arch/riscv/config.cmake index 866601b01c5..34f7e1ef5b1 100644 --- a/src/arch/riscv/config.cmake +++ b/src/arch/riscv/config.cmake @@ -50,21 +50,25 @@ endif() if(KernelSel4ArchRiscV32) set(KernelPTLevels 2 CACHE STRING "" FORCE) -endif() -if(KernelPTLevels EQUAL 2) - if(KernelSel4ArchRiscV32) - # seL4 on RISCV32 uses 32-bit ints for addresses, - # so limit the maximum paddr to 32-bits. - math(EXPR KernelPaddrUserTop "(1 << 32) - 1") + # Actually, RV32 with Sv32 supports a 34-bit (16 GiByte) physical address + # space. However, we only support a 32-bit address space at the moment when + # targeting 32-bit architectures. + set(KernelPhysAddressSpaceBits 32) +elseif(KernelSel4ArchRiscV64) + # The RISC-V privileged spec v1.12 defines that RV64 always uses a 56-bit + # physical address space. + if(KernelPTLevels EQUAL 3) + # structures.bf limits us to a 39-bit physical address space in Sv39 + # mode with a 39-bit VA space and 3 page table levels + set(KernelPhysAddressSpaceBits 39) else() - math(EXPR KernelPaddrUserTop "1 << 34") + # Sv48: 48-bit VA space with 4 page table levels (unsupported) + # Sv57: 57-bit VA space with 5 page table levels (unsupported) + # Sv64: details still unclear + message(FATAL_ERROR "KernelPTLevels=${KernelPTLevels} is unsupported") endif() -elseif(KernelPTLevels EQUAL 3) - # RISC-V technically supports 56-bit paddrs, - # but structures.bf limits us to using 39 of those bits. - math(EXPR KernelPaddrUserTop "1 << 39") -elseif(KernelPTLevels EQUAL 4) - math(EXPR KernelPaddrUserTop "1 << 56") +else() + message(FATAL_ERROR "unsuppored RISC-V architecture") endif() if(KernelRiscvExtD) diff --git a/src/arch/x86/config.cmake b/src/arch/x86/config.cmake index 6cd9ad1c337..2ce48363574 100644 --- a/src/arch/x86/config.cmake +++ b/src/arch/x86/config.cmake @@ -346,9 +346,9 @@ config_option( if(KernelSel4ArchIA32) set(KernelSetTLSBaseSelf ON) - math(EXPR KernelPaddrUserTop "0xffff0000") + set(KernelPhysAddressSpaceBits 32) else() - math(EXPR KernelPaddrUserTop "1 << 47") + set(KernelPhysAddressSpaceBits 47) endif() if(KernelSel4ArchX86_64 AND NOT KernelFSGSBaseInst) set(KernelSetTLSBaseSelf ON) diff --git a/src/kernel/boot.c b/src/kernel/boot.c index 4a5790632d4..a4977e77f6d 100644 --- a/src/kernel/boot.c +++ b/src/kernel/boot.c @@ -666,9 +666,10 @@ BOOT_CODE bool_t create_untypeds(cap_t root_cnode_cap, start = ndks_boot.reserved[i].end; } - if (start < CONFIG_PADDR_USER_DEVICE_TOP) { + if (start < CONFIG_PHYS_ADDR_TOP) { region_t reg = paddr_to_pptr_reg((p_region_t) { - start, CONFIG_PADDR_USER_DEVICE_TOP + .start = start, + .end = CONFIG_PHYS_ADDR_TOP }); if (!create_untypeds_for_region(root_cnode_cap, true, reg, first_untyped_slot)) { diff --git a/src/plat/pc99/machine/hardware.c b/src/plat/pc99/machine/hardware.c index 3c3de243a9c..4765f1a0d18 100644 --- a/src/plat/pc99/machine/hardware.c +++ b/src/plat/pc99/machine/hardware.c @@ -17,16 +17,50 @@ BOOT_CODE bool_t platAddDevices(void) { - /* remove the MSI region as poking at this is undefined and may allow for - * the user to generate arbitrary MSI interrupts. Only need to consider - * this if it would actually be in the user device region */ - if (CONFIG_PADDR_USER_DEVICE_TOP > 0xFFFFFFF8) { - if (!reserve_region((p_region_t) { - (word_t)0xFFFFFFF8, (word_t)0xFFFFFFF8 + 8 - })) { + + /* The last 64 KiByte page of the physical address space is not allowed to + * be used to to prevent userland from exploiting a corner case. If e.g. a + * syscall is placed at the very last instruction, the hardware generates a + * return address of that address +2, which is non-canonical. The kernel + * loads that invalid address into sysret and this may cause undefined + * behavior eventually. + * See also https://sel4.atlassian.net/browse/SELFOUR-1179. + */ + p_region_t p_reg_reserved = { + .start = ROUND_DOWN(CONFIG_PHYS_ADDR_TOP, 16), + .end = CONFIG_PHYS_ADDR_TOP + }; + + if (!reserve_region(p_reg_reserved)) { + printf("ERROR: could not reserve last 64k of phys memory " + "[0x%"SEL4_PRIx_word": 0x%08"SEL4_PRIx_word"\n", + p_reg_reserved.start, p_reg_reserved.end); + return false; + } + +#ifndef CONFIG_ARCH_IA32 + + /* remove the 8 byte MSI region [0xfffffff8 - ffffffff] at the end of the + * 32-bit address range, as poking at this area is undefined and may allow + * for the user to generate arbitrary MSI interrupts. Only need to consider + * this if it would actually be in the user device region. + */ + p_region_t p_reg_msi = { + .start = SEL4_WORD_CONST(0xfffffff8), + .end = SEL4_WORD_CONST(0xffffffff) + }; + + if (CONFIG_PHYS_ADDR_TOP > p_reg_msi.start) { + if (!reserve_region(p_reg_msi)) { + printf("ERROR: could not reserve MSI region " + "[0x%"SEL4_PRIx_word": 0x%08"SEL4_PRIx_word"\n", + p_reg_msi.start, p_reg_msi.end); return false; } } + +#endif /* not CONFIG_ARCH_IA32 */ + return true; } diff --git a/tools/hardware/config.py b/tools/hardware/config.py index 18b4087c19f..4206bbf1f97 100644 --- a/tools/hardware/config.py +++ b/tools/hardware/config.py @@ -17,9 +17,9 @@ class Config: ''' Abstract config class ''' arch = 'unknown' - def __init__(self, sel4arch, addrspace_max): + def __init__(self, sel4arch, phys_addr_space_bits): self.sel4arch = sel4arch - self.addrspace_max = addrspace_max + self.phys_addr_space_bits = phys_addr_space_bits def get_kernel_phys_align(self) -> int: ''' Used to align the base of physical memory. Returns alignment size in bits. ''' @@ -41,6 +41,9 @@ def get_device_page_bits(self) -> int: ''' return self.get_page_bits() + def get_phys_addr_space_bits(self) -> int: + ''' Return the physical address space in 2^n bits. ''' + return self.phys_addr_space_bits class ARMConfig(Config): ''' Config class for ARM ''' @@ -70,7 +73,7 @@ def get_device_page_bits(self) -> int: raise ValueError('Unsupported sel4arch "{}" specified.'.format(self.sel4arch)) -def get_arch_config(sel4arch: str, addrspace_max: int) -> Config: +def get_arch_config(sel4arch: str, phys_addr_space_bits: int) -> Config: ''' Return an appropriate Config object for the given architecture ''' for (ctor, arch_list) in [ @@ -78,6 +81,6 @@ def get_arch_config(sel4arch: str, addrspace_max: int) -> Config: (RISCVConfig, ['riscv32', 'riscv64']), ]: if sel4arch in arch_list: - return ctor(sel4arch, addrspace_max) + return ctor(sel4arch, phys_addr_space_bits) raise ValueError('Unsupported sel4arch "{}" specified.'.format(sel4arch)) diff --git a/tools/hardware/utils/memory.py b/tools/hardware/utils/memory.py index 3ae4820a4af..1b071b034ed 100644 --- a/tools/hardware/utils/memory.py +++ b/tools/hardware/utils/memory.py @@ -129,7 +129,7 @@ def visitor(node: WrappedNode): Region( 0, hardware.utils.align_down( - hw_yaml.config.addrspace_max, + 2**hw_yaml.config.get_phys_addr_space_bits(), hw_yaml.config.get_smallest_kernel_object_alignment())) } diff --git a/tools/hardware_gen.py b/tools/hardware_gen.py index 3171a3154ed..e8d7a9df64c 100644 --- a/tools/hardware_gen.py +++ b/tools/hardware_gen.py @@ -49,7 +49,7 @@ def add_task_args(outputs: dict, parser: argparse.ArgumentParser): def main(args: argparse.Namespace): ''' Parse the DT and hardware config YAML and run each selected output method. ''' - cfg = hardware.config.get_arch_config(args.sel4arch, args.addrspace_max) + cfg = hardware.config.get_arch_config(args.sel4arch, args.phys_addr_space_bits) parsed_dt = FdtParser(args.dtb) rules = yaml.load(args.hardware_config, Loader=yaml.FullLoader) schema = yaml.load(args.hardware_schema, Loader=yaml.FullLoader) @@ -75,9 +75,9 @@ def main(args: argparse.Namespace): required=True, type=argparse.FileType('r')) parser.add_argument('--sel4arch', help='seL4 architecture to generate for', required=True) - parser.add_argument('--addrspace-max', - help='maximum address that is available as device untyped', type=int, default=32) - + parser.add_argument('--phys-addr-space-bits', + help='size of the physical address space, which is available as device untyped', + type=int, default=32) parser.add_argument('--enable-profiling', help='enable profiling', action='store_const', const=True, default=False)