IOMMU: Validate IOMMU Kernel Support

Ensure that the sel4::Config struct has the
iommu flag asserted, indicating the kernel was
built with IOMMU support. If not we fail parsing any
io address space elements encountered in the sdf.

Signed-off-by: Callum <c.berry@student.unsw.edu.au>

Author: cazb2

tool/microkit/src/main.rs

@@ -210,6 +210,11 @@ fn main() -> Result<(), String> {
         _ => false,
     };
 
+    let iommu = match arch {
+        Arch::X86_64 => json_str_as_bool(&kernel_config_json, "IOMMU")?,
+        _ => false,
+    };
+
     let arm_pa_size_bits = match arch {
         Arch::Aarch64 => {
             if json_str_as_bool(&kernel_config_json, "ARM_PA_SIZE_BITS_40")? {
@@ -248,6 +253,7 @@ fn main() -> Result<(), String> {
             "MAX_NUM_BOOTINFO_UNTYPED_CAPS",
         )?,
         hypervisor,
+        iommu,
         benchmark: args.config == "benchmark",
         num_cores: if json_str_as_bool(&kernel_config_json, "ENABLE_SMP_SUPPORT")? {
             json_str_as_u64(&kernel_config_json, "MAX_NUM_NODES")?

tool/microkit/src/sdf.rs

@@ -696,20 +696,12 @@ impl SysMap {
 
 impl SysIOMap {
     fn from_xml(
-        config: &Config,
+        _config: &Config,
         xml_sdf: &XmlSystemDescription,
         node: &roxmltree::Node,
         device: &str,
         identifier: IommuDeviceIdentifier,
     ) -> Result<SysIOMap, String> {
-        if config.arch != Arch::X86_64 {
-            return Err(value_error(
-                xml_sdf,
-                node,
-                "IOMMU is not yet supported on ARM and RISC-V by Microkit".to_string(),
-            ));
-        }
-
         let attrs = vec!["mr", "iovaddr", "perms"];
 
         check_attributes(xml_sdf, node, &attrs)?;
@@ -771,6 +763,14 @@ impl IOAddressSpace {
         device_names: &mut HashSet<String>,
         iommu_device_identifiers: &mut HashSet<IommuDeviceIdentifier>,
     ) -> Result<IOAddressSpace, String> {
+        let pos = xml_sdf.doc.text_pos_at(node.range().start);
+        if !config.iommu {
+            return Err(format!(
+                "Error: io address space requires seL4 to be built with IOMMU support: {}",
+                loc_string(xml_sdf, pos)
+            ));
+        }
+
         check_attributes(xml_sdf, node, &["name", "peripheral_id"])?;
         let device_name = checked_lookup(xml_sdf, node, "name")?;
         if !device_names.insert(device_name.to_string()) {

tool/microkit/src/sel4.rs

@@ -289,6 +289,7 @@ pub struct Config {
     pub cap_address_bits: u64,
     pub fan_out_limit: u64,
     pub max_num_bootinfo_untypeds: u64,
+    pub iommu: bool,
     pub hypervisor: bool,
     pub benchmark: bool,
     pub num_cores: u8,

tool/microkit/tests/sdf/iommu_missing_from_config.system

@@ -0,0 +1,18 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <memory_region name="region" size="0x1000" />
+    <io_address_space name="test_device" peripheral_id="0:3.0">
+        <iomap mr="region" iovaddr="0x80_0000_0000" />
+    </io_address_space>
+    <protection_domain name="test">
+        <program_image path="test" />
+
+        <map mr="region" vaddr="0x5_000_000" />
+
+    </protection_domain>
+</system>

tool/microkit/tests/test.rs

@@ -22,6 +22,7 @@ const DEFAULT_AARCH64_KERNEL_CONFIG: sel4::Config = sel4::Config {
     max_num_bootinfo_untypeds: 230,
     fan_out_limit: 256,
     hypervisor: true,
+    iommu: true,
     benchmark: false,
     num_cores: 1,
     fpu: true,
@@ -46,6 +47,7 @@ const DEFAULT_X86_64_KERNEL_CONFIG: sel4::Config = sel4::Config {
     max_num_bootinfo_untypeds: 230,
     fan_out_limit: 256,
     hypervisor: true,
+    iommu: true,
     benchmark: false,
     num_cores: 1,
     fpu: true,
@@ -707,6 +709,68 @@ mod protection_domain {
 mod iommu {
     use super::*;
 
+    #[test]
+    fn test_iommu_missing_from_config() {
+        check_error(
+            &sel4::Config {
+                iommu: false,
+                ..DEFAULT_X86_64_KERNEL_CONFIG
+            },
+            "iommu_missing_from_config.system",
+            "Error: io address space requires seL4 to be built with IOMMU support: ",
+        );
+    }
+
+    #[test]
+    fn test_iommu_missing_from_aarch64_config() {
+        check_error(
+            &sel4::Config {
+                iommu: false,
+                ..DEFAULT_AARCH64_KERNEL_CONFIG
+            },
+            "iommu_missing_from_config.system",
+            "Error: io address space requires seL4 to be built with IOMMU support: ",
+        );
+    }
+
+    #[test]
+    fn test_iommu_missing_from_riscv64_config() {
+        check_error(
+            &sel4::Config {
+                arch: sel4::Arch::Riscv64,
+                iommu: false,
+                ..DEFAULT_AARCH64_KERNEL_CONFIG
+            },
+            "iommu_missing_from_config.system",
+            "Error: io address space requires seL4 to be built with IOMMU support: ",
+        );
+    }
+
+    #[test]
+    fn test_iommu_unsupported_on_aarch64() {
+        check_error(
+            &sel4::Config {
+                iommu: true,
+                ..DEFAULT_AARCH64_KERNEL_CONFIG
+            },
+            "iommu_missing_from_config.system",
+            "Error: failed to parse device peripheral_id '0:3.0': IOMMU device identifiers are not supported on AArch64 on element 'io_address_space':",
+        );
+    }
+
+    #[test]
+    fn test_iommu_unsupported_on_riscv64() {
+        check_error(
+            &sel4::Config {
+                arch: sel4::Arch::Riscv64,
+                iommu: true,
+                ..DEFAULT_AARCH64_KERNEL_CONFIG
+            },
+            "iommu_missing_from_config.system",
+            "Error: failed to parse device peripheral_id '0:3.0': IOMMU device identifiers are not supported on RISC-V (64-bit) on element 'io_address_space':",
+        );
+    }
+
     #[test]
     fn test_out_of_bound() {
         check_error(