--- src/kernel/sel4/src/arch/x86/object/vcpu.c
+++ src/kernel/sel4/src/arch/x86/object/vcpu.c
@@ -713,6 +727,7 @@ static exception_t decodeWriteVMCS(cap_t cap, word_t length, word_t *buffer)
     case VMX_CONTROL_EXCEPTION_BITMAP:
     case VMX_CONTROL_ENTRY_INTERRUPTION_INFO:
     case VMX_CONTROL_ENTRY_EXCEPTION_ERROR_CODE:
+    case VMX_CONTROL_ENTRY_INSTRUCTION_LENGTH:
         break;
     case VMX_CONTROL_PIN_EXECUTION_CONTROLS:
         value = applyFixedBits(value, pin_control_high, pin_control_low);
@@ -860,6 +875,7 @@ static exception_t decodeReadVMCS(cap_t cap, word_t length, word_t *buffer)
     case VMX_GUEST_CR0:
     case VMX_GUEST_CR3:
     case VMX_GUEST_CR4:
+    case VMX_CONTROL_ENTRY_EXCEPTION_ERROR_CODE:
         break;
     default:
         userError("VCPU ReadVMCS: Invalid field %lx.", (long)field);