seL4_libs: skip tainted untypeds during bootstrap
Untyped slabs are marked tainted when the kerrnel uses them to back
rootserver resources. They should not be used to bootstrap dynamic
allocators because the current logic assumes untypeds provided by
the kernel are empty/unused (so mucking with them will corrupt the
rootserver's VSpace).
Change-Id: I1912131c1cc066224120f73d6abf9daed6b2ced7
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;
}
