Library mcertikos.clib.CalRealIntelModule
Require Export AuxStateDataType.
Require Import Constant.
Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import XOmega.
Require Import CLemmas.
Require Import INVLemmaIntel.
Require Import Values.
Require Import liblayers.compat.CompatGenSem.
Require Import VCGen.
Section REAL_EPT.
Function Calculate_EPDTE_at_j (i: Z) (j: Z) (ept: EPT) : EPT :=
match ZMap.get 0 ept with
| EPML4EValid epdpt ⇒
match ZMap.get i epdpt with
| EPDPTEValid epdt ⇒
ZMap.set 0 (EPML4EValid (ZMap.set i (EPDPTEValid (ZMap.set j (EPDTEValid (ZMap.init EPTEUndef)) epdt)) epdpt)) ept
| _ ⇒ ept
end
| _ ⇒ ept
end.
Fixpoint Calculate_EPDTE (i: Z) (j: nat) (ept: EPT) : EPT :=
match j with
| O ⇒ Calculate_EPDTE_at_j i 0 ept
| S k ⇒ Calculate_EPDTE_at_j i (Z.of_nat (S k)) (Calculate_EPDTE i k ept)
end.
Function Calculate_EPDPTE_at_i (i: Z) (ept: EPT) : EPT :=
match ZMap.get 0 ept with
| EPML4EValid epdpt ⇒
Calculate_EPDTE i 511 (ZMap.set 0 (EPML4EValid (ZMap.set i (EPDPTEValid (ZMap.init EPDTEUndef)) epdpt)) ept)
| _ ⇒ ept
end.
Fixpoint Calculate_EPDPTE (i: nat) (ept: EPT) : EPT :=
match i with
| O ⇒ Calculate_EPDPTE_at_i 0 ept
| S k ⇒ Calculate_EPDPTE_at_i (Z.of_nat (S k)) (Calculate_EPDPTE k ept)
end.
Definition Calculate_EPTPool_at_i (i: Z) (eptpool: EPTPool) : EPTPool :=
ZMap.set i (Calculate_EPDPTE 3 (ZMap.set 0 (EPML4EValid (ZMap.init EPDPTEUndef)) (ZMap.get i eptpool))) eptpool.
Fixpoint Calculate_EPTPool (i: nat) (eptpool: EPTPool) : EPTPool :=
match i with
| O ⇒ Calculate_EPTPool_at_i 0 eptpool
| S k ⇒ Calculate_EPTPool_at_i (Z.of_nat (S k)) (Calculate_EPTPool k eptpool)
end.
Definition real_ept (eptpool: EPTPool) := Calculate_EPTPool (Z.to_nat (NUM_VMS - 1)) eptpool.
End REAL_EPT.
Section REAL_VMCS.
Definition write64_aux (enc: Z) (value: Z64) (d: ZMap.t val) : ZMap.t val :=
let d1 := ZMap.set enc (Vint (Int64.loword (Int64.repr (Z642Z value)))) d in
ZMap.set (enc + 1) (Vint (Int64.hiword (Int64.repr (Z642Z value)))) d1.
Definition write64_block_aux (enc: Z) (value: val) (d: ZMap.t val) : ZMap.t val :=
let d1 := ZMap.set enc value d in
ZMap.set (enc + 1) Vzero d1.
Definition Calculate_VMCS_at_i (cpuid: Z) (curid: Z) (vm: VMCS) (vmi: VMXInfo) (pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b: block):=
match vm with
| VMCSValid revid abrtid m ⇒
let pinbased_ctls := ZMap.get (VMX_INFO_PINBASED_CTLS) vmi in
let procbased_ctls := ZMap.get (VMX_INFO_PROCBASED_CTLS) vmi in
let procbased_ctls2 := ZMap.get (VMX_INFO_PROCBASED_CTLS2) vmi in
let exit_ctls := ZMap.get (VMX_INFO_EXIT_CTLS) vmi in
let entry_ctls := ZMap.get (VMX_INFO_ENTRY_CTLS) vmi in
let cr0_ones_mask := ZMap.get (VMX_INFO_CR0_ONES_MASK) vmi in
let cr0_zeros_mask := ZMap.get (VMX_INFO_CR0_ZEROS_MASK) vmi in
let cr4_ones_mask := ZMap.get (VMX_INFO_CR4_ONES_MASK) vmi in
let cr4_zeros_mask := ZMap.get (VMX_INFO_CR4_ZEROS_MASK) vmi in
let m1 := ZMap.set C_VMCS_PIN_BASED_CTLS (Vint (Int.repr pinbased_ctls)) m in
let m2 := ZMap.set C_VMCS_PRI_PROC_BASED_CTLS (Vint (Int.repr procbased_ctls)) m1 in
let m3 := ZMap.set C_VMCS_SEC_PROC_BASED_CTLS (Vint (Int.repr procbased_ctls2)) m2 in
let m4 := ZMap.set C_VMCS_EXIT_CTLS (Vint (Int.repr exit_ctls)) m3 in
let m5 := ZMap.set C_VMCS_ENTRY_CTLS (Vint (Int.repr entry_ctls)) m4 in
let m6 := ZMap.set C_VMCS_HOST_RIP (Vptr host_rip_b Int.zero) m5 in
let m7 := ZMap.set C_VMCS_HOST_CR0 Vzero m6 in
let m8 := ZMap.set C_VMCS_HOST_CR3 Vzero m7 in
let m9 := ZMap.set C_VMCS_HOST_CR4 Vzero m8 in
let m10 := ZMap.set C_VMCS_HOST_ES_SELECTOR (Vint (Int.repr CPU_GDT_KDATA)) m9 in
let m11 := ZMap.set C_VMCS_HOST_CS_SELECTOR (Vint (Int.repr CPU_GDT_KCODE)) m10 in
let m12 := ZMap.set C_VMCS_HOST_SS_SELECTOR (Vint (Int.repr CPU_GDT_KDATA)) m11 in
let m13 := ZMap.set C_VMCS_HOST_DS_SELECTOR (Vint (Int.repr CPU_GDT_KDATA)) m12 in
let m14 := ZMap.set C_VMCS_HOST_FS_SELECTOR (Vint (Int.repr CPU_GDT_KDATA)) m13 in
let m15 := ZMap.set C_VMCS_HOST_GS_SELECTOR (Vint (Int.repr CPU_GDT_KDATA)) m14 in
let m16 := ZMap.set C_VMCS_HOST_TR_SELECTOR (Vint (Int.repr CPU_GDT_TSS)) m15 in
let m17 := ZMap.set C_VMCS_HOST_FS_BASE Vzero m16 in
let m18 := ZMap.set C_VMCS_HOST_GS_BASE Vzero m17 in
let m19 := ZMap.set C_VMCS_HOST_TR_BASE (Vptr stack_b (Int.repr (curid × PgSize + TSS_OFFSET))) m18 in
let m20 := ZMap.set C_VMCS_HOST_GDTR_BASE (Vptr stack_b (Int.repr (curid × PgSize + GDT_OFFSET))) m19 in
let m21 := ZMap.set C_VMCS_HOST_IDTR_BASE (Vptr idt_b Int.zero) m20 in
let m22 := ZMap.set C_VMCS_HOST_IA32_SYSENTER_CS Vzero m21 in
let m23 := ZMap.set C_VMCS_HOST_IA32_SYSENTER_ESP Vzero m22 in
let m24 := ZMap.set C_VMCS_HOST_IA32_SYSENTER_EIP Vzero m23 in
let m25 := write64_aux C_VMCS_HOST_IA32_PERF_GLOBAL_CTRL (VZ64 0) m24 in
let m26 := write64_aux C_VMCS_HOST_IA32_PAT (VZ64 0) m25 in
let m27 := write64_aux C_VMCS_HOST_IA32_EFER (VZ64 0) m26 in
let m28 := ZMap.set C_VMCS_GUEST_CR0 (Vint (Int.repr (Z.lor v0x60000010 CR0_NE))) m27 in
let m29 := ZMap.set C_VMCS_GUEST_CR3 Vzero m28 in
let m30 := ZMap.set C_VMCS_GUEST_CR4 (Vint (Int.repr CR4_VMXE)) m29 in
let m31 := ZMap.set C_VMCS_GUEST_DR7 (Vint (Int.repr v0x00000400)) m30 in
let m32 := write64_aux C_VMCS_GUEST_IA32_PAT (VZ64 v0x7040600070406) m31 in
let m33 := ZMap.set C_VMCS_GUEST_IA32_SYSENTER_CS Vzero m32 in
let m34 := ZMap.set C_VMCS_GUEST_IA32_SYSENTER_ESP Vzero m33 in
let m35 := ZMap.set C_VMCS_GUEST_IA32_SYSENTER_EIP Vzero m34 in
let m36 := write64_aux C_VMCS_GUEST_IA32_DEBUGCTL (VZ64 0) m35 in
let m37 := write64_block_aux C_VMCS_EPTP (Vptr pml4ept_b (Int.repr (cpuid × EPT_SIZE + EPTP_pml4))) m36 in
let m38 := ZMap.set C_VMCS_VPID Vone m37 in
let m39 := write64_block_aux C_VMCS_MSR_BITMAP (Vptr msr_bitmap_b (Int.repr (cpuid × PgSize))) m38 in
let m40 := write64_aux C_VMCS_LINK_POINTER (VZ64 v0xffffffffffffffff) m39 in
let m41 := ZMap.set C_VMCS_CR0_MASK (Vint (Int.repr (Z.lor cr0_ones_mask cr0_zeros_mask))) m40 in
let m42 := ZMap.set C_VMCS_CR0_SHADOW (Vint (Int.repr cr0_ones_mask)) m41 in
let m43 := ZMap.set C_VMCS_CR4_MASK (Vint (Int.repr (Z.lor cr4_ones_mask cr4_zeros_mask))) m42 in
let m44 := ZMap.set C_VMCS_CR4_SHADOW (Vint (Int.repr cr4_ones_mask)) m43 in
let m45 := write64_block_aux C_VMCS_IO_BITMAP_A (Vptr io_bitmap_b (Int.repr (cpuid × PgSize × 2))) m44 in
let m46 := write64_block_aux C_VMCS_IO_BITMAP_B (Vptr io_bitmap_b (Int.repr (cpuid × PgSize × 2 + PgSize))) m45 in
let m47 := ZMap.set C_VMCS_GUEST_ACTIVITY Vzero m46 in
let m48 := ZMap.set C_VMCS_GUEST_INTERRUPTIBILITY Vzero m47 in
let m49 := ZMap.set C_VMCS_GUEST_PENDING_DBG_EXCEPTIONS Vzero m48 in
let m50 := ZMap.set C_VMCS_ENTRY_INTR_INFO Vzero m49 in
let revid1 := Vzero in
VMCSValid revid1 abrtid m50
end.
Fixpoint Calculate_VMCSPool (i: nat) (cpuid: Z) (curid: Z) (vmcspool: VMCSPool) (vmi: VMXInfo) (pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b: block):=
match i with
| O ⇒ ZMap.set 0 (Calculate_VMCS_at_i cpuid curid (ZMap.get 0 vmcspool) vmi pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b) vmcspool
| S k ⇒ ZMap.set (Z.of_nat (S k)) (Calculate_VMCS_at_i cpuid curid (ZMap.get (Z.of_nat (S k)) vmcspool) vmi pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b) (Calculate_VMCSPool k cpuid curid vmcspool vmi pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b)
end.
Definition real_vmcs (cpuid: Z) (curid: Z) (vmcspool: VMCSPool) (vmi: VMXInfo) (pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b: block):= Calculate_VMCSPool (Z.to_nat (NUM_VMS - 1)) cpuid curid vmcspool vmi pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b.
Lemma real_vmcs_inject_neutral:
∀ vmid curid vm vmi n pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b
host_rip_b,
VMCSPool_inject_neutral vm n →
Mem.flat_inj n pml4ept_b = Some (pml4ept_b, 0) →
Mem.flat_inj n stack_b = Some (stack_b, 0) →
Mem.flat_inj n idt_b = Some (idt_b, 0) →
Mem.flat_inj n msr_bitmap_b = Some (msr_bitmap_b, 0) →
Mem.flat_inj n io_bitmap_b = Some (io_bitmap_b, 0) →
Mem.flat_inj n host_rip_b = Some (host_rip_b, 0) →
0 ≤ vmid < NUM_VMS →
0 ≤ curid < num_proc →
VMCSPool_inject_neutral
(ZMap.set vmid
(Calculate_VMCS_at_i vmid curid (ZMap.get vmid vm) vmi
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b)
vm) n.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold VMCSPool_inject_neutral.
intros; simpl in ×.
unfold VMCSPool_inject_neutral in H.
remember (ZMap.get vmid0 vm) as vmcs0_val; symmetry in Heqvmcs0_val.
remember (ZMap.get vmid vm) as vmcs_val; symmetry in Heqvmcs_val.
generalize Heqvmcs_val, Heqvmcs0_val; intros vmcs_val´ vmcs0_val´.
eapply H in Heqvmcs0_val; eauto.
eapply H in Heqvmcs_val; eauto.
case_eq (zeq vmid0 vmid); intros; subst; simpl in ×.
- rewrite ZMap.gss.
inv Heqvmcs_val.
repeat (eapply VMCS_inject_neutral_gss_Vint_same
|| eapply VMCS_inject_neutral_gss_same); eauto 1;
split; econstructor; eauto;
try (generalize (H11 ofs); intros tmp; destruct tmp; eauto);
discharge_cmp;
try rewrite Z.add_0_r; try reflexivity.
try rewrite Z.add_0_r; try reflexivity.
- rewrite ZMap.gso; auto.
Qed.
End REAL_VMCS.
Section REAL_VMX.
Definition Calculate_VMX_at_i (vm: VMX): VMX :=
let vm1 := ZMap.set VMX_G_RIP´ (Vint (Int.repr v0xfff0)) vm in
let vm2 := ZMap.set VMX_VPID´ Vone vm1 in
let vm3 := ZMap.set VMX_G_CR2´ Vzero vm2 in
let vm4 := ZMap.set VMX_G_DR0´ Vzero vm3 in
let vm5 := ZMap.set VMX_G_DR1´ Vzero vm4 in
let vm6 := ZMap.set VMX_G_DR2´ Vzero vm5 in
let vm7 := ZMap.set VMX_G_DR3´ Vzero vm6 in
ZMap.set VMX_G_DR6´ (Vint (Int.repr v0xffff0ff0)) vm7.
Fixpoint Calculate_VMX (i: nat) (vmxpool: VMXPool) :=
match i with
| O ⇒ ZMap.set 0 (Calculate_VMX_at_i (ZMap.get 0 vmxpool)) vmxpool
| S k ⇒ ZMap.set (Z.of_nat (S k)) (Calculate_VMX_at_i (ZMap.get (Z.of_nat (S k)) vmxpool)) (Calculate_VMX k vmxpool)
end.
Definition real_vmx (vmxpool: VMXPool) := Calculate_VMX (Z.to_nat (NUM_VMS - 1)) vmxpool.
Lemma real_vmx_inject_neutral:
∀ vmid vm n,
VMXPool_inject_neutral vm n →
0 ≤ vmid < NUM_VMS →
VMXPool_inject_neutral
(ZMap.set vmid (Calculate_VMX_at_i (ZMap.get vmid vm)) vm) n.
Proof.
intros.
unfold VMXPool_inject_neutral.
intros.
case_eq (zeq vmid0 vmid); intros; subst.
- rewrite ZMap.gss.
simpl.
repeat eapply VMX_inject_neutral_gss_Vint.
unfold VMXPool_inject_neutral in H.
eapply H in H0; eauto.
- rewrite ZMap.gso; eauto.
Qed.
End REAL_VMX.