rework physical address space limits

- add KernelPhysAddressSpaceBits and PHYS_ADDR_SPACE_BITS
- add KernelPhysAddrTop and CONFIG_PHYS_ADDR_TOP
- make CONFIG_PADDR_USER_DEVICE_TOP an alias
- remove KernelPaddrUserTop from CMake
- remove KernelArmPASizeBits40 from CMake
- remove KernelArmPASizeBits44 from CMake
- improve comment why the last page is always excluded

Signed-off-by: Axel Heider <axelheider@gmx.de>

CHANGES

@@ -38,6 +38,8 @@ Upcoming release: BINARY COMPATIBLE
   constant seL4_GlobalsFrame from libsel4 as well as the IPC buffer in GlobalsFrame caveat from CAVEATS-generic.md
 * Implement KernelArmExportPTMRUser and KernelArmExportVTMRUser options for Arm generic timer use access on aarch32.
 * Removed obsolete define `HAVE_AUTOCONF`
+* 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
 ---

config.cmake

@@ -190,7 +190,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)
@@ -212,7 +212,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(

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

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

src/arch/arm/config.cmake

@@ -10,39 +10,33 @@ if(KernelArchARM)
     set_property(TARGET kernel_config_target APPEND PROPERTY TOPLEVELTYPES pde_C)
 endif()
 
-set(KernelArmPASizeBits40 OFF)
-set(KernelArmPASizeBits44 OFF)
 if(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(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)")
+    set(KernelPhysAddressSpaceBits 44)
+else()
+    # set nothing.
 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}")
 
 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")
+    # a system with ARMv8 64-bit cores may be building in 32-bit mode, so make
+    # sure maximum physical address space is 32-bit then.
+    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 +85,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")

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)

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)

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)) {

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;
 }
 

tools/hardware/config.py

@@ -11,9 +11,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. '''
@@ -30,6 +30,9 @@ def get_device_page_bits(self) -> int:
         ''' Get page size in bits for mapping devices for this arch '''
         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 Config_ARM(Config):
     ''' Config class for ARM '''
@@ -61,13 +64,13 @@ def get_device_page_bits(self) -> int:
         return self.MEGAPAGE_BITS
 
 
-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 '''
     if sel4arch in ['aarch32', 'aarch64', 'arm_hyp']:
-        return Config_ARM(sel4arch, addrspace_max)
+        return Config_ARM(sel4arch, phys_addr_space_bits)
     elif sel4arch == 'riscv32':
-        return Config_RISCV32(sel4arch, addrspace_max)
+        return Config_RISCV32(sel4arch, phys_addr_space_bits)
     elif sel4arch == 'riscv64':
-        return Config_RISCV64(sel4arch, addrspace_max)
+        return Config_RISCV64(sel4arch, phys_addr_space_bits)
     else:
         raise ValueError('Unsupported sel4arch "{}" specified.'.format(sel4arch))

tools/hardware/utils/memory.py

@@ -126,7 +126,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()))
     }
 

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,8 +75,8 @@ 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='maximum address space that is available as device untyped', type=int, default=32)
 
     parser.add_argument('--enable-profiling', help='enable profiling',
                         action='store_const', const=True, default=False)