diff --git a/hermit/arch/x86/kernel/processor.c b/hermit/arch/x86/kernel/processor.c
index 91d60011c..6c9f29712 100644
--- a/hermit/arch/x86/kernel/processor.c
+++ b/hermit/arch/x86/kernel/processor.c
@@ -273,6 +273,8 @@ int cpu_detection(void) {
 		cr4 |= CR4_PGE;
 	if (has_fsgsbase())
 		cr4 |= CR4_FSGSBASE;
+	if (has_vmx())
+		cr4 |= CR4_VMXE;
 	cr4 &= ~CR4_TSD;		// => every privilege level is able to use rdtsc
 	write_cr4(cr4);