Library mcertikos.proc.VMCSIntroGenLink
Require Import LinkTemplate.
Require Import VVMCSIntro.
Require Import VMCSIntroGen.
Require Import VMCSIntroGenLinkSource.
Require Import VEPTInit.
Require Import VEPTInitCSource.
Require Import VEPTInitCode.
Require Import VMCSIntroGenAsm.
Require Import VMCSIntroGenAsm1.
Section WITHCOMPCERTIKOS.
Context `{compcertikos_prf: CompCertiKOS} `{real_params_prf: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{multi_oracle_link: !MultiOracleLink}.
Lemma make_program_find_symbol (CTXT md : module)(m : mem) s :
(p <- make_program s (CTXT ⊕ (md ⊕ VMCS_LOC ↦ v_vmcs) ⊕ ∅) (eptinit ⊕ L64);
ret (Genv.init_mem p) = OK (Some m))
→ ∃ b, find_symbol s VMCS_LOC = Some b ∧
Mem.load Mint32 m b (4096 × GlobalOracle.current_CPU_ID) = Some (Vint Int.zero) ∧
Mem.valid_access m Mint32 b (4096 × GlobalOracle.current_CPU_ID) Writable ∧
Mem.load Mint32 m b (4096 × GlobalOracle.current_CPU_ID + 4) = Some (Vint Int.zero) ∧
Mem.valid_access m Mint32 b (4096 × GlobalOracle.current_CPU_ID + 4) Writable ∧
∀ i : Z, 0 ≤ i ≤ 27670 + 1 →
Mem.valid_access m Mint32 b (4096 × GlobalOracle.current_CPU_ID + i × 4 + 8) Writable.
Proof.
intros mkprog; inv_monad´ mkprog.
assert (mkgenv := make_program_make_globalenv _ _ _ _ mkprog0).
pose proof mkgenv as mkgenv´.
eapply make_globalenv_stencil_matches in mkgenv´.
inv_make_globalenv mkgenv. subst.
rewrite (stencil_matches_symbols _ _ mkgenv´) in ×. inv mkgenv´.
eexists; split; try eassumption.
Opaque Z.mul Z.add.
specialize (Genv.init_mem_characterization _ _ Hbvi H0); eauto.
unfold Genv.perm_globvar; simpl.
change (Z.max (1022 × 4) 0) with (1022 × 4) in ×.
intros (Hperm & _ & init0 & init1 & init2 & init3 & init4 & init5 & init6 & init7 & init8 & init9 & init10 & init11 & init12 & init13 & init14 & init15).
reflexivity.
generalize current_CPU_ID_range; intro.
assert (Mem.valid_access m Mint32 b (4096 × GlobalOracle.current_CPU_ID) Writable).
{
intros; split.
- unfold Mem.range_perm in *; intros. apply Hperm.
simpl in H1.
xomega.
- simpl. ∃ (1024 × GlobalOracle.current_CPU_ID); omega.
}
assert (Mem.valid_access m Mint32 b (4096 × GlobalOracle.current_CPU_ID + 4) Writable).
{
intros; split.
- unfold Mem.range_perm in *; intros. apply Hperm.
simpl in H2.
xomega.
- simpl. ∃ (1024 × GlobalOracle.current_CPU_ID + 1); omega.
}
assert(loads: Mem.load Mint32 m b (4096 × GlobalOracle.current_CPU_ID) = Some (Vint Int.zero) ∧ Mem.load Mint32 m b (4096 × GlobalOracle.current_CPU_ID + 4) = Some (Vint Int.zero)).
{
assert(CPUIDcase: GlobalOracle.current_CPU_ID = 0 ∨
GlobalOracle.current_CPU_ID = 1 ∨
GlobalOracle.current_CPU_ID = 2 ∨
GlobalOracle.current_CPU_ID = 3 ∨
GlobalOracle.current_CPU_ID = 4 ∨
GlobalOracle.current_CPU_ID = 5 ∨
GlobalOracle.current_CPU_ID = 6 ∨
GlobalOracle.current_CPU_ID = 7) by omega.
destruct CPUIDcase as [rw | CPUIDcase].
rewrite rw.
split.
change (4096 × 0) with 0; assumption.
change (4096 × 0 + 4) with 4.
assumption.
destruct CPUIDcase as [rw | CPUIDcase].
rewrite rw.
split; assumption.
destruct CPUIDcase as [rw | CPUIDcase].
rewrite rw.
split; assumption.
destruct CPUIDcase as [rw | CPUIDcase].
rewrite rw.
split; assumption.
destruct CPUIDcase as [rw | CPUIDcase].
rewrite rw.
split; assumption.
destruct CPUIDcase as [rw | CPUIDcase].
rewrite rw.
split; assumption.
destruct CPUIDcase as [rw | rw].
rewrite rw.
split; assumption.
rewrite rw.
destruct init15.
split; assumption.
}
destruct loads.
refine_split; eauto.
intros. { split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H6.
xomega.
- simpl. ∃ (1024 × GlobalOracle.current_CPU_ID + i + 2); omega.
}
Qed.
Lemma init_correct:
init_correct_type VVMCSIntro_module eptinit vmcsintro.
Proof.
init_correct.
exploit make_program_find_symbol; eauto.
intros (b´ & find_symbol_VMCS_LOC & load0 & access0 & load4 & access4 & access).
rewrite ZMap.gi.
econstructor; try eassumption; intros.
rewrite ZMap.gi.
Opaque Z.mul.
simpl.
assert (readable : Mem.valid_access m2 Mint32 b´ (4096 × GlobalOracle.current_CPU_ID + i × 4 + 8) Readable).
{ eapply Mem.valid_access_implies; eauto; constructor. }
exploit Mem.valid_access_load; eauto.
intros [ v load ].
∃ v; split; [| split ]; eauto.
Qed.
Lemma link_correct_aux:
link_correct_aux_type VVMCSIntro_module eptinit vmcsintro.
Proof.
link_correct_aux.
- link_cfunction
vmcs_get_revid_spec_ref
VEPTINITCODE.vmcs_get_revid_code_correct.
- link_cfunction
vmcs_set_revid_spec_ref
VEPTINITCODE.vmcs_set_revid_code_correct.
- link_cfunction
vmcs_get_abrtid_spec_ref
VEPTINITCODE.vmcs_get_abrtid_code_correct.
- link_cfunction
vmcs_set_abrtid_spec_ref
VEPTINITCODE.vmcs_set_abrtid_code_correct.
- link_asmfunction vmcs_readz_spec_ref vmcs_readz_code_correct.
- link_asmfunction vmcs_writez_spec_ref vmcs_writez_code_correct.
- link_asmfunction vmcs_readz64_spec_ref vmcs_readz64_code_correct.
- link_asmfunction vmcs_writez64_spec_ref vmcs_writez64_code_correct.
- link_asmfunction vmcs_write_ident_spec_ref vmcs_write_ident_code_correct.
- link_asmfunction rcr0_spec_ref rcr0_code_correct.
- link_asmfunction rcr3_spec_ref rcr3_code_correct.
- link_asmfunction rcr4_spec_ref rcr4_code_correct.
- link_asmfunction rdmsr_spec_ref rdmsr_code_correct.
- link_asmfunction wrmsr_spec_ref wrmsr_code_correct.
- link_asmfunction vmptrld_spec_ref vmptrld_code_correct.
- link_asmfunction vmx_enable_spec_ref vmx_enable_code_correct.
- apply passthrough_correct.
Qed.
Theorem cl_backward_simulation:
cl_backward_simulation_type VVMCSIntro_module eptinit vmcsintro.
Proof.
cl_backward_simulation init_correct link_correct_aux.
Qed.
Theorem make_program_exists:
make_program_exist_type VVMCSIntro_module eptinit vmcsintro.
Proof.
make_program_exists link_correct_aux.
Qed.
End WITHCOMPCERTIKOS.
Require Import VVMCSIntro.
Require Import VMCSIntroGen.
Require Import VMCSIntroGenLinkSource.
Require Import VEPTInit.
Require Import VEPTInitCSource.
Require Import VEPTInitCode.
Require Import VMCSIntroGenAsm.
Require Import VMCSIntroGenAsm1.
Section WITHCOMPCERTIKOS.
Context `{compcertikos_prf: CompCertiKOS} `{real_params_prf: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{multi_oracle_link: !MultiOracleLink}.
Lemma make_program_find_symbol (CTXT md : module)(m : mem) s :
(p <- make_program s (CTXT ⊕ (md ⊕ VMCS_LOC ↦ v_vmcs) ⊕ ∅) (eptinit ⊕ L64);
ret (Genv.init_mem p) = OK (Some m))
→ ∃ b, find_symbol s VMCS_LOC = Some b ∧
Mem.load Mint32 m b (4096 × GlobalOracle.current_CPU_ID) = Some (Vint Int.zero) ∧
Mem.valid_access m Mint32 b (4096 × GlobalOracle.current_CPU_ID) Writable ∧
Mem.load Mint32 m b (4096 × GlobalOracle.current_CPU_ID + 4) = Some (Vint Int.zero) ∧
Mem.valid_access m Mint32 b (4096 × GlobalOracle.current_CPU_ID + 4) Writable ∧
∀ i : Z, 0 ≤ i ≤ 27670 + 1 →
Mem.valid_access m Mint32 b (4096 × GlobalOracle.current_CPU_ID + i × 4 + 8) Writable.
Proof.
intros mkprog; inv_monad´ mkprog.
assert (mkgenv := make_program_make_globalenv _ _ _ _ mkprog0).
pose proof mkgenv as mkgenv´.
eapply make_globalenv_stencil_matches in mkgenv´.
inv_make_globalenv mkgenv. subst.
rewrite (stencil_matches_symbols _ _ mkgenv´) in ×. inv mkgenv´.
eexists; split; try eassumption.
Opaque Z.mul Z.add.
specialize (Genv.init_mem_characterization _ _ Hbvi H0); eauto.
unfold Genv.perm_globvar; simpl.
change (Z.max (1022 × 4) 0) with (1022 × 4) in ×.
intros (Hperm & _ & init0 & init1 & init2 & init3 & init4 & init5 & init6 & init7 & init8 & init9 & init10 & init11 & init12 & init13 & init14 & init15).
reflexivity.
generalize current_CPU_ID_range; intro.
assert (Mem.valid_access m Mint32 b (4096 × GlobalOracle.current_CPU_ID) Writable).
{
intros; split.
- unfold Mem.range_perm in *; intros. apply Hperm.
simpl in H1.
xomega.
- simpl. ∃ (1024 × GlobalOracle.current_CPU_ID); omega.
}
assert (Mem.valid_access m Mint32 b (4096 × GlobalOracle.current_CPU_ID + 4) Writable).
{
intros; split.
- unfold Mem.range_perm in *; intros. apply Hperm.
simpl in H2.
xomega.
- simpl. ∃ (1024 × GlobalOracle.current_CPU_ID + 1); omega.
}
assert(loads: Mem.load Mint32 m b (4096 × GlobalOracle.current_CPU_ID) = Some (Vint Int.zero) ∧ Mem.load Mint32 m b (4096 × GlobalOracle.current_CPU_ID + 4) = Some (Vint Int.zero)).
{
assert(CPUIDcase: GlobalOracle.current_CPU_ID = 0 ∨
GlobalOracle.current_CPU_ID = 1 ∨
GlobalOracle.current_CPU_ID = 2 ∨
GlobalOracle.current_CPU_ID = 3 ∨
GlobalOracle.current_CPU_ID = 4 ∨
GlobalOracle.current_CPU_ID = 5 ∨
GlobalOracle.current_CPU_ID = 6 ∨
GlobalOracle.current_CPU_ID = 7) by omega.
destruct CPUIDcase as [rw | CPUIDcase].
rewrite rw.
split.
change (4096 × 0) with 0; assumption.
change (4096 × 0 + 4) with 4.
assumption.
destruct CPUIDcase as [rw | CPUIDcase].
rewrite rw.
split; assumption.
destruct CPUIDcase as [rw | CPUIDcase].
rewrite rw.
split; assumption.
destruct CPUIDcase as [rw | CPUIDcase].
rewrite rw.
split; assumption.
destruct CPUIDcase as [rw | CPUIDcase].
rewrite rw.
split; assumption.
destruct CPUIDcase as [rw | CPUIDcase].
rewrite rw.
split; assumption.
destruct CPUIDcase as [rw | rw].
rewrite rw.
split; assumption.
rewrite rw.
destruct init15.
split; assumption.
}
destruct loads.
refine_split; eauto.
intros. { split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H6.
xomega.
- simpl. ∃ (1024 × GlobalOracle.current_CPU_ID + i + 2); omega.
}
Qed.
Lemma init_correct:
init_correct_type VVMCSIntro_module eptinit vmcsintro.
Proof.
init_correct.
exploit make_program_find_symbol; eauto.
intros (b´ & find_symbol_VMCS_LOC & load0 & access0 & load4 & access4 & access).
rewrite ZMap.gi.
econstructor; try eassumption; intros.
rewrite ZMap.gi.
Opaque Z.mul.
simpl.
assert (readable : Mem.valid_access m2 Mint32 b´ (4096 × GlobalOracle.current_CPU_ID + i × 4 + 8) Readable).
{ eapply Mem.valid_access_implies; eauto; constructor. }
exploit Mem.valid_access_load; eauto.
intros [ v load ].
∃ v; split; [| split ]; eauto.
Qed.
Lemma link_correct_aux:
link_correct_aux_type VVMCSIntro_module eptinit vmcsintro.
Proof.
link_correct_aux.
- link_cfunction
vmcs_get_revid_spec_ref
VEPTINITCODE.vmcs_get_revid_code_correct.
- link_cfunction
vmcs_set_revid_spec_ref
VEPTINITCODE.vmcs_set_revid_code_correct.
- link_cfunction
vmcs_get_abrtid_spec_ref
VEPTINITCODE.vmcs_get_abrtid_code_correct.
- link_cfunction
vmcs_set_abrtid_spec_ref
VEPTINITCODE.vmcs_set_abrtid_code_correct.
- link_asmfunction vmcs_readz_spec_ref vmcs_readz_code_correct.
- link_asmfunction vmcs_writez_spec_ref vmcs_writez_code_correct.
- link_asmfunction vmcs_readz64_spec_ref vmcs_readz64_code_correct.
- link_asmfunction vmcs_writez64_spec_ref vmcs_writez64_code_correct.
- link_asmfunction vmcs_write_ident_spec_ref vmcs_write_ident_code_correct.
- link_asmfunction rcr0_spec_ref rcr0_code_correct.
- link_asmfunction rcr3_spec_ref rcr3_code_correct.
- link_asmfunction rcr4_spec_ref rcr4_code_correct.
- link_asmfunction rdmsr_spec_ref rdmsr_code_correct.
- link_asmfunction wrmsr_spec_ref wrmsr_code_correct.
- link_asmfunction vmptrld_spec_ref vmptrld_code_correct.
- link_asmfunction vmx_enable_spec_ref vmx_enable_code_correct.
- apply passthrough_correct.
Qed.
Theorem cl_backward_simulation:
cl_backward_simulation_type VVMCSIntro_module eptinit vmcsintro.
Proof.
cl_backward_simulation init_correct link_correct_aux.
Qed.
Theorem make_program_exists:
make_program_exist_type VVMCSIntro_module eptinit vmcsintro.
Proof.
make_program_exists link_correct_aux.
Qed.
End WITHCOMPCERTIKOS.