diff --git a/xen/arch/x86/hvm/vmx/vmcs.c b/xen/arch/x86/hvm/vmx/vmcs.c
index 8103b20d29..e6ea197230 100644
--- a/xen/arch/x86/hvm/vmx/vmcs.c
+++ b/xen/arch/x86/hvm/vmx/vmcs.c
@@ -144,6 +144,14 @@ static void __init vmx_display_features(void)
         printk(" - none\n");
 }
 
+bool vmx_msr_available(struct vmx_msr_policy *p, uint32_t msr)
+{
+    if ( msr < MSR_IA32_VMX_BASIC || msr > MSR_IA32_VMX_VMFUNC )
+        return 0;
+
+    return p->available & (1u << (msr - MSR_IA32_VMX_BASIC));
+}
+
 static u32 adjust_vmx_controls(
     const char *name, u32 ctl_min, u32 ctl_opt, u32 msr, bool_t *mismatch)
 {
@@ -1956,6 +1964,45 @@ void __init setup_vmcs_dump(void)
     register_keyhandler('v', vmcs_dump, "dump VT-x VMCSs", 1);
 }
 
+static void __init __maybe_unused build_assertions(void)
+{
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.basic) !=
+                 sizeof(raw_vmx_msr_policy.basic.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.pinbased_ctls) !=
+                 sizeof(raw_vmx_msr_policy.pinbased_ctls.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.procbased_ctls) !=
+                 sizeof(raw_vmx_msr_policy.procbased_ctls.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.exit_ctls) !=
+                 sizeof(raw_vmx_msr_policy.exit_ctls.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.entry_ctls) !=
+                 sizeof(raw_vmx_msr_policy.entry_ctls.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.misc) !=
+                 sizeof(raw_vmx_msr_policy.misc.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.cr0_fixed_0) !=
+                 sizeof(raw_vmx_msr_policy.cr0_fixed_0.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.cr0_fixed_1) !=
+                 sizeof(raw_vmx_msr_policy.cr0_fixed_1.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.cr4_fixed_0) !=
+                 sizeof(raw_vmx_msr_policy.cr4_fixed_0.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.cr4_fixed_1) !=
+                 sizeof(raw_vmx_msr_policy.cr4_fixed_1.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.vmcs_enum) !=
+                 sizeof(raw_vmx_msr_policy.vmcs_enum.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.procbased_ctls2) !=
+                 sizeof(raw_vmx_msr_policy.procbased_ctls2.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.ept_vpid_cap) !=
+                 sizeof(raw_vmx_msr_policy.ept_vpid_cap.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.true_pinbased_ctls) !=
+                 sizeof(raw_vmx_msr_policy.true_pinbased_ctls.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.true_procbased_ctls) !=
+                 sizeof(raw_vmx_msr_policy.true_procbased_ctls.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.true_exit_ctls) !=
+                 sizeof(raw_vmx_msr_policy.true_exit_ctls.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.true_entry_ctls) !=
+                 sizeof(raw_vmx_msr_policy.true_entry_ctls.raw));
+    BUILD_BUG_ON(sizeof(raw_vmx_msr_policy.vmfunc) !=
+                 sizeof(raw_vmx_msr_policy.vmfunc.raw));
+}
 
 /*
  * Local variables:
diff --git a/xen/include/asm-x86/hvm/vmx/vmcs.h b/xen/include/asm-x86/hvm/vmx/vmcs.h
index e3cdfdf576..fca1e62e4c 100644
--- a/xen/include/asm-x86/hvm/vmx/vmcs.h
+++ b/xen/include/asm-x86/hvm/vmx/vmcs.h
@@ -562,6 +562,350 @@ void vmx_domain_flush_pml_buffers(struct domain *d);
 
 void vmx_domain_update_eptp(struct domain *d);
 
+union vmx_pin_based_exec_control_bits {
+    uint32_t raw;
+    struct {
+        bool ext_intr_exiting:1;
+        uint32_t             :2;  /* 1:2 reserved */
+        bool      nmi_exiting:1;
+        uint32_t             :1;  /* 4 reserved */
+        bool     virtual_nmis:1;
+        bool    preempt_timer:1;
+        bool posted_interrupt:1;
+        uint32_t             :24; /* 8:31 reserved */
+    };
+};
+
+union vmx_cpu_based_exec_control_bits {
+    uint32_t raw;
+    struct {
+        uint32_t                        :2;  /* 0:1 reserved */
+        bool        virtual_intr_pending:1;
+        bool           use_tsc_offseting:1;
+        uint32_t                        :3;  /* 4:6 reserved */
+        bool                 hlt_exiting:1;
+        uint32_t                        :1;  /* 8 reserved */
+        bool              invlpg_exiting:1;
+        bool               mwait_exiting:1;
+        bool               rdpmc_exiting:1;
+        bool               rdtsc_exiting:1;
+        uint32_t                        :2;  /* 13:14 reserved */
+        bool            cr3_load_exiting:1;
+        bool           cr3_store_exiting:1;
+        uint32_t                        :2;  /* 17:18 reserved */
+        bool            cr8_load_exiting:1;
+        bool           cr8_store_exiting:1;
+        bool                tpr_shadow_0:1;
+        bool         virtual_nmi_pending:1;
+        bool              mov_dr_exiting:1;
+        bool           uncond_io_exiting:1;
+        bool          activate_io_bitmap:1;
+        uint32_t                        :1;  /* 26 reserved */
+        bool           monitor_trap_flag:1;
+        bool         activate_msr_bitmap:1;
+        bool             monitor_exiting:1;
+        bool               pause_exiting:1;
+        bool activate_secondary_controls:1;
+    };
+};
+
+union vmx_vmexit_control_bits {
+    uint32_t raw;
+    struct {
+        uint32_t                    :2;  /* 0:1 reserved */
+        bool       save_debug_cntrls:1;
+        uint32_t                    :6;  /* 3:8 reserved */
+        bool              ia32e_mode:1;
+        uint32_t                    :2;  /* 10:11 reserved */
+        bool   load_perf_global_ctrl:1;
+        uint32_t                    :2;  /* 13:14 reserved */
+        bool        ack_intr_on_exit:1;
+        uint32_t                    :2;  /* 16:17 reserved */
+        bool          save_guest_pat:1;
+        bool           load_host_pat:1;
+        bool         save_guest_efer:1;
+        bool          load_host_efer:1;
+        bool      save_preempt_timer:1;
+        bool           clear_bndcfgs:1;
+        bool conceal_vmexits_from_pt:1;
+        uint32_t                    :7;  /* 25:31 reserved */
+    };
+};
+
+union vmx_vmentry_control_bits {
+    uint32_t raw;
+    struct {
+        uint32_t                        :2;  /* 0:1 reserved */
+        bool           load_debug_cntrls:1;
+        uint32_t                        :6;  /* 3:8 reserved */
+        bool                  ia32e_mode:1;
+        bool                         smm:1;
+        bool          deact_dual_monitor:1;
+        uint32_t                        :1;  /* 12 reserved */
+        bool       load_perf_global_ctrl:1;
+        bool              load_guest_pat:1;
+        bool             load_guest_efer:1;
+        bool                load_bndcfgs:1;
+        bool   conceal_vmentries_from_pt:1;
+        uint32_t                        :14; /* 18:31 reserved */
+    };
+};
+
+union vmx_secondary_exec_control_bits {
+    uint32_t raw;
+    struct {
+        bool    virtualize_apic_accesses:1;
+        bool                  enable_ept:1;
+        bool    descriptor_table_exiting:1;
+        bool               enable_rdtscp:1;
+        bool      virtualize_x2apic_mode:1;
+        bool                 enable_vpid:1;
+        bool              wbinvd_exiting:1;
+        bool          unrestricted_guest:1;
+        bool          apic_register_virt:1;
+        bool       virtual_intr_delivery:1;
+        bool          pause_loop_exiting:1;
+        bool              rdrand_exiting:1;
+        bool              enable_invpcid:1;
+        bool         enable_vm_functions:1;
+        bool       enable_vmcs_shadowing:1;
+        bool               encls_exiting:1;
+        bool              rdseed_exiting:1;
+        bool                  enable_pml:1;
+        bool      enable_virt_exceptions:1;
+        bool conceal_vmx_nonroot_from_pt:1;
+        bool                      xsaves:1;
+        uint32_t                        :1;  /* 21 reserved */
+        bool   ept_mode_based_exec_cntrl:1;
+        uint32_t                        :2;  /* 23:24 reserved */
+        bool                 tsc_scaling:1;
+        uint32_t                        :6;  /* 26:31 reserved */
+    };
+};
+
+struct vmx_msr_policy
+{
+    /*
+     * Bitmap of readable MSRs, starting from MSR_IA32_VMX_BASIC,
+     * derived from contents of MSRs in this structure.
+     */
+    uint32_t available;
+
+    union {
+        uint64_t msr[MSR_IA32_VMX_VMFUNC - MSR_IA32_VMX_BASIC + 1];
+
+        struct {
+            /* MSR 0x480 */
+            union {
+                uint64_t raw;
+                struct {
+                    uint32_t vmcs_revision_id:31;
+                    bool                     :1;  /* 31 always zero */
+                    uint32_t vmcs_region_size:13;
+                    uint32_t                 :3;  /* 45:47 reserved */
+                    bool      addresses_32bit:1;
+                    bool         dual_monitor:1;
+                    uint32_t      memory_type:4;
+                    bool         ins_out_info:1;
+                    bool        default1_zero:1;
+                    uint32_t                 :8;  /* 56:63 reserved */
+                };
+            } basic;
+
+            /* MSR 0x481 */
+            union {
+                uint64_t raw;
+                struct {
+                    union vmx_pin_based_exec_control_bits allowed_0;
+                    union vmx_pin_based_exec_control_bits allowed_1;
+                };
+            } pinbased_ctls;
+
+            /* MSR 0x482 */
+            union {
+                uint64_t raw;
+                struct {
+                    union vmx_cpu_based_exec_control_bits allowed_0;
+                    union vmx_cpu_based_exec_control_bits allowed_1;
+                };
+            } procbased_ctls;
+
+            /* MSR 0x483 */
+            union {
+                uint64_t raw;
+                struct {
+                    union vmx_vmexit_control_bits allowed_0;
+                    union vmx_vmexit_control_bits allowed_1;
+                };
+            } exit_ctls;
+
+            /* MSR 0x484 */
+            union {
+                uint64_t raw;
+                struct {
+                    union vmx_vmentry_control_bits allowed_0;
+                    union vmx_vmentry_control_bits allowed_1;
+                };
+            } entry_ctls;
+
+            /* MSR 0x485 */
+            union {
+                uint64_t raw;
+                struct {
+                    uint32_t      preempt_timer_scale:5;
+                    bool            vmexit_stores_lma:1;
+                    bool           hlt_activity_state:1;
+                    bool      shutdown_activity_state:1;
+                    bool wait_for_sipi_activity_state:1;
+                    uint32_t                         :5;  /* 9:13 reserved */
+                    bool                    pt_in_vmx:1;
+                    bool          ia32_smbase_support:1;
+                    uint32_t               cr3_target:9;
+                    uint32_t       max_msr_load_count:3;
+                    bool    ia32_smm_monitor_ctl_bit2:1;
+                    bool                  vmwrite_all:1;
+                    bool           inject_ilen0_event:1;
+                    uint32_t                         :1;  /* 31 reserved */
+                    uint32_t         mseg_revision_id;
+                };
+            } misc;
+
+            /* MSR 0x486 */
+            union {
+                uint64_t raw;
+                struct {
+                    uint32_t allowed_0;
+                    uint32_t :32;
+                };
+            } cr0_fixed_0;
+
+            /* MSR 0x487 */
+            union {
+                uint64_t raw;
+                struct {
+                    uint32_t allowed_1;
+                    uint32_t :32;
+                };
+            } cr0_fixed_1;
+
+            /* MSR 0x488 */
+            union {
+                uint64_t raw;
+                struct {
+                    uint32_t allowed_0;
+                    uint32_t :32;
+                };
+            } cr4_fixed_0;
+
+            /* MSR 0x489 */
+            union {
+                uint64_t raw;
+                struct {
+                    uint32_t allowed_1;
+                    uint32_t :32;
+                };
+            } cr4_fixed_1;
+
+            /* MSR 0x48A */
+            union {
+                uint64_t raw;
+                struct {
+                    uint32_t                      :1;  /* 0 reserved */
+                    uint32_t vmcs_encoding_max_idx:9;
+                    uint64_t                      :54; /* 10:63 reserved */
+                };
+            } vmcs_enum;
+
+            /* MSR 0x48B */
+            union {
+                uint64_t raw;
+                struct {
+                    union vmx_secondary_exec_control_bits allowed_0;
+                    union vmx_secondary_exec_control_bits allowed_1;
+                };
+            } procbased_ctls2;
+
+            /* MSR 0x48C */
+            union {
+                uint64_t raw;
+                struct {
+                    bool     exec_only_supported:1;
+                    uint32_t                    :5;  /* 1:5 reserved */
+                    bool walk_length_4_supported:1;
+                    uint32_t                    :1;  /* 7 reserved */
+                    bool          memory_type_uc:1;
+                    uint32_t                    :5;  /* 9:13 reserved */
+                    bool          memory_type_wb:1;
+                    uint32_t                    :1;  /* 15 reserved */
+                    bool           superpage_2mb:1;
+                    bool           superpage_1gb:1;
+                    uint32_t                    :2;  /* 18:19 reserved */
+                    bool      invept_instruction:1;
+                    bool                  ad_bit:1;
+                    bool advanced_ept_violations:1;
+                    uint32_t                    :2;  /* 23:24 reserved */
+                    bool   invept_single_context:1;
+                    bool      invept_all_context:1;
+                    uint32_t                    :5;  /* 27:31 reserved */
+                    bool     invvpid_instruction:1;
+                    uint32_t                    :7;  /* 33:39 reserved */
+                    bool invvpid_individual_addr:1;
+                    bool  invvpid_single_context:1;
+                    bool     invvpid_all_context:1;
+                    bool invvpid_single_context_retaining_global:1;
+                    uint32_t                    :20; /* 44:63 reserved */
+                };
+            } ept_vpid_cap;
+
+            /* MSR 0x48D */
+            union {
+                uint64_t raw;
+                struct {
+                    union vmx_pin_based_exec_control_bits allowed_0;
+                    union vmx_pin_based_exec_control_bits allowed_1;
+                };
+            } true_pinbased_ctls;
+
+            /* MSR 0x48E */
+            union {
+                uint64_t raw;
+                struct {
+                    union vmx_cpu_based_exec_control_bits allowed_0;
+                    union vmx_cpu_based_exec_control_bits allowed_1;
+                };
+            } true_procbased_ctls;
+
+            /* MSR 0x48F */
+            union {
+                uint64_t raw;
+                struct {
+                    union vmx_vmexit_control_bits allowed_0;
+                    union vmx_vmexit_control_bits allowed_1;
+                };
+            } true_exit_ctls;
+
+            /* MSR 0x490 */
+            union {
+                uint64_t raw;
+                struct {
+                    union vmx_vmentry_control_bits allowed_0;
+                    union vmx_vmentry_control_bits allowed_1;
+                };
+            } true_entry_ctls;
+
+            /* MSR 0x491 */
+            union {
+                uint64_t raw;
+                struct {
+                    bool eptp_switching:1;
+                };
+            } vmfunc;
+        };
+    };
+};
+
+bool vmx_msr_available(struct vmx_msr_policy *p, uint32_t msr);
+
 #endif /* ASM_X86_HVM_VMX_VMCS_H__ */
 
 /*
