Index: trunk/src/VBox/VMM/VMMAll/PGMAllGst.h
===================================================================
--- trunk/src/VBox/VMM/VMMAll/PGMAllGst.h	(revision 92310)
+++ trunk/src/VBox/VMM/VMMAll/PGMAllGst.h	(revision 92311)
@@ -149,5 +149,5 @@
 # endif
 
-    uint64_t fEffective = X86_PTE_RW | X86_PTE_US | X86_PTE_PWT | X86_PTE_PCD | X86_PTE_A | 1;
+    uint64_t fEffective = X86_PTE_RW | X86_PTE_US | X86_PTE_PWT | X86_PTE_PCD | X86_PTE_A | 1;  /** @todo can this default assignment be removed? */
     {
 # if PGM_GST_TYPE == PGM_TYPE_AMD64
@@ -170,6 +170,6 @@
         else return PGM_GST_NAME(WalkReturnRsvdError)(pVCpu, pWalk, 4);
 
-        pWalk->Core.fEffective = fEffective = (Pml4e.u & (X86_PML4E_RW | X86_PML4E_US | X86_PML4E_PWT | X86_PML4E_PCD | X86_PML4E_A))
-                                            | ((Pml4e.u >> 63) ^ 1) /*NX */;
+        pWalk->Core.fEffective = fEffective = Pml4e.u & (  X86_PML4E_RW  | X86_PML4E_US | X86_PML4E_PWT
+                                                         | X86_PML4E_PCD | X86_PML4E_A  | X86_PML4E_NX);
 
         /*
@@ -205,9 +205,9 @@
 # if PGM_GST_TYPE == PGM_TYPE_AMD64
         pWalk->Core.fEffective = fEffective &= (Pdpe.u & (X86_PDPE_RW | X86_PDPE_US | X86_PDPE_PWT | X86_PDPE_PCD | X86_PDPE_A))
-                                             | ((Pdpe.u >> 63) ^ 1) /*NX */;
-# else
+                                             | (Pdpe.u & X86_PDPE_LM_NX);
+# else
+        /* NX in the legacy-mode PAE PDPE is reserved. The valid check above ensures the NX bit is not set. */
         pWalk->Core.fEffective = fEffective  = X86_PDPE_RW  | X86_PDPE_US | X86_PDPE_A
-                                             | (Pdpe.u & (X86_PDPE_PWT | X86_PDPE_PCD))
-                                             | ((Pdpe.u >> 63) ^ 1) /*NX */;
+                                             | (Pdpe.u & (X86_PDPE_PWT | X86_PDPE_PCD));
 # endif
 
@@ -248,5 +248,5 @@
 # else
             fEffective &= (Pde.u & (X86_PDE4M_RW | X86_PDE4M_US | X86_PDE4M_PWT | X86_PDE4M_PCD | X86_PDE4M_A))
-                        | ((Pde.u >> 63) ^ 1) /*NX */;
+                        | (Pde.u & X86_PDE2M_PAE_NX);
 # endif
             fEffective |= Pde.u & (X86_PDE4M_D | X86_PDE4M_G);
@@ -257,5 +257,5 @@
             pWalk->Core.fEffectiveUS = !!(fEffective & X86_PTE_US);
 # if PGM_GST_TYPE == PGM_TYPE_AMD64 || PGM_GST_TYPE == PGM_TYPE_PAE
-            pWalk->Core.fEffectiveNX = !(fEffective & 1) && GST_IS_NX_ACTIVE(pVCpu);
+            pWalk->Core.fEffectiveNX = (fEffective & X86_PTE_PAE_NX) && GST_IS_NX_ACTIVE(pVCpu);
 # else
             pWalk->Core.fEffectiveNX = false;
@@ -280,5 +280,5 @@
 # else
         pWalk->Core.fEffective = fEffective &= (Pde.u & (X86_PDE_RW | X86_PDE_US | X86_PDE_PWT | X86_PDE_PCD | X86_PDE_A))
-                                             | ((Pde.u >> 63) ^ 1) /*NX */;
+                                             | (Pde.u & X86_PDE_PAE_NX);
 # endif
 
@@ -313,5 +313,5 @@
 # else
         fEffective &= (Pte.u & (X86_PTE_RW | X86_PTE_US | X86_PTE_PWT | X86_PTE_PCD | X86_PTE_A))
-                   |  ((Pte.u >> 63) ^ 1) /*NX */;
+                   |  (Pte.u & X86_PTE_PAE_NX);
 # endif
         fEffective |= Pte.u & (X86_PTE_D | X86_PTE_PAT | X86_PTE_G);
@@ -321,5 +321,5 @@
         pWalk->Core.fEffectiveUS = !!(fEffective & X86_PTE_US);
 # if PGM_GST_TYPE == PGM_TYPE_AMD64 || PGM_GST_TYPE == PGM_TYPE_PAE
-        pWalk->Core.fEffectiveNX = !(fEffective & 1) && GST_IS_NX_ACTIVE(pVCpu);
+        pWalk->Core.fEffectiveNX = (fEffective & X86_PTE_PAE_NX) && GST_IS_NX_ACTIVE(pVCpu);
 # else
         pWalk->Core.fEffectiveNX = false;
@@ -327,5 +327,5 @@
         pWalk->Core.fSucceeded   = true;
 
-        RTGCPHYS GCPhysPte = GST_GET_PDE_GCPHYS(Pte)        /** @todo This should be GST_GET_PTE_GCPHYS. */
+        RTGCPHYS GCPhysPte = GST_GET_PTE_GCPHYS(Pte)
                            | (GCPtr & PAGE_OFFSET_MASK);
 # ifdef VBOX_WITH_NESTED_HWVIRT_VMX_EPT
@@ -387,5 +387,5 @@
                                                 | PGM_PTATTRS_US_MASK))
 # if PGM_WITH_NX(PGM_GST_TYPE, PGM_GST_TYPE)
-                     | ((RT_BF_GET(Walk.Core.fEffective, PGM_PTATTRS_X) ^ 1) << X86_PTE_PAE_BIT_NX)
+                     | (Walk.Core.fEffective & PGM_PTATTRS_NX_MASK)
 # endif
                      ;
@@ -397,5 +397,5 @@
                                                 | PGM_PTATTRS_PAT_MASK))
 # if PGM_WITH_NX(PGM_GST_TYPE, PGM_GST_TYPE)
-                     | ((RT_BF_GET(Walk.Core.fEffective, PGM_PTATTRS_X) ^ 1) << X86_PTE_PAE_BIT_NX)
+                     | (Walk.Core.fEffective & PGM_PTATTRS_NX_MASK)
 # endif
                      ;
Index: trunk/src/VBox/VMM/VMMAll/PGMAllGstSlatEpt.cpp.h
===================================================================
--- trunk/src/VBox/VMM/VMMAll/PGMAllGstSlatEpt.cpp.h	(revision 92310)
+++ trunk/src/VBox/VMM/VMMAll/PGMAllGstSlatEpt.cpp.h	(revision 92311)
@@ -47,4 +47,7 @@
                                             PGSTPTWALK pWalk)
 {
+    /*
+     * Init walk structure.
+     */
     int rc;
     RT_ZERO(*pWalk);
@@ -54,4 +57,27 @@
     pWalk->Core.fIsLinearAddrValid = fIsLinearAddrValid;
 
+    /*
+     * Figure out EPT attributes that are cumulative (logical-AND) across page walks.
+     *   - R, W, X_SUPER are unconditionally cumulative.
+     *     See Intel spec. Table 26-7 "Exit Qualification for EPT Violations".
+     *
+     *   - X_USER is Cumulative but relevant only when mode-based execute control for EPT
+     *     which we currently don't support it (asserted below).
+     *
+     *   - MEMTYPE is not cumulative and only applicable to the final paging entry.
+     *
+     *   - A, D EPT bits map to the regular page-table bit positions. Thus, they're not
+     *     included in the mask below and handled separately. Accessed bits are
+     *     cumulative but dirty bits are not cumulative as they're only applicable to
+     *     the final paging entry.
+     */
+    Assert(!pVCpu->CTX_SUFF(pVM)->cpum.ro.GuestFeatures.fVmxModeBasedExecuteEpt);
+    uint64_t const fCumulativeEpt = PGM_PTATTRS_EPT_R_MASK
+                                  | PGM_PTATTRS_EPT_W_MASK
+                                  | PGM_PTATTRS_EPT_X_SUPER_MASK;
+
+    /*
+     * Do the walk.
+     */
     uint64_t fEffective;
     {
@@ -73,14 +99,9 @@
         Assert(!pVCpu->CTX_SUFF(pVM)->cpum.ro.GuestFeatures.fVmxModeBasedExecuteEpt);
         uint64_t const fEptAttrs     = Pml4e.u & EPT_PML4E_ATTR_MASK;
-        uint8_t const fExecute       = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_EXECUTE);
-        uint8_t const fRead          = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_READ);
-        uint8_t const fWrite         = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_WRITE);
         uint8_t const fAccessed      = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_ACCESSED);
         uint64_t const fEffectiveEpt = (fEptAttrs << PGM_PTATTRS_EPT_SHIFT) & PGM_PTATTRS_EPT_MASK;
-        pWalk->Core.fEffective = fEffective = RT_BF_MAKE(PGM_PTATTRS_X,  fExecute)
-                                            | RT_BF_MAKE(PGM_PTATTRS_RW, fRead & fWrite)
-                                            | RT_BF_MAKE(PGM_PTATTRS_US, 1)
-                                            | RT_BF_MAKE(PGM_PTATTRS_A,  fAccessed)
-                                            | fEffectiveEpt;
+        fEffective = RT_BF_MAKE(PGM_PTATTRS_A, fAccessed)
+                   | fEffectiveEpt;
+        pWalk->Core.fEffective = fEffective;
 
         rc = PGM_GCPHYS_2_PTR_BY_VMCPU(pVCpu, Pml4e.u & EPT_PML4E_PG_MASK, &pWalk->pPdpt);
@@ -100,33 +121,27 @@
         if (GST_IS_PDPE_VALID(pVCpu, Pdpte))
         {
-            uint64_t const fEptAttrs = Pdpte.u & EPT_PDPTE_ATTR_MASK;
-            uint8_t const fExecute   = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_EXECUTE);
-            uint8_t const fWrite     = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_WRITE);
-            uint8_t const fAccessed  = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_ACCESSED);
+            uint64_t const fEptAttrs     = Pdpte.u & EPT_PDPTE_ATTR_MASK;
+            uint8_t const  fAccessed     = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_ACCESSED);
             uint64_t const fEffectiveEpt = (fEptAttrs << PGM_PTATTRS_EPT_SHIFT) & PGM_PTATTRS_EPT_MASK;
-            pWalk->Core.fEffective = fEffective &= RT_BF_MAKE(PGM_PTATTRS_X,  fExecute)
-                                                 | RT_BF_MAKE(PGM_PTATTRS_RW, fWrite)
-                                                 | RT_BF_MAKE(PGM_PTATTRS_US, 1)
-                                                 | RT_BF_MAKE(PGM_PTATTRS_A,  fAccessed)
-                                                 | fEffectiveEpt;
+            fEffective &= RT_BF_MAKE(PGM_PTATTRS_A, fAccessed)
+                       |  (fEffectiveEpt & fCumulativeEpt);
+            pWalk->Core.fEffective = fEffective;
         }
         else if (GST_IS_BIG_PDPE_VALID(pVCpu, Pdpte))
         {
-            uint64_t const fEptAttrs  = Pdpte.u & EPT_PDPTE1G_ATTR_MASK;
-            uint8_t const fExecute    = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_EXECUTE);
-            uint8_t const fWrite      = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_WRITE);
-            uint8_t const fAccessed   = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_ACCESSED);
-            uint8_t const fDirty      = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_DIRTY);
+            uint64_t const fEptAttrs     = Pdpte.u & EPT_PDPTE1G_ATTR_MASK;
+            uint8_t const fAccessed      = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_ACCESSED);
+            uint8_t const fDirty         = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_DIRTY);
+            uint8_t const fMemType       = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_MEMTYPE);
             uint64_t const fEffectiveEpt = (fEptAttrs << PGM_PTATTRS_EPT_SHIFT) & PGM_PTATTRS_EPT_MASK;
-            pWalk->Core.fEffective = fEffective &= RT_BF_MAKE(PGM_PTATTRS_X,           fExecute)
-                                                 | RT_BF_MAKE(PGM_PTATTRS_RW,          fWrite)
-                                                 | RT_BF_MAKE(PGM_PTATTRS_US,          1)
-                                                 | RT_BF_MAKE(PGM_PTATTRS_A,           fAccessed)
-                                                 | RT_BF_MAKE(PGM_PTATTRS_D,           fDirty)
-                                                 | RT_BF_MAKE(PGM_PTATTRS_EPT_MEMTYPE, 0)
-                                                 | fEffectiveEpt;
-            pWalk->Core.fEffectiveRW = !!(fEffective & X86_PTE_RW);
+            fEffective &= RT_BF_MAKE(PGM_PTATTRS_A,           fAccessed)
+                       |  (fEffectiveEpt & fCumulativeEpt);
+            fEffective |= RT_BF_MAKE(PGM_PTATTRS_D,           fDirty)
+                       |  RT_BF_MAKE(PGM_PTATTRS_EPT_MEMTYPE, fMemType);
+            pWalk->Core.fEffective = fEffective;
+
+            pWalk->Core.fEffectiveRW = !!(fEffective & PGM_PTATTRS_RW_MASK);    /** @todo RW isn't copied from EPT R, W. This will break callers who use RW for EPT attributes. */
             pWalk->Core.fEffectiveUS = true;
-            pWalk->Core.fEffectiveNX = !fExecute;
+            pWalk->Core.fEffectiveNX = !(fEffective & PGM_PTATTRS_EPT_X_SUPER_MASK);
             pWalk->Core.fGigantPage  = true;
             pWalk->Core.fSucceeded   = true;
@@ -150,20 +165,18 @@
             else return PGM_GST_SLAT_NAME_EPT(WalkReturnRsvdError)(pVCpu, pWalk, 2);
 
-            uint64_t const fEptAttrs  = Pde.u & EPT_PDE2M_ATTR_MASK;
-            uint8_t const fExecute    = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_EXECUTE);
-            uint8_t const fWrite      = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_WRITE);
-            uint8_t const fAccessed   = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_ACCESSED);
-            uint8_t const fDirty      = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_DIRTY);
+            uint64_t const fEptAttrs     = Pde.u & EPT_PDE2M_ATTR_MASK;
+            uint8_t const fAccessed      = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_ACCESSED);
+            uint8_t const fDirty         = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_DIRTY);
+            uint8_t const fMemType       = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_MEMTYPE);
             uint64_t const fEffectiveEpt = (fEptAttrs << PGM_PTATTRS_EPT_SHIFT) & PGM_PTATTRS_EPT_MASK;
-            pWalk->Core.fEffective = fEffective &= RT_BF_MAKE(PGM_PTATTRS_X,           fExecute)
-                                                 | RT_BF_MAKE(PGM_PTATTRS_RW,          fWrite)
-                                                 | RT_BF_MAKE(PGM_PTATTRS_US,          1)
-                                                 | RT_BF_MAKE(PGM_PTATTRS_A,           fAccessed)
-                                                 | RT_BF_MAKE(PGM_PTATTRS_D,           fDirty)
-                                                 | RT_BF_MAKE(PGM_PTATTRS_EPT_MEMTYPE, 0)
-                                                 | fEffectiveEpt;
-            pWalk->Core.fEffectiveRW = !!(fEffective & X86_PTE_RW);
+
+            fEffective &= RT_BF_MAKE(PGM_PTATTRS_A,           fAccessed)
+                       |  (fEffectiveEpt & fCumulativeEpt);
+            fEffective |= RT_BF_MAKE(PGM_PTATTRS_D,           fDirty)
+                       |  RT_BF_MAKE(PGM_PTATTRS_EPT_MEMTYPE, fMemType);
+            pWalk->Core.fEffective = fEffective;
+            pWalk->Core.fEffectiveRW = !!(fEffective & PGM_PTATTRS_RW_MASK); /** @todo RW isn't copied from EPT R, W. This will break callers who use RW for EPT attributes. */
             pWalk->Core.fEffectiveUS = true;
-            pWalk->Core.fEffectiveNX = !fExecute;
+            pWalk->Core.fEffectiveNX = !(fEffective & PGM_PTATTRS_EPT_X_SUPER_MASK);
             pWalk->Core.fBigPage     = true;
             pWalk->Core.fSucceeded   = true;
@@ -177,14 +190,11 @@
             return PGM_GST_SLAT_NAME_EPT(WalkReturnRsvdError)(pVCpu, pWalk, 2);
 
-        uint64_t const fEptAttrs = Pde.u & EPT_PDE_ATTR_MASK;
-        uint8_t const fExecute   = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_EXECUTE);
-        uint8_t const fWrite     = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_WRITE);
-        uint8_t const fAccessed  = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_ACCESSED);
+        uint64_t const fEptAttrs     = Pde.u & EPT_PDE_ATTR_MASK;
+        uint8_t const fAccessed      = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_ACCESSED);
         uint64_t const fEffectiveEpt = (fEptAttrs << PGM_PTATTRS_EPT_SHIFT) & PGM_PTATTRS_EPT_MASK;
-        pWalk->Core.fEffective = fEffective &= RT_BF_MAKE(PGM_PTATTRS_X,  fExecute)
-                                             | RT_BF_MAKE(PGM_PTATTRS_RW, fWrite)
-                                             | RT_BF_MAKE(PGM_PTATTRS_US, 1)
-                                             | RT_BF_MAKE(PGM_PTATTRS_A,  fAccessed)
-                                             | fEffectiveEpt;
+
+        fEffective &= RT_BF_MAKE(PGM_PTATTRS_A,  fAccessed)
+                   |  (fEffectiveEpt & fCumulativeEpt);
+        pWalk->Core.fEffective = fEffective;
 
         rc = PGM_GCPHYS_2_PTR_BY_VMCPU(pVCpu, GST_GET_PDE_GCPHYS(Pde), &pWalk->pPt);
@@ -204,20 +214,18 @@
         else return PGM_GST_SLAT_NAME_EPT(WalkReturnRsvdError)(pVCpu, pWalk, 1);
 
-        uint64_t const fEptAttrs  = Pte.u & EPT_PTE_ATTR_MASK;
-        uint8_t const fExecute    = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_EXECUTE);
-        uint8_t const fWrite      = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_WRITE);
-        uint8_t const fAccessed   = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_ACCESSED);
-        uint8_t const fDirty      = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_DIRTY);
+        uint64_t const fEptAttrs     = Pte.u & EPT_PTE_ATTR_MASK;
+        uint8_t const fAccessed      = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_ACCESSED);
+        uint8_t const fDirty         = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_DIRTY);
+        uint8_t const fMemType       = RT_BF_GET(fEptAttrs, VMX_BF_EPT_PT_MEMTYPE);
         uint64_t const fEffectiveEpt = (fEptAttrs << PGM_PTATTRS_EPT_SHIFT) & PGM_PTATTRS_EPT_MASK;
-        pWalk->Core.fEffective = fEffective &= RT_BF_MAKE(PGM_PTATTRS_X,           fExecute)
-                                             | RT_BF_MAKE(PGM_PTATTRS_RW,          fWrite)
-                                             | RT_BF_MAKE(PGM_PTATTRS_US,          1)
-                                             | RT_BF_MAKE(PGM_PTATTRS_A,           fAccessed)
-                                             | RT_BF_MAKE(PGM_PTATTRS_D,           fDirty)
-                                             | RT_BF_MAKE(PGM_PTATTRS_EPT_MEMTYPE, 0)
-                                             | fEffectiveEpt;
-        pWalk->Core.fEffectiveRW = !!(fEffective & X86_PTE_RW);
+        fEffective &= RT_BF_MAKE(PGM_PTATTRS_A,           fAccessed)
+                   |  (fEffectiveEpt & fCumulativeEpt);
+        fEffective |= RT_BF_MAKE(PGM_PTATTRS_D,           fDirty)
+                   |  RT_BF_MAKE(PGM_PTATTRS_EPT_MEMTYPE, fMemType);
+        pWalk->Core.fEffective = fEffective;
+
+        pWalk->Core.fEffectiveRW = !!(fEffective & PGM_PTATTRS_RW_MASK); /** @todo RW isn't copied from EPT R, W. This will break callers who use RW for EPT attributes. */
         pWalk->Core.fEffectiveUS = true;
-        pWalk->Core.fEffectiveNX = !fExecute;
+        pWalk->Core.fEffectiveNX = !(fEffective & PGM_PTATTRS_EPT_X_SUPER_MASK);
         pWalk->Core.fSucceeded   = true;
         pWalk->Core.GCPhys       = GST_GET_PTE_GCPHYS(Pte)
Index: trunk/src/VBox/VMM/include/PGMInternal.h
===================================================================
--- trunk/src/VBox/VMM/include/PGMInternal.h	(revision 92310)
+++ trunk/src/VBox/VMM/include/PGMInternal.h	(revision 92311)
@@ -2356,8 +2356,8 @@
  *   - SUPPRESS_VE_XCPT (Suppress \#VE exception) - EPT bit 63 maps to bit 25.
  *
- * Bits 11:9 and bit 43 are deliberately kept unused (they correspond to bits 11:9
- * in the page-table structures and to bit 11 in the EPT structures respectively) as
- * they're reserved for use by software and we may want to preserve them in the
- * future.
+ * Bits 12, 11:9 and 43 are deliberately kept unused (correspond to bit PS and bits
+ * 11:9 in the regular page-table structures and to bit 11 in the EPT structures
+ * respectively) as bit 12 is the page-size bit and bits 11:9 are reserved for
+ * use by software and we may want to use/preserve them in the future.
  *
  * @{ */
@@ -2366,7 +2366,7 @@
 typedef PGMPTATTRS *PPGMPTATTRS;
 
-/** Execute bit (!NX). */
-#define PGM_PTATTRS_X_SHIFT                         0
-#define PGM_PTATTRS_X_MASK                          RT_BIT_64(PGM_PTATTRS_X_SHIFT)
+/** Reserved bit. */
+#define PGM_PTATTRS_RSVD_0_SHIFT                    0
+#define PGM_PTATTRS_RSVD_0_MASK                     RT_BIT_64(PGM_PTATTRS_RSVD_0_SHIFT)
 /** Read and write access bit. */
 #define PGM_PTATTRS_RW_SHIFT                        1
@@ -2393,53 +2393,57 @@
 #define PGM_PTATTRS_G_SHIFT                         8
 #define PGM_PTATTRS_G_MASK                          RT_BIT_64(PGM_PTATTRS_G_SHIFT)
-/** Reserved (bits 11:9) unused. */
-#define PGM_PTATTRS_RSVD_11_9_SHIFT                 9
-#define PGM_PTATTRS_RSVD_11_9_MASK                  UINT64_C(0x0000000000000e00)
+/** Reserved (bits 12:9) unused. */
+#define PGM_PTATTRS_RSVD_12_9_SHIFT                 9
+#define PGM_PTATTRS_RSVD_12_9_MASK                  UINT64_C(0x0000000000001e00)
 /** Read access bit - EPT only. */
-#define PGM_PTATTRS_EPT_R_SHIFT                     12
+#define PGM_PTATTRS_EPT_R_SHIFT                     13
 #define PGM_PTATTRS_EPT_R_MASK                      RT_BIT_64(PGM_PTATTRS_EPT_R_SHIFT)
 /** Write access bit - EPT only. */
-#define PGM_PTATTRS_EPT_W_SHIFT                     13
+#define PGM_PTATTRS_EPT_W_SHIFT                     14
 #define PGM_PTATTRS_EPT_W_MASK                      RT_BIT_64(PGM_PTATTRS_EPT_W_SHIFT)
 /** Execute or execute access for supervisor-mode linear addresses - EPT only. */
-#define PGM_PTATTRS_EPT_X_SUPER_SHIFT               14
+#define PGM_PTATTRS_EPT_X_SUPER_SHIFT               15
 #define PGM_PTATTRS_EPT_X_SUPER_MASK                RT_BIT_64(PGM_PTATTRS_EPT_X_SUPER_SHIFT)
 /** EPT memory type - EPT only. */
-#define PGM_PTATTRS_EPT_MEMTYPE_SHIFT               15
-#define PGM_PTATTRS_EPT_MEMTYPE_MASK                UINT64_C(0x0000000000038000)
+#define PGM_PTATTRS_EPT_MEMTYPE_SHIFT               16
+#define PGM_PTATTRS_EPT_MEMTYPE_MASK                UINT64_C(0x0000000000070000)
 /** Ignore PAT memory type - EPT only. */
-#define PGM_PTATTRS_EPT_IGNORE_PAT_SHIFT            18
+#define PGM_PTATTRS_EPT_IGNORE_PAT_SHIFT            19
 #define PGM_PTATTRS_EPT_IGNORE_PAT_MASK             RT_BIT_64(PGM_PTATTRS_EPT_IGNORE_PAT_SHIFT)
-/** Reserved (bits 21:19) unused. */
-#define PGM_PTATTRS_RSVD_21_19_SHIFT                19
-#define PGM_PTATTRS_RSVD_21_19_MASK                 UINT64_C(0x0000000000380000)
+/** Reserved (bits 22:20) unused. */
+#define PGM_PTATTRS_RSVD_22_20_SHIFT                20
+#define PGM_PTATTRS_RSVD_22_20_MASK                 UINT64_C(0x0000000000700000)
 /** Execute access for user-mode linear addresses - EPT only. */
-#define PGM_PTATTRS_EPT_X_USER_SHIFT                22
+#define PGM_PTATTRS_EPT_X_USER_SHIFT                23
 #define PGM_PTATTRS_EPT_X_USER_MASK                 RT_BIT_64(PGM_PTATTRS_EPT_X_USER_SHIFT)
 /** Reserved (bit 23) - unused. */
-#define PGM_PTATTRS_RSVD_23_SHIFT                   23
-#define PGM_PTATTRS_RSVD_23_MASK                    UINT64_C(0x0000000000800000)
+#define PGM_PTATTRS_RSVD_23_SHIFT                   24
+#define PGM_PTATTRS_RSVD_23_MASK                    UINT64_C(0x0000000001000000)
 /** Supervisor shadow stack - EPT only. */
-#define PGM_PTATTRS_EPT_SUPER_SHW_STACK_SHIFT       24
+#define PGM_PTATTRS_EPT_SUPER_SHW_STACK_SHIFT       25
 #define PGM_PTATTRS_EPT_SUPER_SHW_STACK_MASK        RT_BIT_64(PGM_PTATTRS_EPT_SUPER_SHW_STACK_SHIFT)
 /** Suppress \#VE exception - EPT only. */
-#define PGM_PTATTRS_EPT_SUPPRESS_VE_XCPT_SHIFT      25
+#define PGM_PTATTRS_EPT_SUPPRESS_VE_XCPT_SHIFT      26
 #define PGM_PTATTRS_EPT_SUPPRESS_VE_XCPT_MASK       RT_BIT_64(PGM_PTATTRS_EPT_SUPPRESS_VE_XCPT_SHIFT)
-/** Reserved (bits 63:26) - unused. */
-#define PGM_PTATTRS_RSVD_63_26_SHIFT                26
-#define PGM_PTATTRS_RSVD_63_26_MASK                 UINT64_C(0xfffffffffc000000)
+/** Reserved (bits 62:27) - unused. */
+#define PGM_PTATTRS_RSVD_62_27_SHIFT                27
+#define PGM_PTATTRS_RSVD_62_27_MASK                 UINT64_C(0x7ffffffff8000000)
+/** No-execute bit. */
+#define PGM_PTATTRS_NX_SHIFT                        63
+#define PGM_PTATTRS_NX_MASK                         RT_BIT_64(PGM_PTATTRS_NX_SHIFT)
+
 RT_BF_ASSERT_COMPILE_CHECKS(PGM_PTATTRS_, UINT64_C(0), UINT64_MAX,
-                            (X, RW, US, PWT, PCD, A, D, PAT, G, RSVD_11_9, EPT_R, EPT_W, EPT_X_SUPER, EPT_MEMTYPE, EPT_IGNORE_PAT,
-                             RSVD_21_19, EPT_X_USER, RSVD_23, EPT_SUPER_SHW_STACK, EPT_SUPPRESS_VE_XCPT, RSVD_63_26));
+                            (RSVD_0, RW, US, PWT, PCD, A, D, PAT, G, RSVD_12_9, EPT_R, EPT_W, EPT_X_SUPER, EPT_MEMTYPE,
+                             EPT_IGNORE_PAT, RSVD_22_20, EPT_X_USER, RSVD_23, EPT_SUPER_SHW_STACK, EPT_SUPPRESS_VE_XCPT,
+                             RSVD_62_27, NX));
 
 /** The bit position where the EPT specific attributes begin. */
-#define PGM_PTATTRS_EPT_SHIFT                   PGM_PTATTRS_EPT_R_SHIFT
-/** The mask of EPT bits (bits 63:ATTR_SHIFT). In the future we might choose to
+#define PGM_PTATTRS_EPT_SHIFT                       PGM_PTATTRS_EPT_R_SHIFT
+/** The mask of EPT bits (bits 26:ATTR_SHIFT). In the future we might choose to
  *  use higher unused bits for something else, in that case adjust this mask. */
-#define PGM_PTATTRS_EPT_MASK                        UINT64_C(0xfffffffffffff000)
+#define PGM_PTATTRS_EPT_MASK                        UINT64_C(0x0000000007ffe000)
 
 /** The mask of all PGM page attribute bits for regular page-tables. */
-#define PGM_PTATTRS_PT_VALID_MASK                   (  PGM_PTATTRS_X_MASK \
-                                                     | PGM_PTATTRS_RW_MASK \
+#define PGM_PTATTRS_PT_VALID_MASK                   (  PGM_PTATTRS_RW_MASK \
                                                      | PGM_PTATTRS_US_MASK \
                                                      | PGM_PTATTRS_PWT_MASK \
@@ -2448,11 +2452,9 @@
                                                      | PGM_PTATTRS_D_MASK \
                                                      | PGM_PTATTRS_PAT_MASK \
-                                                     | PGM_PTATTRS_G_MASK)
+                                                     | PGM_PTATTRS_G_MASK \
+                                                     | PGM_PTATTRS_NX_MASK)
 
 /** The mask of all PGM page attribute bits for EPT. */
-#define PGM_PTATTRS_EPT_VALID_MASK                  (  PGM_PTATTRS_X_MASK \
-                                                     | PGM_PTATTRS_RW_MASK \
-                                                     | PGM_PTATTRS_US_MASK \
-                                                     | PGM_PTATTRS_A_MASK \
+#define PGM_PTATTRS_EPT_VALID_MASK                  (  PGM_PTATTRS_A_MASK \
                                                      | PGM_PTATTRS_D_MASK \
                                                      | PGM_PTATTRS_R_MASK \
