diff --git a/libsel4simple-default/src/libsel4simple-default.c b/libsel4simple-default/src/libsel4simple-default.c
index 46cd31469..d12246a1d 100644
--- a/libsel4simple-default/src/libsel4simple-default.c
+++ b/libsel4simple-default/src/libsel4simple-default.c
@@ -100,6 +100,19 @@ seL4_CPtr simple_default_nth_cap(void *data, int n)
         if (true_return >= seL4_CapIOSpace) {
             true_return++;
         }
+#endif
+#ifndef CONFIG_ARM_SMMU
+        /* skip seL4_CapSMMUSIDControl and seL4_CapSMMUCBControl if
+         * SMMU is not supported on this platform */
+        if (true_return >= seL4_CapSMMUSIDControl) {
+            true_return += 2;
+        }
+#endif
+#ifndef CONFIG_KERNEL_MCS
+        /* skip seL4_CapInitThreadSC if MCS is not enabled */
+        if (true_return >= seL4_CapInitThreadSC) {
+            true_return++;
+        }
 #endif
     } else if (n < shared_frame_range) {
         return bi->sharedFrames.start + (n - SIMPLE_NUM_INIT_CAPS);
diff --git a/libsel4simple/arch_include/arm/simple/arch/simple.h b/libsel4simple/arch_include/arm/simple/arch/simple.h
index dac7eb128..574e54cfd 100644
--- a/libsel4simple/arch_include/arm/simple/arch/simple.h
+++ b/libsel4simple/arch_include/arm/simple/arch/simple.h
@@ -16,7 +16,19 @@
 
 /* Simple does not address initial null caps, including seL4_CapNull.
  * seL4_CapIOSpace, seL4_CapIOPortControl are null on architectures other than x86 */
-#define SIMPLE_SKIPPED_INIT_CAPS 3
+#ifdef CONFIG_KERNEL_MCS
+#define SIMPLE_SKIP_THREADSC 0
+#else
+#define SIMPLE_SKIP_THREADSC 1
+#endif
+
+#ifdef CONFIG_ARM_SMMU
+#define SIMPLE_SKIP_SMMU_CAPS 0
+#else
+#define SIMPLE_SKIP_SMMU_CAPS 2
+#endif
+
+#define SIMPLE_SKIPPED_INIT_CAPS (3 + SIMPLE_SKIP_THREADSC + SIMPLE_SKIP_SMMU_CAPS)
 
 /* Request a cap to a specific IRQ number on the system
  *
diff --git a/libsel4simple/arch_include/x86/simple/arch/simple.h b/libsel4simple/arch_include/x86/simple/arch/simple.h
index b1d396ebd..6ae8ee0bd 100644
--- a/libsel4simple/arch_include/x86/simple/arch/simple.h
+++ b/libsel4simple/arch_include/x86/simple/arch/simple.h
@@ -14,14 +14,23 @@
 #include <utils/util.h>
 #include <vka/cspacepath_t.h>
 
-/* Simple does not address initial null caps, including seL4_CapNull */
+/* Simple does not address initial null caps, including seL4_CapNull
+ * seL4_CapSMMUSIDControl, seL4_CapSMMUCBControl are null on x86 */
 #ifdef CONFIG_IOMMU
-#define SIMPLE_SKIPPED_INIT_CAPS 1
+#define SIMPLE_SKIP_IOSPACE 0
 #else
 /* seL4_CapIOSpace is null if IOMMU isn't supported */
-#define SIMPLE_SKIPPED_INIT_CAPS 2
+#define SIMPLE_SKIP_IOSPACE 1
 #endif
 
+#ifdef CONFIG_KERNEL_MCS
+#define SIMPLE_SKIP_THREADSC 0
+#else
+#define SIMPLE_SKIP_THREADSC 1
+#endif
+
+#define SIMPLE_SKIPPED_INIT_CAPS (3 + SIMPLE_SKIP_IOSPACE + SIMPLE_SKIP_THREADSC)
+
 /**
  * Request a cap to the IOPorts
  *