Library mcertikos.security.Security
Require Import Coqlib.
Require Import Maps.
Require Import Streams.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import LAsm.
Require Import XOmega.
Require Import compcert.cfrontend.Ctypes.
Require Import Conventions.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import CertiKOSAux.
Require Import Behavior.
Require Import AbstractDataType.
Require Import Soundness.
Require Import I64Layer.
Require Import LoadStoreSem2.
Require Import MakeProgram.
Require Import SecurityCommon.
Require Import ObsEq.
Require Import SecurityInv.
Require Import Integrity.
Require Import Confidentiality.
Require Import ConfidentialityRestore.
Require Import SecurityBigstep.
Require Import SecurityExtra.
Require Import CertiKOSproof.
Section SECURITY.
Local Open Scope Z_scope.
Variables (sten : stencil) (CTXT kernel : module) (user_prog comb_prog : program).
Hypothesis certikos_ok : CertiKOS.certikos = OK kernel.
Hypothesis make_user_prog :
make_program sten CTXT (TSysCall.tsyscall ⊕ L64) = OK user_prog.
Hypothesis make_comb_prog :
make_program sten (CTXT ⊕ kernel) (MBoot.mboot ⊕ L64) = OK comb_prog.
Section PROCSTARTUSER.
Notation ge := (Genv.globalenv user_prog).
Fact make_globalenv_ge : make_globalenv sten CTXT tsyscall_layer = OK ge.
Proof.
unfold make_globalenv, bind; simpl; unfold Errors.bind; simpl in ×.
unfold tsyscall_layer; rewrite make_user_prog; reflexivity.
Qed.
Fact stencil_matches_ge : stencil_matches sten ge.
Proof.
eapply make_globalenv_stencil_matches; eauto.
eapply make_globalenv_ge.
Qed.
Lemma psu_block_ex : ∃ b, Genv.find_symbol ge proc_start_user = Some b.
Proof.
assert (Hge: make_globalenv sten CTXT tsyscall_layer = ret ge) by (apply make_globalenv_ge).
unfold tsyscall_layer, TSysCall.tsyscall, TSysCall.tsyscall_passthrough in *; inv_make_globalenv Hge.
∃ b0; assumption.
Qed.
Lemma psu_block_con : Genv.find_symbol ge proc_start_user ≠ None.
Proof.
destruct psu_block_ex as [b Hb]; rewrite Hb; discriminate.
Qed.
Definition b : block.
destruct (Genv.find_symbol ge proc_start_user) eqn:Hfs.
apply b.
contradiction (psu_block_con Hfs).
Defined.
Lemma psu_ge : Genv.find_symbol ge proc_start_user = Some b.
Proof.
unfold b.
generalize (fun Hfs0 : Genv.find_symbol ge proc_start_user = None ⇒
False_rect block (psu_block_con Hfs0)); intro f.
destruct (Genv.find_symbol ge proc_start_user) eqn:Hfs; auto.
contradiction (psu_block_con Hfs).
Qed.
Lemma psu_sten : find_symbol sten proc_start_user = Some b.
Proof.
erewrite <- stencil_matches_symbols.
apply psu_ge.
apply stencil_matches_ge.
Qed.
End PROCSTARTUSER.
Hint Resolve make_globalenv_ge stencil_matches_ge psu_ge psu_sten.
Existing Instance MakeProgramImpl.make_program_ops.
Existing Instance MakeProgramImpl.make_program_prf.
Notation state1 := (Asm.state (mem:= mwd (cdata (cdata_ops:= MBoot.mboot_data_ops) RData))).
Notation state2 := (Asm.state (mem:= mwd (cdata (cdata_ops:= PProc.pproc_data_ops) RData))).
Notation mboot := (MBoot.mboot ⊕ L64).
Notation tsyscall := (TSysCall.tsyscall ⊕ L64).
Local Instance : ExternalCallsOps (mwd (cdata RData)) :=
CompatExternalCalls.compatlayer_extcall_ops mboot.
Local Instance : LayerConfigurationOps := compatlayer_configuration_ops mboot.
Local Instance : ExternalCallsOps (mwd (cdata RData)) :=
CompatExternalCalls.compatlayer_extcall_ops tsyscall.
Local Instance : LayerConfigurationOps := compatlayer_configuration_ops tsyscall.
Definition sem1 : semantics int state1 :=
LAsm.semantics (lcfg_ops := LC mboot) comb_prog.
Definition sem2 : semantics int state2 :=
LAsm.semantics (lcfg_ops := LC tsyscall) user_prog.
Section BIGSTEPIMPL.
Variable p : Z.
Record ostate : Type :=
{
observe_rs: option regset;
observe_d: my_obs;
observe_m: mem
}.
Definition xobserve (s : state2) : ostate :=
match s with
| State rs (m,d) ⇒
{|
observe_rs:= if zeq p (cid d) then Some rs else None;
observe_d:= my_observe p d;
observe_m:= m
|}
end.
Notation obs_eq s1 s2 := (xobserve s1 = xobserve s2).
Lemma observe_obs_eq :
∀ s1 s2, obs_eq s1 s2 → observe_lasm _ p s1 = observe_lasm _ p s2.
Proof.
unfold observe; simpl.
intros [rs1 [m1 d1]] [rs2 [m2 d2]] Hobs_eq; simpl in *; inv Hobs_eq; auto.
Qed.
Lemma final_nostep :
∀ s r, final_state sem2 s r → Nostep sem2 s.
Proof.
intros [rs [m d]] r Hfin t s Hstep; inv Hfin; inv Hstep; rewrites.
Qed.
Definition active (s : state2) : Prop :=
match s with State _ (_,d) ⇒ p = cid d end.
Lemma active_obs_eq :
∀ s1 s2, obs_eq s1 s2 → (active s1 ↔ active s2).
Proof.
intros [rs1 [m1 d1]] [rs2 [m2 d2]]; simpl.
intro Hobs_eq; inv Hobs_eq.
destruct (zeq p (cid d1)), (zeq p (cid d2)); inv H6; intuition.
Qed.
Lemma active_dec : ∀ s, Decidable.decidable (active s).
Proof.
intros [rs [m d]]; simpl.
destruct (zeq p (cid d)); [left; auto | right; auto].
Qed.
Definition state_inv (s : state2) : Prop :=
match s with State _ (_,d) ⇒ secure_inv b p d end.
Lemma initial_state_inv :
∀ s, initial_state sem2 s → state_inv s.
Proof.
simpl; intros [rs [m d]] Hinit; inv Hinit; simpl in ×.
unfold Genv.init_mem in *; simpl in ×.
rewrite (InitMem.alloc_globals_with_data _ _ Memimpl.empty (init_adt:cdata RData)) in H0.
elim_none; inv H0; apply secure_inv_init.
Qed.
Lemma state_inv_preserved :
∀ s s' t, Step sem2 s t s' → state_inv s → state_inv s'.
Proof.
intros [rs [m d]] [rs' [m' d']] Hstep Hinv.
simpl in *; eapply secure_inv_preserved; eauto.
Qed.
Definition init (s : state2) : Prop :=
match s with State rs (_,d) ⇒ secure_inv' b p rs d end.
Lemma init_preserved :
∀ s s' t, Step sem2 s t s' → state_inv s → init s → init s'.
Proof.
intros [rs1 [m1 d1]] [rs2 [m2 d2]] t; simpl; intros.
eapply secure_inv'_preserved; eauto.
Qed.
Lemma conf :
p > high_id →
∀ s1 s1' s2 s2' t1 t2,
init s1 → state_inv s1 →
init s2 → state_inv s2 →
active s1 → Step sem2 s1 t1 s1' → Step sem2 s2 t2 s2' →
obs_eq s1 s2 → obs_eq s1' s2'.
Proof.
intros p_prop [rs1 [m1 d1]] [rs1' [m1' d1']] [rs2 [m2 d2]] [rs2' [m2' d2']]; simpl.
intros ? ? ? ? ? ? ? ? ? Hobs_eq.
assert (Hobs_eq': my_obs_eq p d1 d2) by
(apply my_obs_eq_convert; inv Hobs_eq; unfold my_observe; apply f_equal_my_obs; auto).
destruct (zeq p (cid d1)), (zeq p (cid d2)); auto; inv Hobs_eq; try congruence.
edestruct confidentiality; [| | | | | | | eapply H4 | eapply H5 | | |]; eauto.
destruct H6; f_equal; auto.
destruct H3; destruct (zeq (cid d1) (cid d1')), (zeq (cid d1) (cid d2')); auto; intuition.
apply my_obs_eq_convert; auto.
Qed.
Lemma integ :
p > high_id →
∀ s s' t,
init s → state_inv s →
¬ active s → ¬ active s' →
Step sem2 s t s' → obs_eq s s'.
Proof.
intros p_prop [rs [m d]] [rs' [m' d']]; simpl.
intros; edestruct integrity; eauto; f_equal; auto.
destruct (zeq p (cid d)), (zeq p (cid d')); auto; contradiction.
apply my_obs_eq_convert; auto.
Qed.
Lemma conf_restore :
p > high_id →
∀ s1 s1' s2 s2' t1 t2,
init s1 → state_inv s1 →
init s2 → state_inv s2 →
¬ active s1 → active s1' → active s2' →
Step sem2 s1 t1 s1' → Step sem2 s2 t2 s2' →
obs_eq s1 s2 → obs_eq s1' s2'.
Proof.
intros p_prop [rs1 [m1 d1]] [rs1' [m1' d1']] [rs2 [m2 d2]] [rs2' [m2' d2']]; simpl.
intros ? ? ? ? ? ? ? ? ? ? ? Hobs_eq.
assert (Hobs_eq': my_obs_eq p d1 d2) by
(apply my_obs_eq_convert; inv Hobs_eq; unfold my_observe; apply f_equal_my_obs; auto).
inv Hobs_eq.
edestruct confidentiality_restore; [| | | | | | | eapply H6 | eapply H7 | idtac..]; eauto.
destruct H8; f_equal; auto.
destruct (zeq (cid d1') (cid d1')), (zeq (cid d1') (cid d2')); auto; try contradiction; intuition.
apply my_obs_eq_convert; auto.
Qed.
Lemma integ_observe :
∀ s s' t,
init s → state_inv s →
active s → ¬ active s' →
Step sem2 s t s' →
observe_lasm _ p s = observe_lasm _ p s'.
Proof.
intros [rs [m d]] [rs' [m' d']] t Hinit Hinv Hact Hact' Hstep.
simpl in *; unfold ObservationImpl.observe; f_equal.
eapply new_cid_no_output; eauto; congruence.
Qed.
End BIGSTEPIMPL.
Instance tsyscall_bigstep_ops : SecBigstepOps :=
{|
principal_ok p := p > high_id;
xobserve := xobserve;
active := active;
state_inv := state_inv;
init := init
|}.
Hypothesis active_forever :
∀ p,
principal_ok p →
∀ s,
init p s → state_inv p s →
∃ s' t, Plus sem2 s t s' ∧ active p s'.
Instance tsyscall_bigstep : SecBigstep sem2 (observe_lasm _).
Proof.
constructor.
- intros; apply observe_obs_eq; auto.
- intros; eapply final_nostep; eauto.
- intros; apply active_obs_eq; auto.
- apply active_dec.
- apply active_forever.
- intros; apply initial_state_inv; auto.
- intros; eapply state_inv_preserved; eauto.
- intros; eapply init_preserved; eauto.
- apply conf.
- apply integ.
- apply conf_restore.
- intros; eapply integ_observe; eauto.
Qed.
Section WITHPRINCIPAL.
Require Import Observation.
Require Import Determinism.
Variable p : Z.
Hypothesis p_ok : p > high_id.
Notation observe := (observe_lasm _ p).
Definition sem3 : semantics int state2 := sec_sem sem2 p.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Theorem my_simulation : inhabited (simulation sem3 sem1 observe observe).
Proof.
eapply compose_simulation_inhabited.
constructor; eapply secure_sim.
eapply CertiKOS_correct_simulation; eauto.
Qed.
Lemma tsyscall_sec_notrace :
∀ s t s',
init p s → Step sem3 s t s' → t = E0.
Proof.
induction 2; destruct s as [rs [m d]], s' as [rs' [m' d']].
eapply tsyscall_notrace; eauto.
assert (t = E0) by (eapply tsyscall_notrace; eauto); subst.
rewrite IHsec_step; auto.
eapply init_preserved; eauto.
Qed.
Lemma state_inv_preserved_star :
∀ s s' t,
Star sem2 s t s' → state_inv p s → state_inv p s'.
Proof.
induction 1; auto.
intros; apply IHstar; eapply state_inv_preserved; eauto.
Qed.
Variable wi : world.
Theorem end_to_end_security :
∃ sim : simulation sem3 sem1 observe observe,
∀ Si S1 t,
initial_state sem2 Si → Star sem2 Si t S1 → init p S1 →
∀ S2 s1 s2 i1 i2,
state_inv p S2 → init p S2 →
xobserve p S1 = xobserve p S2 → sim i1 S1 s1 → sim i2 S2 s2 →
∀ w1 w2,
state_beh_eq (world_sem int sem1 wi) (world_sem int sem1 wi)
(world_observe observe) (world_observe observe) (s1,w1) (s2,w2).
Proof.
destruct my_simulation as [sim]; ∃ sim.
intros Si S1 t Hinitial Hstar Hinit1 S2 s1 s2 i1 i2 Hinv2 Hinit2 Hobs_eq Hsim1 Hsim2 w1 w2.
assert (Hinv1: state_inv p S1).
{
eapply state_inv_preserved_star; eauto.
apply initial_state_inv; auto.
}
assert (inv_init_preserved:
∀ s t s',
state_inv p s ∧ init p s →
Step sem3 s t s' → state_inv p s' ∧ init p s').
{
intros S t' S' [Hinv Hinit] Hstep; simpl; split.
eapply (sec_state_inv_preserved _ p_ok _ _ _ Hstep); auto.
eapply (sec_init_preserved _ p_ok _ _ _ Hstep); auto.
}
assert (inv_init_no_trace:
∀ s t s',
state_inv p s ∧ init p s → Step sem3 s t s' → t = E0).
{
intros S t' S' [Hinv Hinit] Hstep; eapply tsyscall_sec_notrace; [|eauto]; auto.
}
assert (inv_init_safe:
∀ s, state_inv p s ∧ init p s → safe sem3 s).
{
intros S [Hinv Hinit] S' t' Hstar'.
right; apply sec_safe; auto.
eapply sec_init_preserved_star; eauto.
eapply sec_state_inv_preserved_star; eauto.
}
eapply state_beh_eq_trans.
{
eapply state_beh_eq_sym.
eapply (sim_beh_eq _ _ _ _ sim) with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- eapply soundness_determinate; eauto; decision.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply mboot_behavioral.
- split; [eapply Hinv1 | eapply Hinit1].
- eauto.
}
eapply state_beh_eq_trans.
{
eapply state_beh_eq_sym.
eapply world_state_beh_eq with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- apply ObservationImpl.devact_observation.
- apply sec_final_nostep.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply world_safe with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
}
eapply state_beh_eq_trans.
{
eapply obs_eq_beh_eq; eauto.
apply tsyscall_behavioral.
}
eapply state_beh_eq_trans.
{
eapply world_state_beh_eq with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- apply ObservationImpl.devact_observation.
- apply sec_final_nostep.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply world_safe with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
}
{
eapply (sim_beh_eq _ _ _ _ sim) with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- eapply soundness_determinate; eauto; decision.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply mboot_behavioral.
- eauto.
}
Qed.
Theorem end_to_end_security' :
∃ sim : simulation sem2 sem1 observe observe,
∀ Si S1 t,
initial_state sem2 Si → Star sem2 Si t S1 → init p S1 →
∀ S2 s1 s2 i1 i2,
state_inv p S2 → init p S2 →
xobserve p S1 = xobserve p S2 → sim i1 S1 s1 → sim i2 S2 s2 →
∀ w1 w2,
state_beh_eq (world_sem int sem1 wi) (world_sem int sem1 wi)
(world_observe observe) (world_observe observe) (s1,w1) (s2,w2).
Proof.
edestruct CertiKOS_correct_simulation as [sim]; eauto; ∃ sim.
intros Si S1 t Hinitial Hstar Hinit1 S2 s1 s2 i1 i2 Hinv2 Hinit2 Hobs_eq Hsim1 Hsim2 w1 w2.
assert (Hinv1: state_inv p S1).
{
eapply state_inv_preserved_star; eauto.
apply initial_state_inv; auto.
}
assert (inv_init_preserved:
∀ s t s',
state_inv p s ∧ init p s →
Step sem3 s t s' → state_inv p s' ∧ init p s').
{
intros S t' S' [Hinv Hinit] Hstep; simpl; split.
eapply (sec_state_inv_preserved _ p_ok _ _ _ Hstep); auto.
eapply (sec_init_preserved _ p_ok _ _ _ Hstep); auto.
}
assert (inv_init_no_trace:
∀ s t s',
state_inv p s ∧ init p s → Step sem3 s t s' → t = E0).
{
intros S t' S' [Hinv Hinit] Hstep; eapply tsyscall_sec_notrace; [|eauto]; auto.
}
assert (inv_init_safe:
∀ s, state_inv p s ∧ init p s → safe sem3 s).
{
intros S [Hinv Hinit] S' t' Hstar'.
right; apply sec_safe; auto.
eapply sec_init_preserved_star; eauto.
eapply sec_state_inv_preserved_star; eauto.
}
assert (Hinv1': state_inv p S1).
{
eapply state_inv_preserved_star; eauto.
apply initial_state_inv; auto.
}
assert (inv_init_preserved':
∀ s t s',
state_inv p s ∧ init p s →
Step sem2 s t s' → state_inv p s' ∧ init p s').
{
intros S t' S' [Hinv Hinit] Hstep; simpl; split.
eapply state_inv_preserved; eauto.
eapply init_preserved; eauto.
}
assert (inv_init_no_trace':
∀ s t s',
state_inv p s ∧ init p s → Step sem2 s t s' → t = E0).
{
intros [? [? ?]] t' [? [? ?]] [Hinv Hinit] Hstep; eapply tsyscall_notrace; eauto.
}
assert (inv_init_safe':
∀ s, state_inv p s ∧ init p s → safe sem2 s).
{
intros S [Hinv Hinit] S' t' Hstar'.
destruct active_forever with (s:=S') (p:=p) as [S'' [t'' [Hplus ?]]]; auto.
eapply (init_preserved_star (Hsec:=tsyscall_bigstep_ops)); eauto.
eapply state_inv_preserved_star; eauto.
inv Hplus; right; eauto.
}
eapply state_beh_eq_trans.
{
eapply state_beh_eq_sym.
eapply (sim_beh_eq _ _ _ _ sim) with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- eapply soundness_determinate; eauto; decision.
- apply tsyscall_behavioral.
- apply mboot_behavioral.
- split; [eapply Hinv1 | eapply Hinit1].
- eauto.
}
eapply state_beh_eq_trans.
{
eapply state_beh_eq_sym.
eapply (sim_beh_eq _ _ _ _ (secure_sim p))
with (init:= fun S ⇒ state_inv p S ∧ init p S) (i:= tt); auto.
- eapply soundness_determinate; eauto; decision.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply tsyscall_behavioral.
- split; [eapply Hinv1 | eapply Hinit1].
- simpl; auto.
}
eapply state_beh_eq_trans.
{
eapply state_beh_eq_sym.
eapply world_state_beh_eq with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- apply ObservationImpl.devact_observation.
- apply sec_final_nostep.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply world_safe with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
}
eapply state_beh_eq_trans.
{
eapply obs_eq_beh_eq; eauto.
apply tsyscall_behavioral.
}
eapply state_beh_eq_trans.
{
eapply world_state_beh_eq with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- apply ObservationImpl.devact_observation.
- apply sec_final_nostep.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply world_safe with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
}
eapply state_beh_eq_trans.
{
eapply (sim_beh_eq _ _ _ _ (secure_sim p))
with (init:= fun S ⇒ state_inv p S ∧ init p S) (i:= tt); auto.
- eapply soundness_determinate; eauto; decision.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply tsyscall_behavioral.
- simpl; auto.
}
{
eapply (sim_beh_eq _ _ _ _ sim) with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- eapply soundness_determinate; eauto; decision.
- apply tsyscall_behavioral.
- apply mboot_behavioral.
- eauto.
}
Qed.
End WITHPRINCIPAL.
End SECURITY.
Require Import Maps.
Require Import Streams.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import LAsm.
Require Import XOmega.
Require Import compcert.cfrontend.Ctypes.
Require Import Conventions.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import CertiKOSAux.
Require Import Behavior.
Require Import AbstractDataType.
Require Import Soundness.
Require Import I64Layer.
Require Import LoadStoreSem2.
Require Import MakeProgram.
Require Import SecurityCommon.
Require Import ObsEq.
Require Import SecurityInv.
Require Import Integrity.
Require Import Confidentiality.
Require Import ConfidentialityRestore.
Require Import SecurityBigstep.
Require Import SecurityExtra.
Require Import CertiKOSproof.
Section SECURITY.
Local Open Scope Z_scope.
Variables (sten : stencil) (CTXT kernel : module) (user_prog comb_prog : program).
Hypothesis certikos_ok : CertiKOS.certikos = OK kernel.
Hypothesis make_user_prog :
make_program sten CTXT (TSysCall.tsyscall ⊕ L64) = OK user_prog.
Hypothesis make_comb_prog :
make_program sten (CTXT ⊕ kernel) (MBoot.mboot ⊕ L64) = OK comb_prog.
Section PROCSTARTUSER.
Notation ge := (Genv.globalenv user_prog).
Fact make_globalenv_ge : make_globalenv sten CTXT tsyscall_layer = OK ge.
Proof.
unfold make_globalenv, bind; simpl; unfold Errors.bind; simpl in ×.
unfold tsyscall_layer; rewrite make_user_prog; reflexivity.
Qed.
Fact stencil_matches_ge : stencil_matches sten ge.
Proof.
eapply make_globalenv_stencil_matches; eauto.
eapply make_globalenv_ge.
Qed.
Lemma psu_block_ex : ∃ b, Genv.find_symbol ge proc_start_user = Some b.
Proof.
assert (Hge: make_globalenv sten CTXT tsyscall_layer = ret ge) by (apply make_globalenv_ge).
unfold tsyscall_layer, TSysCall.tsyscall, TSysCall.tsyscall_passthrough in *; inv_make_globalenv Hge.
∃ b0; assumption.
Qed.
Lemma psu_block_con : Genv.find_symbol ge proc_start_user ≠ None.
Proof.
destruct psu_block_ex as [b Hb]; rewrite Hb; discriminate.
Qed.
Definition b : block.
destruct (Genv.find_symbol ge proc_start_user) eqn:Hfs.
apply b.
contradiction (psu_block_con Hfs).
Defined.
Lemma psu_ge : Genv.find_symbol ge proc_start_user = Some b.
Proof.
unfold b.
generalize (fun Hfs0 : Genv.find_symbol ge proc_start_user = None ⇒
False_rect block (psu_block_con Hfs0)); intro f.
destruct (Genv.find_symbol ge proc_start_user) eqn:Hfs; auto.
contradiction (psu_block_con Hfs).
Qed.
Lemma psu_sten : find_symbol sten proc_start_user = Some b.
Proof.
erewrite <- stencil_matches_symbols.
apply psu_ge.
apply stencil_matches_ge.
Qed.
End PROCSTARTUSER.
Hint Resolve make_globalenv_ge stencil_matches_ge psu_ge psu_sten.
Existing Instance MakeProgramImpl.make_program_ops.
Existing Instance MakeProgramImpl.make_program_prf.
Notation state1 := (Asm.state (mem:= mwd (cdata (cdata_ops:= MBoot.mboot_data_ops) RData))).
Notation state2 := (Asm.state (mem:= mwd (cdata (cdata_ops:= PProc.pproc_data_ops) RData))).
Notation mboot := (MBoot.mboot ⊕ L64).
Notation tsyscall := (TSysCall.tsyscall ⊕ L64).
Local Instance : ExternalCallsOps (mwd (cdata RData)) :=
CompatExternalCalls.compatlayer_extcall_ops mboot.
Local Instance : LayerConfigurationOps := compatlayer_configuration_ops mboot.
Local Instance : ExternalCallsOps (mwd (cdata RData)) :=
CompatExternalCalls.compatlayer_extcall_ops tsyscall.
Local Instance : LayerConfigurationOps := compatlayer_configuration_ops tsyscall.
Definition sem1 : semantics int state1 :=
LAsm.semantics (lcfg_ops := LC mboot) comb_prog.
Definition sem2 : semantics int state2 :=
LAsm.semantics (lcfg_ops := LC tsyscall) user_prog.
Section BIGSTEPIMPL.
Variable p : Z.
Record ostate : Type :=
{
observe_rs: option regset;
observe_d: my_obs;
observe_m: mem
}.
Definition xobserve (s : state2) : ostate :=
match s with
| State rs (m,d) ⇒
{|
observe_rs:= if zeq p (cid d) then Some rs else None;
observe_d:= my_observe p d;
observe_m:= m
|}
end.
Notation obs_eq s1 s2 := (xobserve s1 = xobserve s2).
Lemma observe_obs_eq :
∀ s1 s2, obs_eq s1 s2 → observe_lasm _ p s1 = observe_lasm _ p s2.
Proof.
unfold observe; simpl.
intros [rs1 [m1 d1]] [rs2 [m2 d2]] Hobs_eq; simpl in *; inv Hobs_eq; auto.
Qed.
Lemma final_nostep :
∀ s r, final_state sem2 s r → Nostep sem2 s.
Proof.
intros [rs [m d]] r Hfin t s Hstep; inv Hfin; inv Hstep; rewrites.
Qed.
Definition active (s : state2) : Prop :=
match s with State _ (_,d) ⇒ p = cid d end.
Lemma active_obs_eq :
∀ s1 s2, obs_eq s1 s2 → (active s1 ↔ active s2).
Proof.
intros [rs1 [m1 d1]] [rs2 [m2 d2]]; simpl.
intro Hobs_eq; inv Hobs_eq.
destruct (zeq p (cid d1)), (zeq p (cid d2)); inv H6; intuition.
Qed.
Lemma active_dec : ∀ s, Decidable.decidable (active s).
Proof.
intros [rs [m d]]; simpl.
destruct (zeq p (cid d)); [left; auto | right; auto].
Qed.
Definition state_inv (s : state2) : Prop :=
match s with State _ (_,d) ⇒ secure_inv b p d end.
Lemma initial_state_inv :
∀ s, initial_state sem2 s → state_inv s.
Proof.
simpl; intros [rs [m d]] Hinit; inv Hinit; simpl in ×.
unfold Genv.init_mem in *; simpl in ×.
rewrite (InitMem.alloc_globals_with_data _ _ Memimpl.empty (init_adt:cdata RData)) in H0.
elim_none; inv H0; apply secure_inv_init.
Qed.
Lemma state_inv_preserved :
∀ s s' t, Step sem2 s t s' → state_inv s → state_inv s'.
Proof.
intros [rs [m d]] [rs' [m' d']] Hstep Hinv.
simpl in *; eapply secure_inv_preserved; eauto.
Qed.
Definition init (s : state2) : Prop :=
match s with State rs (_,d) ⇒ secure_inv' b p rs d end.
Lemma init_preserved :
∀ s s' t, Step sem2 s t s' → state_inv s → init s → init s'.
Proof.
intros [rs1 [m1 d1]] [rs2 [m2 d2]] t; simpl; intros.
eapply secure_inv'_preserved; eauto.
Qed.
Lemma conf :
p > high_id →
∀ s1 s1' s2 s2' t1 t2,
init s1 → state_inv s1 →
init s2 → state_inv s2 →
active s1 → Step sem2 s1 t1 s1' → Step sem2 s2 t2 s2' →
obs_eq s1 s2 → obs_eq s1' s2'.
Proof.
intros p_prop [rs1 [m1 d1]] [rs1' [m1' d1']] [rs2 [m2 d2]] [rs2' [m2' d2']]; simpl.
intros ? ? ? ? ? ? ? ? ? Hobs_eq.
assert (Hobs_eq': my_obs_eq p d1 d2) by
(apply my_obs_eq_convert; inv Hobs_eq; unfold my_observe; apply f_equal_my_obs; auto).
destruct (zeq p (cid d1)), (zeq p (cid d2)); auto; inv Hobs_eq; try congruence.
edestruct confidentiality; [| | | | | | | eapply H4 | eapply H5 | | |]; eauto.
destruct H6; f_equal; auto.
destruct H3; destruct (zeq (cid d1) (cid d1')), (zeq (cid d1) (cid d2')); auto; intuition.
apply my_obs_eq_convert; auto.
Qed.
Lemma integ :
p > high_id →
∀ s s' t,
init s → state_inv s →
¬ active s → ¬ active s' →
Step sem2 s t s' → obs_eq s s'.
Proof.
intros p_prop [rs [m d]] [rs' [m' d']]; simpl.
intros; edestruct integrity; eauto; f_equal; auto.
destruct (zeq p (cid d)), (zeq p (cid d')); auto; contradiction.
apply my_obs_eq_convert; auto.
Qed.
Lemma conf_restore :
p > high_id →
∀ s1 s1' s2 s2' t1 t2,
init s1 → state_inv s1 →
init s2 → state_inv s2 →
¬ active s1 → active s1' → active s2' →
Step sem2 s1 t1 s1' → Step sem2 s2 t2 s2' →
obs_eq s1 s2 → obs_eq s1' s2'.
Proof.
intros p_prop [rs1 [m1 d1]] [rs1' [m1' d1']] [rs2 [m2 d2]] [rs2' [m2' d2']]; simpl.
intros ? ? ? ? ? ? ? ? ? ? ? Hobs_eq.
assert (Hobs_eq': my_obs_eq p d1 d2) by
(apply my_obs_eq_convert; inv Hobs_eq; unfold my_observe; apply f_equal_my_obs; auto).
inv Hobs_eq.
edestruct confidentiality_restore; [| | | | | | | eapply H6 | eapply H7 | idtac..]; eauto.
destruct H8; f_equal; auto.
destruct (zeq (cid d1') (cid d1')), (zeq (cid d1') (cid d2')); auto; try contradiction; intuition.
apply my_obs_eq_convert; auto.
Qed.
Lemma integ_observe :
∀ s s' t,
init s → state_inv s →
active s → ¬ active s' →
Step sem2 s t s' →
observe_lasm _ p s = observe_lasm _ p s'.
Proof.
intros [rs [m d]] [rs' [m' d']] t Hinit Hinv Hact Hact' Hstep.
simpl in *; unfold ObservationImpl.observe; f_equal.
eapply new_cid_no_output; eauto; congruence.
Qed.
End BIGSTEPIMPL.
Instance tsyscall_bigstep_ops : SecBigstepOps :=
{|
principal_ok p := p > high_id;
xobserve := xobserve;
active := active;
state_inv := state_inv;
init := init
|}.
Hypothesis active_forever :
∀ p,
principal_ok p →
∀ s,
init p s → state_inv p s →
∃ s' t, Plus sem2 s t s' ∧ active p s'.
Instance tsyscall_bigstep : SecBigstep sem2 (observe_lasm _).
Proof.
constructor.
- intros; apply observe_obs_eq; auto.
- intros; eapply final_nostep; eauto.
- intros; apply active_obs_eq; auto.
- apply active_dec.
- apply active_forever.
- intros; apply initial_state_inv; auto.
- intros; eapply state_inv_preserved; eauto.
- intros; eapply init_preserved; eauto.
- apply conf.
- apply integ.
- apply conf_restore.
- intros; eapply integ_observe; eauto.
Qed.
Section WITHPRINCIPAL.
Require Import Observation.
Require Import Determinism.
Variable p : Z.
Hypothesis p_ok : p > high_id.
Notation observe := (observe_lasm _ p).
Definition sem3 : semantics int state2 := sec_sem sem2 p.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Theorem my_simulation : inhabited (simulation sem3 sem1 observe observe).
Proof.
eapply compose_simulation_inhabited.
constructor; eapply secure_sim.
eapply CertiKOS_correct_simulation; eauto.
Qed.
Lemma tsyscall_sec_notrace :
∀ s t s',
init p s → Step sem3 s t s' → t = E0.
Proof.
induction 2; destruct s as [rs [m d]], s' as [rs' [m' d']].
eapply tsyscall_notrace; eauto.
assert (t = E0) by (eapply tsyscall_notrace; eauto); subst.
rewrite IHsec_step; auto.
eapply init_preserved; eauto.
Qed.
Lemma state_inv_preserved_star :
∀ s s' t,
Star sem2 s t s' → state_inv p s → state_inv p s'.
Proof.
induction 1; auto.
intros; apply IHstar; eapply state_inv_preserved; eauto.
Qed.
Variable wi : world.
Theorem end_to_end_security :
∃ sim : simulation sem3 sem1 observe observe,
∀ Si S1 t,
initial_state sem2 Si → Star sem2 Si t S1 → init p S1 →
∀ S2 s1 s2 i1 i2,
state_inv p S2 → init p S2 →
xobserve p S1 = xobserve p S2 → sim i1 S1 s1 → sim i2 S2 s2 →
∀ w1 w2,
state_beh_eq (world_sem int sem1 wi) (world_sem int sem1 wi)
(world_observe observe) (world_observe observe) (s1,w1) (s2,w2).
Proof.
destruct my_simulation as [sim]; ∃ sim.
intros Si S1 t Hinitial Hstar Hinit1 S2 s1 s2 i1 i2 Hinv2 Hinit2 Hobs_eq Hsim1 Hsim2 w1 w2.
assert (Hinv1: state_inv p S1).
{
eapply state_inv_preserved_star; eauto.
apply initial_state_inv; auto.
}
assert (inv_init_preserved:
∀ s t s',
state_inv p s ∧ init p s →
Step sem3 s t s' → state_inv p s' ∧ init p s').
{
intros S t' S' [Hinv Hinit] Hstep; simpl; split.
eapply (sec_state_inv_preserved _ p_ok _ _ _ Hstep); auto.
eapply (sec_init_preserved _ p_ok _ _ _ Hstep); auto.
}
assert (inv_init_no_trace:
∀ s t s',
state_inv p s ∧ init p s → Step sem3 s t s' → t = E0).
{
intros S t' S' [Hinv Hinit] Hstep; eapply tsyscall_sec_notrace; [|eauto]; auto.
}
assert (inv_init_safe:
∀ s, state_inv p s ∧ init p s → safe sem3 s).
{
intros S [Hinv Hinit] S' t' Hstar'.
right; apply sec_safe; auto.
eapply sec_init_preserved_star; eauto.
eapply sec_state_inv_preserved_star; eauto.
}
eapply state_beh_eq_trans.
{
eapply state_beh_eq_sym.
eapply (sim_beh_eq _ _ _ _ sim) with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- eapply soundness_determinate; eauto; decision.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply mboot_behavioral.
- split; [eapply Hinv1 | eapply Hinit1].
- eauto.
}
eapply state_beh_eq_trans.
{
eapply state_beh_eq_sym.
eapply world_state_beh_eq with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- apply ObservationImpl.devact_observation.
- apply sec_final_nostep.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply world_safe with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
}
eapply state_beh_eq_trans.
{
eapply obs_eq_beh_eq; eauto.
apply tsyscall_behavioral.
}
eapply state_beh_eq_trans.
{
eapply world_state_beh_eq with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- apply ObservationImpl.devact_observation.
- apply sec_final_nostep.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply world_safe with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
}
{
eapply (sim_beh_eq _ _ _ _ sim) with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- eapply soundness_determinate; eauto; decision.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply mboot_behavioral.
- eauto.
}
Qed.
Theorem end_to_end_security' :
∃ sim : simulation sem2 sem1 observe observe,
∀ Si S1 t,
initial_state sem2 Si → Star sem2 Si t S1 → init p S1 →
∀ S2 s1 s2 i1 i2,
state_inv p S2 → init p S2 →
xobserve p S1 = xobserve p S2 → sim i1 S1 s1 → sim i2 S2 s2 →
∀ w1 w2,
state_beh_eq (world_sem int sem1 wi) (world_sem int sem1 wi)
(world_observe observe) (world_observe observe) (s1,w1) (s2,w2).
Proof.
edestruct CertiKOS_correct_simulation as [sim]; eauto; ∃ sim.
intros Si S1 t Hinitial Hstar Hinit1 S2 s1 s2 i1 i2 Hinv2 Hinit2 Hobs_eq Hsim1 Hsim2 w1 w2.
assert (Hinv1: state_inv p S1).
{
eapply state_inv_preserved_star; eauto.
apply initial_state_inv; auto.
}
assert (inv_init_preserved:
∀ s t s',
state_inv p s ∧ init p s →
Step sem3 s t s' → state_inv p s' ∧ init p s').
{
intros S t' S' [Hinv Hinit] Hstep; simpl; split.
eapply (sec_state_inv_preserved _ p_ok _ _ _ Hstep); auto.
eapply (sec_init_preserved _ p_ok _ _ _ Hstep); auto.
}
assert (inv_init_no_trace:
∀ s t s',
state_inv p s ∧ init p s → Step sem3 s t s' → t = E0).
{
intros S t' S' [Hinv Hinit] Hstep; eapply tsyscall_sec_notrace; [|eauto]; auto.
}
assert (inv_init_safe:
∀ s, state_inv p s ∧ init p s → safe sem3 s).
{
intros S [Hinv Hinit] S' t' Hstar'.
right; apply sec_safe; auto.
eapply sec_init_preserved_star; eauto.
eapply sec_state_inv_preserved_star; eauto.
}
assert (Hinv1': state_inv p S1).
{
eapply state_inv_preserved_star; eauto.
apply initial_state_inv; auto.
}
assert (inv_init_preserved':
∀ s t s',
state_inv p s ∧ init p s →
Step sem2 s t s' → state_inv p s' ∧ init p s').
{
intros S t' S' [Hinv Hinit] Hstep; simpl; split.
eapply state_inv_preserved; eauto.
eapply init_preserved; eauto.
}
assert (inv_init_no_trace':
∀ s t s',
state_inv p s ∧ init p s → Step sem2 s t s' → t = E0).
{
intros [? [? ?]] t' [? [? ?]] [Hinv Hinit] Hstep; eapply tsyscall_notrace; eauto.
}
assert (inv_init_safe':
∀ s, state_inv p s ∧ init p s → safe sem2 s).
{
intros S [Hinv Hinit] S' t' Hstar'.
destruct active_forever with (s:=S') (p:=p) as [S'' [t'' [Hplus ?]]]; auto.
eapply (init_preserved_star (Hsec:=tsyscall_bigstep_ops)); eauto.
eapply state_inv_preserved_star; eauto.
inv Hplus; right; eauto.
}
eapply state_beh_eq_trans.
{
eapply state_beh_eq_sym.
eapply (sim_beh_eq _ _ _ _ sim) with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- eapply soundness_determinate; eauto; decision.
- apply tsyscall_behavioral.
- apply mboot_behavioral.
- split; [eapply Hinv1 | eapply Hinit1].
- eauto.
}
eapply state_beh_eq_trans.
{
eapply state_beh_eq_sym.
eapply (sim_beh_eq _ _ _ _ (secure_sim p))
with (init:= fun S ⇒ state_inv p S ∧ init p S) (i:= tt); auto.
- eapply soundness_determinate; eauto; decision.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply tsyscall_behavioral.
- split; [eapply Hinv1 | eapply Hinit1].
- simpl; auto.
}
eapply state_beh_eq_trans.
{
eapply state_beh_eq_sym.
eapply world_state_beh_eq with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- apply ObservationImpl.devact_observation.
- apply sec_final_nostep.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply world_safe with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
}
eapply state_beh_eq_trans.
{
eapply obs_eq_beh_eq; eauto.
apply tsyscall_behavioral.
}
eapply state_beh_eq_trans.
{
eapply world_state_beh_eq with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- apply ObservationImpl.devact_observation.
- apply sec_final_nostep.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply world_safe with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
}
eapply state_beh_eq_trans.
{
eapply (sim_beh_eq _ _ _ _ (secure_sim p))
with (init:= fun S ⇒ state_inv p S ∧ init p S) (i:= tt); auto.
- eapply soundness_determinate; eauto; decision.
- apply secure_behavioral; auto; apply tsyscall_behavioral.
- apply tsyscall_behavioral.
- simpl; auto.
}
{
eapply (sim_beh_eq _ _ _ _ sim) with (init:= fun S ⇒ state_inv p S ∧ init p S); auto.
- eapply soundness_determinate; eauto; decision.
- apply tsyscall_behavioral.
- apply mboot_behavioral.
- eauto.
}
Qed.
End WITHPRINCIPAL.
End SECURITY.