diff --git a/libsel4allocman/src/bootstrap.c b/libsel4allocman/src/bootstrap.c
index 0a85761..19ada80 100644
--- a/libsel4allocman/src/bootstrap.c
+++ b/libsel4allocman/src/bootstrap.c
@@ -218,6 +218,10 @@
     }
     for (i = bi->untyped.start; i < bi->untyped.end; i++) {
         size_t index = i - bi->untyped.start;
+        if (bi->untypedList[index].isTainted) {
+            ZF_LOGD("Skip tainted UT slab %ld\n", (unsigned long)index);
+            continue;
+        }
         cspacepath_t slot = bs->boot_cspace.make_path(bs->boot_cspace.cspace, i);
         size_t size_bits = bi->untypedList[index].sizeBits;
         uintptr_t paddr = bi->untypedList[index].paddr;
@@ -243,8 +247,13 @@
         size_t size_bits;
         uintptr_t paddr;
         bool device;
+        bool isTainted;
         cspacepath_t slot = bs->boot_cspace.make_path(bs->boot_cspace.cspace,
-                                                      simple_get_nth_untyped(simple, i, &size_bits, &paddr, &device));
+                                                      simple_get_nth_untyped(simple, i, &size_bits, &paddr, &device, &isTainted));
+        if (isTainted) {
+            ZF_LOGD("Skip tainted UT slab %ld\n", (unsigned long)i);
+            continue;
+        }
         error = _add_ut(bs, slot, size_bits, paddr, device);
         if (error) {
             return error;
@@ -1124,8 +1133,13 @@
         size_t size_bits;
         uintptr_t paddr;
         bool device;
-        cspacepath_t path = allocman_cspace_make_path(alloc, simple_get_nth_untyped(simple, i, &size_bits, &paddr, &device));
+        bool isTainted;
+        cspacepath_t path = allocman_cspace_make_path(alloc, simple_get_nth_untyped(simple, i, &size_bits, &paddr, &device, &isTainted));
         int dev_type = device ? ALLOCMAN_UT_DEV : ALLOCMAN_UT_KERNEL;
+        if (isTainted) {
+            ZF_LOGD("Skip tainted slab %ld\n", (unsigned long)i);
+            continue;
+        }
         // If it is regular UT memory, then we add cap and move on.
         if (dev_type == ALLOCMAN_UT_KERNEL) {
             error = allocman_utspace_add_uts(alloc, 1, &path, &size_bits, &paddr, dev_type);
@@ -1232,6 +1246,10 @@
         cspacepath_t slot;
         size_t size_bits;
         uintptr_t paddr;
+        if (bi->untypedList[index].isTainted) {
+            ZF_LOGD("Skip tainted slab %ld\n", (unsigned long)index);
+            continue;
+        }
         slot = allocman_cspace_make_path(alloc, i);
         size_bits = bi->untypedList[index].sizeBits;
         paddr = bi->untypedList[index].paddr;
diff --git a/libsel4debug/src/bootinfo.c b/libsel4debug/src/bootinfo.c
index 44e01f3..a47b9d7 100644
--- a/libsel4debug/src/bootinfo.c
+++ b/libsel4debug/src/bootinfo.c
@@ -33,15 +33,15 @@
     printf("Initial thread cnode size: %u\n", (int)info->initThreadCNodeSizeBits);
     printf("List of untypeds\n");
     printf("------------------\n");
-    printf("Paddr    | Size   | Device\n");
+    printf("Paddr    | Size   | Tainted | Device\n");
 
     int sizes[CONFIG_WORD_SIZE] = {0};
     for (int i = 0; i < CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS && i < (info->untyped.end - info->untyped.start); i++) {
         int index = info->untypedList[i].sizeBits;
         assert(index < ARRAY_SIZE(sizes));
         sizes[index]++;
-        printf("%p | %zu | %d\n", (void *)info->untypedList[i].paddr, (size_t)info->untypedList[i].sizeBits,
-               (int)info->untypedList[i].isDevice);
+        printf("%p | %zu | %d | %d\n", (void *)info->untypedList[i].paddr, (size_t)info->untypedList[i].sizeBits,
+               (int)info->untypedList[i].isTainted, (int)info->untypedList[i].isDevice);
     }
 
     printf("Untyped summary\n");
diff --git a/libsel4simple-default/src/libsel4simple-default.c b/libsel4simple-default/src/libsel4simple-default.c
index 946b734..9e13fb8 100644
--- a/libsel4simple-default/src/libsel4simple-default.c
+++ b/libsel4simple-default/src/libsel4simple-default.c
@@ -139,7 +139,7 @@
     return ((seL4_BootInfo *)data)->untyped.end - ((seL4_BootInfo *)data)->untyped.start;
 }
 
-seL4_CPtr simple_default_nth_untyped(void *data, int n, size_t *size_bits, uintptr_t *paddr, bool *device)
+seL4_CPtr simple_default_nth_untyped(void *data, int n, size_t *size_bits, uintptr_t *paddr, bool *device, bool *isTainted)
 {
     assert(data);
 
@@ -155,6 +155,9 @@
         if (device != NULL) {
             *device = (bool)bi->untypedList[n].isDevice;
         }
+        if (isTainted != NULL) {
+            *isTainted = (bool)bi->untypedList[n].isTainted;
+        }
         return bi->untyped.start + (n);
     }
 
diff --git a/libsel4simple/include/simple/simple.h b/libsel4simple/include/simple/simple.h
index 11ed8a0..e42b567 100644
--- a/libsel4simple/include/simple/simple.h
+++ b/libsel4simple/include/simple/simple.h
@@ -141,7 +141,7 @@
  * @param the physical address of the returned cap
 */
 
-typedef seL4_CPtr(*simple_get_nth_untyped_fn)(void *data, int n, size_t *size_bits, uintptr_t *paddr, bool *device);
+typedef seL4_CPtr(*simple_get_nth_untyped_fn)(void *data, int n, size_t *size_bits, uintptr_t *paddr, bool *device, bool *isTainted);
 
 /**
  * Get the amount of user image caps available
@@ -445,7 +445,7 @@
 }
 
 static inline seL4_CPtr simple_get_nth_untyped(simple_t *simple, int n, size_t *size_bits, uintptr_t *paddr,
-                                               bool *device)
+                                               bool *device, bool *isTainted)
 {
     if (!simple) {
         ZF_LOGE("Simple is NULL");
@@ -456,7 +456,7 @@
         return seL4_CapNull;
     }
 
-    return simple->nth_untyped(simple->data, n, size_bits, paddr, device);
+    return simple->nth_untyped(simple->data, n, size_bits, paddr, device, isTainted);
 }
 
 static inline int simple_get_userimage_count(simple_t *simple)
diff --git a/libsel4simple/src/simple.c b/libsel4simple/src/simple.c
index 882b1cd..c901810 100644
--- a/libsel4simple/src/simple.c
+++ b/libsel4simple/src/simple.c
@@ -17,7 +17,7 @@
     int i;
 
     for (i = 0; i < simple_get_untyped_count(simple); i++) {
-        seL4_CPtr ut_pos = simple_get_nth_untyped(simple, i, NULL, NULL, NULL);
+        seL4_CPtr ut_pos = simple_get_nth_untyped(simple, i, NULL, NULL, NULL, NULL);
         if (ut_pos == pos) {
             return true;
         }