Module RTLfault

Fault-aware semantics of RTL

Require Import Coqlib Maps List.
Import ListNotations.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL.

Definition ignore_faults (t: trace) :=
filter (fun e => match e with Event_fault _ => false | _ => true end) t.

Compared to RTL, there is an extra type of state: caught by a countermeasure

Inductive fstate : Type :=
  | Valid: state -> fstate
  | Caught: fstate.

Section RELSEM.

Variable ge: genv.

Inductive fstep: fstate -> trace -> fstate -> Prop :=
| exec_nofault: forall st1 t st2,
    step ge st1 t st2 ->
    fstep (Valid st1) t (Valid st2)
| exec_IbuiltinCatch:
  forall s f sp pc rs m pc',
    (fn_code f)!pc = Some(Ibuiltin EF_cm_catch [] BR_none pc') ->
    fstep (Valid (State s f sp pc rs m)) E0 Caught
| exec_Icond_inverted:
  forall s f sp pc rs m cond args ifso ifnot b pc' predb,
    (fn_code f)!pc = Some(Icond cond args ifso ifnot predb) ->
    eval_condition cond rs##args m = Some b ->
    pc' = (if b then ifnot else ifso) ->
    fstep (Valid (State s f sp pc rs m))
      [Event_fault (Fault_invertcond f)]
      (Valid (State s f sp pc' rs m))
| exec_Icall_skip:
  forall s f sp pc rs m sig id args res pc',
    (fn_code f)!pc = Some(Icall sig (inr id) args res pc') ->
    fstep (Valid (State s f sp pc rs m))
      [Event_fault (Fault_skipcall f id)]
      (Valid (State s f sp pc' rs m))
| exec_Icall_wrong:
  forall s f sp pc rs m sig id args res pc' fd,
    (fn_code f)!pc = Some(Icall sig (inr id) args res pc') ->
    (exists fd, find_function ge (inr id) rs = Some fd /\ funsig fd = sig) ->
    Val.has_argtype_list rs##args (funsig fd).(sig_args) ->
    fstep (Valid (State s f sp pc rs m))
      [Event_fault (Fault_wrongcall f id fd)]
      (Valid (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m))
.

End RELSEM.

Initial states are the same as in RTL

Inductive initial_state (p: program): fstate -> Prop :=
  | initial_state_intro: forall st,
      RTL.initial_state p st ->
      initial_state p (Valid st).

A final state is either Returnstate with an empty call stack, or Caught

Inductive final_state: fstate -> int -> Prop :=
  | final_state_return : forall st r,
      RTL.final_state st r ->
      final_state (Valid st) r
  | final_state_caught :
      final_state Caught (Int.repr 21).

Definition fsemantics (p: program) :=
  Semantics fstep (initial_state p) final_state (Genv.globalenv p).

Security properties, single fault model

A fault f occured at the end of the trace

Inductive last_event_is_fault (f: fault): trace -> Prop :=
| leif_last: last_event_is_fault f [Event_fault f]
| leif_cons: forall hd tl,
    last_event_is_fault f tl ->
    (forall f, hd <> Event_fault f) ->
    last_event_is_fault f (hd::tl).

The invalid state st is caught by program p. No observable events are emitted.

Definition gets_caught (p: program) st :=
  star fstep (Genv.globalenv p) st E0 Caught.

Definition secure_against (p: program) (f: fault) :=
  forall st0 t st,
    RTL.initial_state p st0 ->
    star fstep (Genv.globalenv p) (Valid st0) t st ->
    last_event_is_fault f t ->
    gets_caught p st
    \/ exists st' t',
          star fstep (Genv.globalenv p) st t' (Valid st')
        /\ nofault t'
        /\ star step (Genv.globalenv p) st0 (ignore_faults t ** t') st'.

Some helper lemmas

Lemma Caught_or_not : forall st,
{ st = Caught } + { st <> Caught }.

Proof.

intros []; auto.
all:right; congruence.
Qed.

Lemma Caught_stuck : forall ge t st',
star fstep ge Caught t st' ->
t = E0 /\ st' = Caught.

Proof.

  intros * STEPS.
  inv STEPS; auto.
  inv H.
Qed.

Lemma nofault_ignore_faults : forall t1,
nofault t1 ->
ignore_faults t1 = t1.

Proof.

  induction 1; simpl; auto.
  rewrite IHForall.
  destruct x; auto. congruence.
Qed.

Lemma ignore_faults_app : forall t1 t2,
ignore_faults (t1 ** t2) = ignore_faults t1 ** ignore_faults t2.

Proof.

  induction t1; simpl; auto; intros.
  rewrite IHt1.
  destruct a; auto.
Qed.

Lemma fstep_trace_length : forall ge st t st',
fstep ge st t st' ->
(Datatypes.length t <= 1)%nat.

Proof.

inversion 1; subst; eauto using step_trace_length.
Qed.

Lemma last_event_is_fault_app_inv : forall f t1 t2,
last_event_is_fault f (t1 ** t2) ->
(last_event_is_fault f t1 /\ t2 = []) \/ (nofault t1 /\ last_event_is_fault f t2).

Proof.

  induction t1; intros * FAULT; simpl.
  - right. split; auto. constructor.
  - inv FAULT; [left|].
    + (* now *)
      symmetry in H1. apply app_eq_nil in H1 as (?&?); subst.
      auto using last_event_is_fault.
    + (* later *)
      edestruct IHt1 as [(F1&N2)|(NF1&F2)]; eauto; subst.
      * auto using last_event_is_fault.
      * right; split; auto.
        constructor; auto.
Qed.

reference semantics -> semantics with no fault

Lemma step_fstep : forall ge st t st',
step ge st t st' ->
fstep ge (Valid st) t (Valid st').

Proof.

intros * STEP. now constructor.
Qed.

Lemma step_nofault : forall ge st t st',
step ge st t st' ->
nofault t.

Proof.

intros * STEP; inv STEP;
repeat constructor; eauto using external_call_nofault.
Qed.

semantics with no fault -> reference semantics

Lemma fstep_step : forall ge st t st',
    nofault t ->
    fstep ge (Valid st) t (Valid st') ->
    step ge st t st'.

Proof.

intros * NOFAULT STEP; inv STEP; auto.
1-3:inv NOFAULT; congruence.
Qed.

Require Import Coq.Program.Equality.

Lemma star_fstep_step : forall ge st1 t st2,
    nofault t ->
    star fstep ge (Valid st1) t (Valid st2) ->
    star step ge st1 t st2.

Proof.

  intros * NF STAR.
  dependent induction STAR.
  - constructor.
  - destruct (Caught_or_not s2); subst.
    + exfalso.
      apply Caught_stuck in STAR as (?&?); subst.
      destruct st2; simpl in *; congruence.
    + destruct s2; try congruence.
      apply Forall_app in NF as (?&?).
      econstructor; eauto using fstep_step.
Qed.

Determinacy

Lemma fstep_determinacy : forall ge st t1 st1 t2 st2,
    fstep ge st t1 st1 ->
    fstep ge st t2 st2 ->
    nofault t1 -> nofault t2 ->
    match_traces ge t1 t2 /\ (t1 = t2 -> st1 = st2).

Proof.

  intros * STEP1 STEP2 NF1 NF2; inv STEP1; inv STEP2.
  all:repeat
        match goal with
        | H: step _ (RTL.State _ _ _ _ _ _) _ _ |- _ => inv H
        | H1: ?x = _, H2: ?x = _ |- _ => rewrite H1 in H2; inv H2
        | H: nofault [_] |- _ => inv H; congruence
        end; auto using match_traces.
  - eapply step_determinacy with (t1:=t1) in H1 as (M&E); eauto.
    split; auto; intros; subst.
    specialize (E eq_refl); subst; auto.
  - inv H11.
  - inv H11.
Qed.

Lemma star_determinacy : forall ge st0 st1,
    star fstep ge st0 E0 st1 ->
    forall st2 t2,
      nofault t2 ->
      star fstep ge st0 t2 st2 ->
      star fstep ge st1 t2 st2 \/ (star fstep ge st2 t2 st1 /\ t2 = E0).

Proof.

  intros * STAR1. dependent induction STAR1; auto.
  symmetry in H0; apply app_eq_nil in H0 as (?&?); subst.
  intros * NF2 STAR2; auto.
  inv STAR2.
  - right. split; auto. eapply star_step; eauto.
  - (* symmetry in H2; apply app_eq_nil in H2 as (?&?); subst. *)
    assert (s4 = s2 /\ t1 = []) as (?&?); subst; simpl in *.
    { apply Forall_app in NF2 as (?&?).
      eapply fstep_determinacy in H as (MATCH&EQ); eauto. 2:constructor.
      inv MATCH. auto. }
    apply IHSTAR1; auto.
Qed.