Bug detected by Genode and patch provided by Anna Lyons:
http://sel4.systems/pipermail/devel/2018-September/002161.html
--- src/kernel/sel4/src/arch/x86/c_traps.c
+++ src/kernel/sel4/src/arch/x86/c_traps.c
@@ -111,7 +111,7 @@ slowpath(syscall_t syscall)
 {
 
 #ifdef CONFIG_VTX
-    if (syscall == SysVMEnter) {
+    if (syscall == SysVMEnter && NODE_STATE(ksCurThread)->tcbArch.tcbVCPU) {
         vcpu_update_state_sysvmenter(NODE_STATE(ksCurThread)->tcbArch.tcbVCPU);
         if (NODE_STATE(ksCurThread)->tcbBoundNotification && notification_ptr_get_state(NODE_STATE(ksCurThread)->tcbBoundNotification) == NtfnState_Active) {
             completeSignal(NODE_STATE(ksCurThread)->tcbBoundNotification, NODE_STATE(ksCurThread));