diff --git a/include/kernel/boot.h b/include/kernel/boot.h
index 08454ad94..44d7058fd 100644
--- a/include/kernel/boot.h
+++ b/include/kernel/boot.h
@@ -58,7 +58,6 @@ bool_t create_untypeds_for_region(cap_t root_cnode_cap, bool_t device_memory, re
                                   seL4_SlotPos first_untyped_slot);
 bool_t create_kernel_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg, seL4_SlotPos first_untyped_slot);
 void bi_finalise(void);
-bool_t create_irq_cnode(void);
 void create_domain_cap(cap_t root_cnode_cap);
 
 cap_t create_ipcbuf_frame(cap_t root_cnode_cap, cap_t pd_cap, vptr_t vptr);
diff --git a/include/plat/pc99/plat/machine.h b/include/plat/pc99/plat/machine.h
index 71b400438..6094c7926 100644
--- a/include/plat/pc99/plat/machine.h
+++ b/include/plat/pc99/plat/machine.h
@@ -17,6 +17,7 @@
 /* interrupt vectors (corresponds to IDT entries) */
 
 #define IRQ_INT_OFFSET 0x20
+#define IRQ_CNODE_SLOT_BITS 8
 
 typedef enum _interrupt_t {
     int_invalid                 = -1,
diff --git a/include/plat/spike/plat/machine.h b/include/plat/spike/plat/machine.h
index c1db46407..b5e4be51f 100644
--- a/include/plat/spike/plat/machine.h
+++ b/include/plat/spike/plat/machine.h
@@ -28,6 +28,7 @@ enum IRQConstants {
 } platform_interrupt_t;
 
 #define KERNEL_TIMER_IRQ INTERRUPT_TIMER
+#define IRQ_CNODE_SLOT_BITS 3
 
 enum irqNumbers {
     irqInvalid = 6
diff --git a/src/arch/arm/config.cmake b/src/arch/arm/config.cmake
index d033b2702..29e11af82 100644
--- a/src/arch/arm/config.cmake
+++ b/src/arch/arm/config.cmake
@@ -76,6 +76,18 @@ function(declare_default_headers)
         "TIMER_FREQUENCY;MAX_IRQ;INTERRUPT_CONTROLLER;TIMER;SMMU"
         ""
     )
+    # calculate the irq cnode size based on MAX_IRQ
+    set(BITS "0")
+    set(MAX "${CONFIGURE_MAX_IRQ}")
+    while(MAX GREATER "0")
+        math(EXPR BITS "${BITS} + 1")
+        math(EXPR MAX "${MAX} >> 1")
+    endwhile()
+    math(EXPR SLOTS "1 << ${BITS}")
+    if("${SLOTS}" LESS "${CONFIGURE_MAX_IRQ}")
+        math(EXPR BITS "${BITS} + 1")
+    endif()
+    set(CONFIGURE_IRQ_SLOT_BITS "${BITS}")
     # variables parsed by the above will be prepended with CONFIGURE_, so pipe them
     # straight to configure_file
     configure_file(
diff --git a/src/arch/arm/kernel/boot.c b/src/arch/arm/kernel/boot.c
index fed9cb86f..7c468ad1b 100644
--- a/src/arch/arm/kernel/boot.c
+++ b/src/arch/arm/kernel/boot.c
@@ -448,11 +448,6 @@ static BOOT_CODE bool_t try_init_kernel(
     /* create the cap for managing thread domains */
     create_domain_cap(root_cnode_cap);
 
-    /* create the IRQ CNode */
-    if (!create_irq_cnode()) {
-        return false;
-    }
-
     /* initialise the IRQ states and provide the IRQ control cap */
     init_irqs(root_cnode_cap);
 
diff --git a/src/arch/arm/platform_gen.h.in b/src/arch/arm/platform_gen.h.in
index e4b59134c..6cc74f29c 100644
--- a/src/arch/arm/platform_gen.h.in
+++ b/src/arch/arm/platform_gen.h.in
@@ -18,6 +18,7 @@ enum IRQConstants {
     maxIRQ                      = @CONFIGURE_MAX_IRQ@
 } platform_interrupt_t;
 
+#define IRQ_CNODE_SLOT_BITS (@CONFIGURE_IRQ_SLOT_BITS@)
 
 #include <@CONFIGURE_INTERRUPT_CONTROLLER@>
 #include <@CONFIGURE_TIMER@>
diff --git a/src/arch/riscv/kernel/boot.c b/src/arch/riscv/kernel/boot.c
index 40def25f9..23f7a533c 100644
--- a/src/arch/riscv/kernel/boot.c
+++ b/src/arch/riscv/kernel/boot.c
@@ -258,11 +258,6 @@ static BOOT_CODE bool_t try_init_kernel(
     /* create the cap for managing thread domains */
     create_domain_cap(root_cnode_cap);
 
-    /* create the IRQ CNode */
-    if (!create_irq_cnode()) {
-        return false;
-    }
-
     /* initialise the IRQ states and provide the IRQ control cap */
     init_irqs(root_cnode_cap);
 
diff --git a/src/arch/x86/kernel/boot.c b/src/arch/x86/kernel/boot.c
index 06c4dd5f7..c9b329b5c 100644
--- a/src/arch/x86/kernel/boot.c
+++ b/src/arch/x86/kernel/boot.c
@@ -313,11 +313,6 @@ BOOT_CODE bool_t init_sys_state(
     /* create the cap for managing thread domains */
     create_domain_cap(root_cnode_cap);
 
-    /* create the IRQ CNode */
-    if (!create_irq_cnode()) {
-        return false;
-    }
-
     /* initialise the IRQ states and provide the IRQ control cap */
     init_irqs(root_cnode_cap);
 
diff --git a/src/kernel/boot.c b/src/kernel/boot.c
index a2ec7d618..c8f434044 100644
--- a/src/kernel/boot.c
+++ b/src/kernel/boot.c
@@ -22,8 +22,6 @@
 #include <util.h>
 
 /* (node-local) state accessed only during bootstrapping */
-#define IRQ_CNODE_BITS (seL4_WordBits - clzl(maxIRQ * sizeof(cte_t)))
-
 ndks_boot_t ndks_boot BOOT_DATA;
 
 BOOT_CODE bool_t insert_region(region_t reg)
@@ -160,22 +158,6 @@ create_root_cnode(void)
     return cap;
 }
 
-
-BOOT_CODE bool_t create_irq_cnode(void)
-{
-    pptr_t pptr;
-    assert(BIT(IRQ_CNODE_BITS - seL4_SlotBits) > maxIRQ);
-    /* create an empty IRQ CNode */
-    pptr = alloc_region(IRQ_CNODE_BITS);
-    if (!pptr) {
-        printf("Kernel init failing: could not create irq cnode\n");
-        return false;
-    }
-    memzero((void *)pptr, 1 << IRQ_CNODE_BITS);
-    intStateIRQNode = (cte_t *)pptr;
-    return true;
-}
-
 /* Check domain scheduler assumptions. */
 compile_assert(num_domains_valid,
                CONFIG_NUM_DOMAINS >= 1 && CONFIG_NUM_DOMAINS <= 256)
diff --git a/src/model/statedata.c b/src/model/statedata.c
index 352a02abe..b35461dcd 100644
--- a/src/model/statedata.c
+++ b/src/model/statedata.c
@@ -56,9 +56,12 @@ UP_STATE_DEFINE(tcb_t *, ksDebugTCBs);
  * pending interrupts */
 word_t ksWorkUnitsCompleted;
 
-/* CNode containing interrupt handler endpoints */
 irq_state_t intStateIRQTable[maxIRQ + 1];
-cte_t *intStateIRQNode;
+/* CNode containing interrupt handler endpoints - like all seL4 objects, this CNode needs to be
+ * of a size that is a power of 2 and aligned to its size. */
+static cte_t intStateIRQObj[BIT(IRQ_CNODE_SLOT_BITS)] ALIGN(BIT(IRQ_CNODE_SLOT_BITS + seL4_SlotBits));
+cte_t *intStateIRQNode = intStateIRQObj;
+compile_assert(irqCNodeSize, sizeof(intStateIRQObj) >= (maxIRQ *sizeof(cte_t)));
 
 /* Currently active domain */
 dom_t ksCurDomain;