Module IPCFCsecurity


Proof of security of the CFC counter-measure

Require Import Coqlib List Maps Integers.
Import ListNotations.
Require Import AST Linking Smallstep Events.
Require Import Globalenvs Values Kildall.
Require Import Op Registers Memory RTL.
Require Import CounterMeasures IPCFC IPCFCproof.
Require Import RTLtyping RTLpast RTLfault.

Lemma harden_name_ok : forall id,
    qualident_eq_prefix id ipcfc_pre = true ->
    exists id', harden_name id' = Errors.OK id.
Proof.
  intros * EQPREF.
  unfold qualident_eq_prefix, ident_eq in *.
  destruct id as ([|? []]&BOUNDED); simpl in *; try congruence.
  destruct (peq _ _); inv EQPREF. apply negb_true_iff in H0.
  assert (QualIdent.bounded_length (i0::l)) as BOUNDED'.
  { unfold QualIdent.bounded_length in *. simpl in *.
    rewrite Nat.leb_le in *. lia. }
  exists (exist _ (i0 :: l) BOUNDED').
  unfold harden_name; simpl.
  destruct (prefix_qualident_ok (exist _ (i0::l) BOUNDED') ipcfc_pre) as (((?&?)&?&?)&EQ); simpl in *; subst.
  - unfold QualIdent.bounded_length, QualIdent.depth in *. simpl in *.
    clear - BOUNDED. rewrite Nat.leb_le in BOUNDED. lia.
  - unfold qualident_eq_prefix'. simpl. now setoid_rewrite H0.
  - rewrite EQ; simpl.
    repeat f_equal. apply QualIdent.bounded_length_proofs_unicity.
Qed.

Section IPCFC.

Variable prog: program.
Variable tprog: program.
Hypothesis TRANSL: IPCFC.match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

id is the name of an init function
Definition is_init id :=
  ~qualident_prefixed id ipcfc_pre /\ (protected prog)!.id <> None.

id is the name of a protected function
Definition is_protected id :=
  exists id', harden_name id' = Errors.OK id /\ (protected prog)!.id' <> None.

id is either the name of an initialization or protected function
Definition is_init_or_protected id := is_init id \/ is_protected id.

Ltac simpl_equalities :=
  repeat
    match goal with
    | H1: ?x = Some _, H2: ?x = Some _ |- _ =>
        rewrite H1 in H2; inv H2
    | H1: ?x = Errors.OK _, H2: ?x = Errors.OK _ |- _ =>
        rewrite H1 in H2; inv H2
    end.

Static specification

Hint Unfold prot_prologue transf_call transf_return : rtlcm.

Lemma transf_code_call_inv id f f' env : forall pc sig qi rs r pc1,
    wt_function f env ->
    (transf_function_init_prot id f = Errors.OK f' \/ transf_function_prot (protected prog) id f = Errors.OK f') ->
    (fn_code f')!pc = Some (Icall sig (inr qi) rs r pc1) ->
    ((protected prog)!.qi = None -> exists qi', harden_name qi' = Errors.OK qi) ->
    (exists pcf abort sig' qi' rs' e s' k,
        spec_seq_inv (fun pc => pc <> fn_entrypoint f') abort (fn_code f')
          pc (Icall sig (inr qi) rs r pc1)
          pcf (@transf_call' (gsr f) (gsrv f) (tmp1 f) e sig' qi' rs' r s') k
        /\ (forall pcf k cs' pc, concretized pcf s' k cs' -> ~in_cseq abort pc (Icall sig (inr qi) rs r pc1) cs')
        /\ (fn_code f')!abort = Some (Ibuiltin EF_cm_catch [] BR_none abort)).
Proof.
  intros * WT [TR|TR] FIND PROTHARD.
  - (* init prot *)
    unfold transf_function_init_prot, transf_init_prot in *.
    destruct (harden_name id); simpl in *; inv TR.
    destruct (check_params _ _) eqn:PARAMS; simpl in *; inv H0.
    remember (transf_replace_function _ _) as code'; simpl. symmetry in Heqcode'.
    eapply transf_replace_function_inv in Heqcode' as (?&ABORT&SPEC); eauto.
    2:{ repeat constructor. }
    destruct SPEC as [SPEC|EQ]; [|inv EQ].
    inv_transf_function; subst.
    repeat (esplit; eauto).
    + repeat econstructor.
    + simpl. repeat (econstructor; eauto).
    + simpl. repeat esplit; eauto.
      instantiate (1:=xH). instantiate (1:=fun _ => Ireturn _). simpl; eauto.
    + intros * CONC. inv_transf_function.
  - (* prot *)
    unfold transf_function_prot in TR.
    destruct (harden_name id); simpl in *; [|inv TR].
    destruct transf_partial_function as [(?&?)|] eqn:TR'; inv TR. simpl in *.
    eapply transf_partial_function_inv in TR'; eauto.
    3-12:(intros * EQ; autounfold with rtlcm in *; cases; repeat pMonadInv;
          repeat constructor).
    2:{ repeat constructor. }
    2:{ intros ??? EQ0; inv EQ0. }
    inv_transf_function; try congruence.
    cases_eq.
    + pMonadInv; inv_transf_function.
    + apply Errors.bind_inversion in H1 as (?&MON&OK); inv OK.
      assert (sig = transf_sig x0 /\ x3 = r) as (?&?); subst.
      { inv_transf_function. }
      repeat (esplit; eauto).
      intros * CONC. clear - CONC. inv_transf_function.
    + inv_transf_function. exfalso.
      specialize (PROTHARD EQ0) as (?&HARD').
      eapply harden_name_not_twice; eauto.
Qed.


Lemma find_funct_translated_inv_prot:
  forall v tf,
    (forall id, In (id, Gfun (Internal tf)) (prog_defs tprog) -> is_protected id) ->
    Genv.find_funct tge v = Some (Internal tf) ->
    exists id' v' f,
      Genv.find_funct ge v' = Some (Internal f)
      /\ transf_function_prot (protected prog) id' f = Errors.OK tf.
Proof.
  intros * PROT FUNC'. inversion TRANSL.
  unfold Genv.find_funct, Genv.find_funct_ptr in *.
  cases_eq; subst; inv FUNC'.
  eapply Genv.find_def_inversion in EQ1 as (id&INDEF).
  assert ((prog_defmap tprog)!.id = Some (Gfun (Internal tf))) as DEFMAP.
  { subst ge. eapply prog_defmap_norepet; eauto. }
  eapply PROT in INDEF as (?&HARD&TR).
  specialize (match_prog_def x) as DM.
  inv DM; try congruence; simpl_equalities.
  + eapply match_prog_inv in DEFMAP as (?&?); eauto. congruence.
  + exfalso. eapply harden_name_not_twice; eauto.
  + eapply match_prog_inv in DEFMAP as (?&?); eauto. congruence.
  + apply Genv.find_def_symbol in H1 as (?&SYMB'&FUNC').
    unfold ge. repeat (esplit; eauto).
    instantiate (1:=Vptr x0 Ptrofs.zero); simpl. rewrite EQ0. now setoid_rewrite FUNC'.
Qed.

Lemma find_funct_translated_inv:
  forall v tf,
    (forall id, In (id, Gfun (Internal tf)) (prog_defs tprog) -> is_init_or_protected id) ->
    Genv.find_funct tge v = Some (Internal tf) ->
    exists id' v' f,
      Genv.find_funct ge v' = Some (Internal f)
      /\ (transf_function_init_prot id' f = Errors.OK tf
         \/ transf_function_prot (protected prog) id' f = Errors.OK tf).
Proof.
  intros * PROT FUNC'. inversion TRANSL.
  unfold Genv.find_funct, Genv.find_funct_ptr in *.
  cases_eq; subst; inv FUNC'.
  eapply Genv.find_def_inversion in EQ1 as (id&INDEF).
  assert ((prog_defmap tprog)!.id = Some (Gfun (Internal tf))) as DEFMAP.
  { subst ge. eapply prog_defmap_norepet; eauto. }
  apply PROT in INDEF as [(EQPREF&TR)|(id'&EQPREF&TR)].
  - (* is the init prot function *)
    specialize (match_prog_def id) as DM.
    inv DM; try congruence; simpl_equalities.
    + exfalso. eapply harden_name_qualident_prefix in H0; eauto.
    + apply Genv.find_def_symbol in H1 as (?&SYMB'&FUNC').
      unfold ge. repeat esplit; eauto.
      instantiate (1:=Vptr x Ptrofs.zero); simpl. rewrite EQ0. now setoid_rewrite FUNC'.
  - (* is the protected function *)
    specialize (match_prog_def id') as DM.
    inv DM; try congruence; simpl_equalities.
    + eapply match_prog_inv in DEFMAP as (?&?); eauto. congruence.
    + exfalso. eapply harden_name_not_twice; eauto.
    + eapply match_prog_inv in DEFMAP as (?&?); eauto. congruence.
    + apply Genv.find_def_symbol in H1 as (?&SYMB'&FUNC').
      unfold ge. repeat (esplit; eauto).
      instantiate (1:=Vptr x Ptrofs.zero); simpl. rewrite EQ0. now setoid_rewrite FUNC'.
Qed.

Lemma find_funct_ptr_translated_inv_init:
  forall id b tf,
    is_init id ->
    Genv.find_symbol tge id = Some b ->
    Genv.find_funct_ptr tge b = Some (Internal tf) ->
    exists b' f,
      Genv.find_symbol ge id = Some b'
      /\ Genv.find_funct_ptr ge b' = Some (Internal f)
      /\ transf_function_init_prot id f = Errors.OK tf.
Proof.
  intros * (EQPREF&TR) SYMB FUNC'. inversion TRANSL.
  unfold Genv.find_funct_ptr in *.
  destruct (Genv.find_def _ _) as [[|]|] eqn:FUNC; inv FUNC'.
  assert ((prog_defmap tprog)!.id = Some (Gfun (Internal tf))) as DEFMAP.
  { subst ge. apply Genv.find_def_symbol. eauto. }
  specialize (match_prog_def id) as DM.
  inv DM; try congruence; simpl_equalities.
  + exfalso. eapply harden_name_qualident_prefix in H0; eauto.
  + apply Genv.find_def_symbol in H1 as (?&SYMB'&FUNC').
    unfold ge. repeat esplit; eauto. now setoid_rewrite FUNC'.
Qed.

Lemma find_funct_ptr_translated_inv_prot:
  forall id b tf,
    is_protected id ->
    Genv.find_symbol tge id = Some b ->
    Genv.find_funct_ptr tge b = Some (Internal tf) ->
    exists id' b' f,
      Genv.find_symbol ge id' = Some b'
      /\ Genv.find_funct_ptr ge b' = Some (Internal f)
      /\ harden_name id' = Errors.OK id
      /\ transf_function_prot (protected prog) id' f = Errors.OK tf.
Proof.
  intros * (?&HARD&TR) SYMB FUNC'. inversion TRANSL.
  unfold Genv.find_funct_ptr in *.
  destruct (Genv.find_def _ _) as [[|]|] eqn:FUNC; inv FUNC'.
  assert ((prog_defmap tprog)!.id = Some (Gfun (Internal tf))) as DEFMAP.
  { subst ge. apply Genv.find_def_symbol. eauto. }
  specialize (match_prog_def x) as DM.
  inv DM; try congruence; simpl_equalities.
  + eapply match_prog_inv in DEFMAP as (?&?); eauto. congruence.
  + exfalso. eapply harden_name_not_twice; eauto.
  + eapply match_prog_inv in DEFMAP as (?&?); eauto. congruence.
  + apply Genv.find_def_symbol in H1 as (?&SYMB'&FUNC').
    unfold ge. repeat (esplit; eauto). now setoid_rewrite FUNC'.
Qed.

Corollary find_funct_ptr_translated_inv:
  forall id b tf,
    is_init_or_protected id ->
    Genv.find_symbol tge id = Some b ->
    Genv.find_funct_ptr tge b = Some (Internal tf) ->
    exists id' b' f,
      Genv.find_symbol ge id' = Some b'
      /\ Genv.find_funct_ptr ge b' = Some (Internal f)
      /\ ((id' = id /\ transf_function_init_prot id' f = Errors.OK tf)
         \/ (harden_name id' = Errors.OK id /\ transf_function_prot (protected prog) id' f = Errors.OK tf)).
Proof.
  intros * [|] SYMB FUNCT.
  - eapply find_funct_ptr_translated_inv_init in SYMB as (?&?&?&?&?); eauto 8.
  - eapply find_funct_ptr_translated_inv_prot in SYMB as (?&?&?&?&?&?&?); eauto 8.
Qed.

Hypothesis WT: wt_program prog.

Tactic Notation "star_step" int_or_var(n) :=
  do n (try (eapply star_left; eauto using Eapp_E0)); try apply star_refl.

Opaque transf_function.

Ltac extlia := unfold Mem.valid_block, tmp2, tmp1, rts, gsrv, gsr in *; Coqlib.extlia.

Ltac inv_equalities :=
  match goal with
  | H: Some _ = Some _ |- _ => inv H
  | H1: ?x = Some _, H2: ?x = Some _ |- _ => rewrite H2 in H1; inv H1
  end.

Ltac inv_gsr :=
  simpl in *;
  repeat
    match goal with
    | H: list_forall2 _ _ _ |- _ => inv H
    | H: eval_assert_arg _ _ _ _ _ _ |- _ => inv H
    | H: Val.cmp_bool Ceq ?v1 ?v2 = Some true |- _ =>
        destruct v1 eqn:V1, v2 eqn:V2; simpl in H; inversion H as [EQ];
        apply Int.same_if_eq in EQ; subst; auto
    | H: eval_addressing _ _ _ _ = _ |- _ => simpl in H; inv H
    | _ => unfold eval_assert_args in *
    end;
  repeat inv_equalities.


Proof of robustness against call skip


Lemma fault_step_skip: forall st0 t0 st1 st2 (f: function) id,
    (forall id, In (id, Gfun (Internal f)) (prog_defs tprog) -> is_init_or_protected id) ->
    (exists f, In (id, Gfun (Internal f)) (prog_defs tprog) /\ is_init_or_protected id) ->
    RTL.initial_state tprog st0 ->
    star step tge st0 t0 st1 ->
    fstep tge (Valid st1) [Event_fault (Fault_skipcall f id)] st2 ->
    gets_caught tprog st2
    \/ (exists (st' : RTL.state) (t' : trace),
          star fstep tge st2 t' (Valid st') /\ nofault t' /\ star step tge st1 t' st').
Proof.
  intros * CALLERPROT (f'&CALLEEIN&CALLEEPROT) INIT STEPS FSTEP.
  inv FSTEP.
  1:{ apply step_nofault in H0. inv H0.
      specialize (H2 _ eq_refl). inv H2. }
  apply Eqdep.EqdepTheory.inj_pair2 in H0; subst.
  assert (exists b ros, find_function tge b ros = Some (Internal f)) as (?&?&FIND).
  { subst tge.
    eapply steps_has_function in STEPS; eauto. simpl; auto. }
  assert (exists id' f0 env,
             (transf_function_init_prot id' f0 = Errors.OK f \/ transf_function_prot (protected prog) id' f0 = Errors.OK f)
             /\ wt_function f0 env) as (?&?&env&TR&WTF).
  { destruct x; simpl in *.
    - apply find_funct_translated_inv in FIND as (?&?&?&FIND'&TR); eauto.
      apply Genv.find_funct_inversion in FIND' as (?&DEF).
      apply WT in DEF. inv DEF.
      do 4 esplit; eauto.
    - cases_eq; [|inv FIND].
      eapply find_funct_ptr_translated_inv in EQ as (?&?&?&SYMB'&FIND'&TR); eauto.
      2:{ eapply CALLERPROT, in_prog_defmap, Genv.find_def_symbol. do 2 esplit; eauto.
          unfold Genv.find_funct_ptr in *. cases_eq; inv FIND; eauto. }
      apply Genv.find_funct_ptr_inversion in FIND' as (?&DEF).
      apply WT in DEF. inv DEF.
      do 4 esplit; eauto. intuition eauto.
  }
  eapply transf_code_call_inv in TR; eauto.
  2:{ intros NPROT.
      destruct CALLEEPROT as [(?&?)|(?&?&?)]; try congruence; eauto.
  }
  inv_transf_function.
  2:{ exfalso. eapply H0; eauto. }
  do 2 step_back. inv_equalities. inv_gsr.

  left. star_step 5; simpl.
  - eapply step_fstep, exec_Iload; eauto.
    eapply has_loaded_normal; simpl; eauto.
    rewrite Regmap.gso; try extlia. eauto.
  - eapply step_fstep, exec_Iop; eauto; simpl.
    rewrite Regmap.gss.
    eauto.
  - eapply step_fstep, exec_Icond; eauto; simpl.
    rewrite Regmap.gss, ? Regmap.gso; try extlia.
    rewrite V2. simpl.
    instantiate (1:=true). f_equal.
    apply negb_true_iff, Int.eq_false. intros EQ; subst.
    eapply match_prog_sigs_nzero; eauto using Int.xor_zero_inv.
  - eapply step_fstep, exec_Inop; eauto.
  - econstructor; eauto.
Qed.

Theorem transf_program_secure_skip f id:
  (forall id, In (id, Gfun (Internal f)) (prog_defs tprog) -> is_init_or_protected id) ->
  (exists f, In (id, Gfun (Internal f)) (prog_defs tprog) /\ is_init_or_protected id) ->
  (protected prog)!.id <> None ->
  secure_against tprog (Fault_skipcall f id).
Proof.
  intros PROTCALLER PROTCALLEE ??? INIT FSTEP FAULT.
  eapply protected_multi_step with (t1:=E0); eauto using fault_step_skip.
  constructor.
Qed.

Proof of robustness against wrong call


Lemma fault_step_wrong : forall st0 t0 st1 st2 (f: function) id f',
    (forall id, In (id, Gfun (Internal f)) (prog_defs tprog) -> is_init_or_protected id) ->
    (exists f, In (id, Gfun (Internal f)) (prog_defs tprog) /\ is_init_or_protected id) ->
    (exists id, In (id, Gfun (Internal f')) (prog_defs tprog) /\ is_protected id) ->
    RTL.initial_state tprog st0 ->
    star step tge st0 t0 st1 ->
    fstep tge (Valid st1) [Event_fault (Fault_wrongcall f id (Internal f'))] st2 ->
    gets_caught tprog st2
    \/ (exists (st' : RTL.state) (t' : trace),
          star fstep tge st2 t' (Valid st') /\ nofault t' /\ star step tge st1 t' st').
Proof.
  intros * CALLERPROT (f'&CALLEEIN&CALLEEPROT) (id&INDEFS&PROT) INIT STEPS FSTEP.
  inv FSTEP.
  1:{ apply step_nofault in H0. inv H0.
      specialize (H2 _ eq_refl). inv H2. }
  apply Eqdep.EqdepTheory.inj_pair2 in H0; subst.
  assert (exists b ros, find_function tge b ros = Some (Internal f)) as (?&?&FIND).
  { subst tge.
    eapply steps_has_function in STEPS; eauto. simpl; auto. }
  assert (exists id' f0 env,
             (transf_function_init_prot id' f0 = Errors.OK f \/ transf_function_prot (protected prog) id' f0 = Errors.OK f)
             /\ wt_function f0 env) as (?&?&env&TR&WTF).
  { clear H5. destruct x; simpl in *.
    - apply find_funct_translated_inv in FIND as (?&?&?&FIND'&TR); eauto.
      apply Genv.find_funct_inversion in FIND' as (?&DEF).
      apply WT in DEF. inv DEF.
      do 4 esplit; eauto.
    - cases_eq; [|inv FIND].
      eapply find_funct_ptr_translated_inv in EQ as (?&?&?&SYMB'&FIND'&TR); eauto.
      2:{ eapply CALLERPROT, in_prog_defmap, Genv.find_def_symbol. do 2 esplit; eauto.
          unfold Genv.find_funct_ptr in *. cases_eq; inv FIND; eauto. }
      apply Genv.find_funct_ptr_inversion in FIND' as (?&DEF).
      apply WT in DEF. inv DEF.
      do 4 esplit; eauto. intuition eauto.
  }
  eapply transf_code_call_inv in TR; eauto.
  2:{ intros NPROT.
      destruct CALLEEPROT as [(?&?)|(?&?&?)]; try congruence; eauto. }
  inv_transf_function.
  2:{ exfalso. eapply H1; eauto. }

  assert (exists id1 f0,
             In (id1, (Gfun (Internal f0))) (prog_defs prog)
             /\ harden_name id1 = Errors.OK id
             /\ transf_function_prot (protected prog) id1 f0 = Errors.OK f'0) as (?&?&INDEFS'&HARD&TR).
  { apply prog_defmap_norepet in INDEFS; eauto using IPCFC.match_prog_norepet2.
    apply Genv.find_def_symbol in INDEFS as (?&SYMB&DEF).
    eapply find_funct_ptr_translated_inv_prot in SYMB as (?&?&?&SYMB'&DEF'&HARD&TR); eauto.
    2:{ unfold Genv.find_funct_ptr, tge. now rewrite DEF. }
    repeat (esplit; eauto).
    eapply in_prog_defmap, Genv.find_def_symbol. repeat (esplit; eauto).
    unfold Genv.find_funct_ptr, ge in *. cases; inv DEF'; auto.
  }
  apply transf_prot_params in TR as PARAMS.
  apply transf_prot_sig in TR as SIG.
  eapply transf_prot_entry in TR; eauto. inv_transf_function.

  do 2 step_back. inv_equalities. inv_gsr.
  destruct (rs0 # (gsr x2)) eqn:GSRP; simpl in *; try now inv LOAD.

  destruct (QualIdent.eq x4 id); subst.
  - (* same function *) right.
    repeat esplit.
    + star_step 1.
      eapply step_fstep, exec_function_internal; eauto using surjective_pairing.
    + constructor.
    + assert (f' = f'0); subst.
      { destruct TRANSL.
        eapply list_norepet_fst_In with (y1:=Gfun (Internal f')) in match_prog_norepet2; eauto.
          now inv match_prog_norepet2. }
      assert (x9 = Internal f'0); subst.
      { eapply prog_defmap_norepet, Genv.find_def_symbol in INDEFS as (?&SYMB&DEF);
          eauto using IPCFC.match_prog_norepet2.
        unfold tge, Genv.find_funct_ptr in H0. rewrite SYMB, DEF in H0. congruence.
      }
      eapply prog_defmap_norepet, Genv.find_def_symbol in INDEFS as (?&SYMB&DEF); eauto using IPCFC.match_prog_norepet2.
      star_step 2.
      * eapply exec_Icall; eauto.
      * simpl. eapply exec_function_internal; eauto using surjective_pairing.
  - (* different function *) left.
  star_step 6; simpl.
  + eapply step_fstep, exec_function_internal; eauto using surjective_pairing.
  + eapply step_fstep, exec_Iload; eauto; simpl.
    eapply has_loaded_normal; simpl.
    * rewrite PARAMS; simpl. now (rewrite Regmap.gss, Regmap.gso; try extlia).
    * rewrite GSRP; simpl.
      eapply Mem.load_alloc_other; eauto using surjective_pairing.
  + eapply step_fstep, exec_Iop; eauto; simpl.
    rewrite PARAMS; simpl. rewrite Regmap.gss, 2 Regmap.gso, 2 Regmap.gss; try extlia.
    simpl. rewrite <-Int.xor_assoc, Int.xor_idem, Int.xor_zero_l; auto.
  + eapply step_fstep, exec_Icond; eauto.
    simpl. rewrite Regmap.gss; simpl.
    rewrite Int.eq_false; simpl; eauto.
    intros EQ. eapply match_prog_sigs_inj in EQ; eauto.
  + eapply step_fstep, exec_Inop; eauto.
  + eapply exec_IbuiltinCatch; eauto.
Qed.

Theorem transf_program_secure_wrong f id f':
  (forall id, In (id, Gfun (Internal f)) (prog_defs tprog) -> is_init_or_protected id) ->
  (exists f, In (id, Gfun (Internal f)) (prog_defs tprog) /\ is_init_or_protected id) ->
  (exists id, In (id, Gfun (Internal f')) (prog_defs tprog) /\ is_protected id) ->
  (protected prog)!.id <> None ->
  secure_against tprog (Fault_wrongcall f id (Internal f')).
Proof.
  intros PROTCALLER PROTCALLEE ??? INIT FSTEP FAULT.
  eapply protected_multi_step with (t1:=E0); eauto using fault_step_wrong.
  constructor.
Qed.

End IPCFC.
Generated by coq2html