Missing EPT misconfiguration check?

While tracking down an EPT misconfiguration bug I'm seeing in some of my
code (on real hardware), I ran the same code in bochs. I never saw the
misconfiguration occur.

Curious, I broke in to the running guest VM in bochs and saw this EPT 
configuration:

EPT PML4: 0x000000000ec7a027    E W R
EPT PDPE: 0x000000000ec79027    E W R
EPT  PDE: 0x000000000ea49067    E W R
EPT  PTE: 0x00000000075df437    E W R ignore_pat WB

The first three levels of this should be triggering misconfigurations due 
to bit 5 (0x20) being set in the PML4, PDPE, and PDE entries, and also
due to bit 6 (0x40) being set in the PDE. This is the same misconfiguration
I'm seeing on real hardware.

In bochs cpu/paging.cc, these restrictions are even called out:

//                   Format of a EPT Entry
// -----------------------------------------------------------
// 00    | Read access
// 01    | Write access
// 02    | Execute Access
// 05-03 | EPT Memory type (for leaf entries, reserved otherwise)
// 06    | Ignore PAT memory type (for leaf entries, reserved otherwise)
// 07    | Page Size, must be 1 to indicate a Large Page
// 08    | Accessed bit (if supported, ignored otherwise)
// 09    | Dirty bit (for leaf entries, if supported, ignored otherwise)
// 11-10 | (ignored)
// PA-12 | Physical address
// 51-PA | Reserved (must be zero)
// 63-52 | (ignored)
// -----------------------------------------------------------

It does appear that bochs is checking the 51-PA range, as well as ensuring
if bit 7 is set properly (it's only supported in certain levels).

It looks like bochs needs the following check as well? Does this make sense?

-ml


Index: cpu/paging.cc
===================================================================
--- cpu/paging.cc	(revision 12984)
+++ cpu/paging.cc	(working copy)
@@ -1805,6 +1805,12 @@
 
     if (leaf == BX_LEVEL_PTE) break;
 
+    if (curr_entry & 0x60) {
+      BX_DEBUG(("EPT %s: reserved bit is set 0x" FMT_ADDRX64, bx_paging_level[leaf], curr_entry));
+      vmexit_reason = VMX_VMEXIT_EPT_MISCONFIGURATION;
+      break;
+    }
+
     if (curr_entry & 0x80) {
       if (leaf > (BX_LEVEL_PDE + !!is_cpu_extension_supported(BX_ISA_1G_PAGES))) {
         BX_DEBUG(("EPT %s: PS bit set !", bx_paging_level[leaf]));

------------------------------------------------------------------------------
Developer Access Program for Intel Xeon Phi Processors
Access to Intel Xeon Phi processor-based developer platforms.
With one year of Intel Parallel Studio XE.
Training and support from Colfax.
Order your platform today.http://sdm.link/xeonphi