diff --git a/include/object/tcb.h b/include/object/tcb.h
index 3ad0c8bf7..8ada294ba 100644
--- a/include/object/tcb.h
+++ b/include/object/tcb.h
@@ -182,6 +182,8 @@ static inline tcb_queue_t tcbAppend(tcb_t *tcb, tcb_queue_t queue)
     return new_queue;
 }
 
+/* Check for NullCap or EndpointCap with sufficient access rights */
+bool_t validFaultHandler(cap_t cap);
 #else
 
 tcb_queue_t tcbEPAppend(tcb_t *tcb, tcb_queue_t queue);
diff --git a/src/object/tcb.c b/src/object/tcb.c
index 8590c6fa0..521e33bd6 100644
--- a/src/object/tcb.c
+++ b/src/object/tcb.c
@@ -1078,7 +1078,7 @@ exception_t decodeWriteRegisters(cap_t cap, word_t length, word_t *buffer)
 }
 
 #ifdef CONFIG_KERNEL_MCS
-static bool_t validFaultHandler(cap_t cap)
+bool_t validFaultHandler(cap_t cap)
 {
     switch (cap_get_capType(cap)) {
     case cap_endpoint_cap: