diff --git a/libsel4utils/src/vspace/vspace.c b/libsel4utils/src/vspace/vspace.c
index 0e12f76..bd08df7 100644
--- a/libsel4utils/src/vspace/vspace.c
+++ b/libsel4utils/src/vspace/vspace.c
@@ -26,6 +26,149 @@
 
 #include <utils/util.h>
 
+
+// Static pool, set size of items in static pool
+// #define MEMPOOL_USE_STATIC      64
+
+// Use malloc for dynamic pool
+// #define MEMPOOL_USE_MALLOC
+
+// Use vspace to dynamically map a page
+#define MEMPOOL_USE_VSPACE
+
+
+// ----------------------------------------------------------------------------
+#if defined(MEMPOOL_USE_VSPACE)
+#define MEMPOOL_SLOT_PER_PAGE      ((PAGE_SIZE_4K / (sizeof(sel4utils_res_t) + 1)) - 1)
+
+struct MempoolRecord {
+    sel4utils_res_t       slot[MEMPOOL_SLOT_PER_PAGE];
+    char                  busy[MEMPOOL_SLOT_PER_PAGE];
+    size_t                load;     // 0.. MEMPOOL_SLOT_PER_PAGE-1
+    struct MempoolRecord *next;
+};
+
+struct MempoolRecord *_mempoolHead;
+
+static void * mempool_new_pages(vspace_t *vspace, seL4_CapRights_t rights, size_t num_pages, size_t size_bits) {
+    void *vaddr;
+
+    sel4utils_res_t reservation;
+    reservation_t res = {&reservation};
+
+    if (sel4utils_reserve_range_no_alloc_aligned(vspace, 
+                &reservation,
+                num_pages * SIZE_BITS_TO_BYTES(size_bits), 
+                size_bits,
+                rights, 
+                false /* cacheable */, 
+                &vaddr)) {
+        ZF_LOGE("Failed to reserve range");
+        return NULL;
+    }
+
+    UNUSED int error = sel4utils_new_pages_at_vaddr(vspace, vaddr, num_pages, size_bits, res);
+
+    sel4utils_free_reservation(vspace, res);
+
+    if (error) {
+        ZF_LOGE("Error creating new pages, bailing: %d", error);
+        return NULL;
+    }
+
+    return vaddr;
+}
+
+static sel4utils_res_t * mempool_malloc(UNUSED vspace_t *vspace) {
+    int i;
+    struct MempoolRecord *record;
+    if (!_mempoolHead) {
+        _mempoolHead = (struct MempoolRecord *)mempool_new_pages(vspace, seL4_AllRights, 1, PAGE_BITS_4K);
+        if (!_mempoolHead) {
+            return NULL;
+        }
+        // create_level already set the area to zero, no need to initialize
+    }
+    for (record = _mempoolHead; record; record = record->next) {
+        if (record->load < MEMPOOL_SLOT_PER_PAGE) {
+            break;
+        }
+    }
+    if (record->load == MEMPOOL_SLOT_PER_PAGE) {
+        // List is full, expand
+        record->next = (struct MempoolRecord *)mempool_new_pages(vspace, seL4_AllRights, 1, PAGE_BITS_4K);
+        if (!record->next) {
+            // Failed
+            return NULL;
+        }
+        record = record->next;
+    }
+    // Search inside record
+    for (i = 0; i < MEMPOOL_SLOT_PER_PAGE; ++i) {
+        if (!record->busy[i]) {
+            record->busy[i] = 1;
+            ++record->load;
+            return &record->slot[i];
+        }
+    }
+    ZF_LOGF("Found no empty slots");
+}
+
+static void mempool_free(void *ptr) {
+    int i;
+    struct MempoolRecord *record;
+    for (record = _mempoolHead; record; record = record->next) {
+        for (i = 0; i < MEMPOOL_SLOT_PER_PAGE; ++i) {
+            if (&record->slot[i] == ptr) {
+                record->busy[i] = 0;
+                --record->load;
+                return;
+            }
+        }
+    }
+    ZF_LOGF("Found no matching entry");
+}
+
+
+
+// ----------------------------------------------------------------------------
+#elif defined(MEMPOOL_USE_STATIC)
+static sel4utils_res_t _mempool[MEMPOOL_USE_STATIC];
+static int             _mempoolBusy[MEMPOOL_USE_STATIC];
+
+static sel4utils_res_t * mempool_malloc(UNUSED vspace_t *vspace) {
+    int i;
+    for (i = 0; i < MEMPOOL_USE_STATIC; ++i) {
+        if (!_mempoolBusy[i]) {
+            _mempoolBusy[i] = 1;
+            return &_mempool[i];
+        }
+    }
+    // OUT OF MEMORY
+    ZF_LOGW("Out of static pool, using malloc");
+    return (sel4utils_res_t *)malloc(sizeof(sel4utils_res_t));
+}
+
+static void mempool_free(void *ptr) {
+    int i;
+    for (i = 0; i < MEMPOOL_USE_STATIC; ++i) {
+        if (&_mempool[i] == ptr) {
+            _mempoolBusy[i] = 0;
+            return;
+        }
+    }
+    // Not found, free
+    free(ptr);
+}
+
+// ----------------------------------------------------------------------------
+#elif defined(MEMPOOL_USE_MALLOC)
+#define mempool_malloc(vspace)    ((sel4utils_res_t *)malloc(sizeof(sel4utils_res_t)))
+#define mempool_free(ptr)   free(ptr)
+
+#endif
+
+
 void *
 create_level(vspace_t *vspace, size_t size)
 {
@@ -496,7 +639,7 @@ sel4utils_reserve_range_aligned(vspace_t *vspace, size_t bytes, size_t size_bits
         return reservation;
     }
 
-    sel4utils_res_t *res = malloc(sizeof(sel4utils_res_t));
+    sel4utils_res_t *res = mempool_malloc(vspace);
 
     if (res == NULL) {
         ZF_LOGE("Malloc failed");
@@ -507,7 +650,7 @@ sel4utils_reserve_range_aligned(vspace_t *vspace, size_t bytes, size_t size_bits
 
     int error = sel4utils_reserve_range_no_alloc_aligned(vspace, res, bytes, size_bits, rights, cacheable, result);
     if (error) {
-        free(reservation.res);
+        mempool_free(reservation.res);
         reservation.res = NULL;
     }
 
@@ -533,7 +676,7 @@ sel4utils_reserve_range_at(vspace_t *vspace, void *vaddr, size_t size, seL4_CapR
                            rights, int cacheable)
 {
     reservation_t reservation;
-    reservation.res = malloc(sizeof(sel4utils_res_t));
+    reservation.res = mempool_malloc(vspace);
 
     if (reservation.res == NULL) {
         ZF_LOGE("Malloc failed");
@@ -543,7 +686,7 @@ sel4utils_reserve_range_at(vspace_t *vspace, void *vaddr, size_t size, seL4_CapR
     int error = sel4utils_reserve_range_at_no_alloc(vspace, reservation.res, vaddr, size, rights, cacheable);
 
     if (error) {
-        free(reservation.res);
+        mempool_free(reservation.res);
         reservation.res = NULL;
     } else {
         ((sel4utils_res_t *)reservation.res)->malloced = 1;
@@ -561,7 +704,7 @@ sel4utils_free_reservation(vspace_t *vspace, reservation_t reservation)
     clear_entries_range(vspace, res->start, res->end, true);
     remove_reservation(data, res);
     if (res->malloced) {
-        free(reservation.res);
+        mempool_free(reservation.res);
     }
 }