Leakage Traces

src/riscv/Platform/MaterializeRiscvProgram.v

@@ -27,6 +27,7 @@ Section Riscv.
   | GetPrivMode
   | SetPrivMode (_ : PrivMode)
   | Fence (_ : MachineInt) (_ : MachineInt)
+  | LeakEvent (_ : LeakageEvent)
   | GetPC
   | SetPC (_ : word)
   | StartCycle
@@ -52,6 +53,7 @@ Section Riscv.
     | GetPrivMode => PrivMode
     | SetPrivMode _ => unit
     | Fence _ _ => unit
+    | LeakEvent _ => unit
     | GetPC => word
     | SetPC _ => unit
     | StartCycle => unit
@@ -84,6 +86,11 @@ Section Riscv.
     endCycleEarly A := act (EndCycleEarly A) ret;
   |}.
 
+  Global Instance MaterializeWithLeakage : RiscvProgramWithLeakage := {|
+    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/MetricMinimal.v

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

src/riscv/Platform/MetricRiscvMachine.v

@@ -58,6 +58,14 @@ Section Machine.
     fun items '(mkMetricRiscvMachine mach mc) =>
       (mkMetricRiscvMachine (withLogItems items mach) mc).
 
+  Definition withLeakageEvent: LeakageEvent -> MetricRiscvMachine -> MetricRiscvMachine :=
+    fun event '(mkMetricRiscvMachine mach mc) =>
+      (mkMetricRiscvMachine (withLeakageEvent event mach) mc).
+
+  Definition withLeakageEvents: 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

@@ -20,7 +20,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}.
   Context {PRParams: PrimitivesParams M MetricRiscvMachine}.
   Context {mcomp_sat_ok: mcomp_sat_spec PRParams}.
 
@@ -151,6 +151,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.
@@ -165,6 +173,8 @@ Section Sane.
     unfold run1. intros.
     apply Bind_sane; [apply getPC_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

@@ -98,6 +98,11 @@ Section Riscv.
       (* fail hard if exception is thrown because at the moment, we want to prove that
          code output by the compiler never throws exceptions *)
       endCycleEarly{A: Type} := fail_hard;
+    }.
+
+  Instance IsRiscvMachineWithLeakage: @RiscvProgramWithLeakage _ _ _ (OState RiscvMachine) _ _ _ :=  {
+      RVP := IsRiscvMachine;
+      leakEvent e := fail_hard;
   }.
 
   Arguments Memory.load_bytes: simpl never.
@@ -116,7 +121,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,
@@ -229,7 +234,8 @@ Section Riscv.
   Proof.
     constructor.
     all: intros;
-      unfold getRegister, setRegister,
+      unfold IsRiscvMachine, IsRiscvMachineWithLeakage, RVP,
+         getRegister, setRegister,
          loadByte, loadHalf, loadWord, loadDouble,
          storeByte, storeHalf, storeWord, storeDouble,
          getPC, setPC,
@@ -261,4 +267,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 _ 
     | MakeReservation _
     | ClearReservation _
     | CheckReservation _

src/riscv/Platform/MinimalMMIO.v

@@ -114,6 +114,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

@@ -115,6 +115,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) _ _ _ := {|
+      RVP := IsRiscvMachine;
+      leakEvent _ := fun _ _ => False;
+  |}.
+
   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

@@ -141,40 +141,49 @@ Section Machine.
       getMem: Mem;
       getXAddrs: XAddrs;
       getLog: list LogItem;
+      getTrace: list LeakageEvent;
     }.
 
     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: LeakageEvent -> RiscvMachine -> RiscvMachine :=
+      fun event '(mkRiscvMachine regs pc nextPC mem xAddrs log trace) =>
+                 mkRiscvMachine regs pc nextPC mem xAddrs log (event :: trace).
+
+    Definition withLeakageEvents: list LeakageEvent -> RiscvMachine -> RiscvMachine :=
+      fun events '(mkRiscvMachine regs pc nextPC mem xAddrs log trace) =>
+                 mkRiscvMachine regs pc nextPC mem xAddrs log (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

@@ -10,19 +10,22 @@ 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}.
   Context {RVS: RiscvMachine M mword}.
 
   Definition run1(iset: InstructionSet):
     M unit :=
     pc <- getPC;
     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