HMAC-SHA-256 on PPC64LE: verified init/finalize

README.md

@@ -279,7 +279,7 @@ yours to keep:
 
 <td>✅</td>
 
-<td>❌</td>
+<td>✅</td>
 
 </tr>
 

bench/benches/primitives/hmac_sha256.rs

@@ -9,20 +9,6 @@ use verified_garbage::hmac::Hmac;
 /// `ci/bench_arches.py`): this one and those it calls.
 pub const USES: &[&str] = &["hmac_sha256", "sha256"];
 
-#[cfg(not(any(
-    target_arch = "x86_64",
-    target_arch = "aarch64",
-    target_arch = "arm",
-    target_arch = "x86"
-)))]
-pub fn bench(_: &mut Criterion) {}
-
-#[cfg(any(
-    target_arch = "x86_64",
-    target_arch = "aarch64",
-    target_arch = "arm",
-    target_arch = "x86"
-))]
 pub fn bench(c: &mut Criterion) {
     crate::hmac_group(
         c,

lean/VerifiedGarbage/Artifacts/Ct/PPC64LE.lean

@@ -0,0 +1,14 @@
+import VerifiedGarbage.Proof.Ct.PPC64LE
+
+namespace VG.Artifacts.Ct.PPC64LE
+open VG.PPC64LE
+
+def artifacts : List Artifact := [
+  { Spec.Ct.eqApi with
+    target := target
+    doc := Spec.Ct.eqApi.doc
+    code := Impl.Ct.PPC64LE.eq
+    contract := Spec.Ct.eqContract abi
+    verified := Proof.Ct.PPC64LE.verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ }]
+end VG.Artifacts.Ct.PPC64LE

lean/VerifiedGarbage/Artifacts/HmacSha256/PPC64LE.lean

@@ -0,0 +1,37 @@
+import VerifiedGarbage.TCB.PPC64LE.Target
+import VerifiedGarbage.Proof.Hmac.PPC64LE.Shared
+
+/-!
+# HMAC-SHA-256 (RFC 2104) on PPC64LE
+
+A registration file (see `TCB/Emit.lean`): the artifacts it lists are
+emitted. **Review note**: `sig` and `doc` are trusted, as they tie the Rust
+caller to the contract; check them against the contract's `pre`/`post`. An
+artifact made from a function's `Api` (in `Spec/`, reviewed with the
+contract) takes them from there, and this file adds only notes on the
+implementation. The emitter adds the `# Safety` items that depend on the
+target (`Sig.layoutDoc`), from `stack` and `writeArgs`, which `ofSig` checks
+against the contract.
+-/
+
+namespace VG.Artifacts.HmacSha256.PPC64LE
+
+def artifacts : List Artifact := [
+  { Spec.Hmac.initSha256Api with
+    target := PPC64LE.target
+    doc := Spec.Hmac.initSha256Api.doc
+    code := Impl.Hmac.PPC64LE.init
+    contract := Spec.Hmac.initSha256Contract PPC64LE.abi 48
+    stack := 48
+    verified := Proof.Hmac.PPC64LE.Shared.init
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.Hmac.finalizeSha256Api with
+    target := PPC64LE.target
+    doc := Spec.Hmac.finalizeSha256Api.doc
+    code := Impl.Hmac.PPC64LE.finalize
+    contract := Spec.Hmac.finalizeSha256Contract PPC64LE.abi 96
+    stack := 96
+    verified := Proof.Hmac.PPC64LE.Shared.finalize
+    spSafe := Code.all_of_forall (fun _ => rfl) _ }]
+
+end VG.Artifacts.HmacSha256.PPC64LE

lean/VerifiedGarbage/Impl/Ct/PPC64LE.lean

@@ -0,0 +1,32 @@
+import VerifiedGarbage.TCB.PPC64LE.Isa
+
+/-!
+# Constant-time byte comparison on PPC64LE
+
+`vg_ct_eq(a = r3, a_len = r4, b = r5, b_len = r6)`: the same algorithm as
+the AArch64 implementation (`VG.Impl.Ct.AArch64`). The lengths are compared
+first; if they are equal, the XORs of the bytes at each offset are ORed
+together into `r7`, and the result is `(r7 - 1) >> 63`, which is 1 iff `r7`
+is zero. The branches are on the lengths only.
+-/
+
+namespace VG.Impl.Ct.PPC64LE
+open VG.PPC64LE
+
+def step : List Instr := [
+  .add .r10 .r3 .r8, .lbz .r11 .r10 0,
+  .add .r10 .r5 .r8, .lbz .r12 .r10 0,
+  .logic .xor .r11 .r11 .r12, .logic .or .r7 .r7 .r11,
+  .addi .r8 .r8 1, .sub .r9 .r8 .r4]
+
+def finish : Prog isa := .block [.subi .r7 .r7 1, .lsr .d .r3 .r7 63]
+
+def equal : Prog isa :=
+  .seq (.block [.li .r8 0])
+    (.seq (.ite (.zero .d .r4) (.block []) (.loop (.block step) (.nonzero .d .r9))) finish)
+
+def eq : Prog isa :=
+  .seq (.block [.li .r7 0, .sub .r9 .r4 .r6])
+    (.ite (.zero .d .r9) equal (.block [.li .r3 0]))
+
+end VG.Impl.Ct.PPC64LE

lean/VerifiedGarbage/Impl/Hmac/PPC64LE.lean

@@ -0,0 +1,119 @@
+import VerifiedGarbage.Impl.Sha256.PPC64LE.Stream
+
+/-!
+# HMAC-SHA-256: PPC64LE implementation
+
+The same algorithm as on AArch64 (`VG.Impl.Hmac.AArch64`): two SHA-256
+streaming states (`inner`, `outer`; see `VG.Spec.Hmac`).
+
+* `init(inner = r3, outer = r4, key = r5, key_len = r6, scratch = r7)`
+  stores `H⁽⁰⁾` in both states, the block `K₀ ⊕ ipad` in the inner buffer
+  and `K₀ ⊕ opad` in the outer one, and compresses both (calling
+  `vg_sha256_compress`).
+* `finalize(inner = r3, outer = r4, count = r5, scratch = r6)` finalizes the
+  inner state (calling `vg_sha256_finalize`), makes the inner state
+  represent `(K₀ ⊕ opad) ‖ digest` (96 bytes) from the outer hash value and
+  that digest, and finalizes it again, leaving the MAC in
+  `scratch[176..208)`.
+
+Both move the link register to `r0` and save it in a frame around the
+whole function, as the streaming SHA-256 functions do.
+-/
+
+namespace VG.Impl.Hmac.PPC64LE
+
+open VG.PPC64LE
+open VG.Impl.Sha256.PPC64LE.Stream (mov compressAt save restore)
+
+/-! ## `init`
+
+As in the streaming SHA-256 `update`, the call of the compression function
+(`compressAt`: the block at `r4` into the hash value at `r26`, with scratch
+space `r27`) preserves `r14`–`r31`, so our variables live in `r26`–`r31`,
+and our caller's values of those are saved in `scratch[112..160)`.
+
+Registers: `r26` = the state being compressed (`inner`, then `outer`), `r27`
+= `scratch`, `r28` = `outer`, `r29` = the next key byte, `r30` = key bytes
+left, `r31` = the byte index, `r12` = `0x36` (`ipad`), `r0` = `0x5c`
+(`opad`). Byte `r31` of a buffer is addressed as `32(r11)` with
+`r11 = state + r31`. -/
+
+/-- `H⁽⁰⁾` into the state at `b`. -/
+def h0 (b : Reg) : List Instr :=
+  (List.range 8).flatMap fun k =>
+    [.lis .r8 (Spec.Sha256.H0[k]!.extractLsb' 16 16),
+     .ori .r8 .r8 (Spec.Sha256.H0[k]!.extractLsb' 0 16),
+     .store .w .r8 b (4 * k)]
+
+/-- The key bytes, XORed with `ipad` into the inner buffer and `opad` into the outer one. -/
+def keyLoop : Prog isa :=
+  .loop (.block [.lbz .r8 .r29 0,
+    .logic .xor .r9 .r8 .r12, .add .r11 .r26 .r31, .stb .r9 .r11 32,
+    .logic .xor .r9 .r8 .r0, .add .r11 .r28 .r31, .stb .r9 .r11 32,
+    .addi .r29 .r29 1, .addi .r31 .r31 1, .subi .r30 .r30 1]) (.nonzero .d .r30)
+
+/-- The zero bytes after the key (`r10` of them), XORed likewise. -/
+def padLoop : Prog isa :=
+  .loop (.block [.add .r11 .r26 .r31, .stb .r12 .r11 32, .add .r11 .r28 .r31, .stb .r0 .r11 32,
+    .addi .r31 .r31 1, .subi .r10 .r10 1]) (.nonzero .d .r10)
+
+/-- `init`, but for saving the link register. -/
+def initMain : Prog isa :=
+  .seq (.block (save .r7 ++ [mov .r26 .r3, mov .r27 .r7, mov .r28 .r4, mov .r29 .r5, mov .r30 .r6] ++
+      h0 .r26 ++ h0 .r28 ++ [.li .r12 0x36, .li .r0 0x5c, .li .r31 0]))
+  (.seq (.ite (.zero .d .r30) (.block []) keyLoop)
+  (.seq (.block [.li .r10 64, .sub .r10 .r10 .r31])
+  (.seq (.ite (.zero .d .r10) (.block []) padLoop)
+  (.seq (.block [.addi .r4 .r26 32])
+  (.seq compressAt
+  (.seq (.block [mov .r26 .r28, .addi .r4 .r26 32])
+  (.seq compressAt
+    (.block restore))))))))
+
+def init : Prog isa :=
+  .seq (.block [.mflr .r0]) (.seq (.frame (.push .r0) initMain (.pop .r0)) (.block [.mtlr .r0]))
+
+/-! ## `finalize`
+
+The MAC is left in `scratch[176..208)`. The outer hash value is first copied
+to `scratch[208..240)`; the inner state is finalized into
+`scratch[176..208)`; then the inner state is overwritten with the outer hash
+value and that digest, so that it represents `(K₀ ⊕ opad) ‖ digest`, and
+finalized again.
+
+`inner` and `scratch` are kept in `r24` and `r25`, which the calls of
+`vg_sha256_finalize` preserve and never even write (so the taint analysis
+knows they are still public after them); our caller's values of those are
+saved in `scratch[160..176)`, and our return address in a stack frame. -/
+
+/-- Copying 32-bit word `k` from `o₁(src)` to `o₂(dst)`. -/
+def cp32 (src dst : Reg) (o₁ o₂ k : Nat) : List Instr :=
+  [.load .w .r8 src (o₁ + 4 * k), .store .w .r8 dst (o₂ + 4 * k)]
+
+/-- Copying 64-bit word `k` from `o₁(src)` to `o₂(dst)`. -/
+def cp64 (src dst : Reg) (o₁ o₂ k : Nat) : List Instr :=
+  [.load .d .r8 src (o₁ + 8 * k), .store .d .r8 dst (o₂ + 8 * k)]
+
+/-- The outer hash value into `scratch[208..240)`. -/
+def saveOuter : List Instr := (List.range 8).flatMap (cp32 .r4 .r6 0 208)
+
+/-- The outer hash value and the first digest into the inner state. -/
+def loadOuter : List Instr :=
+  (List.range 8).flatMap (cp32 .r25 .r24 208 0) ++ (List.range 4).flatMap (cp64 .r25 .r24 176 32)
+
+/-- A call of `vg_sha256_finalize`. -/
+def sha256Finalize : Prog isa := .call "vg_sha256_finalize" Impl.Sha256.PPC64LE.Stream.finalize
+
+/-- `finalize`, but for saving the link register. -/
+def finalizeMain : Prog isa :=
+  .seq (.block ([.store .d .r24 .r6 160, .store .d .r25 .r6 168, mov .r24 .r3, mov .r25 .r6] ++ saveOuter ++
+      [mov .r4 .r5, .addi .r5 .r6 176]))
+  (.seq sha256Finalize
+  (.seq (.block (loadOuter ++ [mov .r3 .r24, .li .r4 96, .addi .r5 .r25 176, mov .r6 .r25]))
+  (.seq sha256Finalize
+    (.block [.load .d .r24 .r25 160, .load .d .r25 .r25 168]))))
+
+def finalize : Prog isa :=
+  .seq (.block [.mflr .r0]) (.seq (.frame (.push .r0) finalizeMain (.pop .r0)) (.block [.mtlr .r0]))
+
+end VG.Impl.Hmac.PPC64LE