Merge pull request #38 from OwenConoly/ct2

Leakage Traces

src/riscv/Examples/Example64Literal.v

@@ -46,6 +46,7 @@ Definition zeroedRiscvMachine: RiscvMachine := {|
   getMem := map.empty;
   getXAddrs := nil;
   getLog := nil;
+  getTrace := Some nil;
 |}.
 
 Definition initialRiscvMachine(imem: list MachineInt): RiscvMachine :=

src/riscv/Examples/Fib.v

@@ -57,6 +57,7 @@ Definition zeroedRiscvMachine: RiscvMachine := {|
   getMem := map.empty;
   getXAddrs := nil;
   getLog := nil;
+  getTrace := Some nil;
 |}.
 
 Definition initialRiscvMachine(imem: list MachineInt): RiscvMachine :=

src/riscv/Platform/MaterializeRiscvProgram.v

@@ -1,6 +1,7 @@
 Require Import riscv.Utility.Monads.
 Require Import riscv.Utility.FreeMonad.
 Require Import riscv.Spec.Decode.
+Require Import riscv.Spec.LeakageOfInstr.
 Require Import riscv.Spec.Machine.
 Require Import riscv.Utility.MkMachineWidth.
 Require Import riscv.Utility.Utility.
@@ -27,6 +28,7 @@ Section Riscv.
   | GetPrivMode
   | SetPrivMode (_ : PrivMode)
   | Fence (_ : MachineInt) (_ : MachineInt)
+  | LeakEvent (_ : option LeakageEvent)
   | GetPC
   | SetPC (_ : word)
   | StartCycle
@@ -52,6 +54,7 @@ Section Riscv.
     | GetPrivMode => PrivMode
     | SetPrivMode _ => unit
     | Fence _ _ => unit
+    | LeakEvent _ => unit
     | GetPC => word
     | SetPC _ => unit
     | StartCycle => unit
@@ -84,6 +87,11 @@ Section Riscv.
     endCycleEarly A := act (EndCycleEarly A) ret;
   |}.
 
+  Global Instance MaterializeWithLeakage : RiscvProgramWithLeakage (free riscv_primitive primitive_result) word := {|
+    RVP := Materialize;
+    leakEvent a := act (LeakEvent a) ret
+  |}.
+
   (* Not (yet) in Riscv monad, but added here because it's useful to initialize
      nextPc to pc+4 at the beginning of each cycle instead of having to maintain
      a nextPc=pc+4 invariant everywhere *)

src/riscv/Platform/MetricMaterializeRiscvProgram.v

@@ -39,4 +39,9 @@ Section Riscv.
     endCycleEarly A := act (addMetricInstructions 1, EndCycleEarly A) ret;
   |}.
 
+  Global Instance MetricMaterializeWithLeakage : RiscvProgramWithLeakage (free action result) word := {|
+    RVP := MetricMaterialize;
+    leakEvent a := act (id, LeakEvent a) ret
+  |}.
+
 End Riscv.

src/riscv/Platform/MetricMinimal.v

@@ -66,6 +66,11 @@ Section Riscv.
     endCycleEarly{A} := liftL0 (addMetricInstructions 1) (@endCycleEarly _ _ _ _ _ A);
   }.
 
+  Instance IsMetricRiscvMachineWithLeakage: RiscvProgramWithLeakage (OState MetricRiscvMachine) word := {
+      RVP := IsMetricRiscvMachine;
+      leakEvent := liftL1 id leakEvent;
+  }.
+
   Arguments Memory.load_bytes: simpl never.
   Arguments Memory.store_bytes: simpl never.
 

src/riscv/Platform/MetricRiscvMachine.v

@@ -3,6 +3,7 @@ Require Import coqutil.Map.Interface.
 Require Import coqutil.Word.Interface.
 Require Import coqutil.Word.LittleEndian.
 Require Import riscv.Spec.Decode.
+Require Import riscv.Spec.LeakageOfInstr.
 Require Import riscv.Platform.Memory.
 Require Import riscv.Utility.Utility.
 Require Import riscv.Platform.RiscvMachine.
@@ -58,6 +59,14 @@ Section Machine.
     fun items '(mkMetricRiscvMachine mach mc) =>
       (mkMetricRiscvMachine (withLogItems items mach) mc).
 
+  Definition withLeakageEvent: option LeakageEvent -> MetricRiscvMachine -> MetricRiscvMachine :=
+    fun event '(mkMetricRiscvMachine mach mc) =>
+      (mkMetricRiscvMachine (withLeakageEvent event mach) mc).
+
+  Definition withLeakageEvents: option (list LeakageEvent) -> MetricRiscvMachine -> MetricRiscvMachine :=
+    fun events '(mkMetricRiscvMachine mach mc) =>
+      (mkMetricRiscvMachine (withLeakageEvents events mach) mc).
+
   Definition forgetMetrics(m: MetricRiscvMachine): RiscvMachine := m.(getMachine).
   Definition addMetrics(m: RiscvMachine)(mc: MetricLog): MetricRiscvMachine :=
     mkMetricRiscvMachine m mc.

src/riscv/Platform/MetricSane.v

@@ -4,6 +4,7 @@ Require Import coqutil.Tactics.Tactics.
 Require Import riscv.Spec.Machine.
 Require Import riscv.Utility.Monads.
 Require Import riscv.Spec.Decode.
+Require Import riscv.Spec.LeakageOfInstr.
 Require Import riscv.Utility.Utility.
 Require Import riscv.Spec.Primitives.
 Require Import riscv.Platform.RiscvMachine.
@@ -20,7 +21,7 @@ Section Sane.
   Context {mem: map.map word byte}.
   Context {M: Type -> Type}.
   Context {MM: Monad M}.
-  Context {RVM: RiscvProgram M word}.
+  Context {RVM: RiscvProgramWithLeakage M word}.
   Context {PRParams: PrimitivesParams M MetricRiscvMachine}.
   Context {mcomp_sat_ok: mcomp_sat_spec PRParams}.
 
@@ -151,6 +152,14 @@ Section Sane.
 
   Ltac t := repeat (simpl; unfold when; repeat t_step').
 
+  Lemma leakage_of_instr_sane: forall inst,
+      mcomp_sane (leakage_of_instr getRegister inst).
+  Proof.
+    intros.
+    destruct inst as [inst | inst | inst | inst | inst | inst | inst | inst | inst | inst];
+      simpl; destruct inst; t.
+  Qed.
+
   Lemma execute_sane: forall inst,
       mcomp_sane (Execute.execute inst).
   Proof.
@@ -164,7 +173,10 @@ Section Sane.
   Proof.
     unfold run1. intros.
     apply Bind_sane; [apply getPC_sane|intros].
+    apply Bind_sane; [apply leakEvent_sane|intros].
     apply Bind_sane; [apply loadWord_sane|intros].
+    apply Bind_sane; [apply leakage_of_instr_sane|intros].
+    apply Bind_sane; [apply leakEvent_sane|intros].
     apply Bind_sane; [apply execute_sane|intros].
     apply endCycleNormal_sane.
   Qed.

src/riscv/Platform/Minimal.v

@@ -5,6 +5,7 @@ Require Import Coq.Logic.PropExtensionality.
 Require Import riscv.Utility.Monads. Import OStateOperations.
 Require Import riscv.Utility.MonadNotations.
 Require Import riscv.Spec.Decode.
+Require Import riscv.Spec.LeakageOfInstr.
 Require Import riscv.Spec.Machine.
 Require Import riscv.Utility.Utility.
 Require Import riscv.Spec.Primitives.
@@ -99,6 +100,11 @@ Section Riscv.
          code output by the compiler never throws exceptions *)
       endCycleEarly{A: Type} := fail_hard;
   }.
+
+  Instance IsRiscvMachineWithLeakage: RiscvProgramWithLeakage (OState RiscvMachine) word :=  {
+      RVP := IsRiscvMachine;
+      leakEvent e := update (withLeakageEvent e);
+  }.
 
   Arguments Memory.load_bytes: simpl never.
   Arguments Memory.store_bytes: simpl never.
@@ -116,7 +122,7 @@ Section Riscv.
        | |- _ => reflexivity
        | |- _ => progress (
                      unfold computation_satisfies, computation_with_answer_satisfies,
-                            IsRiscvMachine,
+                            IsRiscvMachine, IsRiscvMachineWithLeakage,
                             valid_register,
                             is_initial_register_value,
                             get, put, fail_hard,
@@ -225,11 +231,18 @@ Section Riscv.
     intros. eapply update_sane. intros. exists [e]. destruct mach. reflexivity.
   Qed.
 
+  Lemma leakEvent_sane: forall e,
+      mcomp_sane (leakEvent e).
+  Proof.
+    intros. eapply update_sane. intros. exists nil. destruct mach. reflexivity.
+  Qed.
+
   Instance MinimalSane: PrimitivesSane MinimalPrimitivesParams.
   Proof.
     constructor.
     all: intros;
-      unfold getRegister, setRegister,
+      unfold IsRiscvMachine, IsRiscvMachineWithLeakage, RVP,
+         getRegister, setRegister,
          loadByte, loadHalf, loadWord, loadDouble,
          storeByte, storeHalf, storeWord, storeDouble,
          getPC, setPC,
@@ -239,6 +252,7 @@ Section Riscv.
 
     all: repeat match goal with
                 | |- _ => apply logEvent_sane
+                | |- _ => apply leakEvent_sane
                 | |- mcomp_sane (Bind _ _) => apply Bind_sane
                 | |- _ => apply Return_sane
                 | |- _ => apply get_sane
@@ -261,4 +275,5 @@ End Riscv.
 
 (* needed because defined inside a Section *)
 #[global] Existing Instance IsRiscvMachine.
+#[global] Existing Instance IsRiscvMachineWithLeakage.
 #[global] Existing Instance MinimalSatisfiesPrimitives.

src/riscv/Platform/MinimalCSRs.v

@@ -99,6 +99,7 @@ Section Riscv.
                             | Machine => postF tt mach
                             | User | Supervisor => False
                             end
+    | LeakEvent _ => fun postF postA => postF tt mach
     | MakeReservation _
     | ClearReservation _
     | CheckReservation _

src/riscv/Platform/MinimalMMIO.v

@@ -4,6 +4,7 @@ Require Import riscv.Utility.Monads.
 Require Import riscv.Utility.MonadNotations.
 Require Export riscv.Utility.FreeMonad.
 Require Import riscv.Spec.Decode.
+Require Import riscv.Spec.LeakageOfInstr.
 Require Import riscv.Spec.Machine.
 Require Import riscv.Utility.Utility.
 Require Import riscv.Spec.Primitives.
@@ -114,6 +115,7 @@ Section Riscv.
         postF tt (withNextPc (word.add mach.(getPc) (word.of_Z 4)) mach)
     | EndCycleNormal => fun postF postA => postF tt (updatePc mach)
     | EndCycleEarly _ => fun postF postA => postA (updatePc mach) (* ignores postF containing the continuation *)
+    | LeakEvent e => fun postF postA => postF tt (withLeakageEvent e mach)
     | MakeReservation _
     | ClearReservation _
     | CheckReservation _

src/riscv/Platform/MinimalMMIO_Post.v

@@ -3,6 +3,7 @@ Require Import Coq.ZArith.ZArith.
 Require Import riscv.Utility.Monads.
 Require Import riscv.Utility.MonadNotations.
 Require Import riscv.Spec.Decode.
+Require Import riscv.Spec.LeakageOfInstr.
 Require Import riscv.Spec.Machine.
 Require Import riscv.Utility.Utility.
 Require Import riscv.Spec.Primitives.
@@ -115,6 +116,11 @@ Section Riscv.
   - exact (post tt (withPc mach.(getNextPc) (withNextPc (word.add mach.(getNextPc) (word.of_Z 4)) mach))).
   Defined.
 
+  Instance IsRiscvMachineWithLeakage: RiscvProgramWithLeakage (Post RiscvMachine) word := {|
+      RVP := IsRiscvMachine;
+      leakEvent e := fun mach post => post tt (withLeakageEvent e mach);
+  |}.
+
   Definition MinimalMMIOPrimitivesParams: PrimitivesParams (Post RiscvMachine) RiscvMachine := {|
     Primitives.mcomp_sat A (m: Post RiscvMachine A) mach post := m mach post;
     Primitives.is_initial_register_value x := True;

src/riscv/Platform/RiscvMachine.v

@@ -1,9 +1,11 @@
 Require Import Coq.Strings.String.
 Require Import Coq.ZArith.BinInt.
+Require Import coqutil.Datatypes.Option.
 Require Import coqutil.Map.Interface.
 Require Import coqutil.Word.Interface.
 Require Import coqutil.Word.LittleEndian.
 Require Import riscv.Spec.Decode.
+Require Import riscv.Spec.LeakageOfInstr.
 Require Import riscv.Platform.Memory.
 Require Import riscv.Utility.Utility.
 
@@ -141,40 +143,51 @@ Section Machine.
       getMem: Mem;
       getXAddrs: XAddrs;
       getLog: list LogItem;
+      getTrace: option (list LeakageEvent);
+      (*^Some x means that only x has been leaked;
+        None means there are no guarantees at all about what has been leaked.*)
     }.
 
     Definition withRegs: Registers -> RiscvMachine -> RiscvMachine :=
-      fun regs2 '(mkRiscvMachine regs1 pc nextPC mem xAddrs log) =>
-                  mkRiscvMachine regs2 pc nextPC mem xAddrs log.
+      fun regs2 '(mkRiscvMachine regs1 pc nextPC mem xAddrs log trace) =>
+                  mkRiscvMachine regs2 pc nextPC mem xAddrs log trace.
 
     Definition withPc: word -> RiscvMachine -> RiscvMachine :=
-      fun pc2 '(mkRiscvMachine regs pc1 nextPC mem xAddrs log) =>
-                mkRiscvMachine regs pc2 nextPC mem xAddrs log.
+      fun pc2 '(mkRiscvMachine regs pc1 nextPC mem xAddrs log trace) =>
+                mkRiscvMachine regs pc2 nextPC mem xAddrs log trace.
 
     Definition withNextPc: word -> RiscvMachine -> RiscvMachine :=
-      fun nextPC2 '(mkRiscvMachine regs pc nextPC1 mem xAddrs log) =>
-                    mkRiscvMachine regs pc nextPC2 mem xAddrs log.
+      fun nextPC2 '(mkRiscvMachine regs pc nextPC1 mem xAddrs log trace) =>
+                    mkRiscvMachine regs pc nextPC2 mem xAddrs log trace.
 
     Definition withMem: Mem -> RiscvMachine -> RiscvMachine :=
-      fun mem2 '(mkRiscvMachine regs pc nextPC mem1 xAddrs log)  =>
-                 mkRiscvMachine regs pc nextPC mem2 xAddrs log.
+      fun mem2 '(mkRiscvMachine regs pc nextPC mem1 xAddrs log trace)  =>
+                 mkRiscvMachine regs pc nextPC mem2 xAddrs log trace.
 
     Definition withXAddrs: XAddrs -> RiscvMachine -> RiscvMachine :=
-      fun xAddrs2 '(mkRiscvMachine regs pc nextPC mem xAddrs1 log)  =>
-                    mkRiscvMachine regs pc nextPC mem xAddrs2 log.
+      fun xAddrs2 '(mkRiscvMachine regs pc nextPC mem xAddrs1 log trace)  =>
+                    mkRiscvMachine regs pc nextPC mem xAddrs2 log trace.
 
     Definition withLog: list LogItem -> RiscvMachine -> RiscvMachine :=
-      fun log2 '(mkRiscvMachine regs pc nextPC mem xAddrs log1) =>
-                 mkRiscvMachine regs pc nextPC mem xAddrs log2.
+      fun log2 '(mkRiscvMachine regs pc nextPC mem xAddrs log1 trace) =>
+                 mkRiscvMachine regs pc nextPC mem xAddrs log2 trace.
 
     Definition withLogItem: LogItem -> RiscvMachine -> RiscvMachine :=
-      fun item '(mkRiscvMachine regs pc nextPC mem xAddrs log) =>
-                 mkRiscvMachine regs pc nextPC mem xAddrs (item :: log).
+      fun item '(mkRiscvMachine regs pc nextPC mem xAddrs log trace) =>
+                 mkRiscvMachine regs pc nextPC mem xAddrs (item :: log) trace.
 
     Definition withLogItems: list LogItem -> RiscvMachine -> RiscvMachine :=
-      fun items '(mkRiscvMachine regs pc nextPC mem xAddrs log) =>
-                  mkRiscvMachine regs pc nextPC mem xAddrs (items ++ log).
+      fun items '(mkRiscvMachine regs pc nextPC mem xAddrs log trace) =>
+                  mkRiscvMachine regs pc nextPC mem xAddrs (items ++ log) trace.
 
+    Definition withLeakageEvent: option LeakageEvent -> RiscvMachine -> RiscvMachine :=
+      fun event '(mkRiscvMachine regs pc nextPC mem xAddrs log trace) =>
+                  mkRiscvMachine regs pc nextPC mem xAddrs log (option_map2 cons event trace).
+
+    Definition withLeakageEvents: option (list LeakageEvent) -> RiscvMachine -> RiscvMachine :=
+      fun events '(mkRiscvMachine regs pc nextPC mem xAddrs log trace) =>
+                   mkRiscvMachine regs pc nextPC mem xAddrs log (option_map2 (@app _) events trace).
+
     Definition Z32s_to_bytes(l: list Z): list byte :=
       List.flat_map (fun z => HList.tuple.to_list (LittleEndian.split 4 z)) l.
 

src/riscv/Platform/Run.v

@@ -3,26 +3,31 @@ Require Import coqutil.Word.LittleEndian.
 Require Import riscv.Utility.Monads.
 Require Import riscv.Utility.MonadNotations.
 Require Import riscv.Spec.Decode.
+Require Import riscv.Spec.LeakageOfInstr.
 Require Import riscv.Platform.Memory. (* should go before Program because both define loadByte etc *)
 Require Import riscv.Spec.Machine.
 Require Import riscv.Spec.Execute.
 Require Import riscv.Utility.Utility.
 
 Section Riscv.
 
-  Context {mword: Type}.
+  Context {width} {BW : Bitwidth width} {mword: word.word width}.
   Context {MW: MachineWidth mword}.
 
   Context {M: Type -> Type}.
   Context {MM: Monad M}.
-  Context {RVP: RiscvProgram M mword}.
+  Context {RVM: RiscvProgramWithLeakage M mword}.
   Context {RVS: RiscvMachine M mword}.
 
   Definition run1(iset: InstructionSet):
     M unit :=
     pc <- getPC;
+    leakEvent (Some (fetchInstr pc));;
     inst <- loadWord Fetch pc;
-    execute (decode iset (combine 4 inst));;
+    let inst' := decode iset (combine 4 inst) in
+    leakage_event <- leakage_of_instr getRegister inst';
+    leakEvent leakage_event;;
+    execute inst';;
     endCycleNormal.
 
   (* Note: We cannot use