diff --git a/include/arch/x86/arch/64/mode/object/structures.bf b/include/arch/x86/arch/64/mode/object/structures.bf index e8ff988ec..c1c633617 100644 --- a/include/arch/x86/arch/64/mode/object/structures.bf +++ b/include/arch/x86/arch/64/mode/object/structures.bf @@ -151,6 +151,60 @@ block io_page_table_cap (capType, capIOPTIsMapped, capIOPTLevel, capIOPTMappedAd field_high capIOPTMappedAddress 48 } +block vcpu_cap { + field capVCPUPtr 64 + + field capType 5 + padding 59 +} + +-- Fourth-level EPT page table +block ept_pt_cap (capType, capPTMappedAddress, capPTIsMapped, capPTMappedASID, capPTBasePtr) { + field capPTBasePtr 64 + + field capType 5 + field capPTIsMapped 1 + padding 10 + field_high capPTMappedAddress 27 + field capPTMappedASID 16 + padding 5 +} + +-- third-level EPT page table (page directory) +block ept_pd_cap (capType, capPDMappedAddress, capPDIsMapped, capPDMappedASID, capPDBasePtr) { + field capPDBasePtr 64 + + field capType 5 + field capPDIsMapped 1 + padding 10 + field_high capPDMappedAddress 19 + field capPDMappedASID 16 + padding 13 +} + +-- Second-level EPT page table (page directory pointer table) +block ept_pdpt_cap (capType, capPDPTMappedAddress, capPDPTIsMapped, capPDPTMappedASID, capPDPTBasePtr) { + field capPDPTBasePtr 64 + + field capType 5 + field capPDPTIsMapped 1 + padding 10 + field_high capPDPTMappedAddress 17 + field capPDPTMappedASID 16 + padding 15 +} + +-- First-level EPT pml4 +block ept_pml4_cap (capType, capPML4IsMapped, capPML4MappedASID, capPML4BasePtr) { + field capPML4BasePtr 64 + + field capType 5 + field capPML4IsMapped 1 + padding 42 + + field capPML4MappedASID 16 +} + -- NB: odd numbers are arch caps (see isArchCap()) tagged_union cap capType { -- 5-bit tag caps @@ -177,6 +231,11 @@ tagged_union cap capType { tag io_space_cap 15 tag io_page_table_cap 17 tag io_port_cap 19 + tag vcpu_cap 21 + tag ept_pt_cap 23 + tag ept_pd_cap 25 + tag ept_pdpt_cap 27 + tag ept_pml4_cap 29 } ---- Arch-independent object types @@ -364,9 +423,20 @@ block asid_map_vspace { field type 2 } +#ifdef CONFIG_VTX +block asid_map_ept { + field_high ept_root 48 + padding 14 + field type 2 +} +#endif + tagged_union asid_map type { tag asid_map_none 0 tag asid_map_vspace 1 +#ifdef CONFIG_VTX + tag asid_map_ept 2 +#endif } -- PML4, PDPE, PDs and PTs, assuming 51-bit physical address @@ -485,6 +555,77 @@ block pte { field present 1 } +block ept_pml4e { + padding 13 + field_high pdpt_base_address 39 + padding 9 + field execute 1 + field write 1 + field read 1 +} + +block ept_pdpte { + padding 13 + field_high pd_base_address 39 + field avl_cte_depth 3 + padding 6 + field execute 1 + field write 1 + field read 1 +} + +block ept_pde_2m { + padding 13 + field_high page_base_address 31 + padding 8 + field avl_cte_depth 2 + padding 2 + field page_size 1 + field ignore_pat 1 + field type 3 + field execute 1 + field write 1 + field read 1 +} + +block ept_pde_4k { + padding 13 + field_high pt_base_address 39 + field avl_cte_depth 3 + padding 1 + field page_size 1 + padding 4 + field execute 1 + field write 1 + field read 1 +} + +tagged_union ept_pde page_size { + tag ept_pde_4k 0 + tag ept_pde_2m 1 +} + +block ept_pte { + padding 13 + field_high page_base_address 39 + field avl_cte_depth 2 + padding 3 + field ignore_pat 1 + field type 3 + field execute 1 + field write 1 + field read 1 +} + +block vmx_eptp { + padding 13 + field_high paddr 39 + padding 5 + field flags 1 + field depth_minus_1 3 + field memory_type 3 +} + block cr3 { padding 13 field_high pml4_base_address 39 diff --git a/include/arch/x86/arch/64/mode/object/structures.h b/include/arch/x86/arch/64/mode/object/structures.h index f6a79a28d..18147ecc1 100644 --- a/include/arch/x86/arch/64/mode/object/structures.h +++ b/include/arch/x86/arch/64/mode/object/structures.h @@ -140,6 +140,9 @@ cap_get_capMappedASID(cap_t cap) case cap_page_directory_cap: return cap_page_directory_cap_get_capPDMappedASID(cap); + case cap_ept_pml4_cap: + return cap_ept_pml4_cap_get_capPML4MappedASID(cap); + default: fail("Invalid arch cap type"); } diff --git a/include/arch/x86/arch/object/vcpu.h b/include/arch/x86/arch/object/vcpu.h index 08e910cae..4153cf969 100644 --- a/include/arch/x86/arch/object/vcpu.h +++ b/include/arch/x86/arch/object/vcpu.h @@ -14,6 +14,7 @@ #define __ARCH_OBJECT_VCPU_H #include +#include #define VCPU_VMCS_SIZE 4096 #define VCPU_IOBITMAP_SIZE 8192 diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h index c508cc444..30f8ac94d 100644 --- a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h +++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h @@ -40,6 +40,12 @@ #define seL4_HugePageBits 30 #define seL4_ASIDPoolBits 12 +#define seL4_X86_VCPUBits 14 +#define seL4_X86_EPTPML4Bits 12 +#define seL4_X86_EPTPDPTBits 12 +#define seL4_X86_EPTPDBits 12 +#define seL4_X86_EPTPTBits 12 + /* Untyped size limits */ #define seL4_MinUntypedBits 4 #define seL4_MaxUntypedBits 47 diff --git a/src/arch/x86/64/kernel/vspace.c b/src/arch/x86/64/kernel/vspace.c index 67b4ec74c..8f78b0411 100644 --- a/src/arch/x86/64/kernel/vspace.c +++ b/src/arch/x86/64/kernel/vspace.c @@ -787,10 +787,20 @@ create_mapped_it_frame_cap(cap_t vspace_cap, pptr_t pptr, vptr_t vptr, asid_t as exception_t performASIDPoolInvocation(asid_t asid, asid_pool_t *poolPtr, cte_t *vspaceCapSlot) { - cap_pml4_cap_ptr_set_capPML4MappedASID(&vspaceCapSlot->cap, asid); - cap_pml4_cap_ptr_set_capPML4IsMapped(&vspaceCapSlot->cap, 1); - poolPtr->array[asid & MASK(asidLowBits)] - = asid_map_asid_map_vspace_new(cap_pml4_cap_get_capPML4BasePtr(vspaceCapSlot->cap)); + asid_map_t asid_map; + if (cap_get_capType(vspaceCapSlot->cap) == cap_pml4_cap) { + cap_pml4_cap_ptr_set_capPML4MappedASID(&vspaceCapSlot->cap, asid); + cap_pml4_cap_ptr_set_capPML4IsMapped(&vspaceCapSlot->cap, 1); + asid_map = asid_map_asid_map_vspace_new(cap_pml4_cap_get_capPML4BasePtr(vspaceCapSlot->cap)); + } else { +#ifdef CONFIG_VTX + assert(cap_get_capType(vspaceCapSlot->cap) == cap_ept_pml4_cap); + cap_ept_pml4_cap_ptr_set_capPML4MappedASID(&vspaceCapSlot->cap, asid); + cap_ept_pml4_cap_ptr_set_capPML4IsMapped(&vspaceCapSlot->cap, 1); + asid_map = asid_map_asid_map_ept_new(cap_ept_pml4_cap_get_capPML4BasePtr(vspaceCapSlot->cap)); +#endif + } + poolPtr->array[asid & MASK(asidLowBits)] = asid_map; return EXCEPTION_NONE; } diff --git a/src/arch/x86/64/object/objecttype.c b/src/arch/x86/64/object/objecttype.c index 414aa8ec6..b268de614 100644 --- a/src/arch/x86/64/object/objecttype.c +++ b/src/arch/x86/64/object/objecttype.c @@ -20,6 +20,7 @@ #include #include #include +#include #include #include