Implement verified Triple DES ECB on ARMv7

README.md

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

bench/benches/primitives/triple_des_ecb.rs

@@ -5,7 +5,7 @@ use criterion::Criterion;
 /// The library modules whose code these benchmarks run.
 pub const USES: &[&str] = &["triple_des_ecb", "triple_des"];
 
-#[cfg(any(target_arch = "x86_64", target_arch = "aarch64"))]
+#[cfg(any(target_arch = "x86_64", target_arch = "aarch64", target_arch = "arm"))]
 pub fn bench(c: &mut Criterion) {
     use std::hint::black_box;
 
@@ -59,5 +59,5 @@ pub fn bench(c: &mut Criterion) {
     }
 }
 
-#[cfg(not(any(target_arch = "x86_64", target_arch = "aarch64")))]
+#[cfg(not(any(target_arch = "x86_64", target_arch = "aarch64", target_arch = "arm")))]
 pub fn bench(_: &mut Criterion) {}

lean/VerifiedGarbage/Artifacts/TripleDes/Arm.lean

@@ -0,0 +1,56 @@
+import VerifiedGarbage.Proof.TripleDes.Arm.VerifiedBlock
+import VerifiedGarbage.Proof.TripleDes.Arm.Key.Verified
+import VerifiedGarbage.Proof.TripleDes.Arm.Ecb.Verified
+
+namespace VG.Artifacts.TripleDes.Arm
+
+def artifacts : List Artifact := [
+  { Spec.TripleDes.expandKeyApi with
+    target := Arm.target
+    doc := Spec.TripleDes.expandKeyApi.doc
+      (notes := ["Baseline ARMv7 scalar key expansion with fixed permutations and public round-count branches."])
+    code := Impl.TripleDes.Arm.Key.expandKey
+    contract := Spec.TripleDes.expandKeyContract Arm.abi
+    stack := 0
+    verified := Proof.TripleDes.Arm.Key.verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.TripleDes.encryptBlockApi with
+    target := Arm.target
+    doc := Spec.TripleDes.encryptBlockApi.doc
+      (notes := ["Baseline ARMv7 scalar Boolean S-box circuits; IP and FP shared across all three DES passes."])
+    code := Impl.TripleDes.Arm.encryptBlock
+    contract := Spec.TripleDes.encryptBlockContract Arm.abi
+    stack := 0
+    verified := Proof.TripleDes.Arm.encrypt_verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.TripleDes.decryptBlockApi with
+    target := Arm.target
+    doc := Spec.TripleDes.decryptBlockApi.doc
+      (notes := ["Baseline ARMv7 scalar Boolean S-box circuits with reverse EDE key order."])
+    code := Impl.TripleDes.Arm.decryptBlock
+    contract := Spec.TripleDes.decryptBlockContract Arm.abi
+    stack := 0
+    verified := Proof.TripleDes.Arm.decrypt_verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.TripleDes.ecbEncryptApi with
+    target := Arm.target
+    doc := Spec.TripleDes.ecbEncryptApi.doc
+      (notes := ["Baseline ARMv7, calling the verified Triple DES block primitive for each complete block."])
+    code := Impl.TripleDes.Arm.Ecb.encrypt
+    contract := Spec.TripleDes.ecbEncryptContract Arm.abi 0
+    stack := 0
+    ofSig := ⟨_, _, _, by unfold Spec.TripleDes.ecbEncryptContract Spec.TripleDes.ecbContract; rfl⟩
+    verified := Proof.TripleDes.Arm.Ecb.encrypt_verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.TripleDes.ecbDecryptApi with
+    target := Arm.target
+    doc := Spec.TripleDes.ecbDecryptApi.doc
+      (notes := ["Baseline ARMv7, calling the verified Triple DES block primitive for each complete block."])
+    code := Impl.TripleDes.Arm.Ecb.decrypt
+    contract := Spec.TripleDes.ecbDecryptContract Arm.abi 0
+    stack := 0
+    ofSig := ⟨_, _, _, by unfold Spec.TripleDes.ecbDecryptContract Spec.TripleDes.ecbContract; rfl⟩
+    verified := Proof.TripleDes.Arm.Ecb.decrypt_verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ }]
+
+end VG.Artifacts.TripleDes.Arm

lean/VerifiedGarbage/Impl/TripleDes/Arm/Block.lean

@@ -0,0 +1,66 @@
+import VerifiedGarbage.Impl.TripleDes.Arm.Common
+import VerifiedGarbage.Impl.TripleDes.Arm.Sbox
+
+namespace VG.Impl.TripleDes.Arm
+open VG.Arm
+open VG.Spec.TripleDes (Direction)
+
+def savedRegs : List Reg := [.r4, .r5, .r6, .r7, .r8, .r9, .r10, .r11, .lr]
+def blockSave : List Instr := savedRegs.zipIdx.map fun (r, i) => .str r .r2 (4 * i)
+def blockRestore : List Instr := savedRegs.zipIdx.map fun (r, i) => .ldr r .r2 (4 * i)
+
+def blockLoad : List Instr :=
+  [.ldr .r4 .r1 0, .ldr .r5 .r1 4, .rev .r4 .r4, .rev .r5 .r5] ++
+    permuteCode Spec.TripleDes.ip 64 32 32 .r11 .r10 .r5 .r4 .r12 .r9
+
+def sboxInputs (i : Nat) : List Instr :=
+  (List.range 6).flatMap fun j =>
+    let k := 6 * i + 5 - j
+    let bit := 47 - k
+    [.ldr .lr .r0 (if bit < 32 then 0 else 4), rr (q j) .r11] ++
+      shr (q j) (32 - Spec.TripleDes.expansion.getD k 1) ++
+      [.dp .eor (q j) (q j)
+        (if bit % 32 = 0 then .reg .lr else .shifted .lr .lsr (bit % 32)),
+        .dp .and (q j) (q j) (.imm 1)]
+
+def sboxOutputs (i : Nat) : List Instr :=
+  (List.range 4).flatMap fun j =>
+    let position := 4 * i + 4 - j
+    let dst := (Spec.TripleDes.p.toList.findIdx? (· == position)).getD 0
+    [.dp .and (q j) (q j) (.imm 1)] ++ placeBit (q j) (31 - dst) ++
+      [.dp .eor .r10 .r10 (.reg (q j))]
+
+def box (i : Nat) : List Instr := sboxInputs i ++ sboxCode i ++ sboxOutputs i
+
+def swapHalves : List Instr := [rr .lr .r10, rr .r10 .r11, rr .r11 .lr]
+def roundBody : List Instr := (List.range 8).flatMap box ++ swapHalves
+
+def roundAdvance (d : Direction) : List Instr :=
+  [.dp (if d = .encrypt then .add else .sub) .r0 .r0 (.imm 8), .subs .r9 .r9 (.imm 1)]
+
+/-- Each offset is relative to the pointer left by the preceding pass. -/
+def passStart (offset : Int) : List Instr :=
+  [.dp (if offset < 0 then .sub else .add) .r0 .r0
+    (.imm (BitVec.ofNat 32 offset.natAbs)), imm .r9 16]
+
+def pass (offset : Int) (d : Direction) : Prog isa :=
+  .seq (.block (passStart offset))
+    (.seq (.loop (.block (roundBody ++ roundAdvance d)) .ne) (.block swapHalves))
+
+def blockBody (d : Direction) : Prog isa :=
+  match d with
+  | .encrypt => .seq (pass 0 .encrypt) (.seq (pass 120 .decrypt) (pass 136 .encrypt))
+  | .decrypt => .seq (pass 376 .decrypt) (.seq (pass (-120) .encrypt) (pass (-136) .decrypt))
+
+def blockStore (d : Direction) : List Instr :=
+  permuteCode Spec.TripleDes.fp 64 32 32 .r5 .r4 .r11 .r10 .r12 .r9 ++
+    [.rev .r4 .r4, .rev .r5 .r5, .str .r4 .r1 0, .str .r5 .r1 4,
+      .dp (if d = .encrypt then .sub else .add) .r0 .r0
+        (.imm (if d = .encrypt then 384 else 8))]
+
+def block (d : Direction) : Prog isa :=
+  .seq (.block (blockSave ++ blockLoad))
+    (.seq (blockBody d) (.block (blockStore d ++ blockRestore)))
+def encryptBlock : Prog isa := block .encrypt
+def decryptBlock : Prog isa := block .decrypt
+end VG.Impl.TripleDes.Arm

lean/VerifiedGarbage/Impl/TripleDes/Arm/Common.lean

@@ -0,0 +1,29 @@
+import VerifiedGarbage.Spec.TripleDes
+import VerifiedGarbage.TCB.Arm.Isa
+
+namespace VG.Impl.TripleDes.Arm
+open VG.Arm
+
+def rr (d n : Reg) : Instr := .mov d (.reg n)
+def imm (d : Reg) (n : Nat) : Instr := .mov d (.imm (BitVec.ofNat 32 n))
+def shr (r : Reg) (n : Nat) : List Instr :=
+  if n = 0 then [] else [.mov r (.shifted r .lsr n)]
+def placeBit (r : Reg) (n : Nat) : List Instr :=
+  if n = 0 then [] else [.mov r (.shifted r .ror (32 - n))]
+def mask (r : Reg) (n : Nat) : List Instr :=
+  [.mov r (.shifted r .lsl (32 - n)), .mov r (.shifted r .lsr (32 - n))]
+
+/-- A fixed bit permutation across two words. Each split is the width of
+its low word; unused high bits are zero. -/
+def permuteCode {m : Nat} (positions : Vector Nat m) (n srcSplit dstSplit : Nat)
+    (lo hi srcLo srcHi tmp bit : Reg) : List Instr :=
+  [imm lo 0, imm hi 0, imm bit 1] ++ (List.range m).flatMap fun k =>
+    let source := n - positions.getD k 1
+    let output := m - 1 - k
+    [rr tmp (if source < srcSplit then srcLo else srcHi)] ++
+      shr tmp (if source < srcSplit then source else source - srcSplit) ++
+      [.dp .and tmp tmp (.reg bit)] ++
+      placeBit tmp (if output < dstSplit then output else output - dstSplit) ++
+      [.dp .eor (if output < dstSplit then lo else hi)
+        (if output < dstSplit then lo else hi) (.reg tmp)]
+end VG.Impl.TripleDes.Arm

lean/VerifiedGarbage/Impl/TripleDes/Arm/Ecb.lean

@@ -0,0 +1,18 @@
+import VerifiedGarbage.Impl.TripleDes.Arm.Block
+namespace VG.Impl.TripleDes.Arm.Ecb
+open VG.Arm VG.Impl.TripleDes.Arm
+open VG.Spec.TripleDes (Direction)
+def save : List Instr := [.str .lr .r3 512]
+def setup : List Instr := [rr .r12 .r3, rr .r3 .r2, rr .r2 .r12, .cmp .r3 (.imm 0)]
+def restore : List Instr := [.ldr .lr .r2 512]
+def blockCall (d : Direction) : Prog isa :=
+  match d with
+  | .encrypt => .call "vg_triple_des_encrypt_block" encryptBlock
+  | .decrypt => .call "vg_triple_des_decrypt_block" decryptBlock
+def advance : List Instr := [.dp .add .r1 .r1 (.imm 8), .subs .r3 .r3 (.imm 1)]
+def ecb (d : Direction) : Prog isa :=
+  .seq (.block (save ++ setup)) (.seq (.ite .eq (.block [])
+    (.loop (.seq (blockCall d) (.block advance)) .ne)) (.block restore))
+def encrypt : Prog isa := ecb .encrypt
+def decrypt : Prog isa := ecb .decrypt
+end VG.Impl.TripleDes.Arm.Ecb

lean/VerifiedGarbage/Impl/TripleDes/Arm/ExpandKey.lean

@@ -0,0 +1,38 @@
+import VerifiedGarbage.Impl.TripleDes.Arm.Common
+namespace VG.Impl.TripleDes.Arm.Key
+open VG.Arm VG.Impl.TripleDes.Arm
+
+def savedRegs : List Reg := [.r4, .r5, .r6, .r7, .r8, .r9, .r10, .r11, .lr]
+def save : List Instr := savedRegs.zipIdx.map fun (r, i) => .str r .r3 (4 * i)
+def restore : List Instr := savedRegs.zipIdx.map fun (r, i) => .ldr r .r3 (4 * i)
+
+def load (offset component : Nat) : List Instr :=
+  [.ldr .r4 .r0 offset, .ldr .r5 .r0 (offset + 4), .rev .r4 .r4, .rev .r5 .r5] ++
+    permuteCode Spec.TripleDes.pc1 64 32 28 .r11 .r10 .r5 .r4 .r12 .lr ++
+    [imm .r9 0, .dp .add .r8 .r2 (.imm (BitVec.ofNat 32 (128 * component)))]
+
+def rotate28 (r : Reg) (n : Nat) : List Instr :=
+  [.mov .r4 (.shifted r .lsr (28 - n)), .mov r (.shifted r .ror (32 - n)),
+    .dp .eor r r (.reg .r4)] ++ mask r 28
+
+def rotate (n : Nat) : Prog isa := .block (rotate28 .r10 n ++ rotate28 .r11 n)
+def rotation : Prog isa :=
+  .seq (.block [.mov .r4 (.shifted .r9 .lsr 1), .cmp .r4 (.imm 0)]) (.ite .eq (rotate 1)
+    (.seq (.block [.cmp .r9 (.imm 8)]) (.ite .eq (rotate 1)
+      (.seq (.block [.cmp .r9 (.imm 15)]) (.ite .eq (rotate 1) (rotate 2))))))
+
+def storeRound : List Instr :=
+  permuteCode Spec.TripleDes.pc2 56 28 32 .r4 .r5 .r11 .r10 .r12 .lr ++
+    [.str .r4 .r8 0, .str .r5 .r8 4, .dp .add .r8 .r8 (.imm 8),
+      .dp .add .r9 .r9 (.imm 1), .cmp .r9 (.imm 16)]
+def component (offset index : Nat) : Prog isa :=
+  .seq (.block (load offset index)) (.loop (.seq rotation (.block storeRound)) .ne)
+def copyThird : List Instr :=
+  (List.range 16).flatMap fun j =>
+    [.ldr .r4 .r2 (8 * j), .ldr .r5 .r2 (8 * j + 4),
+      .str .r4 .r2 (256 + 8 * j), .str .r5 .r2 (256 + 8 * j + 4)]
+def expandKey : Prog isa :=
+  .seq (.block save) (.seq (component 0 0) (.seq (component 8 1)
+    (.seq (.block [.cmp .r1 (.imm 16)])
+      (.seq (.ite .eq (.block copyThird) (component 16 2)) (.block restore)))))
+end VG.Impl.TripleDes.Arm.Key

lean/VerifiedGarbage/Impl/TripleDes/Arm/Permutation.lean

@@ -0,0 +1,9 @@
+import VerifiedGarbage.Impl.TripleDes.Arm.Common
+namespace VG.Impl.TripleDes.Arm
+open VG.Arm
+
+def initialPermutation : Prog isa := .block (permuteCode Spec.TripleDes.ip 64 32 32 .r11 .r10 .r5 .r4 .r12 .r9)
+def finalPermutation : Prog isa := .block (permuteCode Spec.TripleDes.fp 64 32 32 .r5 .r4 .r11 .r10 .r12 .r9)
+def keyPermutation1 : Prog isa := .block (permuteCode Spec.TripleDes.pc1 64 32 28 .r11 .r10 .r5 .r4 .r12 .lr)
+def keyPermutation2 : Prog isa := .block (permuteCode Spec.TripleDes.pc2 56 28 32 .r4 .r5 .r11 .r10 .r12 .lr)
+end VG.Impl.TripleDes.Arm

lean/VerifiedGarbage/Impl/TripleDes/Arm/Sbox.lean

@@ -0,0 +1,30 @@
+import VerifiedGarbage.Impl.TripleDes.Circuit
+import VerifiedGarbage.Impl.Aes.Arm.Alloc
+
+namespace VG.Impl.TripleDes.Arm
+
+open VG.Arm
+
+def q : Nat → Reg
+  | 0 => .r4 | 1 => .r5 | 2 => .r6 | 3 => .r7 | 4 => .r8 | _ => .r12
+
+def sboxIns : List (Nat × Reg) := (List.range 6).map fun i => (i, q i)
+
+def sboxOuts (i : Nat) : List (Nat × Reg) :=
+  (List.range 4).map fun j => ((Circuit.outputs i).getD j 0, q j)
+
+/-- Six input planes and one temporary; slots below 16 hold saved registers and control state. -/
+def sboxCode (i : Nat) : List Instr :=
+  VG.Impl.Aes.Arm.compile .r2 (Circuit.gates i) sboxIns (sboxOuts i)
+    [.lr] 15 10000 10001 (List.range' 16 96)
+
+def sbox0 : Prog isa := .block (sboxCode 0)
+def sbox1 : Prog isa := .block (sboxCode 1)
+def sbox2 : Prog isa := .block (sboxCode 2)
+def sbox3 : Prog isa := .block (sboxCode 3)
+def sbox4 : Prog isa := .block (sboxCode 4)
+def sbox5 : Prog isa := .block (sboxCode 5)
+def sbox6 : Prog isa := .block (sboxCode 6)
+def sbox7 : Prog isa := .block (sboxCode 7)
+
+end VG.Impl.TripleDes.Arm

lean/VerifiedGarbage/Proof/TripleDes/Arm/Block.lean

@@ -0,0 +1,92 @@
+import VerifiedGarbage.Proof.TripleDes.Arm.Head
+import VerifiedGarbage.Proof.TripleDes.Arm.Tail
+
+namespace VG.Proof.TripleDes.Arm
+
+open VG VG.Arm VG.Impl.TripleDes.Arm
+open VG.Spec.TripleDes (Direction Schedule)
+
+def blockResult (keys : Schedule) (direction : Direction) (b : Spec.TripleDes.Block) :
+    Spec.TripleDes.Block :=
+  match direction with
+  | .encrypt => Spec.TripleDes.encryptBlock keys b
+  | .decrypt => Spec.TripleDes.decryptBlock keys b
+
+theorem blockResult_core (keys : Schedule) (direction : Direction) (b : Spec.TripleDes.Block) :
+    Spec.TripleDes.encodeBlock (Spec.TripleDes.permute Spec.TripleDes.fp
+      (blockCore (Spec.TripleDes.componentSchedule keys) direction
+        (Spec.TripleDes.permute Spec.TripleDes.ip (Spec.TripleDes.decodeBlock b)))) =
+      blockResult keys direction b := by
+  cases direction
+  · exact (VG.Proof.TripleDes.encryptBlock_eq_cores keys b).symm
+  · exact (VG.Proof.TripleDes.decryptBlock_eq_cores keys b).symm
+
+def blockRegions (s : State) : List Region := [⟨State.addr (s.gpr .r1), 8⟩, ⟨State.addr (s.gpr .r2), 512⟩]
+
+structure BlockPost (keys : Schedule) (direction : Direction) (original s : State) : Prop where
+  result : Spec.TripleDes.blockAt s.mem (State.addr (original.gpr .r1)) =
+    blockResult keys direction (Spec.TripleDes.blockAt original.mem (State.addr (original.gpr .r1)))
+  pointer : s.gpr .r0 = original.gpr .r0
+  saved : ∀ r ∈ savedRegs, s.gpr r = original.gpr r
+  rd : s.rd = original.rd
+  wr : s.wr = original.wr
+  sp : s.sp = original.sp
+  regs : ∀ q ∈ roundStepKept, s.gpr q = original.gpr q
+  frame : Frame (blockRegions original) original.mem s.mem
+
+theorem block_ok (keys : Schedule) (base : BitVec 32) (direction : Direction) (s : State)
+    (hp : HeadPre (Spec.TripleDes.componentSchedule keys) base s)
+    (hwrite : ∀ t < 2, InRegions s.wr (State.addr (s.gpr .r1 + BitVec.ofNat 32 (4 * t))) 4) :
+    WP isa (block direction) s (BlockPost keys direction s) := by
+  apply WP.seq
+  apply WP.mono (blockHead_ok (Spec.TripleDes.componentSchedule keys) base s hp)
+  intro s₁ hs₁
+  apply WP.seq
+  apply WP.mono (blockBody_ok (Spec.TripleDes.componentSchedule keys) base s₁ _ direction ((hs₁.regs .r0 (by decide)).trans hp.pointer) hs₁.ready hs₁.word)
+  intro s₂ hs₂
+  have hregs₂ : ∀ q ∈ roundStepKept, s₂.gpr q = s.gpr q := by
+    intro q hq
+    have hkeep : ∀ r ∈ roundStepKept, r ∈ loadKept := by decide
+    exact (hs₂.2.2.1.regs q hq).trans (hs₁.regs q (hkeep q hq))
+  have saved₂ := hs₁.saved.congr (hs₂.2.2.1.regs .r2 (by decide)) hs₂.2.2.1.frame
+  have savedRead₂ : ∀ i < 9, InRegions (s₂.rd ++ s₂.wr) (State.addr (s₂.gpr .r2) + BitVec.ofNat 64 (4 * i)) 4 := by
+    rw [hs₂.2.2.1.rd, hs₂.2.2.1.wr, hs₁.rd, hs₁.wr, hregs₂ .r2 (by decide)]
+    exact hp.saveRead
+  have hwrite₂ : ∀ t < 2, InRegions s₂.wr (State.addr (s₂.gpr .r1 + BitVec.ofNat 32 (4 * t))) 4 := by
+    rw [hs₂.2.2.1.wr, hs₁.wr, hregs₂ .r1 (by decide)]
+    exact hwrite
+  apply WP.mono (blockTail_ok s s₂ direction _ hs₂.1 saved₂
+    (by rw [hregs₂ .r2 (by decide)]; exact hp.scratchFit)
+    (by rw [hregs₂ .r1 (by decide)]; exact hp.dataFit) savedRead₂ hwrite₂
+    (by rw [saveRegion, hregs₂ .r1 (by decide), hregs₂ .r2 (by decide)]; exact hp.dataSeparate))
+  intro s₃ hs₃
+  refine ⟨?_, ?_, hs₃.saved, hs₃.rd.trans (hs₂.2.2.1.rd.trans hs₁.rd),
+    hs₃.wr.trans (hs₂.2.2.1.wr.trans hs₁.wr),
+    hs₃.sp.trans (hs₂.2.2.1.sp.trans hs₁.sp),
+    fun q hq => (hs₃.regs q hq).trans (hregs₂ q hq), ?_⟩
+  · have hresult := hs₃.result
+    rw [hregs₂ .r1 (by decide)] at hresult
+    exact hresult.trans (blockResult_core keys direction _)
+  · rw [hs₃.pointer, hs₂.2.2.2, hp.pointer]
+    cases direction <;> simp only [reduceCtorEq, ite_true, ite_false,
+      BitVec.add_sub_cancel, BitVec.sub_add_cancel]
+  · have hf₁ : Frame (blockRegions s) s.mem s₁.mem := hs₁.frame.sub (by
+      intro r hr
+      obtain rfl := List.mem_singleton.mp hr
+      exact ⟨⟨State.addr (s.gpr .r2), 512⟩, by simp [blockRegions], Region.sub_prefix (by decide)⟩)
+    have hf₂ : Frame (blockRegions s) s₁.mem s₂.mem := hs₂.2.2.1.frame.sub (by
+      intro r hr
+      obtain rfl := List.mem_singleton.mp hr
+      refine ⟨⟨State.addr (s.gpr .r2), 512⟩, by simp [blockRegions], ?_⟩
+      have hbase := hs₁.regs .r2 (by decide)
+      change Region.Sub ⟨State.addr (s₁.gpr .r2) + BitVec.ofNat 64 60, 388⟩ ⟨State.addr (s.gpr .r2), 512⟩
+      rw [hbase]
+      exact Offset.sub_base _ (by decide))
+    have hf₃ : Frame (blockRegions s) s₂.mem s₃.mem := hs₃.frame.sub (by
+      intro r hr
+      obtain rfl := List.mem_singleton.mp hr
+      rw [hregs₂ .r1 (by decide)]
+      exact ⟨⟨State.addr (s.gpr .r1), 8⟩, by simp [blockRegions], fun _ h => h⟩)
+    exact hf₁.trans (hf₂.trans hf₃)
+
+end VG.Proof.TripleDes.Arm