diff --git a/README.md b/README.md index 3a3053291..825427311 100644 --- a/README.md +++ b/README.md @@ -221,7 +221,7 @@ yours to keep: ✅ -❌ +✅ diff --git a/bench/benches/primitives/cmac_aes.rs b/bench/benches/primitives/cmac_aes.rs index e7bb7a381..8a0f37caf 100644 --- a/bench/benches/primitives/cmac_aes.rs +++ b/bench/benches/primitives/cmac_aes.rs @@ -8,7 +8,12 @@ pub const USES: &[&str] = &["cmac_aes", "aes"]; /// The MAC of a message with a 16-byte key (setup included), computed and /// verified. -#[cfg(any(target_arch = "x86_64", target_arch = "aarch64", target_arch = "arm"))] +#[cfg(any( + target_arch = "x86_64", + target_arch = "aarch64", + target_arch = "arm", + target_arch = "x86" +))] pub fn bench(c: &mut Criterion) { use std::hint::black_box; @@ -63,5 +68,10 @@ pub fn bench(c: &mut Criterion) { g.finish(); } -#[cfg(not(any(target_arch = "x86_64", target_arch = "aarch64", target_arch = "arm")))] +#[cfg(not(any( + target_arch = "x86_64", + target_arch = "aarch64", + target_arch = "arm", + target_arch = "x86" +)))] pub fn bench(_: &mut Criterion) {} diff --git a/lean/VerifiedGarbage/Artifacts/CmacAes/X86.lean b/lean/VerifiedGarbage/Artifacts/CmacAes/X86.lean new file mode 100644 index 000000000..773d7e562 --- /dev/null +++ b/lean/VerifiedGarbage/Artifacts/CmacAes/X86.lean @@ -0,0 +1,53 @@ +import VerifiedGarbage.TCB.X86.Target +import VerifiedGarbage.Proof.CmacAes.X86.Verified + +/-! +# AES-CMAC (NIST SP 800-38B) on x86 + +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. + +Each function calls `vg_aes_ctr32` in a frame that pushes its six stack +arguments, so uses 28 bytes of stack with the return address. +-/ + +namespace VG.Artifacts.CmacAes.X86 + +open VG.Proof.CmacAes.X86 + +/-- How the functions encrypt a block. -/ +def ctrNote : String := "This implementation encrypts each block with `vg_aes_ctr32`." + +def artifacts : List Artifact := [ + { Spec.Cmac.aesSubkeysApi with + target := X86.target + doc := Spec.Cmac.aesSubkeysApi.doc (notes := [ctrNote]) + code := Impl.CmacAes.X86.subkeys + contract := Spec.Cmac.aesSubkeysContract X86.abi 28 + stack := 28 + verified := subkeys_verified + spSafe := Code.all_of_allInstrs (by lit_decide) }, + { Spec.Cmac.aesUpdateApi with + target := X86.target + doc := Spec.Cmac.aesUpdateApi.doc (notes := [ctrNote]) + code := Impl.CmacAes.X86.update + contract := Spec.Cmac.aesUpdateContract X86.abi 28 + stack := 28 + verified := update_verified + spSafe := Code.all_of_allInstrs (by lit_decide) }, + { Spec.Cmac.aesFinalizeApi with + target := X86.target + doc := Spec.Cmac.aesFinalizeApi.doc (notes := [ctrNote]) + code := Impl.CmacAes.X86.finalize + contract := Spec.Cmac.aesFinalizeContract X86.abi 28 + stack := 28 + verified := finalize_verified + spSafe := Code.all_of_allInstrs (by lit_decide) }] + +end VG.Artifacts.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Impl/CmacAes/X86.lean b/lean/VerifiedGarbage/Impl/CmacAes/X86.lean new file mode 100644 index 000000000..cacc5231f --- /dev/null +++ b/lean/VerifiedGarbage/Impl/CmacAes/X86.lean @@ -0,0 +1,179 @@ +import VerifiedGarbage.Impl.Aes.X86.Ctr32 + +/-! +# AES-CMAC: x86 (32-bit) implementation + +`vg_cmac_aes_subkeys(schedule, rounds, subkeys, scratch)`, +`vg_cmac_aes_update(schedule, rounds, state, data, n, scratch)` and +`vg_cmac_aes_finalize(key, rounds, state, last, last_len, scratch)` (see +`VG.Spec.Cmac.aesSubkeysContract` and the others), every argument on the +stack (cdecl), composed of calls of the verified `vg_aes_ctr32`, one block +at a time: with a counter block `X` and a zero data block, it leaves +`CIPH_K(X)` in the data block. + +Each call pushes the six arguments of `vg_aes_ctr32` (`schedule`, `rounds`, +the counter block, the data block, `n = 1` and the working space, last to +first) in a frame of its own, popped (into `eax`) when it returns: with the +return address the call stores, it uses the 28 bytes below `esp`. The +callee preserves `ebx`, `esi`, `edi` and `ebp`; our caller's values of those +are saved in the scratch buffer. + +The scratch buffer (2176 bytes): `[0, 2048)` is the working space of +`vg_aes_ctr32`, `[2048, 2064)` the counter block, and `[2064, 2080)` our +caller's `ebx`, `esi`, `edi` and `ebp`. + +* `subkeys` computes `L = CIPH_K(0)` into the first block of `subkeys`, and + doubles it there (`K1`) and into the second block (`K2`): the block as a + big-endian 128-bit integer in `eax:ecx:edx:esi`, shifted left by one bit + (`add r, r`), and XORed with `0x87` masked by the bit shifted out. +* `update` keeps only the pointer to the next block (`esi`) across the + calls, and reloads its other arguments from the stack; it stops when the + pointer reaches `data + 16 n`. Each block, the counter block is `C ⊕ Mᵢ` + and the state, zeroed, receives `CIPH_K(C ⊕ Mᵢ)`. +* `finalize` forms `Mₙ` in the counter block: `Mₙ* ⊕ K1` for a complete + block, else `Mₙ*` copied a byte at a time onto zeros, `0x80` after it, and + XORed with `K2`. It XORs in the chaining value and calls `vg_aes_ctr32` + last. + +Only the pointers, `rounds`, `n` and `last_len` can affect timing: the +branches are on `n` and `last_len`, and the doubling is masked. +-/ + +namespace VG.Impl.CmacAes.X86 + +open VG.X86 + +/-- `[b + d]` -/ +def at_ (b : Reg) (d : Nat) : MemOp := { base := b, disp := d } + +/-- The stack argument `i` (from 0), `[esp + 4 + 4 i]`. -/ +def argOp (i : Nat) : Src := .mem (at_ .esp (4 + 4 * i)) + +/-- The offset of the counter block in the scratch buffer. -/ +def cOff : Nat := 2048 + +/-- The callee-saved registers, and where they are saved in the scratch buffer. -/ +def saved : List (Reg × Nat) := [(.ebx, 2064), (.esi, 2068), (.edi, 2072), (.ebp, 2076)] + +/-- Save them, with the scratch buffer in `eax`. -/ +def save : List Instr := saved.map fun (r, d) => .store (at_ .eax d) r + +/-- Restore them, with the scratch buffer (the stack argument `i`) loaded into `eax`. -/ +def restore (i : Nat) : List Instr := .mov .eax (argOp i) :: saved.map fun (r, d) => .mov r (.mem (at_ .eax d)) + +/-- The call of `vg_aes_ctr32(eax, ecx, edx, ebx, edi, ebp)`, its arguments +pushed last to first. -/ +def ctrCall : Prog isa := + .frame (.push [.ebp, .edi, .ebx, .edx, .ecx, .eax]) (.call "vg_aes_ctr32" Impl.Aes.X86.ctr32) (.pop .eax 6) + +/-- The arguments of `vg_aes_ctr32` but the data block (`ebx`) and the +working space (`ebp`): the schedule and the rounds (our stack arguments 0 +and 1), the counter block in the scratch buffer and `n = 1`. -/ +def ctrArgs : List Instr := + [.mov .eax (argOp 0), .mov .ecx (argOp 1), .mov .edx (.reg .ebp), .alu .add .edx (.imm (BitVec.ofNat 32 cOff)), + .mov .edi (.imm 1)] + +/-- The four words at `pb + pd` and `qb + qd` XORed into `cb + cd`, with +`eax` and `ecx`. -/ +def xor4 (pb qb cb : Reg) (pd qd cd : Nat) : List Instr := + (List.range 4).flatMap fun i => + [.mov .eax (.mem (at_ pb (pd + 4 * i))), .mov .ecx (.mem (at_ qb (qd + 4 * i))), .alu .xor .eax (.reg .ecx), + .store (at_ cb (cd + 4 * i)) .eax] + +/-- The block at `b + d` zeroed, with `eax`. -/ +def zero4 (b : Reg) (d : Nat) : List Instr := + .mov .eax (.imm 0) :: (List.range 4).map fun i => .store (at_ b (d + 4 * i)) .eax + +/-! ## `vg_cmac_aes_subkeys` -/ + +/-- Saves the registers, keeps `subkeys` in `ebx` and the scratch buffer in +`ebp`, zeroes the counter block and the first block of `subkeys`, and sets +up the arguments of `vg_aes_ctr32`. -/ +def subkeysPre : List Instr := + [.mov .eax (argOp 3)] ++ save ++ [.mov .ebp (.reg .eax), .mov .ebx (argOp 2)] ++ zero4 .ebp cOff ++ + zero4 .ebx 0 ++ ctrArgs + +/-- The block at `ebx + src`, doubled (`VG.Spec.Cmac.dbl 16`), to `ebx + dst`. -/ +def dbl (src dst : Nat) : List Instr := + [.mov .eax (.mem (at_ .ebx src)), .mov .ecx (.mem (at_ .ebx (src + 4))), .mov .edx (.mem (at_ .ebx (src + 8))), + .mov .esi (.mem (at_ .ebx (src + 12))), .bswap .eax, .bswap .ecx, .bswap .edx, .bswap .esi, + .mov .edi (.reg .eax), .shift .shr .edi 31, .mov .ebp (.imm 0), .alu .sub .ebp (.reg .edi), + .alu .and .ebp (.imm 0x87), + .alu .add .eax (.reg .eax), .mov .edi (.reg .ecx), .shift .shr .edi 31, .alu .or .eax (.reg .edi), + .alu .add .ecx (.reg .ecx), .mov .edi (.reg .edx), .shift .shr .edi 31, .alu .or .ecx (.reg .edi), + .alu .add .edx (.reg .edx), .mov .edi (.reg .esi), .shift .shr .edi 31, .alu .or .edx (.reg .edi), + .alu .add .esi (.reg .esi), .alu .xor .esi (.reg .ebp), + .bswap .eax, .bswap .ecx, .bswap .edx, .bswap .esi, + .store (at_ .ebx dst) .eax, .store (at_ .ebx (dst + 4)) .ecx, .store (at_ .ebx (dst + 8)) .edx, + .store (at_ .ebx (dst + 12)) .esi] + +/-- `K1` over `L`, `K2` after it, and the saved registers restored. -/ +def subkeysPost : List Instr := dbl 0 0 ++ dbl 0 16 ++ restore 3 + +def subkeys : Prog isa := .seq (.block subkeysPre) (.seq ctrCall (.block subkeysPost)) + +/-! ## `vg_cmac_aes_update` -/ + +/-- Saves the registers, and the pointer to the first block in `esi`; ZF is +set if there are no blocks. -/ +def setup : List Instr := + [.mov .eax (argOp 5)] ++ save ++ [.mov .esi (argOp 3), .mov .eax (argOp 4), .alu .test .eax (.reg .eax)] + +/-- The counter block `C ⊕ Mᵢ` (the state at `ebx`, the block at `esi`), the +state zeroed, and the arguments of `vg_aes_ctr32`. -/ +def chainIn : List Instr := + [.mov .ebx (argOp 2), .mov .ebp (argOp 5)] ++ xor4 .ebx .esi .ebp 0 0 cOff ++ zero4 .ebx 0 ++ ctrArgs + +/-- On to the next block; ZF is set once `esi` reaches `data + 16 n`. -/ +def advance : List Instr := + [.alu .add .esi (.imm 16), .mov .eax (argOp 4), .alu .add .eax (.reg .eax), .alu .add .eax (.reg .eax), + .alu .add .eax (.reg .eax), .alu .add .eax (.reg .eax), .alu .add .eax (argOp 3), .alu .cmp .esi (.reg .eax)] + +/-- One block. -/ +def body : Prog isa := .seq (.block chainIn) (.seq ctrCall (.block advance)) + +def update : Prog isa := + .seq (.block setup) (.seq (.ite .e (.block []) (.loop body .ne)) (.block (restore 5))) + +/-! ## `vg_cmac_aes_finalize` -/ + +/-- Saves the registers, keeps the scratch buffer in `ebp`; ZF is set if +`last_len` is 16. -/ +def finSave : List Instr := + [.mov .eax (argOp 5)] ++ save ++ [.mov .ebp (.reg .eax), .mov .ecx (argOp 4), .alu .cmp .ecx (.imm 16)] + +/-- `Mₙ = Mₙ* ⊕ K1` (`K1` at `key + 240`), for a complete last block. -/ +def full : List Instr := [.mov .ebx (argOp 3), .mov .edx (argOp 0)] ++ xor4 .ebx .edx .ebp 0 240 cOff + +/-- The counter block zeroed, `edi` pointing at it, `esi` at the last bytes +and `ecx` their number; ZF is set if there are none. -/ +def zero : List Instr := + zero4 .ebp cOff ++ [.mov .edi (.reg .ebp), .alu .add .edi (.imm (BitVec.ofNat 32 cOff)), .mov .esi (argOp 3), + .mov .ecx (argOp 4), .alu .test .ecx (.reg .ecx)] + +/-- The `ecx` (nonzero) bytes at `esi` copied to `edi`, advancing both. -/ +def copy : Prog isa := + .loop (.block [.movzx8 .eax (at_ .esi 0), .store8 (at_ .edi 0) .al, .alu .add .esi (.imm 1), + .alu .add .edi (.imm 1), .alu .sub .ecx (.imm 1)]) .ne + +/-- `0x80` after the bytes (at `edi`), and the block XORed with `K2` (at +`key + 256`). -/ +def padK2 : List Instr := + [.mov .eax (.imm 0x80), .store8 (at_ .edi 0) .al, .mov .edx (argOp 0)] ++ xor4 .ebp .edx .ebp cOff 256 cOff + +/-- `Mₙ = K2 ⊕ (Mₙ* ‖ 10ʲ)`, for a partial last block (`last_len < 16`). -/ +def partialBlock : Prog isa := + .seq (.block zero) (.seq (.ite .e (.block []) copy) (.block padK2)) + +/-- The counter block `C ⊕ Mₙ` (the state at `ebx`), the state zeroed, and +the arguments of `vg_aes_ctr32`. -/ +def finArgs : List Instr := + [.mov .ebx (argOp 2)] ++ xor4 .ebp .ebx .ebp cOff 0 cOff ++ zero4 .ebx 0 ++ ctrArgs + +/-- Everything before the call. -/ +def finPre : Prog isa := + .seq (.block finSave) (.seq (.ite .e (.block full) partialBlock) (.block finArgs)) + +def finalize : Prog isa := .seq finPre (.seq ctrCall (.block (restore 5))) + +end VG.Impl.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/Call.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/Call.lean new file mode 100644 index 000000000..1aaa06bce --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/Call.lean @@ -0,0 +1,189 @@ +import VerifiedGarbage.Proof.Aes.X86.Ctr32 +import VerifiedGarbage.Proof.Cmac.Frame +import VerifiedGarbage.Proof.Framework.X86.CallWith +import VerifiedGarbage.Proof.Framework.X86.RelCT +import VerifiedGarbage.Impl.CmacAes.X86 + +/-! +# AES-CMAC on x86: calling `vg_aes_ctr32` on one block + +Untrusted: everything here is checked by Lean. + +`ctr_call`: the frame that pushes `vg_aes_ctr32`'s six arguments (`eax` the +schedule, `ecx` the rounds, `edx` the counter block `C`, `ebx` the data +block `D` holding zeros, `edi = 1` and `ebp` the working space `S`) around +its call: `D` then holds `CIPH_K(C)`, as bytes (`Cmac.aesWith`), and only +`C`, `D`, `S` and the 28 bytes below `esp` change in memory. `ctr_rel`: such +calls are constant time, by `vg_aes_ctr32`'s own proof. +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 VG.Impl.CmacAes.X86 + +theorem ofBytes_zeros : Spec.Gcm.ofBytes (Spec.Cmac.zeros 16) = 0 := by decide + +theorem toNat_rounds {R : Nat} (hR : R = 10 ∨ R = 12 ∨ R = 14) : (BitVec.ofNat 32 R).toNat = R := by + rw [BitVec.toNat_ofNat]; exact Nat.mod_eq_of_lt (by omega) + +theorem ctr_nosp : NoSp Impl.Aes.X86.ctr32 := NoSp.of_all (by decide +kernel) + +theorem ctr_stack : stackUse Impl.Aes.X86.ctr32 = 0 := by decide +kernel + +/-- The registers the call pushes, as `vg_aes_ctr32`'s arguments. -/ +abbrev ctrRegs : List Reg := [.ebp, .edi, .ebx, .edx, .ecx, .eax] + +/-- What a call of `vg_aes_ctr32` on one block needs. -/ +structure CtrPre (s : State) (W C D S : BitVec 32) (R : Nat) : Prop where + eax : s.gpr .eax = W + ecx : s.gpr .ecx = BitVec.ofNat 32 R + edx : s.gpr .edx = C + ebx : s.gpr .ebx = D + edi : s.gpr .edi = 1 + ebp : s.gpr .ebp = S + rounds : R = 10 ∨ R = 12 ∨ R = 14 + esp : 28 ≤ (s.gpr .esp).toNat + wc : (⟨W.setWidth 64, 240⟩ : Region).Disjoint ⟨C.setWidth 64, 16⟩ + wd : (⟨W.setWidth 64, 240⟩ : Region).Disjoint ⟨D.setWidth 64, 16⟩ + ws : (⟨W.setWidth 64, 240⟩ : Region).Disjoint ⟨S.setWidth 64, 2048⟩ + cd : (⟨C.setWidth 64, 16⟩ : Region).Disjoint ⟨D.setWidth 64, 16⟩ + cs : (⟨C.setWidth 64, 16⟩ : Region).Disjoint ⟨S.setWidth 64, 2048⟩ + ds : (⟨D.setWidth 64, 16⟩ : Region).Disjoint ⟨S.setWidth 64, 2048⟩ + bw : (below (s.gpr .esp) 28).Disjoint ⟨W.setWidth 64, 240⟩ + bc : (below (s.gpr .esp) 28).Disjoint ⟨C.setWidth 64, 16⟩ + bd : (below (s.gpr .esp) 28).Disjoint ⟨D.setWidth 64, 16⟩ + bs : (below (s.gpr .esp) 28).Disjoint ⟨S.setWidth 64, 2048⟩ + hW : W.toNat + 240 ≤ 2 ^ 32 + hC : C.toNat + 16 ≤ 2 ^ 32 + hD : D.toNat + 16 ≤ 2 ^ 32 + hS : S.toNat + 2048 ≤ 2 ^ 32 + reads : Covers [⟨W.setWidth 64, 240⟩] (s.rd ++ s.wr) + writes : Covers [⟨C.setWidth 64, 16⟩, ⟨D.setWidth 64, 16⟩, ⟨S.setWidth 64, 2048⟩] s.wr + zero : Spec.Aes.bytesAt s.mem (D.setWidth 64) 16 = Spec.Cmac.zeros 16 + +/-- What a call of `vg_aes_ctr32` on one block leaves. -/ +structure CtrPost (s : State) (W C D S : BitVec 32) (R : Nat) (s' : State) : Prop where + rd : s'.rd = s.rd + wr : s'.wr = s.wr + saved : ∀ r ∈ calleeSaved, s'.gpr r = s.gpr r + frame : Frame [⟨C.setWidth 64, 16⟩, ⟨D.setWidth 64, 16⟩, ⟨S.setWidth 64, 2048⟩, below (s.gpr .esp) 28] + s.mem s'.mem + out : Spec.Aes.bytesAt s'.mem (D.setWidth 64) 16 = + Spec.Cmac.aesWith R (Spec.Aes.bytesAt s.mem (W.setWidth 64) (16 * (R + 1))) + (Spec.Aes.bytesAt s.mem (C.setWidth 64) 16) + +/-- The regions `vg_aes_ctr32` is called with. -/ +abbrev ctrRd (E W : BitVec 32) : List Region := [⟨W.setWidth 64, 240⟩, ⟨(E - BitVec.ofNat 32 24).setWidth 64, 24⟩] +abbrev ctrWr (C D S : BitVec 32) : List Region := + [⟨C.setWidth 64, 16⟩, ⟨D.setWidth 64, 16⟩, ⟨S.setWidth 64, 2048⟩] + +theorem hrs : Reg.esp ∉ ctrRegs := by decide + +namespace CtrPre +variable {s : State} {W C D S : BitVec 32} {R : Nat} (h : CtrPre s W C D S R) +include h + +theorem fit : 4 * ctrRegs.length + 4 ≤ (s.gpr .esp).toNat := by + have := h.esp; simp only [List.length_cons, List.length_nil]; omega + +theorem args : arg (pushed ctrRegs s).callEntry 0 = W ∧ arg (pushed ctrRegs s).callEntry 1 = BitVec.ofNat 32 R ∧ + arg (pushed ctrRegs s).callEntry 2 = C ∧ arg (pushed ctrRegs s).callEntry 3 = D ∧ + arg (pushed ctrRegs s).callEntry 4 = 1 ∧ arg (pushed ctrRegs s).callEntry 5 = S := by + refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;> + rw [callEntry_arg h.fit hrs (by decide)] <;> simp [h.eax, h.ecx, h.edx, h.ebx, h.edi, h.ebp] + +theorem sub24 : Region.Sub (below (s.gpr .esp) 24) (below (s.gpr .esp) 28) := below_sub (by omega) h.esp + +theorem sub4 : Region.Sub ⟨(s.gpr .esp - BitVec.ofNat 32 28).setWidth 64, 4⟩ (below (s.gpr .esp) 28) := by + have := below_inner (sp := s.gpr .esp) (a := 4) (b := 28) (k := 24) (by omega) h.esp + rw [show s.gpr .esp - BitVec.ofNat 32 28 = s.gpr .esp - BitVec.ofNat 32 24 - BitVec.ofNat 32 4 by + rw [← VG.Offset.sub_add_eq]; rfl] + exact this + +theorem callPre : CallPre Proof.Aes.ctr32X86 ctrRegs (ctrRd (s.gpr .esp) W) (ctrWr C D S) s := by + obtain ⟨a0, a1, a2, a3, a4, a5⟩ := h.args + have hR := toNat_rounds h.rounds + have eA : argAddr (pushed ctrRegs s).callEntry 0 = (s.gpr .esp - BitVec.ofNat 32 24).setWidth 64 := by + rw [callEntry_argAddr0]; rfl + have eSp : (pushed ctrRegs s).callEntry.gpr .esp = s.gpr .esp - BitVec.ofNat 32 28 := by + rw [callEntry_esp']; rfl + refine ⟨?_, ?_, ?_⟩ + · simp only [Proof.Aes.ctr32X86, State.withRegions_rd, State.withRegions_wr, State.withRegions_gpr, + arg_withRegions, argAddr_withRegions, a0, a1, a2, a3, a4, a5, eA, eSp, hR, + show (1 : BitVec 32).toNat = 1 from rfl, Nat.mul_one] + refine ⟨trivial, trivial, h.wc, h.wd, h.ws, h.cd, h.cs, h.ds, (h.bc.sub_left h.sub24).symm.symm, + (h.bd.sub_left h.sub24), (h.bs.sub_left h.sub24), h.bc.sub_left h.sub4, h.bd.sub_left h.sub4, + h.bs.sub_left h.sub4, h.hW, h.hC, h.hD, h.hS, ?_, h.rounds⟩ + rw [sub_toNat (by have := h.esp; omega)]; have := (s.gpr .esp).isLt; omega + · intro a n ⟨r, hr, hcn⟩ + simp only [List.cons_append, List.nil_append, List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl | rfl + · obtain ⟨r', hr', hc'⟩ := h.reads a n ⟨_, List.mem_singleton_self _, hcn⟩ + exact InRegions_append_cons.mpr (.inr ⟨r', hr', hc'⟩) + · exact InRegions_append_cons.mpr (.inl hcn) + all_goals + obtain ⟨r', hr', hc'⟩ := h.writes a n ⟨_, by simp, hcn⟩ + exact InRegions_append_cons.mpr (.inr ⟨r', List.mem_append_right _ hr', hc'⟩) + · intro a n hi + obtain ⟨r', hr', hc'⟩ := h.writes a n hi + exact ⟨r', List.mem_cons_of_mem _ hr', hc'⟩ + +end CtrPre + +theorem ctr_call {s : State} {W C D S : BitVec 32} {R : Nat} (h : CtrPre s W C D S R) : + WP isa ctrCall s (CtrPost s W C D S R) := by + have hR := toNat_rounds h.rounds + have hR' : 16 * (R + 1) ≤ 240 := by rcases h.rounds with h' | h' | h' <;> omega + unfold ctrCall + refine WP.callWith (rs := ctrRegs) (k := Proof.Aes.ctr32X86) Proof.Aes.X86.ctr32_correct ctr_nosp (by simp) hrs + (by rw [ctr_stack]; have := h.esp; simp only [List.length_cons, List.length_nil]; omega) h.callPre + fun s' rd' wr' cs' f' ⟨s₂, m₂, post⟩ => ?_ + obtain ⟨a0, a1, a2, a3, a4, a5⟩ := h.args + rw [ctr_stack] at f' + have fE := callEntry_frame h.fit hrs + rw [show 4 * ctrRegs.length + 4 = 28 from rfl] at fE + have keep : ∀ {p : BitVec 32} {n k : Nat}, (below (s.gpr .esp) 28).Disjoint ⟨p.setWidth 64, n⟩ → k ≤ n → + n ≤ 240 → + Spec.Aes.bytesAt (pushed ctrRegs s).callEntry.mem (p.setWidth 64) k = Spec.Aes.bytesAt s.mem (p.setWidth 64) k := + fun hd hk hn => Proof.Cmac.bytesAt_frame fE (fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact (hd.sub_right (Region.sub_prefix hk)).symm) (by omega) + obtain ⟨hdata, -⟩ := post + simp only [arg_withRegions, State.withRegions_mem, a0, a1, a2, a3, a4, hR, + show (1 : BitVec 32).toNat = 1 from rfl, m₂] at hdata + have one : ∀ m : Mem, Spec.Gcm.blocksAt m (D.setWidth 64) 1 = [Spec.Gcm.blockAt m (D.setWidth 64)] := + fun m => by simp [Spec.Gcm.blocksAt] + have bD : Spec.Gcm.blockAt (pushed ctrRegs s).callEntry.mem (D.setWidth 64) = 0 := by + rw [Spec.Gcm.blockAt, keep h.bd (le_refl _) (by decide), h.zero, ofBytes_zeros] + rw [one, one, bD, Proof.Cmac.ctr32_one, List.cons.injEq] at hdata + refine ⟨rd', wr', cs', ?_, ?_⟩ + · exact f'.mono fun r hr => by simp only [List.cons_append, List.nil_append] at hr; simpa using hr + · rw [Proof.Cmac.bytesAt_blockAt, hdata.1, Spec.Gcm.blockAt, keep h.bw hR' (le_refl _), keep h.bc (le_refl _) (by decide), + Proof.Cmac.aesWith_bytes _ _ (Proof.Cmac.bytesAt_length _ _ _)] + +/-- Calls of `vg_aes_ctr32` on one block, with the same arguments and stack +pointer in both runs, are constant time. -/ +theorem ctr_rel {W C D S E : BitVec 32} {R : Nat} {P : State → State → Prop} + (h : ∀ s₁ s₂, P s₁ s₂ → CtrPre s₁ W C D S R ∧ CtrPre s₂ W C D S R ∧ s₁.gpr .esp = E ∧ s₂.gpr .esp = E) : + RelCT isa P ctrCall fun _ _ => True := by + refine RelCT.callWith Proof.Aes.X86.ctr32_correct Proof.Aes.X86.ctr32_ct (ctrRd E W) (ctrWr C D S) + fun s₁ s₂ hp => ?_ + obtain ⟨h₁, h₂, e₁, e₂⟩ := h s₁ s₂ hp + have p₁ := h₁.callPre + have p₂ := h₂.callPre + rw [e₁] at p₁ + rw [e₂] at p₂ + refine ⟨p₁, p₂, e₁.trans e₂.symm, ?_⟩ + obtain ⟨a0, a1, a2, a3, a4, a5⟩ := h₁.args + obtain ⟨b0, b1, b2, b3, b4, b5⟩ := h₂.args + refine ⟨by simp only [State.withRegions_gpr, callEntry_esp', e₁, e₂], fun i hi => ?_⟩ + simp only [arg_withRegions] + rcases (by omega : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5) with rfl | rfl | rfl | rfl | rfl | rfl + · rw [a0, b0] + · rw [a1, b1] + · rw [a2, b2] + · rw [a3, b3] + · rw [a4, b4] + · rw [a5, b5] + +end VG.Proof.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/Contract.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/Contract.lean new file mode 100644 index 000000000..fab2784bf --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/Contract.lean @@ -0,0 +1,100 @@ +import VerifiedGarbage.Proof.Cmac.Spec +import VerifiedGarbage.TCB.X86.Target +import VerifiedGarbage.Impl.CmacAes.X86 + +/-! +# AES-CMAC on x86: the contracts the proofs are written against + +Untrusted: everything here is checked by Lean. The artifacts' contracts are +the shared ones of `Spec/Cmac/Contract.lean`, which imply these +(`Verified.lean`). The arguments are on the stack, from `[esp + 4]` (cdecl). +Each call of `vg_aes_ctr32` pushes its six arguments and the return address +in the 28 bytes below `esp`, which may not overlap any buffer. +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 + +/-- `CIPH_K` for AES with the key schedule at `w` for `R` rounds, in `m`. -/ +abbrev ciphAt (m : Mem) (w : Addr) (R : Nat) : Spec.Cmac.Cipher := + Spec.Cmac.aesWith R (Spec.Aes.bytesAt m w (16 * (R + 1))) + +/-- `vg_cmac_aes_update(schedule, rounds, state, data, n, scratch)`. -/ +def updateX86 : Contract isa where + pre s := + let sched : Region := ⟨(arg s 0).setWidth 64, 240⟩ + let state : Region := ⟨(arg s 2).setWidth 64, 16⟩ + let data : Region := ⟨(arg s 3).setWidth 64, 16 * (arg s 4).toNat⟩ + let scr : Region := ⟨(arg s 5).setWidth 64, 2176⟩ + let args : Region := ⟨argAddr s 0, 24⟩ + let ret : Region := ⟨(s.gpr .esp).setWidth 64, 4⟩ + let stack : Region := ⟨(s.gpr .esp).setWidth 64 - BitVec.ofNat 64 28, 28⟩ + s.rd = [sched, data, args] ∧ s.wr = [state, scr] ∧ + sched.Disjoint state ∧ sched.Disjoint scr ∧ data.Disjoint state ∧ data.Disjoint scr ∧ + state.Disjoint scr ∧ args.Disjoint state ∧ args.Disjoint scr ∧ + ret.Disjoint state ∧ ret.Disjoint scr ∧ + stack.Disjoint sched ∧ stack.Disjoint data ∧ stack.Disjoint state ∧ stack.Disjoint scr ∧ + (arg s 0).toNat + 240 ≤ 2 ^ 32 ∧ (arg s 2).toNat + 16 ≤ 2 ^ 32 ∧ + (arg s 3).toNat + 16 * (arg s 4).toNat ≤ 2 ^ 32 ∧ (arg s 5).toNat + 2176 ≤ 2 ^ 32 ∧ + 28 ≤ (s.gpr .esp).toNat ∧ (s.gpr .esp).toNat + 28 ≤ 2 ^ 32 ∧ + ((arg s 1).toNat = 10 ∨ (arg s 1).toNat = 12 ∨ (arg s 1).toNat = 14) + post s s' := + Spec.Aes.bytesAt s'.mem ((arg s 2).setWidth 64) 16 = + Spec.Cmac.chain (ciphAt s.mem ((arg s 0).setWidth 64) (arg s 1).toNat) + (Spec.Aes.bytesAt s.mem ((arg s 2).setWidth 64) 16) + (Spec.Cmac.blocksAt s.mem ((arg s 3).setWidth 64) 16 (arg s 4).toNat) + pub s₁ s₂ := s₁.gpr .esp = s₂.gpr .esp ∧ ∀ i < 6, arg s₁ i = arg s₂ i + +/-- `vg_cmac_aes_subkeys(schedule, rounds, subkeys, scratch)`. -/ +def subkeysX86 : Contract isa where + pre s := + let sched : Region := ⟨(arg s 0).setWidth 64, 240⟩ + let subk : Region := ⟨(arg s 2).setWidth 64, 32⟩ + let scr : Region := ⟨(arg s 3).setWidth 64, 2176⟩ + let args : Region := ⟨argAddr s 0, 16⟩ + let ret : Region := ⟨(s.gpr .esp).setWidth 64, 4⟩ + let stack : Region := ⟨(s.gpr .esp).setWidth 64 - BitVec.ofNat 64 28, 28⟩ + s.rd = [sched, args] ∧ s.wr = [subk, scr] ∧ + sched.Disjoint subk ∧ sched.Disjoint scr ∧ subk.Disjoint scr ∧ + args.Disjoint subk ∧ args.Disjoint scr ∧ ret.Disjoint subk ∧ ret.Disjoint scr ∧ + stack.Disjoint sched ∧ stack.Disjoint subk ∧ stack.Disjoint scr ∧ + (arg s 0).toNat + 240 ≤ 2 ^ 32 ∧ (arg s 2).toNat + 32 ≤ 2 ^ 32 ∧ + (arg s 3).toNat + 2176 ≤ 2 ^ 32 ∧ 28 ≤ (s.gpr .esp).toNat ∧ (s.gpr .esp).toNat + 20 ≤ 2 ^ 32 ∧ + ((arg s 1).toNat = 10 ∨ (arg s 1).toNat = 12 ∨ (arg s 1).toNat = 14) + post s s' := + let ks := Spec.Cmac.subkeys (ciphAt s.mem ((arg s 0).setWidth 64) (arg s 1).toNat) 16 + Spec.Aes.bytesAt s'.mem ((arg s 2).setWidth 64) 32 = ks.1 ++ ks.2 + pub s₁ s₂ := s₁.gpr .esp = s₂.gpr .esp ∧ ∀ i < 4, arg s₁ i = arg s₂ i + +/-- `vg_cmac_aes_finalize(key, rounds, state, last, last_len, scratch)`. -/ +def finalizeX86 : Contract isa where + pre s := + let key : Region := ⟨(arg s 0).setWidth 64, 272⟩ + let state : Region := ⟨(arg s 2).setWidth 64, 16⟩ + let last : Region := ⟨(arg s 3).setWidth 64, (arg s 4).toNat⟩ + let scr : Region := ⟨(arg s 5).setWidth 64, 2176⟩ + let args : Region := ⟨argAddr s 0, 24⟩ + let ret : Region := ⟨(s.gpr .esp).setWidth 64, 4⟩ + let stack : Region := ⟨(s.gpr .esp).setWidth 64 - BitVec.ofNat 64 28, 28⟩ + s.rd = [key, last, args] ∧ s.wr = [state, scr] ∧ + key.Disjoint state ∧ key.Disjoint scr ∧ last.Disjoint state ∧ last.Disjoint scr ∧ + state.Disjoint scr ∧ args.Disjoint state ∧ args.Disjoint scr ∧ + ret.Disjoint state ∧ ret.Disjoint scr ∧ + stack.Disjoint key ∧ stack.Disjoint last ∧ stack.Disjoint state ∧ stack.Disjoint scr ∧ + (arg s 0).toNat + 272 ≤ 2 ^ 32 ∧ (arg s 2).toNat + 16 ≤ 2 ^ 32 ∧ + (arg s 3).toNat + (arg s 4).toNat ≤ 2 ^ 32 ∧ (arg s 5).toNat + 2176 ≤ 2 ^ 32 ∧ + 28 ≤ (s.gpr .esp).toNat ∧ (s.gpr .esp).toNat + 28 ≤ 2 ^ 32 ∧ + ((arg s 1).toNat = 10 ∨ (arg s 1).toNat = 12 ∨ (arg s 1).toNat = 14) ∧ (arg s 4).toNat ≤ 16 + post s s' := + let ciph := ciphAt s.mem ((arg s 0).setWidth 64) (arg s 1).toNat + let ks := Spec.Cmac.subkeys ciph 16 + Spec.Aes.bytesAt s.mem ((arg s 0).setWidth 64 + 240) 32 = ks.1 ++ ks.2 → + ∀ msg : List Byte, msg.length % 16 = 0 → (msg = [] ∨ 0 < (arg s 4).toNat) → + Spec.Aes.bytesAt s.mem ((arg s 2).setWidth 64) 16 = + Spec.Cmac.chain ciph (Spec.Cmac.zeros 16) (Spec.Cmac.blocks 16 msg) → + Spec.Aes.bytesAt s'.mem ((arg s 2).setWidth 64) 16 = + Spec.Cmac.macFull ciph 16 (msg ++ Spec.Aes.bytesAt s.mem ((arg s 3).setWidth 64) (arg s 4).toNat) + pub s₁ s₂ := s₁.gpr .esp = s₂.gpr .esp ∧ ∀ i < 6, arg s₁ i = arg s₂ i + +end VG.Proof.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/Dbl.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/Dbl.lean new file mode 100644 index 000000000..3dfb86dfb --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/Dbl.lean @@ -0,0 +1,136 @@ +import VerifiedGarbage.Proof.CmacAes.X86.Save +import VerifiedGarbage.Proof.Cmac.Dbl32 +import VerifiedGarbage.Proof.Cmac.Dbl + +/-! +# AES-CMAC on x86: doubling a block in four 32-bit words + +Untrusted: everything here is checked by Lean. `dbl src dst` loads a block +as four byte-reversed words (`bswap`), the block as a big-endian integer +(`Cmac.ofBytes_rev4`), doubles the integer a word at a time +(`Cmac.dbl_words4`, shifting by `add r, r`), and stores the words +byte-reversed again (`Cmac.le4_rev4`). +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 VG.Impl.CmacAes.X86 +open VG.Proof.MdStream.X86 (Upd Mupd wp_mov wp_movi wp_movm wp_store wp_add wp_sub wp_andi wp_or wp_shr wp_bswap) + +theorem bswap_eq (a : BitVec 32) : bswap a = byteRev32 a := rfl + +theorem add_self_shl (x : BitVec 32) : x + x = x <<< 1 := by + apply BitVec.eq_of_toNat_eq + simp only [BitVec.toNat_add, BitVec.toNat_shiftLeft, Nat.shiftLeft_eq] + omega + +/-- The memory after `dbl src dst`, with `ebx` pointing at `A`. -/ +def dblMem (m : Mem) (A : Addr) (src dst : Nat) : Mem := + let P := A + BitVec.ofNat 64 src + let b₀ := byteRev32 (m.readW P 32) + let b₁ := byteRev32 (m.readW (P + BitVec.ofNat 64 4) 32) + let b₂ := byteRev32 (m.readW (P + BitVec.ofNat 64 8) 32) + let b₃ := byteRev32 (m.readW (P + BitVec.ofNat 64 12) 32) + Proof.Cmac.store4 m (A + BitVec.ofNat 64 dst) (byteRev32 (Proof.Cmac.dblW0 b₀ b₁)) + (byteRev32 (Proof.Cmac.dblW0 b₁ b₂)) (byteRev32 (Proof.Cmac.dblW0 b₂ b₃)) (byteRev32 (Proof.Cmac.dblW3 b₀ b₃)) + +theorem dblMem_frame (m : Mem) (A : Addr) (src dst : Nat) : + Frame [⟨A + BitVec.ofNat 64 dst, 16⟩] m (dblMem m A src dst) := + Proof.Cmac.frame_store4 _ _ _ _ _ + +theorem dblMem_bytes (m : Mem) (A : Addr) (src dst : Nat) : + Spec.Aes.bytesAt (dblMem m A src dst) (A + BitVec.ofNat 64 dst) 16 = + Spec.Cmac.dbl 16 (Spec.Aes.bytesAt m (A + BitVec.ofNat 64 src) 16) := by + simp only [dblMem] + rw [Proof.Cmac.bytesAt_store4, Proof.Cmac.le4_rev4, Proof.Cmac.dbl_words4, + Proof.Cmac.dbl_eq (Proof.Cmac.bytesAt_length _ _ _), Proof.Cmac.ofBytes_rev4] + +/-- `dbl src dst`, with `ebx` pointing at `K`. -/ +theorem dbl_wp {is : List Instr} {s : State} {Q : State → Prop} {K : BitVec 32} {src dst : Nat} + (hb : s.gpr .ebx = K) (fs : K.toNat + src + 16 ≤ 2 ^ 32) (fd : K.toNat + dst + 16 ≤ 2 ^ 32) + (rS : Covers [⟨K.setWidth 64 + BitVec.ofNat 64 src, 16⟩] (s.rd ++ s.wr)) + (wD : Covers [⟨K.setWidth 64 + BitVec.ofNat 64 dst, 16⟩] s.wr) + (k : ∀ s', (∀ r, r ≠ .eax → r ≠ .ecx → r ≠ .edx → r ≠ .esi → r ≠ .edi → r ≠ .ebp → s'.gpr r = s.gpr r) → + s'.mem = dblMem s.mem (K.setWidth 64) src dst → s'.rd = s.rd → s'.wr = s.wr → WP isa (.block is) s' Q) : + WP isa (.block (dbl src dst ++ is)) s Q := by + simp only [dbl, List.cons_append, List.nil_append] + refine wp_movm (a := K.setWidth 64 + BitVec.ofNat 64 src) (by rw [ea_at', hb]; exact addr_eq (by omega)) + (in_word0 rS) fun s₁ u₁ => ?_ + refine wp_movm (a := K.setWidth 64 + BitVec.ofNat 64 src + BitVec.ofNat 64 4) + (by rw [ea_at', u₁.other _ (by decide), hb]; exact addr_word 4 fs (by decide)) + (by rw [u₁.rd, u₁.wr]; exact in_word rS (by decide)) fun s₂ u₂ => ?_ + refine wp_movm (a := K.setWidth 64 + BitVec.ofNat 64 src + BitVec.ofNat 64 8) + (by rw [ea_at', u₂.other _ (by decide), u₁.other _ (by decide), hb]; exact addr_word 8 fs (by decide)) + (by rw [u₂.rd, u₂.wr, u₁.rd, u₁.wr]; exact in_word rS (by decide)) fun s₃ u₃ => ?_ + refine wp_movm (a := K.setWidth 64 + BitVec.ofNat 64 src + BitVec.ofNat 64 12) + (by rw [ea_at', u₃.other _ (by decide), u₂.other _ (by decide), u₁.other _ (by decide), hb] + exact addr_word 12 fs (by decide)) + (by rw [u₃.rd, u₃.wr, u₂.rd, u₂.wr, u₁.rd, u₁.wr]; exact in_word rS (by decide)) fun s₄ u₄ => ?_ + refine wp_bswap fun s₅ u₅ => wp_bswap fun s₆ u₆ => wp_bswap fun s₇ u₇ => wp_bswap fun s₈ u₈ => ?_ + refine wp_mov fun s₉ u₉ => wp_shr (by decide) fun s₁₀ u₁₀ => wp_movi fun s₁₁ u₁₁ => + wp_sub fun s₁₂ u₁₂ _ => wp_andi fun s₁₃ u₁₃ => ?_ + refine wp_add fun s₁₄ u₁₄ => wp_mov fun s₁₅ u₁₅ => wp_shr (by decide) fun s₁₆ u₁₆ => wp_or fun s₁₇ u₁₇ => ?_ + refine wp_add fun s₁₈ u₁₈ => wp_mov fun s₁₉ u₁₉ => wp_shr (by decide) fun s₂₀ u₂₀ => wp_or fun s₂₁ u₂₁ => ?_ + refine wp_add fun s₂₂ u₂₂ => wp_mov fun s₂₃ u₂₃ => wp_shr (by decide) fun s₂₄ u₂₄ => wp_or fun s₂₅ u₂₅ => ?_ + refine wp_add fun s₂₆ u₂₆ => wp_xor fun s₂₇ u₂₇ => ?_ + refine wp_bswap fun s₂₈ u₂₈ => wp_bswap fun s₂₉ u₂₉ => wp_bswap fun s₃₀ u₃₀ => wp_bswap fun s₃₁ u₃₁ => ?_ + have g : ∀ r, r ≠ .eax → r ≠ .ecx → r ≠ .edx → r ≠ .esi → r ≠ .edi → r ≠ .ebp → s₃₁.gpr r = s.gpr r := + fun r ha hc hd hs hi hp => by + rw [u₃₁.other _ hs, u₃₀.other _ hd, u₂₉.other _ hc, u₂₈.other _ ha, u₂₇.other _ hs, u₂₆.other _ hs, + u₂₅.other _ hd, u₂₄.other _ hi, u₂₃.other _ hi, u₂₂.other _ hd, u₂₁.other _ hc, u₂₀.other _ hi, + u₁₉.other _ hi, u₁₈.other _ hc, u₁₇.other _ ha, u₁₆.other _ hi, u₁₅.other _ hi, u₁₄.other _ ha, + u₁₃.other _ hp, u₁₂.other _ hp, u₁₁.other _ hp, u₁₀.other _ hi, u₉.other _ hi, u₈.other _ hs, + u₇.other _ hd, u₆.other _ hc, u₅.other _ ha, u₄.other _ hs, u₃.other _ hd, u₂.other _ hc, u₁.other _ ha] + have gb : s₃₁.gpr .ebx = K := by + rw [g _ (by decide) (by decide) (by decide) (by decide) (by decide) (by decide), hb] + have m31 : s₃₁.mem = s.mem := by + rw [u₃₁.mem, u₃₀.mem, u₂₉.mem, u₂₈.mem, u₂₇.mem, u₂₆.mem, u₂₅.mem, u₂₄.mem, u₂₃.mem, u₂₂.mem, u₂₁.mem, + u₂₀.mem, u₁₉.mem, u₁₈.mem, u₁₇.mem, u₁₆.mem, u₁₅.mem, u₁₄.mem, u₁₃.mem, u₁₂.mem, u₁₁.mem, u₁₀.mem, + u₉.mem, u₈.mem, u₇.mem, u₆.mem, u₅.mem, u₄.mem, u₃.mem, u₂.mem, u₁.mem] + have rd31 : s₃₁.rd = s.rd := by + rw [u₃₁.rd, u₃₀.rd, u₂₉.rd, u₂₈.rd, u₂₇.rd, u₂₆.rd, u₂₅.rd, u₂₄.rd, u₂₃.rd, u₂₂.rd, u₂₁.rd, + u₂₀.rd, u₁₉.rd, u₁₈.rd, u₁₇.rd, u₁₆.rd, u₁₅.rd, u₁₄.rd, u₁₃.rd, u₁₂.rd, u₁₁.rd, u₁₀.rd, + u₉.rd, u₈.rd, u₇.rd, u₆.rd, u₅.rd, u₄.rd, u₃.rd, u₂.rd, u₁.rd] + have wr31 : s₃₁.wr = s.wr := by + rw [u₃₁.wr, u₃₀.wr, u₂₉.wr, u₂₈.wr, u₂₇.wr, u₂₆.wr, u₂₅.wr, u₂₄.wr, u₂₃.wr, u₂₂.wr, u₂₁.wr, + u₂₀.wr, u₁₉.wr, u₁₈.wr, u₁₇.wr, u₁₆.wr, u₁₅.wr, u₁₄.wr, u₁₃.wr, u₁₂.wr, u₁₁.wr, u₁₀.wr, + u₉.wr, u₈.wr, u₇.wr, u₆.wr, u₅.wr, u₄.wr, u₃.wr, u₂.wr, u₁.wr] + -- The four words, byte-reversed. + have b₀ : s₈.gpr .eax = byteRev32 (s.mem.readW (K.setWidth 64 + BitVec.ofNat 64 src) 32) := by + rw [u₈.other _ (by decide), u₇.other _ (by decide), u₆.other _ (by decide), u₅.gpr, u₄.other _ (by decide), + u₃.other _ (by decide), u₂.other _ (by decide), u₁.gpr, bswap_eq] + have b₁ : s₈.gpr .ecx = byteRev32 (s.mem.readW (K.setWidth 64 + BitVec.ofNat 64 src + BitVec.ofNat 64 4) 32) := by + rw [u₈.other _ (by decide), u₇.other _ (by decide), u₆.gpr, u₅.other _ (by decide), u₄.other _ (by decide), + u₃.other _ (by decide), u₂.gpr, u₁.mem, bswap_eq] + have b₂ : s₈.gpr .edx = byteRev32 (s.mem.readW (K.setWidth 64 + BitVec.ofNat 64 src + BitVec.ofNat 64 8) 32) := by + rw [u₈.other _ (by decide), u₇.gpr, u₆.other _ (by decide), u₅.other _ (by decide), u₄.other _ (by decide), + u₃.gpr, u₂.mem, u₁.mem, bswap_eq] + have b₃ : s₈.gpr .esi = byteRev32 (s.mem.readW (K.setWidth 64 + BitVec.ofNat 64 src + BitVec.ofNat 64 12) 32) := by + rw [u₈.gpr, u₇.other _ (by decide), u₆.other _ (by decide), u₅.other _ (by decide), u₄.gpr, u₃.mem, u₂.mem, + u₁.mem, bswap_eq] + have v : s₃₁.gpr .eax = byteRev32 (Proof.Cmac.dblW0 (s₈.gpr .eax) (s₈.gpr .ecx)) ∧ + s₃₁.gpr .ecx = byteRev32 (Proof.Cmac.dblW0 (s₈.gpr .ecx) (s₈.gpr .edx)) ∧ + s₃₁.gpr .edx = byteRev32 (Proof.Cmac.dblW0 (s₈.gpr .edx) (s₈.gpr .esi)) ∧ + s₃₁.gpr .esi = byteRev32 (Proof.Cmac.dblW3 (s₈.gpr .eax) (s₈.gpr .esi)) := by + simp (disch := decide) only [u₃₁.gpr, u₃₁.other, u₃₀.gpr, u₃₀.other, u₂₉.gpr, u₂₉.other, u₂₈.gpr, u₂₈.other, u₂₇.gpr, u₂₇.other, u₂₆.gpr, u₂₆.other, u₂₅.gpr, u₂₅.other, u₂₄.gpr, u₂₄.other, u₂₃.gpr, u₂₃.other, u₂₂.gpr, u₂₂.other, u₂₁.gpr, u₂₁.other, u₂₀.gpr, u₂₀.other, u₁₉.gpr, u₁₉.other, u₁₈.gpr, u₁₈.other, u₁₇.gpr, u₁₇.other, u₁₆.gpr, u₁₆.other, u₁₅.gpr, u₁₅.other, u₁₄.gpr, u₁₄.other, u₁₃.gpr, u₁₃.other, u₁₂.gpr, u₁₂.other, u₁₁.gpr, u₁₁.other, u₁₀.gpr, u₁₀.other, u₉.gpr, u₉.other, + bswap_eq, add_self_shl, Proof.Cmac.dblW0, Proof.Cmac.dblW3, and_self] + obtain ⟨v₀, v₁, v₂, v₃⟩ := v + refine wp_store (a := K.setWidth 64 + BitVec.ofNat 64 dst) (by rw [ea_at', gb]; exact addr_eq (by omega)) + (by rw [wr31]; exact in_word0 wD) fun s₃₂ v₃₂ => ?_ + refine wp_store (a := K.setWidth 64 + BitVec.ofNat 64 dst + BitVec.ofNat 64 4) + (by rw [ea_at', v₃₂.gpr, gb]; exact addr_word 4 fd (by decide)) + (by rw [v₃₂.wr, wr31]; exact in_word wD (by decide)) fun s₃₃ v₃₃ => ?_ + refine wp_store (a := K.setWidth 64 + BitVec.ofNat 64 dst + BitVec.ofNat 64 8) + (by rw [ea_at', v₃₃.gpr, v₃₂.gpr, gb]; exact addr_word 8 fd (by decide)) + (by rw [v₃₃.wr, v₃₂.wr, wr31]; exact in_word wD (by decide)) fun s₃₄ v₃₄ => ?_ + refine wp_store (a := K.setWidth 64 + BitVec.ofNat 64 dst + BitVec.ofNat 64 12) + (by rw [ea_at', v₃₄.gpr, v₃₃.gpr, v₃₂.gpr, gb]; exact addr_word 12 fd (by decide)) + (by rw [v₃₄.wr, v₃₃.wr, v₃₂.wr, wr31]; exact in_word wD (by decide)) fun s₃₅ v₃₅ => k s₃₅ ?_ ?_ ?_ ?_ + · intro r ha hc hd hs hi hp + rw [v₃₅.gpr, v₃₄.gpr, v₃₃.gpr, v₃₂.gpr, g r ha hc hd hs hi hp] + · rw [v₃₅.mem, v₃₄.mem, v₃₃.mem, v₃₂.mem, v₃₄.gpr, v₃₃.gpr, v₃₂.gpr, m31, v₀, v₁, v₂, v₃, b₀, b₁, b₂, b₃] + rfl + · rw [v₃₅.rd, v₃₄.rd, v₃₃.rd, v₃₂.rd, rd31] + · rw [v₃₅.wr, v₃₄.wr, v₃₃.wr, v₃₂.wr, wr31] + +end VG.Proof.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/Finalize.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/Finalize.lean new file mode 100644 index 000000000..031238ad3 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/Finalize.lean @@ -0,0 +1,473 @@ +import VerifiedGarbage.Proof.CmacAes.X86.UpdateCorrect +import VerifiedGarbage.Proof.Cmac.Block +import VerifiedGarbage.Proof.Framework.WriteBytes + +/-! +# AES-CMAC on x86: `vg_cmac_aes_finalize`, the last block + +Untrusted: everything here is checked by Lean. The steps that form the last +block `Mₙ` (§6.2 step 4) in the counter block, before the chaining value is +XORed in: `Mₙ* ⊕ K1` for a complete block (`full_wp`), else `Mₙ*` copied a +byte at a time onto zeros (`copy_wp`), `0x80` after it, and the block XORed +with `K2` (`partial_wp`). The arguments are those of `vg_cmac_aes_update` +but `last` (`Dp`) and `last_len` (`N`), so its abbreviations serve. +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 VG.Impl.CmacAes.X86 +open VG.Proof.MdStream.X86 (Upd Mupd Fupd wp_mov wp_movi wp_addi wp_subi wp_cmpi wp_test wp_movzx8 wp_store8 + eval_e eval_ne ofNat_beq_zero sub_ofNat) +open VG.WriteBytes (writeBytes writeBytes_nil writeBytes_snoc writeBytes_frame) + +section +variable (s₀ : State) + +/-- The key: the schedule and the subkeys `K1` and `K2` after it. -/ +abbrev keyR : Region := ⟨(W s₀).setWidth 64, 272⟩ +/-- The last bytes `Mₙ*`. -/ +abbrev lastR : Region := ⟨(Dp s₀).setWidth 64, N s₀⟩ + +/-- The last block `Mₙ` (§6.2 step 4), from the key and the last bytes. -/ +abbrev mn : List Byte := + Spec.Cmac.lastBlock 16 (Spec.Aes.bytesAt s₀.mem ((W s₀).setWidth 64 + BitVec.ofNat 64 240) 16) + (Spec.Aes.bytesAt s₀.mem ((W s₀).setWidth 64 + BitVec.ofNat 64 256) 16) + (Spec.Aes.bytesAt s₀.mem ((Dp s₀).setWidth 64) (N s₀)) + +/-- The counter block. -/ +abbrev Ca : Addr := (S s₀).setWidth 64 + BitVec.ofNat 64 2048 + +end + +/-- The precondition, by name. -/ +structure FPre (s₀ : State) : Prop where + rd : s₀.rd = [keyR s₀, lastR s₀, argsR s₀] + wr : s₀.wr = [stR s₀, scrR s₀] + key_st : (keyR s₀).Disjoint (stR s₀) + key_scr : (keyR s₀).Disjoint (scrR s₀) + last_st : (lastR s₀).Disjoint (stR s₀) + last_scr : (lastR s₀).Disjoint (scrR s₀) + st_scr : (stR s₀).Disjoint (scrR s₀) + args_st : (argsR s₀).Disjoint (stR s₀) + args_scr : (argsR s₀).Disjoint (scrR s₀) + ret_st : (retR s₀).Disjoint (stR s₀) + ret_scr : (retR s₀).Disjoint (scrR s₀) + b_key : (stkR s₀).Disjoint (keyR s₀) + b_last : (stkR s₀).Disjoint (lastR s₀) + b_st : (stkR s₀).Disjoint (stR s₀) + b_scr : (stkR s₀).Disjoint (scrR s₀) + key_fit : (W s₀).toNat + 272 ≤ 2 ^ 32 + st_fit : (St s₀).toNat + 16 ≤ 2 ^ 32 + last_fit : (Dp s₀).toNat + N s₀ ≤ 2 ^ 32 + scr_fit : (S s₀).toNat + 2176 ≤ 2 ^ 32 + esp28 : 28 ≤ (E s₀).toNat + esp_fit : (E s₀).toNat + 28 ≤ 2 ^ 32 + rounds : R s₀ = 10 ∨ R s₀ = 12 ∨ R s₀ = 14 + len : N s₀ ≤ 16 + +theorem FPre.of {s₀ : State} (h : finalizeX86.pre s₀) : FPre s₀ := + let ⟨a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, t, u, v, w, x⟩ := h + ⟨a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, t, u, v, w, x⟩ + +theorem in_cov {rs : List Region} {a : Addr} {n : Nat} (h : Covers [⟨a, n⟩] rs) : InRegions rs a n := + h _ _ ⟨_, List.mem_singleton_self _, Region.contains_self _ _⟩ + +section +variable {s₀ : State} (hp : FPre s₀) +include hp + +theorem FPre.below_eq : below (E s₀) 28 = stkR s₀ := by + simp only [below]; rw [Taint.sub_setWidth hp.esp28] + +theorem FPre.argA {i : Nat} (hi : i < 6) : argAddr s₀ i = argAddr s₀ 0 + BitVec.ofNat 64 (4 * i) := by + have : (s₀.gpr .esp).toNat + 28 ≤ 2 ^ 32 := hp.esp_fit + simp only [argAddr] + rw [show (s₀.gpr .esp + BitVec.ofNat 32 (4 + 4 * i)).setWidth 64 = addr (s₀.gpr .esp) (4 + 4 * i) from rfl, + show (s₀.gpr .esp + BitVec.ofNat 32 (4 + 4 * 0)).setWidth 64 = addr (s₀.gpr .esp) (4 + 4 * 0) from rfl, + addr_eq (by omega), addr_eq (by omega), Offset.add_add] + +theorem FPre.arg_sub {i : Nat} (hi : i < 6) : Region.Sub ⟨argAddr s₀ i, 4⟩ (argsR s₀) := by + rw [hp.argA hi]; exact Offset.sub_base _ (by omega) + +theorem FPre.arg_in {i : Nat} (hi : i < 6) : InRegions (s₀.rd ++ s₀.wr) (argAddr s₀ i) 4 := by + refine ⟨argsR s₀, by simp [hp.rd], ?_⟩ + rw [hp.argA hi]; exact Offset.contains_base _ (by omega) (by omega) + +theorem FPre.args_stk : (argsR s₀).Disjoint (stkR s₀) := by + have : (s₀.gpr .esp).toNat + 28 ≤ 2 ^ 32 := hp.esp_fit + have e : argAddr s₀ 0 = (E s₀).setWidth 64 + BitVec.ofNat 64 4 := addr_eq (by omega) + show Region.Disjoint ⟨argAddr s₀ 0, 24⟩ _ + rw [e]; exact (Offset.disjoint_below_above _ (by decide)).symm + +/-- The stack arguments are unchanged where only `Big` changes. -/ +theorem FPre.arg_keep {m : Mem} (hf : Frame (Big s₀) s₀.mem m) {i : Nat} (hi : i < 6) : + m.readW (argAddr s₀ i) 32 = arg s₀ i := + hf.readW (Region.contains_self _ _) (fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact hp.args_st.sub_left (hp.arg_sub hi) + · exact hp.args_scr.sub_left (hp.arg_sub hi) + · exact hp.args_stk.sub_left (hp.arg_sub hi)) (by decide) + +theorem FPre.cS {d n : Nat} (h : d + n ≤ 2176) : + Covers [⟨(S s₀).setWidth 64 + BitVec.ofNat 64 d, n⟩] s₀.wr := by + rw [hp.wr] + exact Covers.of_sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; exact ⟨scrR s₀, by simp, d, rfl, h⟩ + +theorem FPre.cKey {d n : Nat} (h : d + n ≤ 272) : + Covers [⟨(W s₀).setWidth 64 + BitVec.ofNat 64 d, n⟩] (s₀.rd ++ s₀.wr) := by + rw [hp.rd] + exact Covers.of_sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; exact ⟨keyR s₀, by simp, d, rfl, h⟩ + +theorem FPre.cLast {d n : Nat} (h : d + n ≤ N s₀) : + Covers [⟨(Dp s₀).setWidth 64 + BitVec.ofNat 64 d, n⟩] (s₀.rd ++ s₀.wr) := by + rw [hp.rd] + exact Covers.of_sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; exact ⟨lastR s₀, by simp, d, rfl, h⟩ + +theorem FPre.ca_key {d n : Nat} (h : d + n ≤ 272) : + (⟨Ca s₀, 16⟩ : Region).Disjoint ⟨(W s₀).setWidth 64 + BitVec.ofNat 64 d, n⟩ := + (hp.key_scr.symm.sub_left (Offset.sub_base _ (by decide))).sub_right (Offset.sub_base _ h) + +theorem FPre.ca_last : (⟨Ca s₀, 16⟩ : Region).Disjoint (lastR s₀) := + hp.last_scr.symm.sub_left (Offset.sub_base _ (by decide)) + +theorem FPre.cA : (S s₀ + BitVec.ofNat 32 2048).setWidth 64 = Ca s₀ := + addr_eq (by have := hp.scr_fit; omega) + +theorem FPre.key_bytes {d : Nat} (h : d + 16 ≤ 272) : + Spec.Aes.bytesAt (savedMem s₀) ((W s₀).setWidth 64 + BitVec.ofNat 64 d) 16 = + Spec.Aes.bytesAt s₀.mem ((W s₀).setWidth 64 + BitVec.ofNat 64 d) 16 := + Proof.Cmac.bytesAt_frame16 (savedMem_frame s₀) fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact hp.key_scr.sub_left (Offset.sub_base _ h) + +theorem FPre.last_bytes : Spec.Aes.bytesAt (savedMem s₀) ((Dp s₀).setWidth 64) (N s₀) = + Spec.Aes.bytesAt s₀.mem ((Dp s₀).setWidth 64) (N s₀) := + Proof.Cmac.bytesAt_frame (savedMem_frame s₀) (fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; exact hp.last_scr) (by have := hp.len; omega) + +end + +/-! ## Saving the registers -/ + +theorem finSave_eq : finSave = .mov .eax (argOp 5) :: (saved.map (fun p => Instr.store (at_ .eax p.2) p.1) ++ + ([.mov .ebp (.reg .eax), .mov .ecx (argOp 4), .alu .cmp .ecx (.imm 16)] : List Instr)) := rfl + +/-- What `finSave` leaves. -/ +structure FS (s₀ s : State) : Prop where + keep : ∀ r, r ≠ .eax → r ≠ .ecx → r ≠ .ebp → s.gpr r = s₀.gpr r + ecx : s.gpr .ecx = BitVec.ofNat 32 (N s₀) + ebp : s.gpr .ebp = S s₀ + zf : s.zf = some (decide (N s₀ = 16)) + mem : s.mem = savedMem s₀ + rd : s.rd = s₀.rd + wr : s.wr = s₀.wr + +theorem finSave_wp {s₀ : State} (hp : FPre s₀) : WP isa (.block finSave) s₀ (FS s₀) := by + have hsc := hp.scr_fit + rw [finSave_eq] + refine wp_arg (s₀ := s₀) rfl (hp.arg_in (by decide)) rfl fun s₁ u₁ => ?_ + have h₁ : s₁.gpr .eax = S s₀ := u₁.gpr + refine saveList_ok saved s₁ _ (fun p hp' => ?_) fun s₂ g₂ rd₂ wr₂ m₂ => ?_ + · have hb := saved_bound p hp' + rw [h₁, u₁.wr, hp.wr] + exact ⟨by omega, ⟨scrR s₀, by simp, Offset.contains_base _ (by omega) (by omega)⟩⟩ + have hm₂ : s₂.mem = savedMem s₀ := by + rw [m₂, u₁.mem, h₁, savedMem] + exact saveMem_congr _ _ _ fun p hp' => u₁.other _ (saved_ne_eax p hp') + have esp₂ : s₂.gpr .esp = s₀.gpr .esp := by rw [g₂, u₁.other _ (by decide)] + have rw₂ : s₂.rd ++ s₂.wr = s₀.rd ++ s₀.wr := by rw [rd₂, wr₂, u₁.rd, u₁.wr] + refine wp_mov fun s₃ u₃ => ?_ + refine wp_arg (s₀ := s₀) (by rw [u₃.other _ (by decide), esp₂]) + (by rw [u₃.rd, u₃.wr, rw₂]; exact hp.arg_in (by decide)) + (by rw [u₃.mem, hm₂]; exact hp.arg_keep (savedMem_big s₀) (by decide)) fun s₄ u₄ => ?_ + refine wp_cmpi fun s₅ f₅ _ z₅ => WP.block_nil ⟨fun r ha hc hb => ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ + · rw [f₅.gpr, u₄.other _ hc, u₃.other _ hb, g₂, u₁.other _ ha] + · rw [f₅.gpr, u₄.gpr]; exact arg_ofNat s₀ 4 + · rw [f₅.gpr, u₄.other _ (by decide), u₃.gpr, g₂, h₁] + · rw [z₅, u₄.gpr, arg_ofNat s₀ 4, show (16 : BitVec 32) = BitVec.ofNat 32 16 from rfl, + MdStream.X86.sub_beq (arg s₀ 4).isLt (by decide)] + · rw [f₅.mem, u₄.mem, u₃.mem, hm₂] + · rw [f₅.rd, u₄.rd, u₃.rd, rd₂, u₁.rd] + · rw [f₅.wr, u₄.wr, u₃.wr, wr₂, u₁.wr] + +/-! ## The last block -/ + +/-- What the branch on the length leaves: `Mₙ` in the counter block. -/ +structure BPost (s₀ s : State) : Prop where + ebp : s.gpr .ebp = S s₀ + esp : s.gpr .esp = E s₀ + rd : s.rd = s₀.rd + wr : s.wr = s₀.wr + frame : Frame [⟨Ca s₀, 16⟩] (savedMem s₀) s.mem + blk : Spec.Aes.bytesAt s.mem (Ca s₀) 16 = mn s₀ + +theorem full_eq : full = .mov .ebx (argOp 3) :: .mov .edx (argOp 0) :: (xor4 .ebx .edx .ebp 0 240 2048 ++ []) := rfl + +theorem full_wp {s₀ : State} (hp : FPre s₀) (hL : N s₀ = 16) {s : State} (h : FS s₀ s) : + WP isa (.block full) s (BPost s₀) := by + have sf := hp.scr_fit + have kf := hp.key_fit + have lf := hp.last_fit + have hrw : s.rd ++ s.wr = s₀.rd ++ s₀.wr := by rw [h.rd, h.wr] + have esp : s.gpr .esp = E s₀ := h.keep _ (by decide) (by decide) (by decide) + rw [full_eq] + refine wp_arg (s₀ := s₀) esp (by rw [hrw]; exact hp.arg_in (by decide)) + (by rw [h.mem]; exact hp.arg_keep (savedMem_big s₀) (by decide)) fun s₁ u₁ => ?_ + refine wp_arg (s₀ := s₀) (by rw [u₁.other _ (by decide), esp]) + (by rw [u₁.rd, u₁.wr, hrw]; exact hp.arg_in (by decide)) + (by rw [u₁.mem, h.mem]; exact hp.arg_keep (savedMem_big s₀) (by decide)) fun s₂ u₂ => ?_ + have b₂ : s₂.gpr .ebx = Dp s₀ := by rw [u₂.other _ (by decide), u₁.gpr] + have d₂ : s₂.gpr .edx = W s₀ := u₂.gpr + have p₂ : s₂.gpr .ebp = S s₀ := by rw [u₂.other _ (by decide), u₁.other _ (by decide), h.ebp] + have rw₂ : s₂.rd ++ s₂.wr = s₀.rd ++ s₀.wr := by rw [u₂.rd, u₂.wr, u₁.rd, u₁.wr, hrw] + have w₂ : s₂.wr = s₀.wr := by rw [u₂.wr, u₁.wr, h.wr] + have lf' : (Dp s₀).toNat + 16 ≤ 2 ^ 32 := by rw [← hL]; exact lf + refine xor4_ok (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) + (by rw [b₂]; omega) (by rw [d₂]; omega) (by rw [p₂]; omega) + (by rw [b₂, rw₂]; exact hp.cLast (by omega)) (by rw [d₂, rw₂]; exact hp.cKey (by decide)) + (by rw [p₂, w₂]; exact hp.cS (by decide)) fun s₃ g₃ => WP.block_nil ?_ + refine ⟨by rw [g₃.gpr _ (by decide) (by decide), p₂], + by rw [g₃.gpr _ (by decide) (by decide), u₂.other _ (by decide), u₁.other _ (by decide), esp], + by rw [g₃.rd, u₂.rd, u₁.rd, h.rd], by rw [g₃.wr, w₂], ?_, ?_⟩ + · rw [g₃.mem, p₂, u₂.mem, u₁.mem, h.mem]; exact Proof.Cmac.xor4Mem_frame _ _ _ _ + · rw [g₃.mem, p₂, b₂, d₂, u₂.mem, u₁.mem, h.mem, add0, Proof.Cmac.xor4Mem_bytes _ + (Proof.Cmac.Sep4.of_disjoint (hp.ca_last.sub_right (Region.sub_prefix (by omega)))) + (Proof.Cmac.Sep4.of_disjoint (hp.ca_key (by decide))), hp.key_bytes (by decide)] + have lb := hp.last_bytes + rw [hL] at lb + rw [lb] + simp only [mn, Spec.Cmac.lastBlock, Proof.Cmac.bytesAt_length, hL, ite_true] + exact Proof.Cmac.xor_comm _ _ + +/-! ## Copying the last bytes -/ + +theorem byte_rt32 (b : BitVec 8) : (b.setWidth 32).setWidth 8 = b := by + apply BitVec.eq_of_toNat_eq + have := b.isLt + simp only [BitVec.toNat_setWidth] + omega + +theorem addr_at {p : BitVec 32} {i : Nat} (h : p.toNat + i < 2 ^ 32) : + addr (p + BitVec.ofNat 32 i) 0 = p.setWidth 64 + BitVec.ofNat 64 i := by + simp only [addr, add0']; exact addr_eq h + +theorem copy_wp {s : State} {p c : BitVec 32} {L : Nat} (hL₀ : 0 < L) (hL : L ≤ 16) + (hsi : s.gpr .esi = p) (hdi : s.gpr .edi = c) (hcx : s.gpr .ecx = BitVec.ofNat 32 L) + (fp : p.toNat + L ≤ 2 ^ 32) (fc : c.toNat + 16 ≤ 2 ^ 32) + (hr : Covers [⟨p.setWidth 64, L⟩] (s.rd ++ s.wr)) (hw : Covers [⟨c.setWidth 64, 16⟩] s.wr) + (hd : (⟨p.setWidth 64, L⟩ : Region).Disjoint ⟨c.setWidth 64, 16⟩) : + WP isa copy s fun s' => + s'.mem = writeBytes s.mem (c.setWidth 64) (Spec.Aes.bytesAt s.mem (p.setWidth 64) L) ∧ + s'.gpr .edi = c + BitVec.ofNat 32 L ∧ + (∀ r, r ≠ .eax → r ≠ .ecx → r ≠ .esi → r ≠ .edi → s'.gpr r = s.gpr r) ∧ + s'.rd = s.rd ∧ s'.wr = s.wr := by + refine WP.loop (M := isa) (body := .block [.movzx8 .eax (at_ .esi 0), .store8 (at_ .edi 0) .al, + .alu .add .esi (.imm 1), .alu .add .edi (.imm 1), .alu .sub .ecx (.imm 1)]) (c := .ne) + (fun (n : Nat) (t : State) => ∃ i, n = L - i ∧ i < L ∧ t.gpr .esi = p + BitVec.ofNat 32 i ∧ + t.gpr .edi = c + BitVec.ofNat 32 i ∧ t.gpr .ecx = BitVec.ofNat 32 (L - i) ∧ + t.mem = writeBytes s.mem (c.setWidth 64) (Spec.Aes.bytesAt s.mem (p.setWidth 64) i) ∧ + (∀ r, r ≠ .eax → r ≠ .ecx → r ≠ .esi → r ≠ .edi → t.gpr r = s.gpr r) ∧ + t.rd = s.rd ∧ t.wr = s.wr) ?_ (L - 0) _ + ⟨0, rfl, hL₀, by rw [hsi, add0'], by rw [hdi, add0'], by rw [hcx, Nat.sub_zero], + by simp [Spec.Aes.bytesAt, writeBytes_nil], fun _ _ _ _ _ => rfl, rfl, rfl⟩ + rintro n t ⟨i, rfl, hi, xsi, xdi, xcx, mem, g, rd, wr⟩ + refine wp_movzx8 (a := p.setWidth 64 + BitVec.ofNat 64 i) (by rw [ea_at', xsi]; exact addr_at (by omega)) + (by rw [rd, wr]; exact hr _ _ ⟨_, List.mem_singleton_self _, Offset.contains_base _ (by omega) (by omega)⟩) + fun t₁ u₁ => ?_ + refine wp_store8 (a := c.setWidth 64 + BitVec.ofNat 64 i) + (by rw [ea_at', u₁.other _ (by decide), xdi]; exact addr_at (by omega)) + (by rw [u₁.wr, wr]; exact hw _ _ ⟨_, List.mem_singleton_self _, Offset.contains_base _ (by omega) (by omega)⟩) + fun t₂ v₂ => ?_ + refine wp_addi fun t₃ u₃ => wp_addi fun t₄ u₄ => wp_subi fun t₅ u₅ z₅ => WP.block_nil ?_ + have hlen : (Spec.Aes.bytesAt s.mem (p.setWidth 64) i).length = i := Proof.Cmac.bytesAt_length _ _ _ + have hx : writeBytes s.mem (c.setWidth 64) (Spec.Aes.bytesAt s.mem (p.setWidth 64) i) + (p.setWidth 64 + BitVec.ofNat 64 i) = s.mem (p.setWidth 64 + BitVec.ofNat 64 i) := + (writeBytes_frame s.mem (c.setWidth 64) _ (R := ⟨c.setWidth 64, i⟩) (by rw [hlen]; exact Region.contains_self _ _)) _ + fun r hr hcon => by + simp only [List.mem_singleton] at hr; subst hr + exact hd _ (Offset.contains_base _ (by omega) (by omega)) (Region.sub_prefix (by omega) _ hcon) + have al : t₁.gpr Reg8.al.reg = (t.mem (p.setWidth 64 + BitVec.ofNat 64 i)).setWidth 32 := u₁.gpr + have hmem : t₅.mem = writeBytes s.mem (c.setWidth 64) (Spec.Aes.bytesAt s.mem (p.setWidth 64) (i + 1)) := by + rw [u₅.mem, u₄.mem, u₃.mem, v₂.mem, al, u₁.mem, mem, byte_rt32, hx, Proof.Cmac.bytesAt_succ, + writeBytes_snoc s.mem _ _ _ (by rw [hlen]; omega), hlen] + have cx₄ : t₄.gpr .ecx = BitVec.ofNat 32 (L - i) := by + rw [u₄.other _ (by decide), u₃.other _ (by decide), v₂.gpr, u₁.other _ (by decide), xcx] + have xcx' : t₅.gpr .ecx = BitVec.ofNat 32 (L - (i + 1)) := by + rw [u₅.gpr, cx₄, show (1 : BitVec 32) = BitVec.ofNat 32 1 from rfl, sub_ofNat (by omega), Nat.sub_sub] + have ev : isa.eval .ne t₅ = some !decide (L - (i + 1) = 0) := by + show VG.X86.eval .ne t₅ = _ + rw [eval_ne, z₅, cx₄, show (1 : BitVec 32) = BitVec.ofNat 32 1 from rfl, sub_ofNat (by omega), Nat.sub_sub, + ofNat_beq_zero (by omega)] + rfl + have gg : ∀ r, r ≠ .eax → r ≠ .ecx → r ≠ .esi → r ≠ .edi → t₅.gpr r = s.gpr r := fun r ha hc hs hd' => by + rw [u₅.other _ hc, u₄.other _ hd', u₃.other _ hs, v₂.gpr, u₁.other _ ha, g r ha hc hs hd'] + have xdi' : t₅.gpr .edi = c + BitVec.ofNat 32 (i + 1) := by + rw [u₅.other _ (by decide), u₄.gpr, u₃.other _ (by decide), v₂.gpr, u₁.other _ (by decide), xdi, + show (1 : BitVec 32) = BitVec.ofNat 32 1 from rfl, Offset.add_add] + have xsi' : t₅.gpr .esi = p + BitVec.ofNat 32 (i + 1) := by + rw [u₅.other _ (by decide), u₄.other _ (by decide), u₃.gpr, v₂.gpr, u₁.other _ (by decide), xsi, + show (1 : BitVec 32) = BitVec.ofNat 32 1 from rfl, Offset.add_add] + have rd' : t₅.rd = s.rd := by rw [u₅.rd, u₄.rd, u₃.rd, v₂.rd, u₁.rd, rd] + have wr' : t₅.wr = s.wr := by rw [u₅.wr, u₄.wr, u₃.wr, v₂.wr, u₁.wr, wr] + by_cases he : i + 1 = L + · left + exact ⟨by rw [ev]; simp [he], by rw [hmem, he], by rw [xdi', he], gg, rd', wr'⟩ + · right + exact ⟨by rw [ev]; simp; omega, L - (i + 1), by omega, i + 1, rfl, by omega, xsi', xdi', xcx', hmem, gg, + rd', wr'⟩ + +/-! ## A partial last block -/ + +theorem zero_eq : zero = zero4 .ebp 2048 ++ ([.mov .edi (.reg .ebp), .alu .add .edi (.imm (BitVec.ofNat 32 2048)), + .mov .esi (argOp 3), .mov .ecx (argOp 4), .alu .test .ecx (.reg .ecx)] : List Instr) := rfl + +theorem padK2_eq : padK2 = .mov .eax (.imm 0x80) :: .store8 (at_ .edi 0) .al :: .mov .edx (argOp 0) :: + (xor4 .ebp .edx .ebp 2048 256 2048 ++ []) := rfl + +theorem b80 : ((0x80 : BitVec 32).setWidth 8 : Byte) = 0x80 := by decide + +theorem partial_wp {s₀ : State} (hp : FPre s₀) (hL : N s₀ < 16) {s : State} (h : FS s₀ s) : + WP isa partialBlock s (BPost s₀) := by + have sf := hp.scr_fit + have sf' : (arg s₀ 5).toNat + 2176 ≤ 2 ^ 32 := sf + have kf := hp.key_fit + have lf := hp.last_fit + have hrw : s.rd ++ s.wr = s₀.rd ++ s₀.wr := by rw [h.rd, h.wr] + have cA := hp.cA + -- Zero the counter block. + refine WP.seq ?_ + rw [zero_eq] + refine zero4_ok (b := .ebp) (d := 2048) (by decide) (by rw [h.ebp]; omega) + (by rw [h.ebp, h.wr]; exact hp.cS (by decide)) fun s₁ g₁ m₁ rd₁ wr₁ => ?_ + have p₁ : s₁.gpr .ebp = S s₀ := by rw [g₁ _ (by decide), h.ebp] + have esp₁ : s₁.gpr .esp = E s₀ := by rw [g₁ _ (by decide), h.keep _ (by decide) (by decide) (by decide)] + have fz : Frame [⟨Ca s₀, 16⟩] (savedMem s₀) (Proof.Cmac.zero4 (savedMem s₀) (Ca s₀)) := + Proof.Cmac.frame_store4 _ _ _ _ _ + have mem₁ : s₁.mem = Proof.Cmac.zero4 (savedMem s₀) (Ca s₀) := by rw [m₁, h.ebp, h.mem] + have big₁ : Frame (Big s₀) s₀.mem s₁.mem := by + rw [mem₁] + exact (savedMem_big s₀).trans (fz.sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨scrR s₀, by simp, Offset.sub_base _ (by decide)⟩) + have rw₁ : s₁.rd ++ s₁.wr = s₀.rd ++ s₀.wr := by rw [rd₁, wr₁, hrw] + refine wp_mov fun s₂ u₂ => wp_addi fun s₃ u₃ => ?_ + refine wp_arg (s₀ := s₀) (by rw [u₃.other _ (by decide), u₂.other _ (by decide), esp₁]) + (by rw [u₃.rd, u₃.wr, u₂.rd, u₂.wr, rw₁]; exact hp.arg_in (by decide)) + (by rw [u₃.mem, u₂.mem]; exact hp.arg_keep big₁ (by decide)) fun s₄ u₄ => ?_ + refine wp_arg (s₀ := s₀) (by rw [u₄.other _ (by decide), u₃.other _ (by decide), u₂.other _ (by decide), esp₁]) + (by rw [u₄.rd, u₄.wr, u₃.rd, u₃.wr, u₂.rd, u₂.wr, rw₁]; exact hp.arg_in (by decide)) + (by rw [u₄.mem, u₃.mem, u₂.mem]; exact hp.arg_keep big₁ (by decide)) fun s₅ u₅ => ?_ + refine wp_test fun s₆ f₆ z₆ => WP.block_nil ?_ + have k₆ : ∀ r, r ≠ .ecx → r ≠ .esi → r ≠ .edi → s₆.gpr r = s₁.gpr r := fun r hc hs hd => by + rw [f₆.gpr, u₅.other _ hc, u₄.other _ hs, u₃.other _ hd, u₂.other _ hd] + have edi₆ : s₆.gpr .edi = S s₀ + BitVec.ofNat 32 2048 := by + rw [f₆.gpr, u₅.other _ (by decide), u₄.other _ (by decide), u₃.gpr, u₂.gpr, p₁] + have esi₆ : s₆.gpr .esi = Dp s₀ := by rw [f₆.gpr, u₅.other _ (by decide), u₄.gpr] + have ecx₆ : s₆.gpr .ecx = BitVec.ofNat 32 (N s₀) := by rw [f₆.gpr, u₅.gpr]; exact arg_ofNat s₀ 4 + have mem₆ : s₆.mem = Proof.Cmac.zero4 (savedMem s₀) (Ca s₀) := by + rw [f₆.mem, u₅.mem, u₄.mem, u₃.mem, u₂.mem, mem₁] + have rd₆ : s₆.rd = s₀.rd := by rw [f₆.rd, u₅.rd, u₄.rd, u₃.rd, u₂.rd, rd₁, h.rd] + have wr₆ : s₆.wr = s₀.wr := by rw [f₆.wr, u₅.wr, u₄.wr, u₃.wr, u₂.wr, wr₁, h.wr] + have ev : isa.eval .e s₆ = some (decide (N s₀ = 0)) := by + show VG.X86.eval .e s₆ = _ + rw [eval_e, z₆, u₅.gpr, arg_ofNat s₀ 4, ofNat_and_self_beq (arg s₀ 4).isLt] + have lastZ : Spec.Aes.bytesAt (Proof.Cmac.zero4 (savedMem s₀) (Ca s₀)) ((Dp s₀).setWidth 64) (N s₀) = + Spec.Aes.bytesAt s₀.mem ((Dp s₀).setWidth 64) (N s₀) := by + rw [Proof.Cmac.bytesAt_frame fz (fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; exact hp.ca_last.symm) (by omega), hp.last_bytes] + -- Copy the last bytes. + refine WP.seq (WP.mono (Q := fun (s₇ : State) => + s₇.mem = writeBytes (Proof.Cmac.zero4 (savedMem s₀) (Ca s₀)) (Ca s₀) + (Spec.Aes.bytesAt s₀.mem ((Dp s₀).setWidth 64) (N s₀)) ∧ + s₇.gpr .edi = S s₀ + BitVec.ofNat 32 (2048 + N s₀) ∧ + (∀ r, r ≠ .eax → r ≠ .ecx → r ≠ .esi → r ≠ .edi → s₇.gpr r = s₆.gpr r) ∧ + s₇.rd = s₀.rd ∧ s₇.wr = s₀.wr) ?_ fun s₇ h₇ => ?_) + · by_cases hL0 : N s₀ = 0 + · refine WP.ite true (by rw [ev]; simp [hL0]) (fun _ => WP.block_nil ?_) (fun h => by cases h) + refine ⟨by rw [mem₆, hL0]; simp [Spec.Aes.bytesAt, writeBytes_nil], by rw [edi₆, hL0], + fun _ _ _ _ _ => rfl, rd₆, wr₆⟩ + · refine WP.ite false (by rw [ev]; simp [hL0]) (fun h => by cases h) fun _ => ?_ + have hr := hp.cLast (d := 0) (n := N s₀) (by omega) + rw [add0] at hr + refine WP.mono (copy_wp (p := Dp s₀) (c := S s₀ + BitVec.ofNat 32 2048) (L := N s₀) (by omega) (by omega) + esi₆ edi₆ ecx₆ lf + (by rw [BitVec.toNat_add, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (a := 2048) (by decide), + Nat.mod_eq_of_lt (by omega)]; omega) + (by rw [rd₆, wr₆]; exact hr) (by rw [cA, wr₆]; exact hp.cS (by decide)) + (by rw [cA]; exact hp.ca_last.symm)) ?_ + rintro s₇ ⟨m₇, di₇, g₇, rd₇, wr₇⟩ + exact ⟨by rw [m₇, mem₆, cA, lastZ], by rw [di₇, Offset.add_add], g₇, by rw [rd₇, rd₆], by rw [wr₇, wr₆]⟩ + · obtain ⟨m₇, di₇, g₇, rd₇, wr₇⟩ := h₇ + rw [padK2_eq] + refine wp_movi fun s₈ u₈ => ?_ + refine wp_store8 (a := Ca s₀ + BitVec.ofNat 64 (N s₀)) + (by + rw [ea_at', u₈.other _ (by decide), di₇, addr_at (by omega)] + show _ = (S s₀).setWidth 64 + BitVec.ofNat 64 2048 + BitVec.ofNat 64 (N s₀) + rw [Offset.add_add]) + (by + rw [u₈.wr, wr₇] + show InRegions s₀.wr ((S s₀).setWidth 64 + BitVec.ofNat 64 2048 + BitVec.ofNat 64 (N s₀)) 1 + rw [Offset.add_add] + exact in_cov (hp.cS (d := 2048 + N s₀) (n := 1) (by omega))) fun s₉ v₉ => ?_ + have g₉ : ∀ r, r ≠ .eax → r ≠ .ecx → r ≠ .esi → r ≠ .edi → s₉.gpr r = s₁.gpr r := fun r ha hc hs hd => by + rw [v₉.gpr, u₈.other _ ha, g₇ r ha hc hs hd, k₆ r hc hs hd] + have esp₉ : s₉.gpr .esp = E s₀ := by + rw [g₉ _ (by decide) (by decide) (by decide) (by decide), esp₁] + have rw₉ : s₉.rd ++ s₉.wr = s₀.rd ++ s₀.wr := by rw [v₉.rd, v₉.wr, u₈.rd, u₈.wr, rd₇, wr₇] + have hlen : (Spec.Aes.bytesAt s₀.mem ((Dp s₀).setWidth 64) (N s₀)).length = N s₀ := + Proof.Cmac.bytesAt_length _ _ _ + have m₉ : s₉.mem = (writeBytes (Proof.Cmac.zero4 (savedMem s₀) (Ca s₀)) (Ca s₀) + (Spec.Aes.bytesAt s₀.mem ((Dp s₀).setWidth 64) (N s₀))).writeW (Ca s₀ + BitVec.ofNat 64 (N s₀)) + (0x80 : Byte) := by + have : s₈.gpr Reg8.al.reg = 0x80 := u₈.gpr + rw [v₉.mem, this, u₈.mem, m₇, b80] + have fW : Frame [⟨Ca s₀, 16⟩] (savedMem s₀) s₉.mem := by + rw [m₉] + refine (fz.trans (writeBytes_frame _ _ _ ?_)).trans + ((Frame.refl _ _).writeW (List.mem_singleton_self _) _ (Offset.contains_base _ (by omega) (by omega))) + rw [hlen]; simpa using Offset.contains_base (Ca s₀) (d := 0) (n := N s₀) (k := 16) (by omega) (by decide) + have big₉ : Frame (Big s₀) s₀.mem s₉.mem := + (savedMem_big s₀).trans (fW.sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨scrR s₀, by simp, Offset.sub_base _ (by decide)⟩) + refine wp_arg (s₀ := s₀) esp₉ (by rw [rw₉]; exact hp.arg_in (by decide)) (hp.arg_keep big₉ (by decide)) + fun s₁₀ u₁₀ => ?_ + have p₁₀ : s₁₀.gpr .ebp = S s₀ := by + rw [u₁₀.other _ (by decide), g₉ _ (by decide) (by decide) (by decide) (by decide), p₁] + have d₁₀ : s₁₀.gpr .edx = W s₀ := u₁₀.gpr + have rw₁₀ : s₁₀.rd ++ s₁₀.wr = s₀.rd ++ s₀.wr := by rw [u₁₀.rd, u₁₀.wr, rw₉] + have w₁₀ : s₁₀.wr = s₀.wr := by rw [u₁₀.wr, v₉.wr, u₈.wr, wr₇] + refine xor4_ok (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) + (by rw [p₁₀]; omega) (by rw [d₁₀]; omega) (by rw [p₁₀]; omega) + (by + rw [p₁₀, rw₁₀] + exact fun a n hi => (hp.cS (d := 2048) (n := 16) (by decide)) a n hi |> + fun ⟨r, hr, hc⟩ => ⟨r, List.mem_append_right _ hr, hc⟩) + (by rw [d₁₀, rw₁₀]; exact hp.cKey (by decide)) (by rw [p₁₀, w₁₀]; exact hp.cS (by decide)) + fun s₁₁ g₁₁ => WP.block_nil ?_ + have pad : Spec.Aes.bytesAt s₉.mem (Ca s₀) 16 = + Spec.Aes.bytesAt s₀.mem ((Dp s₀).setWidth 64) (N s₀) ++ [0x80] ++ Spec.Cmac.zeros (16 - N s₀ - 1) := by + have := Proof.Cmac.padded_bytes (Proof.Cmac.zero4 (savedMem s₀) (Ca s₀)) (Ca s₀) + (Spec.Aes.bytesAt s₀.mem ((Dp s₀).setWidth 64) (N s₀)) (by rw [hlen]; exact hL) + (Proof.Cmac.zero4_bytes _ _) + rw [hlen] at this + rw [m₉]; exact this + have k2 : Spec.Aes.bytesAt s₉.mem ((W s₀).setWidth 64 + BitVec.ofNat 64 256) 16 = + Spec.Aes.bytesAt s₀.mem ((W s₀).setWidth 64 + BitVec.ofNat 64 256) 16 := by + rw [Proof.Cmac.bytesAt_frame16 fW (fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; exact (hp.ca_key (by decide)).symm), hp.key_bytes (by decide)] + refine ⟨by rw [g₁₁.gpr _ (by decide) (by decide), p₁₀], + by rw [g₁₁.gpr _ (by decide) (by decide), u₁₀.other _ (by decide), esp₉], + by rw [g₁₁.rd, u₁₀.rd, v₉.rd, u₈.rd, rd₇], by rw [g₁₁.wr, w₁₀], ?_, ?_⟩ + · rw [g₁₁.mem, p₁₀, u₁₀.mem]; exact fW.trans (Proof.Cmac.xor4Mem_frame _ _ _ _) + · rw [g₁₁.mem, p₁₀, d₁₀, u₁₀.mem, Proof.Cmac.xor4Mem_bytes _ (Proof.Cmac.Sep4.self _) + (Proof.Cmac.Sep4.of_disjoint (hp.ca_key (by decide))), pad, k2] + simp only [mn, Spec.Cmac.lastBlock, hlen, show N s₀ ≠ 16 by omega, ite_false] + exact Proof.Cmac.xor_comm _ _ + +end VG.Proof.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/FinalizeCT.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/FinalizeCT.lean new file mode 100644 index 000000000..d30fb850c --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/FinalizeCT.lean @@ -0,0 +1,91 @@ +import VerifiedGarbage.Proof.CmacAes.X86.FinalizeCorrect +import VerifiedGarbage.Proof.CmacAes.X86.UpdateCT + +/-! +# AES-CMAC on x86: `vg_cmac_aes_finalize` is constant time + +Untrusted: everything here is checked by Lean. The code before the call is +checked by the taint analysis, from `esp` and the stack arguments (its +branches and the copy loop depend only on `last_len`), the call of +`vg_aes_ctr32`, in its frame, is constant time by its own proof +(`ctr_rel`), its arguments pinned by the correctness proof (`FMid`), and the +restore after it by the taint analysis again. +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 VG.Impl.CmacAes.X86 + +theorem FPre.argsOut {s₀ : State} (hp : FPre s₀) {s : State} (hesp : s.gpr .esp = E s₀) (hwr : s.wr = s₀.wr) : + ArgsOut 6 s := by + have hs : (s₀.gpr .esp).toNat + 28 ≤ 2 ^ 32 := hp.esp_fit + refine ⟨by rw [hesp]; omega, ?_⟩ + rw [hwr, hp.wr, hesp] + simp only [List.mem_cons, List.not_mem_nil, or_false] + rintro r (rfl | rfl) + · exact VG.X86.Taint.frame_disjoint (n := 24) (by omega) hp.ret_st hp.args_st + · exact VG.X86.Taint.frame_disjoint (n := 24) (by omega) hp.ret_scr hp.args_scr + +/-- Two runs agree on `esp`, the stack arguments and the registers `rs`. -/ +theorem fagree {s₀ s₀' : State} (hq : finalizeX86.pub s₀ s₀') (hp : FPre s₀) (hp' : FPre s₀') {rs : List Reg} + {s₁ s₂ : State} (h₁ : Pt s₀ s₁) (h₂ : Pt s₀' s₂) (hr : ∀ r ∈ rs, s₁.gpr r = s₂.gpr r) : + VG.X86.Taint.Agree (argTaint rs (4 + 4 * 6)) s₁ s₂ := + agree_argTaint hr (by rw [h₁.esp, h₂.esp]; exact hq.1) (hp.argsOut h₁.esp h₁.wr) (hp'.argsOut h₂.esp h₂.wr) + fun i hi => by rw [arg_cur (h₁.esp) (h₁.args i hi), arg_cur (h₂.esp) (h₂.args i hi), hq.2 i hi] + +theorem FMid.f {s₀ s : State} (h : FMid s₀ s) : + Frame [stR s₀, ⟨(S s₀).setWidth 64, 2064⟩, stkR s₀] (savedMem s₀) s.mem := + h.frame.sub fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl + · exact ⟨⟨(S s₀).setWidth 64, 2064⟩, by simp, Offset.sub_base _ (by decide)⟩ + · exact ⟨stR s₀, by simp, fun _ h => h⟩ + +theorem FMid.pt {s₀ : State} (hp : FPre s₀) {s : State} (h : FMid s₀ s) : Pt s₀ s := + ⟨h.esp, h.wr, fun _ hi => hp.arg_keep (UPre.big_of h.f) hi⟩ + +theorem fcall_after {s₀ : State} (hp : FPre s₀) {s : State} (h : FMid s₀ s) : WP isa ctrCall s (Pt s₀) := + WP.mono (ctr_call h.pre) fun s' hc => by + have hb : below (s.gpr .esp) 28 = stkR s₀ := by rw [h.esp]; exact hp.below_eq + have fr := hc.frame + rw [hb, hp.cA] at fr + have big := UPre.big_of (h.f.trans (fr.sub fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · exact ⟨⟨(S s₀).setWidth 64, 2064⟩, by simp, Offset.sub_base _ (by decide)⟩ + · exact ⟨stR s₀, by simp, fun _ h => h⟩ + · exact ⟨⟨(S s₀).setWidth 64, 2064⟩, by simp, Region.sub_prefix (by decide)⟩ + · exact ⟨stkR s₀, by simp, fun _ h => h⟩)) + exact ⟨by rw [hc.saved .esp (by simp [calleeSaved]), h.esp], by rw [hc.wr, h.wr], + fun _ hi => hp.arg_keep big hi⟩ + +theorem finalize_rel {s₀ s₀' : State} (h0 : finalizeX86.pre s₀) (h0' : finalizeX86.pre s₀') + (hq : finalizeX86.pub s₀ s₀') : + RelCT isa (fun a b => a = s₀ ∧ b = s₀') finalize fun _ _ => True := by + have hp := FPre.of h0 + have hp' := FPre.of h0' + have eW : W s₀ = W s₀' := hq.2 0 (by decide) + have eR : R s₀ = R s₀' := by rw [R, R, hq.2 1 (by decide)] + have eSt : St s₀ = St s₀' := hq.2 2 (by decide) + have eS : S s₀ = S s₀' := hq.2 5 (by decide) + have pt₀ : ∀ {t : State}, Pt t t := ⟨rfl, rfl, fun _ _ => rfl⟩ + have a := ((RelCT.taint (A := taint) (P := fun a b => a = s₀ ∧ b = s₀') (argTaint [] (4 + 4 * 6)) + (fun a b h => by + obtain ⟨rfl, rfl⟩ := h + exact fagree hq hp hp' pt₀ pt₀ fun r hr => by simp at hr) + (c := finPre) (by taint_decide)).wp (F₁ := FMid s₀) (F₂ := FMid s₀') + fun a b h => by obtain ⟨rfl, rfl⟩ := h; exact ⟨finPre_wp hp, finPre_wp hp'⟩).mono (fun _ _ h => h) + fun _ _ h => h.2 + have c := ((ctr_rel (E := E s₀) (P := fun s₁ s₂ => FMid s₀ s₁ ∧ FMid s₀' s₂) fun s₁ s₂ h => + ⟨h.1.pre, by rw [eW, eS, eSt, eR]; exact h.2.pre, h.1.esp, h.2.esp.trans hq.1.symm⟩).wp + (F₁ := Pt s₀) (F₂ := Pt s₀') fun _ _ h => ⟨fcall_after hp h.1, fcall_after hp' h.2⟩).mono + (fun _ _ h => h) fun _ _ h => h.2 + have b := RelCT.taint (A := taint) (P := fun s₁ s₂ => Pt s₀ s₁ ∧ Pt s₀' s₂) (argTaint [] (4 + 4 * 6)) + (fun _ _ h => fagree hq hp hp' h.1 h.2 fun r hr => by simp at hr) + (c := .block (restore 5)) (by taint_decide) + exact a.seq (c.seq b) + +theorem finalize_ct : ConstantTime isa finalizeX86.pre finalizeX86.pub finalize := + fun _ _ _ _ _ _ h₁ h₂ hq e₁ e₂ => (finalize_rel h₁ h₂ hq _ _ _ _ _ _ ⟨rfl, rfl⟩ e₁ e₂).1 + +end VG.Proof.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/FinalizeCorrect.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/FinalizeCorrect.lean new file mode 100644 index 000000000..5d8841ed2 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/FinalizeCorrect.lean @@ -0,0 +1,237 @@ +import VerifiedGarbage.Proof.CmacAes.X86.Finalize + +/-! +# AES-CMAC on x86: `vg_cmac_aes_finalize` is correct + +Untrusted: everything here is checked by Lean. Before the call, the +counter block holds `Mₙ ⊕ C`, for the last block `Mₙ` of §6.2 step 4 and the +chaining value `C` at `state`, and the state is zeroed; the call leaves +`CIPH_K(C ⊕ Mₙ)` there, the MAC (`Cmac.macFull_split`). +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 VG.Impl.CmacAes.X86 +open VG.Proof.MdStream.X86 (Upd wp_mov wp_movi wp_addi eval_e) + +/-! ## Up to the call -/ + +/-- What the code before the call leaves. -/ +structure FMid (s₀ s : State) : Prop where + pre : CtrPre s (W s₀) (S s₀ + BitVec.ofNat 32 2048) (St s₀) (S s₀) (R s₀) + blk : Spec.Aes.bytesAt s.mem (Ca s₀) 16 = + Spec.Cmac.xor (mn s₀) (Spec.Aes.bytesAt s₀.mem ((St s₀).setWidth 64) 16) + frame : Frame [⟨Ca s₀, 16⟩, stR s₀] (savedMem s₀) s.mem + esp : s.gpr .esp = E s₀ + rd : s.rd = s₀.rd + wr : s.wr = s₀.wr + +theorem finArgs_eq : finArgs = .mov .ebx (argOp 2) :: (xor4 .ebp .ebx .ebp 2048 0 2048 ++ (zero4 .ebx 0 ++ ctrArgs)) := + rfl + +theorem finArgs_wp {s₀ : State} (hp : FPre s₀) {s : State} (h : BPost s₀ s) : + WP isa (.block finArgs) s (FMid s₀) := by + have sf := hp.scr_fit + have tf := hp.st_fit + have hR := hp.rounds + have cA := hp.cA + have hrw : s.rd ++ s.wr = s₀.rd ++ s₀.wr := by rw [h.rd, h.wr] + have cSt : (⟨Ca s₀, 16⟩ : Region).Disjoint (stR s₀) := hp.st_scr.symm.sub_left (Offset.sub_base _ (by decide)) + have wSt : Covers [stR s₀] s₀.wr := by + rw [hp.wr] + exact Covers.of_sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; exact ⟨stR s₀, by simp, 0, by simp, by simp⟩ + have big : Frame (Big s₀) s₀.mem s.mem := + (savedMem_big s₀).trans (h.frame.sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨scrR s₀, by simp, Offset.sub_base _ (by decide)⟩) + rw [finArgs_eq] + refine wp_arg (s₀ := s₀) h.esp (by rw [hrw]; exact hp.arg_in (by decide)) (hp.arg_keep big (by decide)) + fun s₁ u₁ => ?_ + have b₁ : s₁.gpr .ebx = St s₀ := u₁.gpr + have p₁ : s₁.gpr .ebp = S s₀ := by rw [u₁.other _ (by decide), h.ebp] + have rw₁ : s₁.rd ++ s₁.wr = s₀.rd ++ s₀.wr := by rw [u₁.rd, u₁.wr, hrw] + refine xor4_ok (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) + (by rw [p₁]; omega) (by rw [b₁]; omega) (by rw [p₁]; omega) + (by + rw [p₁, rw₁] + exact fun a n hi => (hp.cS (d := 2048) (n := 16) (by decide)) a n hi |> + fun ⟨r, hr, hc⟩ => ⟨r, List.mem_append_right _ hr, hc⟩) + (by + rw [b₁, add0, rw₁] + exact fun a n hi => wSt a n hi |> fun ⟨r, hr, hc⟩ => ⟨r, List.mem_append_right _ hr, hc⟩) + (by rw [p₁, u₁.wr, h.wr]; exact hp.cS (by decide)) fun s₂ g₂ => ?_ + have b₂ : s₂.gpr .ebx = St s₀ := by rw [g₂.gpr _ (by decide) (by decide), b₁] + refine zero4_ok (by decide) (by rw [b₂]; omega) (by rw [b₂, add0, g₂.wr, u₁.wr, h.wr]; exact wSt) + fun s₃ g₃ m₃ rd₃ wr₃ => ?_ + have esp₃ : s₃.gpr .esp = E s₀ := by + rw [g₃ _ (by decide), g₂.gpr _ (by decide) (by decide), u₁.other _ (by decide), h.esp] + have rd₃' : s₃.rd = s₀.rd := by rw [rd₃, g₂.rd, u₁.rd, h.rd] + have wr₃' : s₃.wr = s₀.wr := by rw [wr₃, g₂.wr, u₁.wr, h.wr] + have mem₃ : s₃.mem = Proof.Cmac.zero4 (Proof.Cmac.xor4Mem s.mem (Ca s₀) (Ca s₀) ((St s₀).setWidth 64)) + ((St s₀).setWidth 64) := by + rw [m₃, b₂, add0, g₂.mem, p₁, b₁, add0, u₁.mem] + have fr₃ : Frame [⟨Ca s₀, 16⟩, stR s₀] (savedMem s₀) s₃.mem := by + rw [mem₃] + exact ((h.frame.trans (Proof.Cmac.xor4Mem_frame _ _ _ _)).mono (by simp)).trans + ((Proof.Cmac.frame_store4 _ _ _ _ _).mono (by simp)) + have big₃ : Frame (Big s₀) s₀.mem s₃.mem := + (savedMem_big s₀).trans (fr₃.sub fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl + · exact ⟨scrR s₀, by simp, Offset.sub_base _ (by decide)⟩ + · exact ⟨stR s₀, by simp, fun _ h => h⟩) + rw [ctrArgs_eq] + refine wp_arg (s₀ := s₀) esp₃ (by rw [rd₃', wr₃']; exact hp.arg_in (by decide)) (hp.arg_keep big₃ (by decide)) + fun s₄ u₄ => ?_ + refine wp_arg (s₀ := s₀) (by rw [u₄.other _ (by decide), esp₃]) + (by rw [u₄.rd, u₄.wr, rd₃', wr₃']; exact hp.arg_in (by decide)) + (by rw [u₄.mem]; exact hp.arg_keep big₃ (by decide)) fun s₅ u₅ => ?_ + refine wp_mov fun s₆ u₆ => wp_addi fun s₇ u₇ => wp_movi fun s₈ u₈ => WP.block_nil ?_ + have keep : ∀ r, r ≠ .eax → r ≠ .ecx → r ≠ .edx → r ≠ .edi → s₈.gpr r = s₃.gpr r := fun r ha hc hd hi => by + rw [u₈.other _ hi, u₇.other _ hd, u₆.other _ hd, u₅.other _ hc, u₄.other _ ha] + have p₃ : s₃.gpr .ebp = S s₀ := by rw [g₃ _ (by decide), g₂.gpr _ (by decide) (by decide), p₁] + have b₃ : s₃.gpr .ebx = St s₀ := by rw [g₃ _ (by decide), b₂] + have sp₈ : s₈.gpr .esp = E s₀ := by rw [keep _ (by decide) (by decide) (by decide) (by decide), esp₃] + have rd₈ : s₈.rd = s₀.rd := by rw [u₈.rd, u₇.rd, u₆.rd, u₅.rd, u₄.rd, rd₃'] + have wr₈ : s₈.wr = s₀.wr := by rw [u₈.wr, u₇.wr, u₆.wr, u₅.wr, u₄.wr, wr₃'] + have mem₈ : s₈.mem = s₃.mem := by rw [u₈.mem, u₇.mem, u₆.mem, u₅.mem, u₄.mem] + have hb : below (s₈.gpr .esp) 28 = stkR s₀ := by rw [sp₈]; exact hp.below_eq + have stS : Spec.Aes.bytesAt s.mem ((St s₀).setWidth 64) 16 = + Spec.Aes.bytesAt s₀.mem ((St s₀).setWidth 64) 16 := + Proof.Cmac.bytesAt_frame16 ((savedMem_frame s₀).trans (h.frame.sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨scrR s₀, List.mem_singleton_self _, Offset.sub_base _ (by decide)⟩)) fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; exact hp.st_scr + refine ⟨⟨?_, ?_, ?_, ?_, u₈.gpr, ?_, hR, by rw [sp₈]; exact hp.esp28, ?_, + hp.key_st.sub_left (Region.sub_prefix (by decide)), + (hp.key_scr.sub_left (Region.sub_prefix (by decide))).sub_right (Region.sub_prefix (by decide)), + by rw [cA]; exact cSt, by rw [cA]; exact Offset.disjoint_base _ (by decide) (by omega), + hp.st_scr.sub_right (Region.sub_prefix (by decide)), + by rw [hb]; exact hp.b_key.sub_right (Region.sub_prefix (by decide)), + by rw [hb, cA]; exact hp.b_scr.sub_right (Offset.sub_base _ (by decide)), by rw [hb]; exact hp.b_st, + by rw [hb]; exact hp.b_scr.sub_right (Region.sub_prefix (by decide)), by have := hp.key_fit; omega, ?_, tf, + by omega, ?_, ?_, ?_⟩, ?_, ?_, sp₈, rd₈, wr₈⟩ + · rw [u₈.other _ (by decide), u₇.other _ (by decide), u₆.other _ (by decide), u₅.other _ (by decide), u₄.gpr] + · rw [u₈.other _ (by decide), u₇.other _ (by decide), u₆.other _ (by decide), u₅.gpr]; exact arg_ofNat s₀ 1 + · rw [u₈.other _ (by decide), u₇.gpr, u₆.gpr, u₅.other _ (by decide), u₄.other _ (by decide), p₃] + · rw [keep _ (by decide) (by decide) (by decide) (by decide), b₃] + · rw [keep _ (by decide) (by decide) (by decide) (by decide), p₃] + · rw [cA]; exact (hp.ca_key (d := 0) (n := 240) (by decide)).symm |> fun d => by simpa using d + · rw [BitVec.toNat_add, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (a := 2048) (by decide), + Nat.mod_eq_of_lt (by omega)]; omega + · rw [rd₈, wr₈, hp.rd] + exact Covers.of_sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨keyR s₀, by simp, 0, by simp, by simp⟩ + · rw [wr₈, hp.wr, cA] + refine Covers.of_sub fun r hr => ?_ + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact ⟨scrR s₀, by simp, 2048, rfl, by simp⟩ + · exact ⟨stR s₀, by simp, 0, by simp, by simp⟩ + · exact ⟨scrR s₀, by simp, 0, by simp, by simp⟩ + · rw [mem₈, mem₃]; exact Proof.Cmac.zero4_bytes _ _ + · rw [mem₈, mem₃, Proof.Cmac.zero4, Proof.Cmac.bytesAt_frame16 (Proof.Cmac.frame_store4 _ _ _ _ _) (fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; exact cSt), + Proof.Cmac.xor4Mem_bytes _ (Proof.Cmac.Sep4.self _) (Proof.Cmac.Sep4.of_disjoint cSt), h.blk, stS] + · rw [mem₈]; exact fr₃ + +theorem finPre_wp {s₀ : State} (hp : FPre s₀) : WP isa finPre s₀ (FMid s₀) := by + refine WP.seq (WP.mono (finSave_wp hp) fun s₁ h₁ => ?_) + refine WP.seq (WP.mono (Q := BPost s₀) ?_ fun _ h => finArgs_wp hp h) + have ev : isa.eval .e s₁ = some (decide (N s₀ = 16)) := by + show VG.X86.eval .e s₁ = _; rw [eval_e, h₁.zf] + by_cases hL : N s₀ = 16 + · exact WP.ite true (by rw [ev]; simp [hL]) (fun _ => full_wp hp hL h₁) (fun h => by cases h) + · exact WP.ite false (by rw [ev]; simp [hL]) (fun h => by cases h) + (fun _ => partial_wp hp (by have := hp.len; omega) h₁) + +/-! ## The whole function -/ + +theorem finalize_wp {s₀ : State} (h0 : finalizeX86.pre s₀) : + WP isa finalize s₀ fun s' => abiPreserved s₀ s' ∧ finalizeX86.post s₀ s' := by + have hp := FPre.of h0 + have hR := hp.rounds + have hRb : 16 * (R s₀ + 1) ≤ 240 := by rcases hR with h | h | h <;> omega + have hsc : (arg s₀ 5).toNat + 2176 ≤ 2 ^ 32 := hp.scr_fit + have cA := hp.cA + unfold finalize + refine WP.seq (WP.mono (finPre_wp hp) fun s₁ h₁ => ?_) + refine WP.seq (WP.mono (ctr_call h₁.pre) fun s₂ h₂ => ?_) + have hb : below (s₁.gpr .esp) 28 = stkR s₀ := by rw [h₁.esp]; exact hp.below_eq + have f₁ : Frame [stR s₀, ⟨(S s₀).setWidth 64, 2064⟩, stkR s₀] (savedMem s₀) s₁.mem := + h₁.frame.sub fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl + · exact ⟨⟨(S s₀).setWidth 64, 2064⟩, by simp, Offset.sub_base _ (by decide)⟩ + · exact ⟨stR s₀, by simp, fun _ h => h⟩ + have f₂ : Frame [stR s₀, ⟨(S s₀).setWidth 64, 2064⟩, stkR s₀] (savedMem s₀) s₂.mem := by + have fr := h₂.frame + rw [hb, cA] at fr + refine f₁.trans (fr.sub fun r hr => ?_) + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · exact ⟨⟨(S s₀).setWidth 64, 2064⟩, by simp, Offset.sub_base _ (by decide)⟩ + · exact ⟨stR s₀, by simp, fun _ h => h⟩ + · exact ⟨⟨(S s₀).setWidth 64, 2064⟩, by simp, Region.sub_prefix (by decide)⟩ + · exact ⟨stkR s₀, by simp, fun _ h => h⟩ + have big₁ := UPre.big_of f₁ + have big₂ := UPre.big_of f₂ + have esp₂ : s₂.gpr .esp = E s₀ := by rw [h₂.saved .esp (by simp [calleeSaved]), h₁.esp] + have rdwr₂ : s₂.rd ++ s₂.wr = [keyR s₀, lastR s₀, argsR s₀, stR s₀, scrR s₀] := by + rw [h₂.rd, h₂.wr, h₁.rd, h₁.wr, hp.rd, hp.wr]; rfl + have hrw₂ : s₂.rd ++ s₂.wr = s₀.rd ++ s₀.wr := by rw [h₂.rd, h₂.wr, h₁.rd, h₁.wr] + have sl : ∀ r d, (r, d) ∈ saved → s₂.mem.readW ((S s₀).setWidth 64 + BitVec.ofNat 64 d) 32 = s₀.gpr r := by + intro r d hrd + have hb := saved_bound _ hrd + rw [f₂.readW (r := ⟨(S s₀).setWidth 64 + BitVec.ofNat 64 d, 4⟩) (Region.contains_self _ _) (fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact hp.st_scr.symm.sub_left (UPre.scr_sub (by omega)) + · exact Offset.disjoint_base _ hb.1 (by omega) + · exact hp.b_scr.symm.sub_left (UPre.scr_sub (by omega))) (by decide), savedMem_slot s₀ hrd] + have sch : Spec.Aes.bytesAt s₁.mem ((W s₀).setWidth 64) (16 * (R s₀ + 1)) = + Spec.Aes.bytesAt s₀.mem ((W s₀).setWidth 64) (16 * (R s₀ + 1)) := + Proof.Cmac.bytesAt_frame big₁ (fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact hp.key_st.sub_left (Region.sub_prefix (by omega)) + · exact hp.key_scr.sub_left (Region.sub_prefix (by omega)) + · exact hp.b_key.symm.sub_left (Region.sub_prefix (by omega))) (by omega) + rw [restore_eq] + refine wp_arg (s₀ := s₀) esp₂ (by rw [hrw₂]; exact hp.arg_in (by decide)) (hp.arg_keep big₂ (by decide)) + fun s₃ u₃ => ?_ + refine restoreList_ok saved s₃ _ saved_nodup (fun p hp' => ?_) fun s₄ ld₄ ho₄ m₄ rd₄ wr₄ => WP.block_nil ?_ + · have hb := saved_bound p hp' + rw [u₃.gpr, u₃.rd, u₃.wr, rdwr₂] + exact ⟨saved_ne_eax p hp', by omega, ⟨scrR s₀, by simp, Offset.contains_base _ (by omega) (by omega)⟩⟩ + refine ⟨⟨fun r hr => ?_, ?_⟩, ?_⟩ + · simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl | rfl + · rw [ld₄ (.ebx, 2064) (by decide), u₃.gpr, u₃.mem, sl .ebx 2064 (by decide)] + · rw [ld₄ (.esi, 2068) (by decide), u₃.gpr, u₃.mem, sl .esi 2068 (by decide)] + · rw [ld₄ (.edi, 2072) (by decide), u₃.gpr, u₃.mem, sl .edi 2072 (by decide)] + · rw [ld₄ (.ebp, 2076) (by decide), u₃.gpr, u₃.mem, sl .ebp 2076 (by decide)] + · rw [ho₄ _ (by decide), u₃.other _ (by decide), esp₂] + · rw [m₄, u₃.mem] + have rs : (retR s₀).Disjoint (stkR s₀) := by + have := Offset.disjoint_below_above ((E s₀).setWidth 64) (m := 28) (a := 0) (l := 4) (by decide) + rw [add0] at this + exact this.symm + exact big₂.readW (r := retR s₀) (Region.contains_self _ _) (fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact hp.ret_st + · exact hp.ret_scr + · exact rs) (by decide) + · intro hk msg hm hne hst + have hk' : Spec.Aes.bytesAt s₀.mem ((W s₀).setWidth 64 + BitVec.ofNat 64 240) 32 = + (Spec.Cmac.subkeys (ciph s₀) 16).1 ++ (Spec.Cmac.subkeys (ciph s₀) 16).2 := hk + obtain ⟨e1, e2⟩ := Proof.Cmac.k1k2 (Proof.Cmac.subkeys_aes_length _ _) hk' + show Spec.Aes.bytesAt s₄.mem ((St s₀).setWidth 64) 16 = _ + rw [m₄, u₃.mem, h₂.out, sch, cA, h₁.blk, mn, e1, e2, hst, + Proof.Cmac.macFull_split _ hm (by rw [Proof.Cmac.bytesAt_length]; exact hp.len) + (by rw [Proof.Cmac.bytesAt_length]; exact hne), Proof.Cmac.xor_comm] + +end VG.Proof.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/Save.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/Save.lean new file mode 100644 index 000000000..e5446f383 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/Save.lean @@ -0,0 +1,137 @@ +import VerifiedGarbage.Proof.CmacAes.X86.Words +import VerifiedGarbage.Proof.CmacAes.X86.Call + +/-! +# AES-CMAC on x86: saving registers and reading the stack arguments + +Untrusted: everything here is checked by Lean. Weakest preconditions of +the stores that save registers in the scratch buffer (`saveList_ok`), of +the loads that restore them (`restoreList_ok`), and of instructions with a +stack argument as their source (`wp_arg`, `wp_addArg`). +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 VG.Impl.CmacAes.X86 +open VG.Proof.MdStream.X86 (Upd Mupd WP.cons wp_movm wp_store) + +/-- The memory after storing the registers `l` (values `g`) at `B + offset`. -/ +def saveMem (m : Mem) (B : Addr) (g : Reg → BitVec 32) : List (Reg × Nat) → Mem + | [] => m + | (r, d) :: l => saveMem (m.writeW (B + BitVec.ofNat 64 d) (g r)) B g l + +theorem saveList_ok {rest : List Instr} (l : List (Reg × Nat)) : + ∀ (s : State) (Q : State → Prop), + (∀ p ∈ l, (s.gpr .eax).toNat + p.2 < 2 ^ 32 ∧ + InRegions s.wr ((s.gpr .eax).setWidth 64 + BitVec.ofNat 64 p.2) 4) → + (∀ s', s'.gpr = s.gpr → s'.rd = s.rd → s'.wr = s.wr → + s'.mem = saveMem s.mem ((s.gpr .eax).setWidth 64) s.gpr l → WP isa (.block rest) s' Q) → + WP isa (.block (l.map (fun p => Instr.store (at_ .eax p.2) p.1) ++ rest)) s Q := by + induction l with + | nil => intro s Q _ k; exact k s rfl rfl rfl rfl + | cons p l ih => + intro s Q hl k + obtain ⟨h1, h2⟩ := hl p (by simp) + refine wp_store (by rw [ea_at']; exact addr_eq h1) h2 fun s₁ u₁ => ?_ + refine ih s₁ Q (fun q hq => ?_) fun s' g rd wr m => k s' (g.trans u₁.gpr) (rd.trans u₁.rd) + (wr.trans u₁.wr) ?_ + · rw [u₁.gpr, u₁.wr]; exact hl q (List.mem_cons_of_mem _ hq) + · rw [m, u₁.mem, u₁.gpr]; rfl + +theorem saveMem_frame (m : Mem) (B : Addr) (g : Reg → BitVec 32) {L : Nat} (hL : L < 2 ^ 32) : + ∀ (l : List (Reg × Nat)), (∀ p ∈ l, p.2 + 4 ≤ L) → Frame [⟨B, L⟩] m (saveMem m B g l) := by + intro l + induction l generalizing m with + | nil => intro _; exact Frame.refl _ _ + | cons p l ih => + intro hl + have h := hl p (by simp) + exact ((Frame.refl _ _).writeW (List.mem_singleton_self _) _ + (Offset.contains_base (n := 32 / 8) _ h (by omega))).trans (ih _ fun q hq => hl q (List.mem_cons_of_mem _ hq)) + +theorem saveMem_congr (m : Mem) (B : Addr) {g g' : Reg → BitVec 32} : + ∀ (l : List (Reg × Nat)), (∀ p ∈ l, g p.1 = g' p.1) → saveMem m B g l = saveMem m B g' l := by + intro l + induction l generalizing m with + | nil => intro _; rfl + | cons p l ih => + intro h + simp only [saveMem] + rw [h p (List.mem_cons_self ..)] + exact ih _ fun q hq => h q (List.mem_cons_of_mem _ hq) + +theorem readW_writeW_save (m : Mem) (B : Addr) (v : BitVec 32) {d e : Nat} (hd : d < 2 ^ 32) + (he : e < 2 ^ 32) (h : d + 4 ≤ e ∨ e + 4 ≤ d) : + (m.writeW (B + BitVec.ofNat 64 e) v).readW (B + BitVec.ofNat 64 d) 32 = m.readW (B + BitVec.ofNat 64 d) 32 := + Mem.readW_writeW_sep (Offset.sep _ h (by omega) (by omega)) (by decide) + +set_option simprocs false in +/-- Each slot of `saved` holds the register saved there. -/ +theorem saveMem_slot (m : Mem) (B : Addr) (g : Reg → BitVec 32) {r : Reg} {d : Nat} (h : (r, d) ∈ saved) : + (saveMem m B g saved).readW (B + BitVec.ofNat 64 d) 32 = g r := by + simp only [saved, List.mem_cons, List.not_mem_nil, or_false, Prod.mk.injEq] at h + rcases h with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ <;> + simp (disch := decide) only [saved, saveMem, Mem.readW_writeW_self32, readW_writeW_save] + +theorem saved_bound : ∀ p ∈ saved, 2064 ≤ p.2 ∧ p.2 + 4 ≤ 2080 := by decide + +theorem saved_ne_eax : ∀ p ∈ saved, p.1 ≠ .eax := by decide + +theorem save_eq : save = saved.map fun p => Instr.store (at_ .eax p.2) p.1 := rfl + +/-- Loads of the registers `l` from `eax + offset`, none of them `eax`. -/ +theorem restoreList_ok {rest : List Instr} (l : List (Reg × Nat)) : + ∀ (s : State) (Q : State → Prop), (l.map Prod.fst).Nodup → + (∀ p ∈ l, p.1 ≠ .eax ∧ (s.gpr .eax).toNat + p.2 < 2 ^ 32 ∧ + InRegions (s.rd ++ s.wr) ((s.gpr .eax).setWidth 64 + BitVec.ofNat 64 p.2) 4) → + (∀ s', (∀ p ∈ l, s'.gpr p.1 = s.mem.readW ((s.gpr .eax).setWidth 64 + BitVec.ofNat 64 p.2) 32) → + (∀ r, r ∉ l.map Prod.fst → s'.gpr r = s.gpr r) → s'.mem = s.mem → s'.rd = s.rd → s'.wr = s.wr → + WP isa (.block rest) s' Q) → + WP isa (.block (l.map (fun p => Instr.mov p.1 (.mem (at_ .eax p.2))) ++ rest)) s Q := by + induction l with + | nil => intro s Q _ _ k; exact k s (fun _ h => by cases h) (fun _ _ => rfl) rfl rfl rfl + | cons p l ih => + intro s Q hnd hl k + obtain ⟨h0, h1, h2⟩ := hl p (by simp) + simp only [List.map_cons, List.nodup_cons] at hnd + refine wp_movm (by rw [ea_at']; exact addr_eq h1) h2 fun s₁ u₁ => ?_ + have eb : s₁.gpr .eax = s.gpr .eax := u₁.other _ (Ne.symm h0) + refine ih s₁ Q hnd.2 (fun q hq => ?_) fun s' hl' ho hm hrd hwr => k s' (fun q hq => ?_) + (fun r hr => ?_) (hm.trans u₁.mem) (hrd.trans u₁.rd) (hwr.trans u₁.wr) + · rw [eb, u₁.rd, u₁.wr]; exact hl q (List.mem_cons_of_mem _ hq) + · rcases List.mem_cons.mp hq with rfl | hq + · rw [ho _ hnd.1, u₁.gpr] + · rw [hl' q hq, u₁.mem, eb] + · simp only [List.map_cons, List.mem_cons, not_or] at hr + rw [ho r hr.2, u₁.other r hr.1] + +theorem restore_eq (i : Nat) : + restore i = .mov .eax (argOp i) :: (saved.map fun p => Instr.mov p.1 (.mem (at_ .eax p.2))) ++ [] := by + simp [restore] + +/-! ## The stack arguments -/ + +section +variable {is : List Instr} {s : State} {Q : State → Prop} + +/-- `mov d, [esp + 4 + 4 i]`, the stack argument `i` of the entry state `s₀`. -/ +theorem wp_arg {d : Reg} {i : Nat} {s₀ : State} (hesp : s.gpr .esp = s₀.gpr .esp) + (hin : InRegions (s.rd ++ s.wr) (argAddr s₀ i) 4) (hv : s.mem.readW (argAddr s₀ i) 32 = arg s₀ i) + (k : ∀ s', Upd s s' d (arg s₀ i) → WP isa (.block is) s' Q) : + WP isa (.block (.mov d (argOp i) :: is)) s Q := + wp_movm (by rw [ea_at', hesp]; rfl) hin fun s' u => k s' (hv ▸ u) + +/-- `add d, [esp + 4 + 4 i]`. -/ +theorem wp_addArg {d : Reg} {i : Nat} {s₀ : State} (hesp : s.gpr .esp = s₀.gpr .esp) + (hin : InRegions (s.rd ++ s.wr) (argAddr s₀ i) 4) (hv : s.mem.readW (argAddr s₀ i) 32 = arg s₀ i) + (k : ∀ s', Upd s s' d (s.gpr d + arg s₀ i) → WP isa (.block is) s' Q) : + WP isa (.block (.alu .add d (argOp i) :: is)) s Q := by + refine WP.cons (s' := (arithFlags s (s.gpr d + arg s₀ i) + (2 ^ 32 ≤ (s.gpr d).toNat + (arg s₀ i).toNat) (addOverflow (s.gpr d) (arg s₀ i) (s.gpr d + arg s₀ i))).setReg d + (s.gpr d + arg s₀ i)) ?_ (k _ (MdStream.X86.Upd.flags _ _ _ _ _ _)) + have ea : s.ea (at_ .esp (4 + 4 * i)) = argAddr s₀ i := by rw [ea_at', hesp]; rfl + simp [exec, execAlu, readSrc, argOp, State.load32, ea, hin, hv] + +end + +end VG.Proof.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/Subkeys.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/Subkeys.lean new file mode 100644 index 000000000..e3f2597e4 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/Subkeys.lean @@ -0,0 +1,375 @@ +import VerifiedGarbage.Proof.CmacAes.X86.Dbl +import VerifiedGarbage.Proof.CmacAes.X86.UpdateCorrect + +/-! +# AES-CMAC on x86: `vg_cmac_aes_subkeys` + +Untrusted: everything here is checked by Lean. `L = CIPH_K(0)` is computed +into the first block of the subkeys (a zero counter block and a zero data +block), then doubled there (`K1`) and into the second block (`K2`). Only +the subkeys, the scratch buffer and the 28 bytes below `esp` change, so the +stack arguments, which are reloaded from the stack, and the return address +are intact. +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 VG.Impl.CmacAes.X86 +open VG.Proof.MdStream.X86 (Upd wp_mov wp_movi wp_addi) + +section +variable (s₀ : State) + +/-- The subkeys. -/ +abbrev Kb : BitVec 32 := arg s₀ 2 +/-- The scratch buffer. -/ +abbrev Sc : BitVec 32 := arg s₀ 3 + +abbrev kR : Region := ⟨(Kb s₀).setWidth 64, 32⟩ +abbrev scR : Region := ⟨(Sc s₀).setWidth 64, 2176⟩ +abbrev kArgsR : Region := ⟨argAddr s₀ 0, 16⟩ + +/-- The regions the function writes, with the stack below it. -/ +abbrev SBig : List Region := [kR s₀, scR s₀, stkR s₀] + +/-- The memory after saving the registers in the scratch buffer. -/ +def sSaved : Mem := saveMem s₀.mem ((Sc s₀).setWidth 64) s₀.gpr saved + +/-- The memory before the call. -/ +def sPreMem : Mem := + Proof.Cmac.zero4 (Proof.Cmac.zero4 (sSaved s₀) ((Sc s₀).setWidth 64 + BitVec.ofNat 64 2048)) ((Kb s₀).setWidth 64) + +end + +/-- The precondition, by name. -/ +structure SPre (s₀ : State) : Prop where + rd : s₀.rd = [schR s₀, kArgsR s₀] + wr : s₀.wr = [kR s₀, scR s₀] + sch_k : (schR s₀).Disjoint (kR s₀) + sch_scr : (schR s₀).Disjoint (scR s₀) + k_scr : (kR s₀).Disjoint (scR s₀) + args_k : (kArgsR s₀).Disjoint (kR s₀) + args_scr : (kArgsR s₀).Disjoint (scR s₀) + ret_k : (retR s₀).Disjoint (kR s₀) + ret_scr : (retR s₀).Disjoint (scR s₀) + b_sch : (stkR s₀).Disjoint (schR s₀) + b_k : (stkR s₀).Disjoint (kR s₀) + b_scr : (stkR s₀).Disjoint (scR s₀) + sch_fit : (W s₀).toNat + 240 ≤ 2 ^ 32 + k_fit : (Kb s₀).toNat + 32 ≤ 2 ^ 32 + scr_fit : (Sc s₀).toNat + 2176 ≤ 2 ^ 32 + esp28 : 28 ≤ (E s₀).toNat + esp_fit : (E s₀).toNat + 20 ≤ 2 ^ 32 + rounds : R s₀ = 10 ∨ R s₀ = 12 ∨ R s₀ = 14 + +theorem SPre.of {s₀ : State} (h : subkeysX86.pre s₀) : SPre s₀ := + let ⟨a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r⟩ := h + ⟨a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r⟩ + +/-! ## Addresses and regions -/ + +theorem ret_stk (s₀ : State) : (retR s₀).Disjoint (stkR s₀) := by + have := Offset.disjoint_below_above ((E s₀).setWidth 64) (m := 28) (a := 0) (l := 4) (by decide) + rw [add0] at this + exact this.symm + +theorem sSaved_frame (s₀ : State) : Frame [scR s₀] s₀.mem (sSaved s₀) := + saveMem_frame _ _ _ (by decide) saved fun p hp => by have := saved_bound p hp; omega + +section +variable {s₀ : State} (hp : SPre s₀) +include hp + +theorem SPre.below_eq : below (E s₀) 28 = stkR s₀ := by + simp only [below]; rw [Taint.sub_setWidth hp.esp28] + +theorem SPre.argA {i : Nat} (hi : i < 4) : argAddr s₀ i = argAddr s₀ 0 + BitVec.ofNat 64 (4 * i) := by + have : (s₀.gpr .esp).toNat + 20 ≤ 2 ^ 32 := hp.esp_fit + simp only [argAddr] + rw [show (s₀.gpr .esp + BitVec.ofNat 32 (4 + 4 * i)).setWidth 64 = addr (s₀.gpr .esp) (4 + 4 * i) from rfl, + show (s₀.gpr .esp + BitVec.ofNat 32 (4 + 4 * 0)).setWidth 64 = addr (s₀.gpr .esp) (4 + 4 * 0) from rfl, + addr_eq (by omega), addr_eq (by omega), Offset.add_add] + +theorem SPre.arg_sub {i : Nat} (hi : i < 4) : Region.Sub ⟨argAddr s₀ i, 4⟩ (kArgsR s₀) := by + rw [hp.argA hi]; exact Offset.sub_base _ (by omega) + +theorem SPre.arg_in {i : Nat} (hi : i < 4) : InRegions (s₀.rd ++ s₀.wr) (argAddr s₀ i) 4 := by + refine ⟨kArgsR s₀, by simp [hp.rd], ?_⟩ + rw [hp.argA hi]; exact Offset.contains_base _ (by omega) (by omega) + +theorem SPre.args_stk : (kArgsR s₀).Disjoint (stkR s₀) := by + have : (s₀.gpr .esp).toNat + 20 ≤ 2 ^ 32 := hp.esp_fit + have e : argAddr s₀ 0 = (E s₀).setWidth 64 + BitVec.ofNat 64 4 := addr_eq (by omega) + show Region.Disjoint ⟨argAddr s₀ 0, 16⟩ _ + rw [e]; exact (Offset.disjoint_below_above _ (by decide)).symm + +/-- The stack arguments are unchanged where only `SBig` changes. -/ +theorem SPre.arg_keep {m : Mem} (hf : Frame (SBig s₀) s₀.mem m) {i : Nat} (hi : i < 4) : + m.readW (argAddr s₀ i) 32 = arg s₀ i := + hf.readW (Region.contains_self _ _) (fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact hp.args_k.sub_left (hp.arg_sub hi) + · exact hp.args_scr.sub_left (hp.arg_sub hi) + · exact hp.args_stk.sub_left (hp.arg_sub hi)) (by decide) + +theorem SPre.sched_bytes {m : Mem} (hf : Frame (SBig s₀) s₀.mem m) : + Spec.Aes.bytesAt m ((W s₀).setWidth 64) (16 * (R s₀ + 1)) = + Spec.Aes.bytesAt s₀.mem ((W s₀).setWidth 64) (16 * (R s₀ + 1)) := by + have hR : 16 * (R s₀ + 1) ≤ 240 := by rcases hp.rounds with h | h | h <;> omega + refine Proof.Cmac.bytesAt_frame hf (fun r hr => ?_) (by omega) + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact hp.sch_k.sub_left (Region.sub_prefix hR) + · exact hp.sch_scr.sub_left (Region.sub_prefix hR) + · exact hp.b_sch.symm.sub_left (Region.sub_prefix hR) + +theorem SPre.ret_keep {m : Mem} (hf : Frame (SBig s₀) s₀.mem m) : + m.readW ((E s₀).setWidth 64) 32 = s₀.mem.readW ((E s₀).setWidth 64) 32 := + hf.readW (r := retR s₀) (Region.contains_self _ _) (fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact hp.ret_k + · exact hp.ret_scr + · exact ret_stk s₀) (by decide) + +theorem SPre.cA : (Sc s₀ + BitVec.ofNat 32 2048).setWidth 64 = (Sc s₀).setWidth 64 + BitVec.ofNat 64 2048 := + addr_eq (by have := hp.scr_fit; omega) + +end + +/-- The frame of the code that changes only the subkeys, the scratch buffer +but the saved registers, and the stack below `esp`. -/ +theorem sbig_of {s₀ : State} {m : Mem} + (hf : Frame [kR s₀, ⟨(Sc s₀).setWidth 64, 2064⟩, stkR s₀] (sSaved s₀) m) : Frame (SBig s₀) s₀.mem m := + ((sSaved_frame s₀).mono (by simp)).trans (hf.sub fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact ⟨kR s₀, by simp, fun _ h => h⟩ + · exact ⟨scR s₀, by simp, Region.sub_prefix (by decide)⟩ + · exact ⟨stkR s₀, by simp, fun _ h => h⟩) + +/-! ## Before the call -/ + +/-- What the code before the call leaves. -/ +structure SAfter (s₀ s : State) : Prop where + pre : CtrPre s (W s₀) (Sc s₀ + BitVec.ofNat 32 2048) (Kb s₀) (Sc s₀) (R s₀) + esp : s.gpr .esp = E s₀ + rd : s.rd = s₀.rd + wr : s.wr = s₀.wr + mem : s.mem = sPreMem s₀ + +theorem subkeysPre_eq : subkeysPre = .mov .eax (argOp 3) :: (saved.map (fun p => Instr.store (at_ .eax p.2) p.1) ++ + (.mov .ebp (.reg .eax) :: .mov .ebx (argOp 2) :: (zero4 .ebp 2048 ++ (zero4 .ebx 0 ++ ctrArgs)))) := rfl + +theorem sPreMem_frame (s₀ : State) : + Frame [kR s₀, ⟨(Sc s₀).setWidth 64, 2064⟩, stkR s₀] (sSaved s₀) (sPreMem s₀) := + ((Proof.Cmac.frame_store4 _ _ _ _ _).sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨⟨(Sc s₀).setWidth 64, 2064⟩, by simp, Offset.sub_base _ (by decide)⟩).trans + ((Proof.Cmac.frame_store4 _ _ _ _ _).sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨kR s₀, by simp, Region.sub_prefix (by decide)⟩) + +theorem spre_wp {s₀ : State} (hp : SPre s₀) : WP isa (.block subkeysPre) s₀ (SAfter s₀) := by + have hsc := hp.scr_fit + have hk := hp.k_fit + have cA := hp.cA + rw [subkeysPre_eq] + refine wp_arg (s₀ := s₀) rfl (hp.arg_in (by decide)) rfl fun s₁ u₁ => ?_ + have h₁ : s₁.gpr .eax = Sc s₀ := u₁.gpr + refine saveList_ok saved s₁ _ (fun p hp' => ?_) fun s₂ g₂ rd₂ wr₂ m₂ => ?_ + · have hb := saved_bound p hp' + rw [h₁, u₁.wr, hp.wr] + exact ⟨by omega, ⟨scR s₀, by simp, Offset.contains_base _ (by omega) (by omega)⟩⟩ + have hm₂ : s₂.mem = sSaved s₀ := by + rw [m₂, u₁.mem, h₁, sSaved] + exact saveMem_congr _ _ _ fun p hp' => u₁.other _ (saved_ne_eax p hp') + have esp₂ : s₂.gpr .esp = E s₀ := by rw [g₂, u₁.other _ (by decide)] + have rw₂ : s₂.rd ++ s₂.wr = s₀.rd ++ s₀.wr := by rw [rd₂, wr₂, u₁.rd, u₁.wr] + have big₂ : Frame (SBig s₀) s₀.mem s₂.mem := by rw [hm₂]; exact (sSaved_frame s₀).mono (by simp) + refine wp_mov fun s₃ u₃ => ?_ + refine wp_arg (s₀ := s₀) (by rw [u₃.other _ (by decide), esp₂]) + (by rw [u₃.rd, u₃.wr, rw₂]; exact hp.arg_in (by decide)) + (by rw [u₃.mem]; exact hp.arg_keep big₂ (by decide)) fun s₄ u₄ => ?_ + have p₄ : s₄.gpr .ebp = Sc s₀ := by rw [u₄.other _ (by decide), u₃.gpr, g₂, h₁] + have b₄ : s₄.gpr .ebx = Kb s₀ := u₄.gpr + have w₄ : s₄.wr = s₀.wr := by rw [u₄.wr, u₃.wr, wr₂, u₁.wr] + refine zero4_ok (b := .ebp) (d := 2048) (by decide) (by rw [p₄]; omega) ?_ fun s₅ g₅ m₅ rd₅ wr₅ => ?_ + · rw [p₄, w₄, hp.wr] + exact Covers.of_sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨scR s₀, by simp, 2048, rfl, by simp⟩ + have b₅ : s₅.gpr .ebx = Kb s₀ := by rw [g₅ _ (by decide), b₄] + refine zero4_ok (b := .ebx) (d := 0) (by decide) (by rw [b₅]; omega) ?_ fun s₆ g₆ m₆ rd₆ wr₆ => ?_ + · rw [b₅, add0, wr₅, w₄, hp.wr] + exact Covers.of_sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨kR s₀, by simp, 0, by simp, by simp⟩ + have esp₆ : s₆.gpr .esp = E s₀ := by + rw [g₆ _ (by decide), g₅ _ (by decide), u₄.other _ (by decide), u₃.other _ (by decide), esp₂] + have mem₆ : s₆.mem = sPreMem s₀ := by + rw [m₆, b₅, add0, m₅, p₄, u₄.mem, u₃.mem, hm₂]; rfl + have big₆ : Frame (SBig s₀) s₀.mem s₆.mem := by rw [mem₆]; exact sbig_of (sPreMem_frame s₀) + have rw₆ : s₆.rd ++ s₆.wr = s₀.rd ++ s₀.wr := by rw [rd₆, wr₆, rd₅, wr₅, u₄.rd, u₄.wr, u₃.rd, u₃.wr, rw₂] + rw [ctrArgs_eq] + refine wp_arg (s₀ := s₀) esp₆ (by rw [rw₆]; exact hp.arg_in (by decide)) (hp.arg_keep big₆ (by decide)) + fun s₇ u₇ => ?_ + refine wp_arg (s₀ := s₀) (by rw [u₇.other _ (by decide), esp₆]) + (by rw [u₇.rd, u₇.wr, rw₆]; exact hp.arg_in (by decide)) + (by rw [u₇.mem]; exact hp.arg_keep big₆ (by decide)) fun s₈ u₈ => ?_ + refine wp_mov fun s₉ u₉ => wp_addi fun s₁₀ u₁₀ => wp_movi fun s₁₁ u₁₁ => WP.block_nil ?_ + have keep : ∀ r, r ≠ .eax → r ≠ .ecx → r ≠ .edx → r ≠ .edi → s₁₁.gpr r = s₆.gpr r := fun r ha hc hd hi => by + rw [u₁₁.other _ hi, u₁₀.other _ hd, u₉.other _ hd, u₈.other _ hc, u₇.other _ ha] + have p₆ : s₆.gpr .ebp = Sc s₀ := by rw [g₆ _ (by decide), g₅ _ (by decide), p₄] + have b₆ : s₆.gpr .ebx = Kb s₀ := by rw [g₆ _ (by decide), b₅] + have sp₁₁ : s₁₁.gpr .esp = E s₀ := by rw [keep _ (by decide) (by decide) (by decide) (by decide), esp₆] + have rd₁₁ : s₁₁.rd = s₀.rd := by rw [u₁₁.rd, u₁₀.rd, u₉.rd, u₈.rd, u₇.rd, rd₆, rd₅, u₄.rd, u₃.rd, rd₂, u₁.rd] + have wr₁₁ : s₁₁.wr = s₀.wr := by rw [u₁₁.wr, u₁₀.wr, u₉.wr, u₈.wr, u₇.wr, wr₆, wr₅, w₄] + have mem₁₁ : s₁₁.mem = sPreMem s₀ := by rw [u₁₁.mem, u₁₀.mem, u₉.mem, u₈.mem, u₇.mem, mem₆] + have hb : below (s₁₁.gpr .esp) 28 = stkR s₀ := by rw [sp₁₁]; exact hp.below_eq + refine ⟨⟨?_, ?_, ?_, ?_, u₁₁.gpr, ?_, hp.rounds, by rw [sp₁₁]; exact hp.esp28, ?_, + hp.sch_k.sub_right (Region.sub_prefix (by decide)), hp.sch_scr.sub_right (Region.sub_prefix (by decide)), + ?_, ?_, (hp.k_scr.sub_left (Region.sub_prefix (by decide))).sub_right (Region.sub_prefix (by decide)), + by rw [hb]; exact hp.b_sch, ?_, by rw [hb]; exact hp.b_k.sub_right (Region.sub_prefix (by decide)), + by rw [hb]; exact hp.b_scr.sub_right (Region.sub_prefix (by decide)), hp.sch_fit, ?_, by omega, by omega, + ?_, ?_, ?_⟩, sp₁₁, rd₁₁, wr₁₁, mem₁₁⟩ + · rw [u₁₁.other _ (by decide), u₁₀.other _ (by decide), u₉.other _ (by decide), u₈.other _ (by decide), u₇.gpr] + · rw [u₁₁.other _ (by decide), u₁₀.other _ (by decide), u₉.other _ (by decide), u₈.gpr]; exact arg_ofNat s₀ 1 + · rw [u₁₁.other _ (by decide), u₁₀.gpr, u₉.gpr, u₈.other _ (by decide), u₇.other _ (by decide), p₆] + · rw [keep _ (by decide) (by decide) (by decide) (by decide), b₆] + · rw [keep _ (by decide) (by decide) (by decide) (by decide), p₆] + · rw [cA]; exact hp.sch_scr.sub_right (Offset.sub_base _ (by decide)) + · rw [cA] + exact (hp.k_scr.symm.sub_left (Offset.sub_base _ (by decide))).sub_right (Region.sub_prefix (by decide)) + · rw [cA]; exact Offset.disjoint_base _ (by decide) (by omega) + · rw [hb, cA]; exact hp.b_scr.sub_right (Offset.sub_base _ (by decide)) + · rw [BitVec.toNat_add, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (a := 2048) (by decide), + Nat.mod_eq_of_lt (by omega)]; omega + · rw [rd₁₁, wr₁₁, hp.rd] + exact Covers.of_sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨schR s₀, by simp, 0, by simp, by simp⟩ + · rw [wr₁₁, hp.wr, cA] + refine Covers.of_sub fun r hr => ?_ + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact ⟨scR s₀, by simp, 2048, rfl, by simp⟩ + · exact ⟨kR s₀, by simp, 0, by simp, by simp⟩ + · exact ⟨scR s₀, by simp, 0, by simp, by simp⟩ + · rw [mem₁₁, sPreMem]; exact Proof.Cmac.zero4_bytes _ _ + +/-! ## The call, the doubling and the restore -/ + +theorem subkeysPost_eq : subkeysPost = dbl 0 0 ++ (dbl 0 16 ++ (.mov .eax (argOp 3) :: + (saved.map fun p => Instr.mov p.1 (.mem (at_ .eax p.2))) ++ [])) := rfl + +theorem subkeys_wp {s₀ : State} (h0 : subkeysX86.pre s₀) : + WP isa subkeys s₀ fun s' => abiPreserved s₀ s' ∧ subkeysX86.post s₀ s' := by + have hp := SPre.of h0 + have hk := hp.k_fit + have hsc := hp.scr_fit + have hR := hp.rounds + have hRb : 16 * (R s₀ + 1) ≤ 240 := by rcases hR with h | h | h <;> omega + have cA := hp.cA + have cK : ∀ d n, d + n ≤ 32 → Covers [⟨(Kb s₀).setWidth 64 + BitVec.ofNat 64 d, n⟩] s₀.wr := fun d n h => by + rw [hp.wr] + exact Covers.of_sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; exact ⟨kR s₀, by simp, d, rfl, h⟩ + have cKr : ∀ d n, d + n ≤ 32 → Covers [⟨(Kb s₀).setWidth 64 + BitVec.ofNat 64 d, n⟩] (s₀.rd ++ s₀.wr) := + fun d n h a k hi => by + obtain ⟨r, hr, hc⟩ := cK d n h a k hi; exact ⟨r, List.mem_append_right _ hr, hc⟩ + unfold subkeys + refine WP.seq (WP.mono (spre_wp hp) fun s₁ a => ?_) + refine WP.seq (WP.mono (ctr_call a.pre) fun s₂ h₂ => ?_) + have hb : below (s₁.gpr .esp) 28 = stkR s₀ := by rw [a.esp]; exact hp.below_eq + -- The memory after the call. + have f₂ : Frame [kR s₀, ⟨(Sc s₀).setWidth 64, 2064⟩, stkR s₀] (sPreMem s₀) s₂.mem := by + have fr := h₂.frame + rw [hb, cA, a.mem] at fr + exact fr.sub fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · exact ⟨⟨(Sc s₀).setWidth 64, 2064⟩, by simp, Offset.sub_base _ (by decide)⟩ + · exact ⟨kR s₀, by simp, Region.sub_prefix (by decide)⟩ + · exact ⟨⟨(Sc s₀).setWidth 64, 2064⟩, by simp, Region.sub_prefix (by decide)⟩ + · exact ⟨stkR s₀, by simp, fun _ h => h⟩ + have fr₂ := (sPreMem_frame s₀).trans f₂ + have kC : (⟨(Kb s₀).setWidth 64, 16⟩ : Region).Disjoint ⟨(Sc s₀).setWidth 64 + BitVec.ofNat 64 2048, 16⟩ := + (hp.k_scr.sub_left (Region.sub_prefix (by decide))).sub_right (Offset.sub_base _ (by decide)) + have zC : Spec.Aes.bytesAt (sPreMem s₀) ((Sc s₀).setWidth 64 + BitVec.ofNat 64 2048) 16 = Spec.Cmac.zeros 16 := by + rw [sPreMem, Proof.Cmac.zero4, Proof.Cmac.bytesAt_frame16 (Proof.Cmac.frame_store4 _ _ _ _ _) (by + intro r hr; simp only [List.mem_singleton] at hr; subst hr; exact kC.symm)] + exact Proof.Cmac.zero4_bytes _ _ + have L : Spec.Aes.bytesAt s₂.mem ((Kb s₀).setWidth 64) 16 = ciph s₀ (Spec.Cmac.zeros 16) := by + have out := h₂.out + rw [hp.sched_bytes (by rw [a.mem]; exact sbig_of (sPreMem_frame s₀)), cA, a.mem, zC] at out + exact out + have b₂ : s₂.gpr .ebx = Kb s₀ := by rw [h₂.saved .ebx (by simp [calleeSaved]), a.pre.ebx] + have rdwr₂ : s₂.rd ++ s₂.wr = s₀.rd ++ s₀.wr := by rw [h₂.rd, h₂.wr, a.rd, a.wr] + have wr₂ : s₂.wr = s₀.wr := by rw [h₂.wr, a.wr] + -- The doubling. + rw [subkeysPost_eq] + refine dbl_wp b₂ (by omega) (by omega) (by rw [rdwr₂]; exact cKr 0 16 (by decide)) + (by rw [wr₂]; exact cK 0 16 (by decide)) fun s₃ g₃ m₃ rd₃ wr₃ => ?_ + have b₃ : s₃.gpr .ebx = Kb s₀ := by + rw [g₃ _ (by decide) (by decide) (by decide) (by decide) (by decide) (by decide), b₂] + refine dbl_wp b₃ (by omega) (by omega) (by rw [rd₃, wr₃, rdwr₂]; exact cKr 0 16 (by decide)) + (by rw [wr₃, wr₂]; exact cK 16 16 (by decide)) fun s₄ g₄ m₄ rd₄ wr₄ => ?_ + have f₄ : Frame [kR s₀, ⟨(Sc s₀).setWidth 64, 2064⟩, stkR s₀] (sSaved s₀) s₄.mem := by + refine fr₂.trans (((dblMem_frame _ _ _ _).sub fun r hr => ?_).trans ((dblMem_frame _ _ _ _).sub fun r hr => ?_)) + |> fun h => by rw [m₄, m₃]; exact h + all_goals simp only [List.mem_singleton] at hr; subst hr + · exact ⟨kR s₀, by simp, Offset.sub_base _ (by decide)⟩ + · exact ⟨kR s₀, by simp, Offset.sub_base _ (by decide)⟩ + have big₄ := sbig_of f₄ + have esp₄ : s₄.gpr .esp = E s₀ := by + rw [g₄ _ (by decide) (by decide) (by decide) (by decide) (by decide) (by decide), + g₃ _ (by decide) (by decide) (by decide) (by decide) (by decide) (by decide), + h₂.saved .esp (by simp [calleeSaved]), a.esp] + have rdwr₄ : s₄.rd ++ s₄.wr = s₀.rd ++ s₀.wr := by rw [rd₄, wr₄, rd₃, wr₃, rdwr₂] + -- The restore. + refine wp_arg (s₀ := s₀) esp₄ (by rw [rdwr₄]; exact hp.arg_in (by decide)) (hp.arg_keep big₄ (by decide)) + fun s₅ u₅ => ?_ + have sl : ∀ r d, (r, d) ∈ saved → s₄.mem.readW ((Sc s₀).setWidth 64 + BitVec.ofNat 64 d) 32 = s₀.gpr r := by + intro r d hrd + have hb := saved_bound _ hrd + rw [f₄.readW (r := ⟨(Sc s₀).setWidth 64 + BitVec.ofNat 64 d, 4⟩) (Region.contains_self _ _) (fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact hp.k_scr.symm.sub_left (Offset.sub_base _ (by omega)) + · exact Offset.disjoint_base _ hb.1 (by omega) + · exact hp.b_scr.symm.sub_left (Offset.sub_base _ (by omega))) (by decide)] + exact saveMem_slot _ _ _ hrd + refine restoreList_ok saved s₅ _ saved_nodup (fun p hp' => ?_) fun s₆ ld₆ ho₆ m₆ rd₆ wr₆ => WP.block_nil ?_ + · have hb := saved_bound p hp' + have hsc' : (arg s₀ 3).toNat + 2176 ≤ 2 ^ 32 := hsc + rw [u₅.gpr, u₅.rd, u₅.wr, rdwr₄, hp.rd, hp.wr] + exact ⟨saved_ne_eax p hp', by omega, ⟨scR s₀, by simp, Offset.contains_base _ (by omega) (by omega)⟩⟩ + refine ⟨⟨fun r hr => ?_, ?_⟩, ?_⟩ + · simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl | rfl + · rw [ld₆ (.ebx, 2064) (by decide), u₅.gpr, u₅.mem, sl .ebx 2064 (by decide)] + · rw [ld₆ (.esi, 2068) (by decide), u₅.gpr, u₅.mem, sl .esi 2068 (by decide)] + · rw [ld₆ (.edi, 2072) (by decide), u₅.gpr, u₅.mem, sl .edi 2072 (by decide)] + · rw [ld₆ (.ebp, 2076) (by decide), u₅.gpr, u₅.mem, sl .ebp 2076 (by decide)] + · rw [ho₆ _ (by decide), u₅.other _ (by decide), esp₄] + · rw [m₆, u₅.mem]; exact hp.ret_keep big₄ + · show Spec.Aes.bytesAt s₆.mem ((Kb s₀).setWidth 64) 32 = _ + have b₃' : Spec.Aes.bytesAt s₃.mem ((Kb s₀).setWidth 64) 16 = + Spec.Cmac.dbl 16 (Spec.Aes.bytesAt s₂.mem ((Kb s₀).setWidth 64) 16) := by + have := dblMem_bytes s₂.mem ((Kb s₀).setWidth 64) 0 0 + rw [add0] at this; rw [m₃, this] + have lo : Spec.Aes.bytesAt s₄.mem ((Kb s₀).setWidth 64) 16 = Spec.Aes.bytesAt s₃.mem ((Kb s₀).setWidth 64) 16 := by + rw [m₄] + exact Proof.Cmac.bytesAt_frame16 (dblMem_frame _ _ _ _) fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact (Offset.disjoint_base _ (by decide) (by omega)).symm + have hi : Spec.Aes.bytesAt s₄.mem ((Kb s₀).setWidth 64 + BitVec.ofNat 64 16) 16 = + Spec.Cmac.dbl 16 (Spec.Aes.bytesAt s₃.mem ((Kb s₀).setWidth 64) 16) := by + have := dblMem_bytes s₃.mem ((Kb s₀).setWidth 64) 0 16 + rw [add0] at this; rw [m₄, this] + rw [m₆, u₅.mem, Proof.Cmac.bytesAt_32, lo, hi, b₃', L] + rfl + +end VG.Proof.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/SubkeysCT.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/SubkeysCT.lean new file mode 100644 index 000000000..e6fbc4480 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/SubkeysCT.lean @@ -0,0 +1,103 @@ +import VerifiedGarbage.Proof.CmacAes.X86.Subkeys +import VerifiedGarbage.Proof.CmacAes.X86.UpdateCT + +/-! +# AES-CMAC on x86: `vg_cmac_aes_subkeys` is constant time + +Untrusted: everything here is checked by Lean. The code before the call is +checked by the taint analysis from `esp` and the stack arguments (which +nothing writes, `argTaint`), the call of `vg_aes_ctr32`, in its frame, is +constant time by its own proof (`ctr_rel`), and the code after it by the +taint analysis again, from `esp`, the stack arguments and `ebx` (the +subkeys, which the correctness proof pins). +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 VG.Impl.CmacAes.X86 + +theorem SPre.argsOut {s₀ : State} (hp : SPre s₀) {s : State} (hesp : s.gpr .esp = E s₀) (hwr : s.wr = s₀.wr) : + ArgsOut 4 s := by + have hs : (s₀.gpr .esp).toNat + 20 ≤ 2 ^ 32 := hp.esp_fit + refine ⟨by rw [hesp]; omega, ?_⟩ + rw [hwr, hp.wr, hesp] + simp only [List.mem_cons, List.not_mem_nil, or_false] + rintro r (rfl | rfl) + · exact VG.X86.Taint.frame_disjoint (n := 16) (by omega) hp.ret_k hp.args_k + · exact VG.X86.Taint.frame_disjoint (n := 16) (by omega) hp.ret_scr hp.args_scr + +/-- What two runs agree on at a point between the calls. -/ +structure SPt (s₀ : State) (s : State) : Prop where + esp : s.gpr .esp = E s₀ + wr : s.wr = s₀.wr + args : ∀ i < 4, s.mem.readW (argAddr s₀ i) 32 = arg s₀ i + +section +variable {s₀ s₀' : State} (hq : subkeysX86.pub s₀ s₀') +include hq + +theorem spub_arg {i : Nat} (hi : i < 4) : arg s₀ i = arg s₀' i := hq.2 i hi + +/-- Two runs agree on `esp`, the stack arguments and the registers `rs`. -/ +theorem SPt.agree (hp : SPre s₀) (hp' : SPre s₀') {rs : List Reg} {s₁ s₂ : State} (h₁ : SPt s₀ s₁) + (h₂ : SPt s₀' s₂) (hr : ∀ r ∈ rs, s₁.gpr r = s₂.gpr r) : + VG.X86.Taint.Agree (argTaint rs (4 + 4 * 4)) s₁ s₂ := + agree_argTaint hr (by rw [h₁.esp, h₂.esp]; exact hq.1) (hp.argsOut h₁.esp h₁.wr) (hp'.argsOut h₂.esp h₂.wr) + fun i hi => by rw [arg_cur (h₁.esp) (h₁.args i hi), arg_cur (h₂.esp) (h₂.args i hi), spub_arg hq hi] + +end + +theorem SAfter.pt {s₀ : State} (hp : SPre s₀) {s : State} (h : SAfter s₀ s) : SPt s₀ s := + ⟨h.esp, h.wr, fun _ hi => hp.arg_keep (by rw [h.mem]; exact sbig_of (sPreMem_frame s₀)) hi⟩ + +/-- What is known after the call. -/ +structure SPost (s₀ : State) (s : State) : Prop where + ebx : s.gpr .ebx = Kb s₀ + pt : SPt s₀ s + +theorem spost_wp {s₀ : State} (hp : SPre s₀) {s : State} (h : SAfter s₀ s) : WP isa ctrCall s (SPost s₀) := + WP.mono (ctr_call h.pre) fun s' hc => by + have hb : below (s.gpr .esp) 28 = stkR s₀ := by rw [h.esp]; exact hp.below_eq + have fr := hc.frame + rw [hb, hp.cA, h.mem] at fr + have big : Frame (SBig s₀) s₀.mem s'.mem := (sbig_of (sPreMem_frame s₀)).trans (fr.sub fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · exact ⟨scR s₀, by simp, Offset.sub_base _ (by decide)⟩ + · exact ⟨kR s₀, by simp, Region.sub_prefix (by decide)⟩ + · exact ⟨scR s₀, by simp, Region.sub_prefix (by decide)⟩ + · exact ⟨stkR s₀, by simp, fun _ h => h⟩) + exact ⟨by rw [hc.saved .ebx (by simp [calleeSaved]), h.pre.ebx], + ⟨by rw [hc.saved .esp (by simp [calleeSaved]), h.esp], by rw [hc.wr, h.wr], fun _ hi => hp.arg_keep big hi⟩⟩ + +theorem subkeys_rel {s₀ s₀' : State} (h0 : subkeysX86.pre s₀) (h0' : subkeysX86.pre s₀') + (hq : subkeysX86.pub s₀ s₀') : + RelCT isa (fun a b => a = s₀ ∧ b = s₀') subkeys fun _ _ => True := by + have hp := SPre.of h0 + have hp' := SPre.of h0' + have eW : W s₀ = W s₀' := spub_arg hq (by decide) + have eR : R s₀ = R s₀' := by rw [R, R, spub_arg hq (by decide)] + have eK : Kb s₀ = Kb s₀' := spub_arg hq (by decide) + have eS : Sc s₀ = Sc s₀' := spub_arg hq (by decide) + have pt₀ : ∀ {t : State}, SPt t t := ⟨rfl, rfl, fun _ _ => rfl⟩ + have a := ((RelCT.taint (A := taint) (P := fun a b => a = s₀ ∧ b = s₀') (argTaint [] (4 + 4 * 4)) + (fun a b h => by + obtain ⟨rfl, rfl⟩ := h + exact SPt.agree hq hp hp' pt₀ pt₀ fun r hr => by simp at hr) + (c := .block subkeysPre) (by taint_decide)).wp (F₁ := SAfter s₀) (F₂ := SAfter s₀') + fun a b h => by obtain ⟨rfl, rfl⟩ := h; exact ⟨spre_wp hp, spre_wp hp'⟩).mono (fun _ _ h => h) + fun _ _ h => h.2 + have c := ((ctr_rel (E := E s₀) (P := fun s₁ s₂ => SAfter s₀ s₁ ∧ SAfter s₀' s₂) fun s₁ s₂ h => + ⟨h.1.pre, by rw [eW, eS, eK, eR]; exact h.2.pre, h.1.esp, h.2.esp.trans hq.1.symm⟩).wp + (F₁ := SPost s₀) (F₂ := SPost s₀') fun _ _ h => ⟨spost_wp hp h.1, spost_wp hp' h.2⟩).mono + (fun _ _ h => h) fun _ _ h => h.2 + have b := RelCT.taint (A := taint) (P := fun s₁ s₂ => SPost s₀ s₁ ∧ SPost s₀' s₂) (argTaint [.ebx] (4 + 4 * 4)) + (fun _ _ h => SPt.agree hq hp hp' h.1.pt h.2.pt fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; rw [h.1.ebx, h.2.ebx, eK]) + (c := .block subkeysPost) (by taint_decide) + exact a.seq (c.seq b) + +theorem subkeys_ct : ConstantTime isa subkeysX86.pre subkeysX86.pub subkeys := + fun _ _ _ _ _ _ h₁ h₂ hq e₁ e₂ => (subkeys_rel h₁ h₂ hq _ _ _ _ _ _ ⟨rfl, rfl⟩ e₁ e₂).1 + +end VG.Proof.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/Update.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/Update.lean new file mode 100644 index 000000000..288ea0c31 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/Update.lean @@ -0,0 +1,214 @@ +import VerifiedGarbage.Proof.CmacAes.X86.Save + +/-! +# AES-CMAC on x86: `vg_cmac_aes_update`, the blocks before and in the loop + +Untrusted: everything here is checked by Lean. The invariant after `k` +blocks (`LInv`): `esi` points at the next block, `esp` is unchanged, only +the state, the first 2064 bytes of the scratch buffer and the 28 bytes below +`esp` have changed since the registers were saved, and the state is the +chaining value after the first `k` blocks. Everything else is reloaded from +the stack arguments, which nothing writes. +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 VG.Impl.CmacAes.X86 +open VG.Proof.MdStream.X86 (Upd Mupd Fupd wp_mov wp_movi wp_addi wp_add wp_cmp wp_test) + +section +variable (s₀ : State) + +abbrev E : BitVec 32 := s₀.gpr .esp +abbrev W : BitVec 32 := arg s₀ 0 +abbrev R : Nat := (arg s₀ 1).toNat +abbrev St : BitVec 32 := arg s₀ 2 +abbrev Dp : BitVec 32 := arg s₀ 3 +abbrev N : Nat := (arg s₀ 4).toNat +abbrev S : BitVec 32 := arg s₀ 5 + +abbrev schR : Region := ⟨(W s₀).setWidth 64, 240⟩ +abbrev stR : Region := ⟨(St s₀).setWidth 64, 16⟩ +abbrev dataR : Region := ⟨(Dp s₀).setWidth 64, 16 * N s₀⟩ +abbrev scrR : Region := ⟨(S s₀).setWidth 64, 2176⟩ +abbrev argsR : Region := ⟨argAddr s₀ 0, 24⟩ +abbrev retR : Region := ⟨(E s₀).setWidth 64, 4⟩ +abbrev stkR : Region := ⟨(E s₀).setWidth 64 - BitVec.ofNat 64 28, 28⟩ + +/-- The cipher. -/ +abbrev ciph : Spec.Cmac.Cipher := ciphAt s₀.mem ((W s₀).setWidth 64) (R s₀) + +/-- The message blocks. -/ +abbrev blks : List (List Byte) := Spec.Cmac.blocksAt s₀.mem ((Dp s₀).setWidth 64) 16 (N s₀) + +/-- The memory after saving the registers in the scratch buffer. -/ +def savedMem : Mem := saveMem s₀.mem ((S s₀).setWidth 64) s₀.gpr saved + +end + +/-- The precondition, by name. -/ +structure UPre (s₀ : State) : Prop where + rd : s₀.rd = [schR s₀, dataR s₀, argsR s₀] + wr : s₀.wr = [stR s₀, scrR s₀] + sch_st : (schR s₀).Disjoint (stR s₀) + sch_scr : (schR s₀).Disjoint (scrR s₀) + data_st : (dataR s₀).Disjoint (stR s₀) + data_scr : (dataR s₀).Disjoint (scrR s₀) + st_scr : (stR s₀).Disjoint (scrR s₀) + args_st : (argsR s₀).Disjoint (stR s₀) + args_scr : (argsR s₀).Disjoint (scrR s₀) + ret_st : (retR s₀).Disjoint (stR s₀) + ret_scr : (retR s₀).Disjoint (scrR s₀) + b_sch : (stkR s₀).Disjoint (schR s₀) + b_data : (stkR s₀).Disjoint (dataR s₀) + b_st : (stkR s₀).Disjoint (stR s₀) + b_scr : (stkR s₀).Disjoint (scrR s₀) + sch_fit : (W s₀).toNat + 240 ≤ 2 ^ 32 + st_fit : (St s₀).toNat + 16 ≤ 2 ^ 32 + data_fit : (Dp s₀).toNat + 16 * N s₀ ≤ 2 ^ 32 + scr_fit : (S s₀).toNat + 2176 ≤ 2 ^ 32 + esp28 : 28 ≤ (E s₀).toNat + esp_fit : (E s₀).toNat + 28 ≤ 2 ^ 32 + rounds : R s₀ = 10 ∨ R s₀ = 12 ∨ R s₀ = 14 + +theorem UPre.of {s₀ : State} (h : updateX86.pre s₀) : UPre s₀ := + let ⟨a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, t, u, v, w⟩ := h + ⟨a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, t, u, v, w⟩ + +/-- The loop invariant, after `k` blocks. -/ +structure LInv (s₀ : State) (k : Nat) (s : State) : Prop where + esi : s.gpr .esi = Dp s₀ + BitVec.ofNat 32 (16 * k) + esp : s.gpr .esp = E s₀ + rd : s.rd = s₀.rd + wr : s.wr = s₀.wr + frame : Frame [stR s₀, ⟨(S s₀).setWidth 64, 2064⟩, stkR s₀] (savedMem s₀) s.mem + state : Spec.Aes.bytesAt s.mem ((St s₀).setWidth 64) 16 = + Spec.Cmac.chain (ciph s₀) (Spec.Aes.bytesAt s₀.mem ((St s₀).setWidth 64) 16) ((blks s₀).take k) + +/-! ## Addresses and regions -/ + +theorem add0 (p : Addr) : p + BitVec.ofNat 64 0 = p := BitVec.add_zero p + +theorem add0' (p : BitVec 32) : p + BitVec.ofNat 32 0 = p := BitVec.add_zero p + +/-- The regions the function writes, with the stack below it. -/ +abbrev Big (s₀ : State) : List Region := [stR s₀, scrR s₀, stkR s₀] + +section +variable {s₀ : State} (hp : UPre s₀) +include hp + +theorem UPre.below_eq : below (E s₀) 28 = stkR s₀ := by + simp only [below]; rw [Taint.sub_setWidth hp.esp28] + +theorem UPre.argA {i : Nat} (hi : i < 6) : argAddr s₀ i = argAddr s₀ 0 + BitVec.ofNat 64 (4 * i) := by + have : (s₀.gpr .esp).toNat + 28 ≤ 2 ^ 32 := hp.esp_fit + simp only [argAddr] + rw [show (s₀.gpr .esp + BitVec.ofNat 32 (4 + 4 * i)).setWidth 64 = addr (s₀.gpr .esp) (4 + 4 * i) from rfl, + show (s₀.gpr .esp + BitVec.ofNat 32 (4 + 4 * 0)).setWidth 64 = addr (s₀.gpr .esp) (4 + 4 * 0) from rfl, + addr_eq (by omega), addr_eq (by omega), Offset.add_add] + +theorem UPre.arg_sub {i : Nat} (hi : i < 6) : Region.Sub ⟨argAddr s₀ i, 4⟩ (argsR s₀) := by + rw [hp.argA hi]; exact Offset.sub_base _ (by omega) + +theorem UPre.arg_in {i : Nat} (hi : i < 6) : InRegions (s₀.rd ++ s₀.wr) (argAddr s₀ i) 4 := by + refine ⟨argsR s₀, by simp [hp.rd], ?_⟩ + rw [hp.argA hi]; exact Offset.contains_base _ (by omega) (by omega) + +theorem UPre.args_stk : (argsR s₀).Disjoint (stkR s₀) := by + have : (s₀.gpr .esp).toNat + 28 ≤ 2 ^ 32 := hp.esp_fit + have e : argAddr s₀ 0 = (E s₀).setWidth 64 + BitVec.ofNat 64 4 := addr_eq (by omega) + show Region.Disjoint ⟨argAddr s₀ 0, 24⟩ _ + rw [e]; exact (Offset.disjoint_below_above _ (by decide)).symm + +/-- The stack arguments are unchanged where only `Big` changes. -/ +theorem UPre.arg_keep {m : Mem} (hf : Frame (Big s₀) s₀.mem m) {i : Nat} (hi : i < 6) : + m.readW (argAddr s₀ i) 32 = arg s₀ i := + hf.readW (Region.contains_self _ _) (fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact hp.args_st.sub_left (hp.arg_sub hi) + · exact hp.args_scr.sub_left (hp.arg_sub hi) + · exact hp.args_stk.sub_left (hp.arg_sub hi)) (by decide) + +theorem UPre.dataA {k : Nat} (hk : k < N s₀) : + addr (Dp s₀) (16 * k) = (Dp s₀).setWidth 64 + BitVec.ofNat 64 (16 * k) := + addr_eq (by have := hp.data_fit; omega) + +theorem UPre.dataN {k : Nat} (hk : k < N s₀) : + (Dp s₀ + BitVec.ofNat 32 (16 * k)).toNat = (Dp s₀).toNat + 16 * k := by + have := hp.data_fit + rw [BitVec.toNat_add, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (a := 16 * k) (by omega), + Nat.mod_eq_of_lt (by omega)] + +theorem UPre.scrN {d : Nat} (hd : d < 2176) : (S s₀ + BitVec.ofNat 32 d).toNat = (S s₀).toNat + d := by + have := hp.scr_fit + rw [BitVec.toNat_add, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (a := d) (by omega), Nat.mod_eq_of_lt (by omega)] + +theorem UPre.scrA {d : Nat} (hd : d < 2176) : + (S s₀ + BitVec.ofNat 32 d).setWidth 64 = (S s₀).setWidth 64 + BitVec.ofNat 64 d := + addr_eq (by have := hp.scr_fit; omega) + +end + +theorem UPre.scr_sub {s₀ : State} {d n : Nat} (h : d + n ≤ 2176) : + Region.Sub ⟨(S s₀).setWidth 64 + BitVec.ofNat 64 d, n⟩ (scrR s₀) := + Offset.sub_base _ h + +theorem UPre.data_sub {s₀ : State} {k : Nat} (hk : k < N s₀) : + Region.Sub ⟨(Dp s₀).setWidth 64 + BitVec.ofNat 64 (16 * k), 16⟩ (dataR s₀) := + Offset.sub_base _ (by omega) + +theorem savedMem_frame (s₀ : State) : Frame [scrR s₀] s₀.mem (savedMem s₀) := + saveMem_frame _ _ _ (by decide) saved fun p hp => by have := saved_bound p hp; omega + +theorem savedMem_slot (s₀ : State) {r : Reg} {d : Nat} (h : (r, d) ∈ saved) : + (savedMem s₀).readW ((S s₀).setWidth 64 + BitVec.ofNat 64 d) 32 = s₀.gpr r := + saveMem_slot _ _ _ h + +/-- `savedMem` changes only `Big`. -/ +theorem savedMem_big (s₀ : State) : Frame (Big s₀) s₀.mem (savedMem s₀) := + (savedMem_frame s₀).mono (by simp) + +/-! ## The prologue -/ + +theorem setup_eq : setup = .mov .eax (argOp 5) :: (saved.map (fun p => Instr.store (at_ .eax p.2) p.1) ++ + ([.mov .esi (argOp 3), .mov .eax (argOp 4), .alu .test .eax (.reg .eax)] : List Instr)) := rfl + +theorem ofNat_and_self_beq {k : Nat} (h : k < 2 ^ 32) : (BitVec.ofNat 32 k &&& BitVec.ofNat 32 k == 0) = decide (k = 0) := by + rw [BitVec.and_self]; exact MdStream.X86.ofNat_beq_zero h + +theorem arg_ofNat (s₀ : State) (i : Nat) : arg s₀ i = BitVec.ofNat 32 (arg s₀ i).toNat := by simp + +theorem prologue_wp {s₀ : State} (hp : UPre s₀) : + WP isa (.block setup) s₀ fun s => LInv s₀ 0 s ∧ s.zf = some (decide (N s₀ = 0)) := by + have hsc := hp.scr_fit + rw [setup_eq] + refine wp_arg (s₀ := s₀) rfl (hp.arg_in (by decide)) rfl fun s₁ u₁ => ?_ + have h₁ : s₁.gpr .eax = S s₀ := u₁.gpr + refine saveList_ok saved s₁ _ (fun p hp' => ?_) fun s₂ g₂ rd₂ wr₂ m₂ => ?_ + · have hb := saved_bound p hp' + rw [h₁, u₁.wr, hp.wr] + exact ⟨by omega, ⟨scrR s₀, by simp, Offset.contains_base _ (by omega) (by omega)⟩⟩ + have hm₂ : s₂.mem = savedMem s₀ := by + rw [m₂, u₁.mem, h₁, savedMem] + exact saveMem_congr _ _ _ fun p hp' => u₁.other _ (saved_ne_eax p hp') + have esp₂ : s₂.gpr .esp = s₀.gpr .esp := by rw [g₂, u₁.other _ (by decide)] + have rw₂ : s₂.rd ++ s₂.wr = s₀.rd ++ s₀.wr := by rw [rd₂, wr₂, u₁.rd, u₁.wr] + refine wp_arg (s₀ := s₀) esp₂ (by rw [rw₂]; exact hp.arg_in (by decide)) + (by rw [hm₂]; exact hp.arg_keep (savedMem_big s₀) (by decide)) fun s₃ u₃ => ?_ + refine wp_arg (s₀ := s₀) (by rw [u₃.other _ (by decide), esp₂]) + (by rw [u₃.rd, u₃.wr, rw₂]; exact hp.arg_in (by decide)) + (by rw [u₃.mem, hm₂]; exact hp.arg_keep (savedMem_big s₀) (by decide)) fun s₄ u₄ => ?_ + refine wp_test fun s₅ f₅ z₅ => WP.block_nil ⟨⟨?_, ?_, ?_, ?_, ?_, ?_⟩, ?_⟩ + · rw [f₅.gpr, u₄.other _ (by decide), u₃.gpr, Nat.mul_zero, add0'] + · rw [f₅.gpr, u₄.other _ (by decide), u₃.other _ (by decide), esp₂] + · rw [f₅.rd, u₄.rd, u₃.rd, rd₂, u₁.rd] + · rw [f₅.wr, u₄.wr, u₃.wr, wr₂, u₁.wr] + · rw [f₅.mem, u₄.mem, u₃.mem, hm₂]; exact Frame.refl _ _ + · rw [f₅.mem, u₄.mem, u₃.mem, hm₂, Proof.Cmac.bytesAt_frame16 (savedMem_frame s₀) (fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; exact hp.st_scr)] + rfl + · rw [z₅, u₄.gpr, arg_ofNat s₀ 4, ofNat_and_self_beq (arg s₀ 4).isLt] + +end VG.Proof.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/UpdateCT.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/UpdateCT.lean new file mode 100644 index 000000000..e634d623c --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/UpdateCT.lean @@ -0,0 +1,220 @@ +import VerifiedGarbage.Proof.CmacAes.X86.UpdateCorrect +import VerifiedGarbage.Proof.Framework.X86.ArgTaint + +/-! +# AES-CMAC on x86: `vg_cmac_aes_update` is constant time + +Untrusted: everything here is checked by Lean. The taint analysis does not +analyse frames, so two runs from states that agree on the public arguments +are related piece by piece (`RelCT`): the taint analysis covers the code +between the calls, from `esp`, the stack arguments (which nothing writes, +`argTaint`) and `esi` (the next block, which the correctness proof pins to +the public arguments), and each call of `vg_aes_ctr32`, in its frame, is +constant time by its own proof (`ctr_rel`). +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 VG.Impl.CmacAes.X86 +open VG.Proof.MdStream.X86 (eval_e eval_ne) + +/-- The stack arguments of a state with the entry stack pointer, from +those of the entry state. -/ +theorem arg_cur {s₀ s : State} (hesp : s.gpr .esp = s₀.gpr .esp) {i : Nat} + (hm : s.mem.readW (argAddr s₀ i) 32 = arg s₀ i) : arg s i = arg s₀ i := by + show s.mem.readW (argAddr s i) 32 = _ + rw [show argAddr s i = argAddr s₀ i by simp only [argAddr, hesp]]; exact hm + +theorem UPre.argsOut {s₀ : State} (hp : UPre s₀) {s : State} (hesp : s.gpr .esp = E s₀) (hwr : s.wr = s₀.wr) : + ArgsOut 6 s := by + have hs : (s₀.gpr .esp).toNat + 28 ≤ 2 ^ 32 := hp.esp_fit + refine ⟨by rw [hesp]; omega, ?_⟩ + rw [hwr, hp.wr, hesp] + simp only [List.mem_cons, List.not_mem_nil, or_false] + rintro r (rfl | rfl) + · exact VG.X86.Taint.frame_disjoint (n := 24) (by omega) hp.ret_st hp.args_st + · exact VG.X86.Taint.frame_disjoint (n := 24) (by omega) hp.ret_scr hp.args_scr + +/-- What two runs agree on at a point between the calls. -/ +structure Pt (s₀ : State) (s : State) : Prop where + esp : s.gpr .esp = E s₀ + wr : s.wr = s₀.wr + args : ∀ i < 6, s.mem.readW (argAddr s₀ i) 32 = arg s₀ i + +section +variable {s₀ s₀' : State} (hq : updateX86.pub s₀ s₀') +include hq + +theorem pub_E : E s₀ = E s₀' := hq.1 +theorem pub_arg {i : Nat} (hi : i < 6) : arg s₀ i = arg s₀' i := hq.2 i hi +theorem pub_N : N s₀ = N s₀' := by rw [N, N, pub_arg hq (by decide)] +theorem pub_W : W s₀ = W s₀' := pub_arg hq (by decide) +theorem pub_R : R s₀ = R s₀' := by rw [R, R, pub_arg hq (by decide)] +theorem pub_St : St s₀ = St s₀' := pub_arg hq (by decide) +theorem pub_Dp : Dp s₀ = Dp s₀' := pub_arg hq (by decide) +theorem pub_S : S s₀ = S s₀' := pub_arg hq (by decide) +theorem pub_Cb : Cb s₀ = Cb s₀' := by rw [Cb, Cb, pub_S hq] + +/-- Two runs agree on `esp`, the stack arguments and the registers `rs`. -/ +theorem Pt.agree (hp : UPre s₀) (hp' : UPre s₀') {rs : List Reg} {s₁ s₂ : State} (h₁ : Pt s₀ s₁) + (h₂ : Pt s₀' s₂) (hr : ∀ r ∈ rs, s₁.gpr r = s₂.gpr r) : + VG.X86.Taint.Agree (argTaint rs (4 + 4 * 6)) s₁ s₂ := + agree_argTaint hr (by rw [h₁.esp, h₂.esp, pub_E hq]) (hp.argsOut h₁.esp h₁.wr) (hp'.argsOut h₂.esp h₂.wr) + fun i hi => by rw [arg_cur (h₁.esp) (h₁.args i hi), arg_cur (h₂.esp) (h₂.args i hi), pub_arg hq hi] + +end + +theorem LInv.pt {s₀ : State} (hp : UPre s₀) {k : Nat} {s : State} (h : LInv s₀ k s) : Pt s₀ s := + ⟨h.esp, h.wr, fun _ hi => hp.arg_keep (UPre.big_of h.frame) hi⟩ + +/-! ## One block -/ + +/-- What is known between the code before the call and the call. -/ +structure Mid (s₀ : State) (k : Nat) (s : State) : Prop where + pre : CtrPre s (W s₀) (Cb s₀) (St s₀) (S s₀) (R s₀) + esi : s.gpr .esi = Dp s₀ + BitVec.ofNat 32 (16 * k) + pt : Pt s₀ s + big : Frame (Big s₀) s₀.mem s.mem + +theorem bodyMid_wp {s₀ : State} (hp : UPre s₀) {k : Nat} (hk : k < N s₀) {s : State} (h : LInv s₀ k s) : + WP isa (.block chainIn) s (Mid s₀ k) := + WP.mono (bodyA_wp hp hk h) fun s₁ a => by + have big : Frame (Big s₀) s₀.mem s₁.mem := (UPre.big_of h.frame).trans (by + rw [a.mem] + exact (Proof.Cmac.chainMem4_frame _ _ _ _).sub fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl + · exact ⟨scrR s₀, by simp, UPre.scr_sub (by decide)⟩ + · exact ⟨stR s₀, by simp, fun _ h => h⟩) + exact ⟨a.pre, by rw [a.esi, h.esi], ⟨by rw [a.esp, h.esp], by rw [a.wr, h.wr], + fun _ hi => hp.arg_keep big hi⟩, big⟩ + +/-- What is known after the call. -/ +structure After (s₀ : State) (k : Nat) (s : State) : Prop where + esi : s.gpr .esi = Dp s₀ + BitVec.ofNat 32 (16 * k) + pt : Pt s₀ s + +theorem call_after {s₀ : State} (hp : UPre s₀) {k : Nat} {s : State} (h : Mid s₀ k s) : + WP isa ctrCall s (After s₀ k) := + WP.mono (ctr_call h.pre) fun s' hc => by + have hb : below (s.gpr .esp) 28 = stkR s₀ := by rw [h.pt.esp]; exact hp.below_eq + have cA : (Cb s₀).setWidth 64 = (S s₀).setWidth 64 + BitVec.ofNat 64 2048 := hp.scrA (by decide) + have fr := hc.frame + rw [hb, cA] at fr + have big : Frame (Big s₀) s₀.mem s'.mem := h.big.trans (fr.sub fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · exact ⟨scrR s₀, by simp, UPre.scr_sub (by decide)⟩ + · exact ⟨stR s₀, by simp, fun _ h => h⟩ + · exact ⟨scrR s₀, by simp, Region.sub_prefix (by decide)⟩ + · exact ⟨stkR s₀, by simp, fun _ h => h⟩) + exact ⟨by rw [hc.saved .esi (by simp [calleeSaved]), h.esi], + ⟨by rw [hc.saved .esp (by simp [calleeSaved]), h.pt.esp], by rw [hc.wr, h.pt.wr], + fun _ hi => hp.arg_keep big hi⟩⟩ + +/-- The relation before a block, in two runs. -/ +def BRel (s₀ s₀' : State) (k : Nat) (s₁ s₂ : State) : Prop := + (k < N s₀ ∧ LInv s₀ k s₁) ∧ (k < N s₀' ∧ LInv s₀' k s₂) + +theorem body_ct {s₀ s₀' : State} (hp : UPre s₀) (hp' : UPre s₀') (hq : updateX86.pub s₀ s₀') (k : Nat) : + RelCT isa (BRel s₀ s₀' k) body fun _ _ => True := by + have a := ((RelCT.taint (A := taint) (P := BRel s₀ s₀' k) (argTaint [.esi] (4 + 4 * 6)) + (fun _ _ h => Pt.agree hq hp hp' (h.1.2.pt hp) (h.2.2.pt hp') fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; rw [h.1.2.esi, h.2.2.esi, pub_Dp hq]) + (c := .block chainIn) (by taint_decide)).wp (F₁ := Mid s₀ k) (F₂ := Mid s₀' k) + fun _ _ h => ⟨bodyMid_wp hp h.1.1 h.1.2, bodyMid_wp hp' h.2.1 h.2.2⟩).mono (fun _ _ h => h) + fun _ _ h => h.2 + have c := ((ctr_rel (E := E s₀) (P := fun s₁ s₂ => Mid s₀ k s₁ ∧ Mid s₀' k s₂) fun s₁ s₂ h => + ⟨h.1.pre, by rw [pub_W hq, pub_Cb hq, pub_St hq, pub_S hq, pub_R hq]; exact h.2.pre, h.1.pt.esp, + h.2.pt.esp.trans (pub_E hq).symm⟩).wp (F₁ := After s₀ k) (F₂ := After s₀' k) + fun _ _ h => ⟨call_after hp h.1, call_after hp' h.2⟩).mono (fun _ _ h => h) fun _ _ h => h.2 + have b := RelCT.taint (A := taint) (P := fun s₁ s₂ => After s₀ k s₁ ∧ After s₀' k s₂) + (argTaint [.esi] (4 + 4 * 6)) + (fun _ _ h => Pt.agree hq hp hp' h.1.pt h.2.pt fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; rw [h.1.esi, h.2.esi, pub_Dp hq]) + (c := .block advance) (by taint_decide) + exact a.seq (c.seq b) + +/-! ## The loop -/ + +/-- The loop's relation, with the number of iterations left. -/ +def LRel (s₀ s₀' : State) (n : Nat) (s₁ s₂ : State) : Prop := + ∃ k, n = N s₀ - k ∧ BRel s₀ s₀' k s₁ s₂ + +theorem loop_ct {s₀ s₀' : State} (hp : UPre s₀) (hp' : UPre s₀') (hq : updateX86.pub s₀ s₀') (n : Nat) : + RelCT isa (LRel s₀ s₀' n) (.loop body .ne) fun s₁ s₂ => LInv s₀ (N s₀) s₁ ∧ LInv s₀' (N s₀') s₂ := by + refine RelCT.loop (M := isa) (LRel s₀ s₀') (fun n => ?_) n + have hN := pub_N hq + refine (RelCT.exists_ fun k => ?_).mono (fun s₁ s₂ (h : LRel s₀ s₀' n s₁ s₂) => h) fun _ _ h => h + by_cases hn : n = N s₀ - k + swap + · exact RelCT.of_false fun _ _ h => hn h.1 + subst hn + have ct := (body_ct hp hp' hq k).wp + (F₁ := fun (s : State) => (LInv s₀ (k + 1) s ∧ s.zf = some (decide (k + 1 = N s₀))) ∧ k < N s₀) + (F₂ := fun (s : State) => LInv s₀' (k + 1) s ∧ s.zf = some (decide (k + 1 = N s₀'))) + fun _ _ h => ⟨WP.mono (body_ok hp h.1.1 h.1.2) fun _ r => ⟨r, h.1.1⟩, body_ok hp' h.2.1 h.2.2⟩ + refine ct.mono (fun _ _ h => h.2) fun s₁ s₂ ⟨_, ⟨⟨l₁, z₁⟩, hk⟩, ⟨l₂, z₂⟩⟩ => ?_ + have e₁ : isa.eval .ne s₁ = some !decide (k + 1 = N s₀) := by + show VG.X86.eval .ne s₁ = _; rw [eval_ne, z₁]; rfl + have e₂ : isa.eval .ne s₂ = some !decide (k + 1 = N s₀) := by + show VG.X86.eval .ne s₂ = _; rw [eval_ne, z₂, ← hN]; rfl + refine ⟨by rw [e₁, e₂], fun hf => ?_, fun ht => ?_⟩ + · rw [e₁] at hf + have h0 : k + 1 = N s₀ := by simpa using hf + exact ⟨h0 ▸ l₁, by rw [← hN, ← h0]; exact l₂⟩ + · rw [e₁] at ht + have h0 : k + 1 ≠ N s₀ := by simpa using ht + exact ⟨N s₀ - (k + 1), by omega, k + 1, rfl, ⟨by omega, l₁⟩, ⟨by omega, l₂⟩⟩ + +/-! ## The whole function -/ + +theorem update_rel {s₀ s₀' : State} (h0 : updateX86.pre s₀) (h0' : updateX86.pre s₀') + (hq : updateX86.pub s₀ s₀') : + RelCT isa (fun a b => a = s₀ ∧ b = s₀') update fun _ _ => True := by + have hp := UPre.of h0 + have hp' := UPre.of h0' + have hN := pub_N hq + have pt₀ : ∀ {t : State}, UPre t → Pt t t := fun h => ⟨rfl, rfl, fun _ _ => rfl⟩ + have pro := ((RelCT.taint (A := taint) (P := fun a b => a = s₀ ∧ b = s₀') (argTaint [] (4 + 4 * 6)) + (fun a b h => by + obtain ⟨rfl, rfl⟩ := h + exact Pt.agree hq hp hp' (pt₀ hp) (pt₀ hp') fun r hr => by simp at hr) + (c := .block setup) (by taint_decide)).wp + (F₁ := fun (s : State) => LInv s₀ 0 s ∧ s.zf = some (decide (N s₀ = 0))) + (F₂ := fun (s : State) => LInv s₀' 0 s ∧ s.zf = some (decide (N s₀' = 0))) + fun a b h => by obtain ⟨rfl, rfl⟩ := h; exact ⟨prologue_wp hp, prologue_wp hp'⟩).mono (fun _ _ h => h) + fun _ _ h => h.2 + have ev {s : State} (h : s.zf = some (decide (N s₀ = 0))) : isa.eval .e s = some (decide (N s₀ = 0)) := by + show VG.X86.eval .e s = _; rw [eval_e, h] + have ev' {s : State} (h : s.zf = some (decide (N s₀' = 0))) : isa.eval .e s = some (decide (N s₀ = 0)) := by + show VG.X86.eval .e s = _; rw [eval_e, h, hN] + have nil := RelCT.taint (A := taint) + (P := fun a b => ((LInv s₀ 0 a ∧ a.zf = some (decide (N s₀ = 0))) ∧ + (LInv s₀' 0 b ∧ b.zf = some (decide (N s₀' = 0)))) ∧ isa.eval .e a = some true) (argTaint [] (4 + 4 * 6)) + (fun _ _ h => Pt.agree hq hp hp' (h.1.1.1.pt hp) (h.1.2.1.pt hp') fun r hr => by simp at hr) + (c := .block []) (by taint_decide) + have mid : RelCT isa (fun a b => (LInv s₀ 0 a ∧ a.zf = some (decide (N s₀ = 0))) ∧ + (LInv s₀' 0 b ∧ b.zf = some (decide (N s₀' = 0)))) + (.ite .e (.block []) (.loop body .ne)) (fun a b => LInv s₀ (N s₀) a ∧ LInv s₀' (N s₀') b) := by + refine RelCT.ite (fun a b h => by rw [ev h.1.2, ev' h.2.2]) ?_ ?_ + · refine (nil.wp (F₁ := LInv s₀ (N s₀)) (F₂ := LInv s₀' (N s₀')) fun a b h => ?_).mono + (fun _ _ h => h) fun _ _ h => h.2 + have h0 : N s₀ = 0 := by + have := h.2; rw [ev h.1.1.2] at this; simpa using this + exact ⟨WP.block_nil (h0 ▸ h.1.1.1), WP.block_nil (by rw [← hN, h0]; exact h.1.2.1)⟩ + · refine (loop_ct hp hp' hq (N s₀ - 0)).mono (fun a b h => ⟨0, rfl, ⟨?_, h.1.1.1⟩, ⟨?_, h.1.2.1⟩⟩) + fun _ _ h => h + all_goals + have := h.2; rw [ev h.1.1.2] at this + have : N s₀ ≠ 0 := by simpa using this + omega + have epi := RelCT.taint (A := taint) (P := fun a b => LInv s₀ (N s₀) a ∧ LInv s₀' (N s₀') b) + (argTaint [] (4 + 4 * 6)) (fun _ _ h => Pt.agree hq hp hp' (h.1.pt hp) (h.2.pt hp') fun r hr => by simp at hr) + (c := .block (restore 5)) (by taint_decide) + exact pro.seq (mid.seq epi) + +theorem update_ct : ConstantTime isa updateX86.pre updateX86.pub update := + fun _ _ _ _ _ _ h₁ h₂ hq e₁ e₂ => (update_rel h₁ h₂ hq _ _ _ _ _ _ ⟨rfl, rfl⟩ e₁ e₂).1 + +end VG.Proof.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/UpdateCorrect.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/UpdateCorrect.lean new file mode 100644 index 000000000..92e54d51f --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/UpdateCorrect.lean @@ -0,0 +1,90 @@ +import VerifiedGarbage.Proof.CmacAes.X86.UpdateLoop + +/-! +# AES-CMAC on x86: `vg_cmac_aes_update` is correct + +Untrusted: everything here is checked by Lean. +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 VG.Impl.CmacAes.X86 +open VG.Proof.MdStream.X86 (eval_e) + +theorem slot_read {s₀ : State} (hp : UPre s₀) {m : Mem} + (hf : Frame [stR s₀, ⟨(S s₀).setWidth 64, 2064⟩, stkR s₀] (savedMem s₀) m) {d : Nat} (h₁ : 2064 ≤ d) + (h₂ : d + 4 ≤ 2080) : + m.readW ((S s₀).setWidth 64 + BitVec.ofNat 64 d) 32 = + (savedMem s₀).readW ((S s₀).setWidth 64 + BitVec.ofNat 64 d) 32 := + hf.readW (r := ⟨(S s₀).setWidth 64 + BitVec.ofNat 64 d, 4⟩) (Region.contains_self _ _) (fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact hp.st_scr.symm.sub_left (UPre.scr_sub (by omega)) + · exact Offset.disjoint_base _ h₁ (by omega) + · exact hp.b_scr.symm.sub_left (UPre.scr_sub (by omega))) (by decide) + +theorem UPre.ret_stk {s₀ : State} (_hp : UPre s₀) : (retR s₀).Disjoint (stkR s₀) := by + have := Offset.disjoint_below_above ((E s₀).setWidth 64) (m := 28) (a := 0) (l := 4) (by decide) + rw [add0] at this + exact this.symm + +/-- The return address, which nothing writes. -/ +theorem ret_read {s₀ : State} (hp : UPre s₀) {m : Mem} + (hf : Frame [stR s₀, ⟨(S s₀).setWidth 64, 2064⟩, stkR s₀] (savedMem s₀) m) : + m.readW ((E s₀).setWidth 64) 32 = s₀.mem.readW ((E s₀).setWidth 64) 32 := + (UPre.big_of hf).readW (r := retR s₀) (Region.contains_self _ _) (fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact hp.ret_st + · exact hp.ret_scr + · exact hp.ret_stk) (by decide) + +theorem saved_nodup : (saved.map Prod.fst).Nodup := by decide + +theorem epilogue_wp {s₀ : State} (hp : UPre s₀) {s : State} (h : LInv s₀ (N s₀) s) : + WP isa (.block (restore 5)) s fun s' => abiPreserved s₀ s' ∧ updateX86.post s₀ s' := by + have hsc : (arg s₀ 5).toNat + 2176 ≤ 2 ^ 32 := hp.scr_fit + have rdwr : s.rd ++ s.wr = [schR s₀, dataR s₀, argsR s₀, stR s₀, scrR s₀] := by + rw [h.rd, h.wr, hp.rd, hp.wr]; rfl + have hrw : s.rd ++ s.wr = s₀.rd ++ s₀.wr := by rw [h.rd, h.wr] + have sl : ∀ r d, (r, d) ∈ saved → s.mem.readW ((S s₀).setWidth 64 + BitVec.ofNat 64 d) 32 = s₀.gpr r := + fun r d hrd => by + have hb := saved_bound _ hrd + rw [slot_read hp h.frame hb.1 hb.2, savedMem_slot s₀ hrd] + rw [restore_eq] + refine wp_arg (s₀ := s₀) h.esp (by rw [hrw]; exact hp.arg_in (by decide)) + (hp.arg_keep (UPre.big_of h.frame) (by decide)) fun s₁ u₁ => ?_ + refine restoreList_ok saved s₁ _ saved_nodup (fun p hp' => ?_) fun s₂ ld₂ ho₂ m₂ rd₂ wr₂ => WP.block_nil ?_ + · have hb := saved_bound p hp' + rw [u₁.gpr, u₁.rd, u₁.wr, rdwr] + exact ⟨saved_ne_eax p hp', by omega, ⟨scrR s₀, by simp, Offset.contains_base _ (by omega) (by omega)⟩⟩ + refine ⟨⟨fun r hr => ?_, ?_⟩, ?_⟩ + · simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl | rfl + · rw [ld₂ (.ebx, 2064) (by decide), u₁.gpr, u₁.mem, sl .ebx 2064 (by decide)] + · rw [ld₂ (.esi, 2068) (by decide), u₁.gpr, u₁.mem, sl .esi 2068 (by decide)] + · rw [ld₂ (.edi, 2072) (by decide), u₁.gpr, u₁.mem, sl .edi 2072 (by decide)] + · rw [ld₂ (.ebp, 2076) (by decide), u₁.gpr, u₁.mem, sl .ebp 2076 (by decide)] + · rw [ho₂ _ (by decide), u₁.other _ (by decide), h.esp] + · rw [m₂, u₁.mem]; exact ret_read hp h.frame + · show Spec.Aes.bytesAt s₂.mem ((St s₀).setWidth 64) 16 = Spec.Cmac.chain (ciph s₀) _ (blks s₀) + rw [m₂, u₁.mem, h.state, List.take_of_length_le (by simp [Spec.Cmac.blocksAt])] + +theorem mid_wp {s₀ : State} (hp : UPre s₀) {s₁ : State} (h : LInv s₀ 0 s₁) + (hz : s₁.zf = some (decide (N s₀ = 0))) : + WP isa (.ite .e (.block []) (.loop body .ne)) s₁ (LInv s₀ (N s₀)) := by + have ev : isa.eval .e s₁ = some (decide (N s₀ = 0)) := by + show VG.X86.eval .e s₁ = _; rw [eval_e, hz] + by_cases hn : N s₀ = 0 + · refine WP.ite true (by rw [ev]; simp [hn]) (fun _ => WP.block_nil ?_) (fun h => by cases h) + rw [hn]; exact h + · refine WP.ite false (by rw [ev]; simp [hn]) (fun h => by cases h) fun _ => ?_ + exact loop_ok hp (by omega) h + +theorem update_wp {s₀ : State} (h0 : updateX86.pre s₀) : + WP isa update s₀ fun s' => abiPreserved s₀ s' ∧ updateX86.post s₀ s' := by + have hp := UPre.of h0 + exact WP.seq (WP.mono (prologue_wp hp) fun s₁ ⟨h₁, hz⟩ => + WP.seq (WP.mono (mid_wp hp h₁ hz) fun _ h₂ => epilogue_wp hp h₂)) + +end VG.Proof.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/UpdateLoop.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/UpdateLoop.lean new file mode 100644 index 000000000..880701b52 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/UpdateLoop.lean @@ -0,0 +1,317 @@ +import VerifiedGarbage.Proof.CmacAes.X86.Update + +/-! +# AES-CMAC on x86: the loop of `vg_cmac_aes_update` + +Untrusted: everything here is checked by Lean. One block keeps the loop +invariant (`body_ok`): the counter block is `C ⊕ Mᵢ` and the state is +zeroed (`Cmac.chainMem4`), the call of `vg_aes_ctr32` leaves +`CIPH_K(C ⊕ Mᵢ)` in the state, and ZF is set once `esi` reaches +`data + 16 n` (`adv_zf`). +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 VG.Impl.CmacAes.X86 +open VG.Proof.MdStream.X86 (Upd Mupd Fupd wp_mov wp_movi wp_addi wp_add wp_cmp eval_ne) + +theorem take_succ_blks (s₀ : State) {k : Nat} (hk : k < N s₀) : + (blks s₀).take (k + 1) = + (blks s₀).take k ++ [Spec.Aes.bytesAt s₀.mem ((Dp s₀).setWidth 64 + BitVec.ofNat 64 (16 * k)) 16] := by + rw [List.take_add_one, List.getElem?_eq_getElem (by simp [Spec.Cmac.blocksAt]; omega)] + simp [Spec.Cmac.blocksAt] + +/-! ## Memory outside the writable regions -/ + +section +variable {s₀ : State} (hp : UPre s₀) +include hp + +theorem UPre.sched_bytes {m : Mem} (hf : Frame (Big s₀) s₀.mem m) : + Spec.Aes.bytesAt m ((W s₀).setWidth 64) (16 * (R s₀ + 1)) = + Spec.Aes.bytesAt s₀.mem ((W s₀).setWidth 64) (16 * (R s₀ + 1)) := by + have hR : 16 * (R s₀ + 1) ≤ 240 := by rcases hp.rounds with h | h | h <;> omega + refine Proof.Cmac.bytesAt_frame hf (fun r hr => ?_) (by omega) + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact hp.sch_st.sub_left (Region.sub_prefix hR) + · exact hp.sch_scr.sub_left (Region.sub_prefix hR) + · exact hp.b_sch.symm.sub_left (Region.sub_prefix hR) + +theorem UPre.block_bytes {m : Mem} (hf : Frame (Big s₀) s₀.mem m) {k : Nat} (hk : k < N s₀) : + Spec.Aes.bytesAt m ((Dp s₀).setWidth 64 + BitVec.ofNat 64 (16 * k)) 16 = + Spec.Aes.bytesAt s₀.mem ((Dp s₀).setWidth 64 + BitVec.ofNat 64 (16 * k)) 16 := by + refine Proof.Cmac.bytesAt_frame hf (fun r hr => ?_) (by decide) + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact hp.data_st.sub_left (UPre.data_sub hk) + · exact hp.data_scr.sub_left (UPre.data_sub hk) + · exact hp.b_data.symm.sub_left (UPre.data_sub hk) + +end + +theorem UPre.big_of {s₀ : State} {m : Mem} + (hf : Frame [stR s₀, ⟨(S s₀).setWidth 64, 2064⟩, stkR s₀] (savedMem s₀) m) : Frame (Big s₀) s₀.mem m := + (savedMem_big s₀).trans (hf.sub fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact ⟨stR s₀, by simp, fun _ h => h⟩ + · exact ⟨scrR s₀, by simp, Region.sub_prefix (by decide)⟩ + · exact ⟨stkR s₀, by simp, fun _ h => h⟩) + +/-! ## The end of a block -/ + +theorem dbl4 (n : BitVec 32) : n + n + (n + n) + (n + n + (n + n)) + (n + n + (n + n) + (n + n + (n + n))) = + BitVec.ofNat 32 (16 * n.toNat) := by + apply BitVec.eq_of_toNat_eq + simp only [BitVec.toNat_add, BitVec.toNat_ofNat] + omega + +theorem adv_zf {D n : BitVec 32} {k : Nat} (hk : k < n.toNat) (hfit : D.toNat + 16 * n.toNat ≤ 2 ^ 32) : + (D + BitVec.ofNat 32 (16 * k) + 16 - ((n + n + (n + n) + (n + n + (n + n)) + + (n + n + (n + n) + (n + n + (n + n)))) + D) == 0) = decide (k + 1 = n.toNat) := by + rw [dbl4, Bool.eq_iff_iff, beq_iff_eq, decide_eq_true_iff, ← BitVec.toNat_inj] + simp only [BitVec.toNat_sub, BitVec.toNat_add, BitVec.toNat_ofNat, Nat.reducePow] + have := D.isLt + have h16 : (16 : BitVec 32).toNat = 16 := rfl + have h0 : (0 : BitVec 32).toNat = 0 := rfl + omega + +theorem advance_eq : advance = .alu .add .esi (.imm 16) :: .mov .eax (argOp 4) :: .alu .add .eax (.reg .eax) :: + .alu .add .eax (.reg .eax) :: .alu .add .eax (.reg .eax) :: .alu .add .eax (.reg .eax) :: + .alu .add .eax (argOp 3) :: .alu .cmp .esi (.reg .eax) :: [] := rfl + +theorem advance_wp {s₀ : State} (hp : UPre s₀) {k : Nat} (hk : k < N s₀) {s : State} + (hesi : s.gpr .esi = Dp s₀ + BitVec.ofNat 32 (16 * k)) (hesp : s.gpr .esp = E s₀) + (hargs : ∀ i < 6, s.mem.readW (argAddr s₀ i) 32 = arg s₀ i) (hrw : s.rd ++ s.wr = s₀.rd ++ s₀.wr) : + WP isa (.block advance) s fun s' => s'.gpr .esi = Dp s₀ + BitVec.ofNat 32 (16 * (k + 1)) ∧ + s'.gpr .esp = E s₀ ∧ (∀ r, r ≠ .eax → r ≠ .esi → s'.gpr r = s.gpr r) ∧ s'.mem = s.mem ∧ + s'.rd = s.rd ∧ s'.wr = s.wr ∧ s'.zf = some (decide (k + 1 = N s₀)) := by + rw [advance_eq] + refine wp_addi fun s₁ u₁ => ?_ + refine wp_arg (s₀ := s₀) (by rw [u₁.other _ (by decide), hesp]) (by rw [u₁.rd, u₁.wr, hrw]; exact hp.arg_in (by decide)) + (by rw [u₁.mem]; exact hargs 4 (by decide)) fun s₂ u₂ => ?_ + refine wp_add fun s₃ u₃ => wp_add fun s₄ u₄ => wp_add fun s₅ u₅ => wp_add fun s₆ u₆ => ?_ + refine wp_addArg (s₀ := s₀) + (by rw [u₆.other _ (by decide), u₅.other _ (by decide), u₄.other _ (by decide), u₃.other _ (by decide), + u₂.other _ (by decide), u₁.other _ (by decide), hesp]) + (by rw [u₆.rd, u₆.wr, u₅.rd, u₅.wr, u₄.rd, u₄.wr, u₃.rd, u₃.wr, u₂.rd, u₂.wr, u₁.rd, u₁.wr, hrw] + exact hp.arg_in (by decide)) + (by rw [u₆.mem, u₅.mem, u₄.mem, u₃.mem, u₂.mem, u₁.mem]; exact hargs 3 (by decide)) fun s₇ u₇ => ?_ + refine wp_cmp fun s₈ f₈ _ z₈ => WP.block_nil ⟨?_, ?_, fun r h₁ h₂ => ?_, ?_, ?_, ?_, ?_⟩ + · rw [f₈.gpr, u₇.other _ (by decide), u₆.other _ (by decide), u₅.other _ (by decide), u₄.other _ (by decide), + u₃.other _ (by decide), u₂.other _ (by decide), u₁.gpr, hesi, show (16 : BitVec 32) = BitVec.ofNat 32 16 from rfl, + Offset.add_add_eq _ (c := 16 * (k + 1)) (by omega)] + · rw [f₈.gpr, u₇.other _ (by decide), u₆.other _ (by decide), u₅.other _ (by decide), u₄.other _ (by decide), + u₃.other _ (by decide), u₂.other _ (by decide), u₁.other _ (by decide), hesp] + · rw [f₈.gpr, u₇.other _ h₁, u₆.other _ h₁, u₅.other _ h₁, u₄.other _ h₁, u₃.other _ h₁, u₂.other _ h₁, + u₁.other _ h₂] + · rw [f₈.mem, u₇.mem, u₆.mem, u₅.mem, u₄.mem, u₃.mem, u₂.mem, u₁.mem] + · rw [f₈.rd, u₇.rd, u₆.rd, u₅.rd, u₄.rd, u₃.rd, u₂.rd, u₁.rd] + · rw [f₈.wr, u₇.wr, u₆.wr, u₅.wr, u₄.wr, u₃.wr, u₂.wr, u₁.wr] + · rw [z₈, u₇.gpr, u₇.other _ (by decide), u₆.gpr, u₆.other _ (by decide), u₅.gpr, u₅.other _ (by decide), + u₄.gpr, u₄.other _ (by decide), u₃.gpr, u₃.other _ (by decide), u₂.gpr, u₂.other _ (by decide), u₁.gpr, hesi] + exact congrArg some (adv_zf hk hp.data_fit) + +/-! ## One block -/ + +/-- The counter block's address. -/ +abbrev Cb (s₀ : State) : BitVec 32 := S s₀ + BitVec.ofNat 32 2048 + +/-- What the code before the call leaves. -/ +structure BodyA (s₀ : State) (k : Nat) (s s₁ : State) : Prop where + pre : CtrPre s₁ (W s₀) (Cb s₀) (St s₀) (S s₀) (R s₀) + esi : s₁.gpr .esi = s.gpr .esi + esp : s₁.gpr .esp = s.gpr .esp + mem : s₁.mem = Proof.Cmac.chainMem4 s.mem ((S s₀).setWidth 64 + BitVec.ofNat 64 2048) ((St s₀).setWidth 64) + ((Dp s₀).setWidth 64 + BitVec.ofNat 64 (16 * k)) + rd : s₁.rd = s.rd + wr : s₁.wr = s.wr + +theorem ctrArgs_eq : ctrArgs = [.mov .eax (argOp 0), .mov .ecx (argOp 1), .mov .edx (.reg .ebp), + .alu .add .edx (.imm (BitVec.ofNat 32 2048)), .mov .edi (.imm 1)] := rfl + +theorem chainIn_eq : chainIn = .mov .ebx (argOp 2) :: .mov .ebp (argOp 5) :: + (xor4 .ebx .esi .ebp 0 0 2048 ++ (zero4 .ebx 0 ++ ctrArgs)) := rfl + +theorem bodyA_wp {s₀ : State} (hp : UPre s₀) {k : Nat} (hk : k < N s₀) {s : State} (h : LInv s₀ k s) : + WP isa (.block chainIn) s (BodyA s₀ k s) := by + have hRegs : s.rd ++ s.wr = [schR s₀, dataR s₀, argsR s₀, stR s₀, scrR s₀] := by + rw [h.rd, h.wr, hp.rd, hp.wr]; rfl + have hrw : s.rd ++ s.wr = s₀.rd ++ s₀.wr := by rw [h.rd, h.wr] + have hW : s.wr = [stR s₀, scrR s₀] := by rw [h.wr, hp.wr] + have hsc := hp.scr_fit + have hst := hp.st_fit + have hdf := hp.data_fit + have qN := hp.dataN hk + have big := UPre.big_of h.frame + have hargs : ∀ i < 6, s.mem.readW (argAddr s₀ i) 32 = arg s₀ i := fun i hi => hp.arg_keep big hi + rw [chainIn_eq] + refine wp_arg (s₀ := s₀) h.esp (by rw [hrw]; exact hp.arg_in (by decide)) (hargs 2 (by decide)) + fun s₁ u₁ => ?_ + refine wp_arg (s₀ := s₀) (by rw [u₁.other _ (by decide), h.esp]) (by rw [u₁.rd, u₁.wr, hrw]; exact hp.arg_in (by decide)) + (by rw [u₁.mem]; exact hargs 5 (by decide)) fun s₂ u₂ => ?_ + have b₂ : s₂.gpr .ebx = St s₀ := by rw [u₂.other _ (by decide), u₁.gpr] + have p₂ : s₂.gpr .ebp = S s₀ := u₂.gpr + have i₂ : s₂.gpr .esi = Dp s₀ + BitVec.ofNat 32 (16 * k) := by + rw [u₂.other _ (by decide), u₁.other _ (by decide), h.esi] + have rw₂ : s₂.rd ++ s₂.wr = [schR s₀, dataR s₀, argsR s₀, stR s₀, scrR s₀] := by + rw [u₂.rd, u₂.wr, u₁.rd, u₁.wr, hRegs] + have w₂ : s₂.wr = [stR s₀, scrR s₀] := by rw [u₂.wr, u₁.wr, hW] + refine xor4_ok (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) + (by rw [b₂]; omega) (by rw [i₂, qN]; omega) (by rw [p₂]; omega) ?_ ?_ ?_ fun s₃ g₃ => ?_ + · rw [b₂, add0, rw₂] + exact Covers.of_sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨stR s₀, by simp, 0, by simp, by simp⟩ + · rw [i₂, add0, show (Dp s₀ + BitVec.ofNat 32 (16 * k)).setWidth 64 = addr (Dp s₀) (16 * k) from rfl, + hp.dataA hk, rw₂] + exact Covers.of_sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨dataR s₀, by simp, 16 * k, rfl, by simp; omega⟩ + · rw [p₂, w₂] + exact Covers.of_sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨scrR s₀, by simp, 2048, rfl, by simp⟩ + have b₃ : s₃.gpr .ebx = St s₀ := by rw [g₃.gpr _ (by decide) (by decide), b₂] + refine zero4_ok (by decide) (by rw [b₃]; omega) ?_ fun s₄ g₄ m₄ rd₄ wr₄ => ?_ + · rw [b₃, add0, g₃.wr, w₂] + exact Covers.of_sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨stR s₀, by simp, 0, by simp, by simp⟩ + have esp₄ : s₄.gpr .esp = E s₀ := by + rw [g₄ _ (by decide), g₃.gpr _ (by decide) (by decide), u₂.other _ (by decide), u₁.other _ (by decide), h.esp] + have rd₄' : s₄.rd = s.rd := by rw [rd₄, g₃.rd, u₂.rd, u₁.rd] + have wr₄' : s₄.wr = s.wr := by rw [wr₄, g₃.wr, u₂.wr, u₁.wr] + have mem₄ : s₄.mem = Proof.Cmac.chainMem4 s.mem ((S s₀).setWidth 64 + BitVec.ofNat 64 2048) + ((St s₀).setWidth 64) ((Dp s₀).setWidth 64 + BitVec.ofNat 64 (16 * k)) := by + rw [m₄, b₃, add0, g₃.mem, p₂, b₂, i₂, add0, add0, + show (Dp s₀ + BitVec.ofNat 32 (16 * k)).setWidth 64 = addr (Dp s₀) (16 * k) from rfl, hp.dataA hk, + u₂.mem, u₁.mem] + rfl + have hargs₄ : ∀ i < 6, s₄.mem.readW (argAddr s₀ i) 32 = arg s₀ i := by + intro i hi + rw [mem₄] + refine (Proof.Cmac.chainMem4_frame _ _ _ _).readW (Region.contains_self _ _) (fun r hr => ?_) (by decide) |>.trans + (hargs i hi) + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl + · exact (hp.args_scr.sub_left (hp.arg_sub hi)).sub_right (UPre.scr_sub (by decide)) + · exact hp.args_st.sub_left (hp.arg_sub hi) + rw [ctrArgs_eq] + refine wp_arg (s₀ := s₀) esp₄ (by rw [rd₄', wr₄', hrw]; exact hp.arg_in (by decide)) (hargs₄ 0 (by decide)) + fun s₅ u₅ => ?_ + refine wp_arg (s₀ := s₀) (by rw [u₅.other _ (by decide), esp₄]) + (by rw [u₅.rd, u₅.wr, rd₄', wr₄', hrw]; exact hp.arg_in (by decide)) + (by rw [u₅.mem]; exact hargs₄ 1 (by decide)) fun s₆ u₆ => ?_ + refine wp_mov fun s₇ u₇ => wp_addi fun s₈ u₈ => wp_movi fun s₉ u₉ => WP.block_nil ?_ + have keep : ∀ r, r ≠ .eax → r ≠ .ecx → r ≠ .edx → r ≠ .edi → s₉.gpr r = s₄.gpr r := fun r ha hc hd hi => by + rw [u₉.other _ hi, u₈.other _ hd, u₇.other _ hd, u₆.other _ hc, u₅.other _ ha] + have p₄ : s₄.gpr .ebp = S s₀ := by rw [g₄ _ (by decide), g₃.gpr _ (by decide) (by decide), p₂] + have b₄ : s₄.gpr .ebx = St s₀ := by rw [g₄ _ (by decide), b₃] + have sp₉ : s₉.gpr .esp = E s₀ := by rw [keep _ (by decide) (by decide) (by decide) (by decide), esp₄] + have rd₉ : s₉.rd = s.rd := by rw [u₉.rd, u₈.rd, u₇.rd, u₆.rd, u₅.rd, rd₄'] + have wr₉ : s₉.wr = s.wr := by rw [u₉.wr, u₈.wr, u₇.wr, u₆.wr, u₅.wr, wr₄'] + have mem₉ : s₉.mem = s₄.mem := by rw [u₉.mem, u₈.mem, u₇.mem, u₆.mem, u₅.mem] + have hb : below (s₉.gpr .esp) 28 = stkR s₀ := by rw [sp₉]; exact hp.below_eq + have cA : (Cb s₀).setWidth 64 = (S s₀).setWidth 64 + BitVec.ofNat 64 2048 := hp.scrA (by decide) + have cSt : (⟨(Cb s₀).setWidth 64, 16⟩ : Region).Disjoint (stR s₀) := by + rw [cA]; exact hp.st_scr.symm.sub_left (UPre.scr_sub (by decide)) + refine ⟨⟨?_, ?_, ?_, ?_, u₉.gpr, ?_, hp.rounds, by rw [sp₉]; exact hp.esp28, ?_, hp.sch_st, ?_, cSt, + ?_, ?_, by rw [hb]; exact hp.b_sch, ?_, by rw [hb]; exact hp.b_st, ?_, hp.sch_fit, ?_, hp.st_fit, ?_, ?_, ?_, + ?_⟩, ?_, ?_, ?_, ?_, ?_⟩ + · rw [u₉.other _ (by decide), u₈.other _ (by decide), u₇.other _ (by decide), u₆.other _ (by decide), u₅.gpr] + · rw [u₉.other _ (by decide), u₈.other _ (by decide), u₇.other _ (by decide), u₆.gpr]; exact arg_ofNat s₀ 1 + · rw [u₉.other _ (by decide), u₈.gpr, u₇.gpr, u₆.other _ (by decide), u₅.other _ (by decide), p₄] + · rw [keep _ (by decide) (by decide) (by decide) (by decide), b₄] + · rw [keep _ (by decide) (by decide) (by decide) (by decide), p₄] + · rw [cA]; exact hp.sch_scr.sub_right (UPre.scr_sub (by decide)) + · exact hp.sch_scr.sub_right (Region.sub_prefix (by decide)) + · rw [cA]; exact Offset.disjoint_base _ (by decide) (by omega) + · exact hp.st_scr.sub_right (Region.sub_prefix (by decide)) + · rw [hb, cA]; exact hp.b_scr.sub_right (UPre.scr_sub (by decide)) + · rw [hb]; exact hp.b_scr.sub_right (Region.sub_prefix (by decide)) + · rw [hp.scrN (by decide)]; omega + · omega + · rw [rd₉, wr₉, hRegs] + exact Covers.of_sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact ⟨schR s₀, by simp, 0, by simp, by simp⟩ + · rw [wr₉, hW, cA] + refine Covers.of_sub fun r hr => ?_ + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact ⟨scrR s₀, by simp, 2048, rfl, by simp⟩ + · exact ⟨stR s₀, by simp, 0, by simp, by simp⟩ + · exact ⟨scrR s₀, by simp, 0, by simp, by simp⟩ + · rw [mem₉, mem₄]; exact Proof.Cmac.chainMem4_state _ _ _ _ + · rw [keep _ (by decide) (by decide) (by decide) (by decide), g₄ _ (by decide), g₃.gpr _ (by decide) (by decide), + u₂.other _ (by decide), u₁.other _ (by decide)] + · rw [sp₉, h.esp] + · rw [mem₉, mem₄] + · exact rd₉ + · exact wr₉ + +theorem body_ok {s₀ : State} (hp : UPre s₀) {k : Nat} (hk : k < N s₀) {s : State} (h : LInv s₀ k s) : + WP isa body s fun s' => LInv s₀ (k + 1) s' ∧ s'.zf = some (decide (k + 1 = N s₀)) := by + have hdf := hp.data_fit + refine WP.seq (WP.mono (bodyA_wp hp hk h) fun s₁ a => ?_) + refine WP.seq (WP.mono (ctr_call a.pre) fun s₂ h₂ => ?_) + have esp₁ : s₁.gpr .esp = E s₀ := by rw [a.esp, h.esp] + have hb : below (s₁.gpr .esp) 28 = stkR s₀ := by rw [esp₁]; exact hp.below_eq + have cA : (Cb s₀).setWidth 64 = (S s₀).setWidth 64 + BitVec.ofNat 64 2048 := hp.scrA (by decide) + have f₁ : Frame [⟨(S s₀).setWidth 64 + BitVec.ofNat 64 2048, 16⟩, stR s₀] s.mem s₁.mem := by + rw [a.mem]; exact Proof.Cmac.chainMem4_frame _ _ _ _ + have f₂ : Frame [stR s₀, ⟨(S s₀).setWidth 64, 2064⟩, stkR s₀] s₁.mem s₂.mem := by + have fr := h₂.frame + rw [hb, cA] at fr + exact fr.sub fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · exact ⟨⟨(S s₀).setWidth 64, 2064⟩, by simp, Offset.sub_base _ (by decide)⟩ + · exact ⟨stR s₀, by simp, fun _ h => h⟩ + · exact ⟨⟨(S s₀).setWidth 64, 2064⟩, by simp, Region.sub_prefix (by decide)⟩ + · exact ⟨stkR s₀, by simp, fun _ h => h⟩ + have f₁' : Frame [stR s₀, ⟨(S s₀).setWidth 64, 2064⟩, stkR s₀] s.mem s₁.mem := f₁.sub fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl + · exact ⟨⟨(S s₀).setWidth 64, 2064⟩, by simp, Offset.sub_base _ (by decide)⟩ + · exact ⟨stR s₀, by simp, fun _ h => h⟩ + have fr₂ : Frame [stR s₀, ⟨(S s₀).setWidth 64, 2064⟩, stkR s₀] (savedMem s₀) s₂.mem := + (h.frame.trans f₁').trans f₂ + have big₂ := UPre.big_of fr₂ + have big₁ := UPre.big_of (h.frame.trans f₁') + have esi₂ : s₂.gpr .esi = Dp s₀ + BitVec.ofNat 32 (16 * k) := by + rw [h₂.saved .esi (by simp [calleeSaved]), a.esi, h.esi] + have esp₂ : s₂.gpr .esp = E s₀ := by rw [h₂.saved .esp (by simp [calleeSaved]), esp₁] + have rw₂ : s₂.rd ++ s₂.wr = s₀.rd ++ s₀.wr := by rw [h₂.rd, h₂.wr, a.rd, a.wr, h.rd, h.wr] + refine WP.mono (advance_wp hp hk esi₂ esp₂ (fun i hi => hp.arg_keep big₂ hi) rw₂) fun s₃ ⟨esi₃, esp₃, _, mem₃, + rd₃, wr₃, zf₃⟩ => ⟨⟨esi₃, esp₃, by rw [rd₃, h₂.rd, a.rd, h.rd], by rw [wr₃, h₂.wr, a.wr, h.wr], + by rw [mem₃]; exact fr₂, ?_⟩, zf₃⟩ + have cst : (⟨(S s₀).setWidth 64 + BitVec.ofNat 64 2048, 16⟩ : Region).Disjoint (stR s₀) := + hp.st_scr.symm.sub_left (UPre.scr_sub (by decide)) + have cq : (⟨(S s₀).setWidth 64 + BitVec.ofNat 64 2048, 16⟩ : Region).Disjoint + ⟨(Dp s₀).setWidth 64 + BitVec.ofNat 64 (16 * k), 16⟩ := + (hp.data_scr.symm.sub_left (UPre.scr_sub (by decide))).sub_right (UPre.data_sub hk) + have out := h₂.out + rw [UPre.sched_bytes hp big₁, cA, a.mem, Proof.Cmac.chainMem4_counter _ cst cq, h.state, + UPre.block_bytes hp (UPre.big_of h.frame) hk] at out + rw [mem₃, out, take_succ_blks s₀ hk, Proof.Cmac.chain_append, Proof.Cmac.chain_single] + +theorem loop_ok {s₀ : State} (hp : UPre s₀) {k : Nat} (hk : k < N s₀) {s : State} (h : LInv s₀ k s) : + WP isa (.loop body .ne) s (LInv s₀ (N s₀)) := by + refine WP.loop (M := isa) (body := body) (c := .ne) (Q := LInv s₀ (N s₀)) + (fun (n : Nat) (t : State) => ∃ j, n = N s₀ - j ∧ j < N s₀ ∧ LInv s₀ j t) ?_ (N s₀ - k) s + ⟨k, rfl, hk, h⟩ + rintro n s ⟨k, rfl, hk, h⟩ + refine WP.mono (body_ok hp hk h) fun s' ⟨h', hz⟩ => ?_ + have ev : isa.eval .ne s' = some !decide (k + 1 = N s₀) := by + show VG.X86.eval .ne s' = _; rw [eval_ne, hz]; rfl + by_cases hz' : k + 1 = N s₀ + · left + refine ⟨by rw [ev]; simp [hz'], ?_⟩ + rwa [← hz'] + · right + refine ⟨by rw [ev]; simp [hz'], N s₀ - (k + 1), by omega, k + 1, rfl, by omega, h'⟩ + +end VG.Proof.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/Verified.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/Verified.lean new file mode 100644 index 000000000..019152f63 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/Verified.lean @@ -0,0 +1,89 @@ +import VerifiedGarbage.Proof.CmacAes.X86.UpdateCT +import VerifiedGarbage.Proof.CmacAes.X86.SubkeysCT +import VerifiedGarbage.Proof.CmacAes.X86.FinalizeCT +import VerifiedGarbage.Proof.Framework.Contract +import VerifiedGarbage.Spec.Cmac.Contract + +/-! +# AES-CMAC on x86: `Verified` + +Untrusted: everything here is checked by Lean. Correctness and constant +time, a state satisfying each precondition, and the shared contracts of +`Spec/Cmac/Contract.lean`, with 28 bytes of stack: each call of +`vg_aes_ctr32` pushes its six arguments and the return address. +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 VG.Impl.CmacAes.X86 + +/-- A state satisfying `vg_cmac_aes_subkeys`'s precondition: the schedule +at `0x1000`, 10 rounds, the subkeys at `0x2000` and the scratch buffer at +`0x4000`, as stack arguments at `0x8004`. -/ +def subSat : State where + gpr r := match r with | .esp => 0x8000 | _ => 0 + cf := none + zf := none + sf := none + of := none + mem a := if a = 0x8005 then 0x10 else if a = 0x8008 then 10 + else if a = 0x800d then 0x20 else if a = 0x8011 then 0x40 else 0 + rd := [⟨0x1000, 240⟩, ⟨0x8004, 16⟩] + wr := [⟨0x2000, 32⟩, ⟨0x4000, 2176⟩] + +theorem subkeys_verified : Verified X86.target subkeys (Spec.Cmac.aesSubkeysContract X86.abi 28) := + Verified.of_correct (fun _ hs => subkeys_wp hs) subkeys_ct (by + have a0 : arg subSat 0 = 0x1000 := by decide + have a1 : arg subSat 1 = 10 := by decide + have a2 : arg subSat 2 = 0x2000 := by decide + have a3 : arg subSat 3 = 0x4000 := by decide + have e : argAddr subSat 0 = 0x8004 := by decide + have esp : subSat.gpr .esp = 0x8000 := rfl + sig_implies [Spec.Cmac.aesSubkeysContract, Spec.Cmac.aesSubkeysSig, X86.abi, X86.argSlots, + X86.argVal, X86.argBytes, subkeysX86] [a0, a1, a2, a3, e, esp] using subSat) + +/-- A state satisfying `vg_cmac_aes_finalize`'s precondition: the key at +`0x1000`, 10 rounds, the state at `0x2000`, no last bytes at `0x3000` and +the scratch buffer at `0x4000`, as stack arguments at `0x8004`. -/ +def finSat : State where + gpr r := match r with | .esp => 0x8000 | _ => 0 + cf := none + zf := none + sf := none + of := none + mem a := if a = 0x8005 then 0x10 else if a = 0x8008 then 10 + else if a = 0x800d then 0x20 else if a = 0x8011 then 0x30 else if a = 0x8019 then 0x40 else 0 + rd := [⟨0x1000, 272⟩, ⟨0x3000, 0⟩, ⟨0x8004, 24⟩] + wr := [⟨0x2000, 16⟩, ⟨0x4000, 2176⟩] + +theorem finalize_verified : Verified X86.target finalize (Spec.Cmac.aesFinalizeContract X86.abi 28) := + Verified.of_correct (fun _ hs => finalize_wp hs) finalize_ct (by + have a0 : arg finSat 0 = 0x1000 := by decide + have a1 : arg finSat 1 = 10 := by decide + have a2 : arg finSat 2 = 0x2000 := by decide + have a3 : arg finSat 3 = 0x3000 := by decide + have a4 : arg finSat 4 = 0 := by decide + have a5 : arg finSat 5 = 0x4000 := by decide + have e : argAddr finSat 0 = 0x8004 := by decide + have esp : finSat.gpr .esp = 0x8000 := rfl + sig_implies [Spec.Cmac.aesFinalizeContract, Spec.Cmac.aesFinalizeSig, X86.abi, X86.argSlots, + X86.argVal, X86.argBytes, finalizeX86] [a0, a1, a2, a3, a4, a5, e, esp] using finSat) + +/-- A state satisfying `vg_cmac_aes_update`'s precondition: as `finSat`, +with no blocks. -/ +def updSat : State := { finSat with rd := [⟨0x1000, 240⟩, ⟨0x3000, 0⟩, ⟨0x8004, 24⟩] } + +theorem update_verified : Verified X86.target update (Spec.Cmac.aesUpdateContract X86.abi 28) := + Verified.of_correct (fun _ hs => update_wp hs) update_ct (by + have a0 : arg updSat 0 = 0x1000 := by decide + have a1 : arg updSat 1 = 10 := by decide + have a2 : arg updSat 2 = 0x2000 := by decide + have a3 : arg updSat 3 = 0x3000 := by decide + have a4 : arg updSat 4 = 0 := by decide + have a5 : arg updSat 5 = 0x4000 := by decide + have e : argAddr updSat 0 = 0x8004 := by decide + have esp : updSat.gpr .esp = 0x8000 := rfl + sig_implies [Spec.Cmac.aesUpdateContract, Spec.Cmac.aesUpdateSig, X86.abi, X86.argSlots, + X86.argVal, X86.argBytes, updateX86] [a0, a1, a2, a3, a4, a5, e, esp] using updSat) + +end VG.Proof.CmacAes.X86 diff --git a/lean/VerifiedGarbage/Proof/CmacAes/X86/Words.lean b/lean/VerifiedGarbage/Proof/CmacAes/X86/Words.lean new file mode 100644 index 000000000..9b33b7600 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/CmacAes/X86/Words.lean @@ -0,0 +1,162 @@ +import VerifiedGarbage.Proof.CmacAes.X86.Contract +import VerifiedGarbage.Proof.Cmac.Block32 +import VerifiedGarbage.Proof.MdStream.X86.Common + +/-! +# AES-CMAC on x86: blocks formed a word at a time + +Untrusted: everything here is checked by Lean. Weakest preconditions of the +instruction sequences the functions build blocks with: the XOR of the blocks +at `pb + pd` and `qb + qd` stored at `cb + cd` through `eax` and `ecx` +(`xor4`, which leaves `Cmac.xor4Mem`), and four stores of a zeroed `eax` +(`zero4`, which leaves `Cmac.zero4`). +-/ + +namespace VG.Proof.CmacAes.X86 + +open VG VG.X86 VG.Impl.CmacAes.X86 +open VG.Proof.MdStream.X86 (Upd Mupd WP.cons wp_movm wp_movi wp_store) + +/-- The `xor4` instructions, written out. -/ +def xorBlk (pb qb cb : Reg) (pd qd cd : Nat) : List Instr := + [.mov .eax (.mem (at_ pb pd)), .mov .ecx (.mem (at_ qb qd)), .alu .xor .eax (.reg .ecx), .store (at_ cb cd) .eax, + .mov .eax (.mem (at_ pb (pd + 4))), .mov .ecx (.mem (at_ qb (qd + 4))), .alu .xor .eax (.reg .ecx), + .store (at_ cb (cd + 4)) .eax, + .mov .eax (.mem (at_ pb (pd + 8))), .mov .ecx (.mem (at_ qb (qd + 8))), .alu .xor .eax (.reg .ecx), + .store (at_ cb (cd + 8)) .eax, + .mov .eax (.mem (at_ pb (pd + 12))), .mov .ecx (.mem (at_ qb (qd + 12))), .alu .xor .eax (.reg .ecx), + .store (at_ cb (cd + 12)) .eax] + +theorem xor4_eq (pb qb cb : Reg) (pd qd cd : Nat) : xor4 pb qb cb pd qd cd = xorBlk pb qb cb pd qd cd := rfl + +theorem zero4_eq (b : Reg) (d : Nat) : zero4 b d = + [.mov .eax (.imm 0), .store (at_ b d) .eax, .store (at_ b (d + 4)) .eax, .store (at_ b (d + 8)) .eax, + .store (at_ b (d + 12)) .eax] := rfl + +/-- `s'` is `s` with memory `m`, and `eax` and `ecx` (and the flags) clobbered. -/ +structure Step (s s' : State) (m : Mem) : Prop where + gpr : ∀ r, r ≠ .eax → r ≠ .ecx → s'.gpr r = s.gpr r + mem : s'.mem = m + rd : s'.rd = s.rd + wr : s'.wr = s.wr + +theorem wp_xor {is : List Instr} {s : State} {Q : State → Prop} {d r : Reg} + (k : ∀ s', Upd s s' d (s.gpr d ^^^ s.gpr r) → WP isa (.block is) s' Q) : + WP isa (.block (.alu .xor d (.reg r) :: is)) s Q := + WP.cons rfl (k _ (MdStream.X86.Upd.flags _ _ _ _ _ _)) + +theorem ea_at' (s : State) (b : Reg) (d : Nat) : s.ea (at_ b d) = addr (s.gpr b) d := rfl + +/-- One word. -/ +theorem xw_ok {pb qb cb : Reg} {pd qd cd : Nat} {is : List Instr} {s : State} {Q : State → Prop} + {P Q' C : Addr} (hq : qb ≠ .eax) (hc₁ : cb ≠ .eax) (hc₂ : cb ≠ .ecx) + (hP : addr (s.gpr pb) pd = P) (hQ : addr (s.gpr qb) qd = Q') (hC : addr (s.gpr cb) cd = C) + (rP : InRegions (s.rd ++ s.wr) P 4) (rQ : InRegions (s.rd ++ s.wr) Q' 4) (wC : InRegions s.wr C 4) + (k : ∀ s', Step s s' (s.mem.writeW C (s.mem.readW P 32 ^^^ s.mem.readW Q' 32)) → WP isa (.block is) s' Q) : + WP isa (.block (.mov .eax (.mem (at_ pb pd)) :: .mov .ecx (.mem (at_ qb qd)) :: .alu .xor .eax (.reg .ecx) :: + .store (at_ cb cd) .eax :: is)) s Q := by + subst hP hQ hC + refine wp_movm (ea_at' _ _ _) rP fun s₁ u₁ => ?_ + refine wp_movm (by rw [ea_at', u₁.other _ hq]) (by rw [u₁.rd, u₁.wr]; exact rQ) fun s₂ u₂ => ?_ + refine wp_xor fun s₃ u₃ => ?_ + refine wp_store (by rw [ea_at', u₃.other _ hc₁, u₂.other _ hc₂, u₁.other _ hc₁]) + (by rw [u₃.wr, u₂.wr, u₁.wr]; exact wC) fun s₄ u₄ => k s₄ ⟨fun r h₁ h₂ => ?_, ?_, ?_, ?_⟩ + · rw [u₄.gpr, u₃.other _ h₁, u₂.other _ h₂, u₁.other _ h₁] + · rw [u₄.mem, u₃.gpr, u₂.other _ (by decide), u₂.gpr, u₁.gpr, u₃.mem, u₂.mem, u₁.mem] + · rw [u₄.rd, u₃.rd, u₂.rd, u₁.rd] + · rw [u₄.wr, u₃.wr, u₂.wr, u₁.wr] + +/-- Word `i` of a block that does not wrap the 32-bit space. -/ +theorem addr_word {b : BitVec 32} {d : Nat} (i : Nat) (h : b.toNat + d + 16 ≤ 2 ^ 32) (hi : i ≤ 12) : + addr b (d + i) = b.setWidth 64 + BitVec.ofNat 64 d + BitVec.ofNat 64 i := by + rw [addr_eq (by omega), Offset.add_add] + +theorem in_word {rs : List Region} {P : Addr} (h : Covers [⟨P, 16⟩] rs) {i : Nat} (hi : i ≤ 12) : + InRegions rs (P + BitVec.ofNat 64 i) 4 := + h _ _ ⟨_, List.mem_singleton_self _, Offset.contains_base P (by omega) (by omega)⟩ + +theorem in_word0 {rs : List Region} {P : Addr} (h : Covers [⟨P, 16⟩] rs) : InRegions rs P 4 := by + have c := Offset.contains_base P (d := 0) (n := 4) (k := 16) (by decide) (by decide) + rw [show P + BitVec.ofNat 64 0 = P from BitVec.add_zero P] at c + exact h _ _ ⟨_, List.mem_singleton_self _, c⟩ + +/-- The XOR of the blocks at `pb + pd` and `qb + qd`, stored at `cb + cd`. -/ +theorem xor4_ok {pb qb cb : Reg} {pd qd cd : Nat} {is : List Instr} {s : State} {Q : State → Prop} + (hp₁ : pb ≠ .eax) (hp₂ : pb ≠ .ecx) (hq₁ : qb ≠ .eax) (hq₂ : qb ≠ .ecx) (hc₁ : cb ≠ .eax) + (hc₂ : cb ≠ .ecx) + (fp : (s.gpr pb).toNat + pd + 16 ≤ 2 ^ 32) (fq : (s.gpr qb).toNat + qd + 16 ≤ 2 ^ 32) + (fc : (s.gpr cb).toNat + cd + 16 ≤ 2 ^ 32) + (rP : Covers [⟨(s.gpr pb).setWidth 64 + BitVec.ofNat 64 pd, 16⟩] (s.rd ++ s.wr)) + (rQ : Covers [⟨(s.gpr qb).setWidth 64 + BitVec.ofNat 64 qd, 16⟩] (s.rd ++ s.wr)) + (wC : Covers [⟨(s.gpr cb).setWidth 64 + BitVec.ofNat 64 cd, 16⟩] s.wr) + (k : ∀ s', Step s s' (Proof.Cmac.xor4Mem s.mem ((s.gpr cb).setWidth 64 + BitVec.ofNat 64 cd) + ((s.gpr pb).setWidth 64 + BitVec.ofNat 64 pd) ((s.gpr qb).setWidth 64 + BitVec.ofNat 64 qd)) → + WP isa (.block is) s' Q) : + WP isa (.block (xor4 pb qb cb pd qd cd ++ is)) s Q := by + rw [xor4_eq] + simp only [xorBlk, List.cons_append, List.nil_append] + refine xw_ok hq₁ hc₁ hc₂ (addr_eq (by omega)) (addr_eq (by omega)) (addr_eq (by omega)) + (in_word0 rP) (in_word0 rQ) (in_word0 wC) fun s₁ g₁ => ?_ + have e₁ : ∀ r, r ≠ .eax → r ≠ .ecx → s₁.gpr r = s.gpr r := g₁.gpr + refine xw_ok (P := (s.gpr pb).setWidth 64 + BitVec.ofNat 64 pd + BitVec.ofNat 64 4) + (Q' := (s.gpr qb).setWidth 64 + BitVec.ofNat 64 qd + BitVec.ofNat 64 4) + (C := (s.gpr cb).setWidth 64 + BitVec.ofNat 64 cd + BitVec.ofNat 64 4) hq₁ hc₁ hc₂ + (by rw [e₁ _ hp₁ hp₂]; exact addr_word 4 fp (by decide)) + (by rw [e₁ _ hq₁ hq₂]; exact addr_word 4 fq (by decide)) + (by rw [e₁ _ hc₁ hc₂]; exact addr_word 4 fc (by decide)) + (by rw [g₁.rd, g₁.wr]; exact in_word rP (by decide)) (by rw [g₁.rd, g₁.wr]; exact in_word rQ (by decide)) + (by rw [g₁.wr]; exact in_word wC (by decide)) fun s₂ g₂ => ?_ + have e₂ : ∀ r, r ≠ .eax → r ≠ .ecx → s₂.gpr r = s.gpr r := fun r h₁ h₂ => by rw [g₂.gpr r h₁ h₂, e₁ r h₁ h₂] + refine xw_ok (P := (s.gpr pb).setWidth 64 + BitVec.ofNat 64 pd + BitVec.ofNat 64 8) + (Q' := (s.gpr qb).setWidth 64 + BitVec.ofNat 64 qd + BitVec.ofNat 64 8) + (C := (s.gpr cb).setWidth 64 + BitVec.ofNat 64 cd + BitVec.ofNat 64 8) hq₁ hc₁ hc₂ + (by rw [e₂ _ hp₁ hp₂]; exact addr_word 8 fp (by decide)) + (by rw [e₂ _ hq₁ hq₂]; exact addr_word 8 fq (by decide)) + (by rw [e₂ _ hc₁ hc₂]; exact addr_word 8 fc (by decide)) + (by rw [g₂.rd, g₂.wr, g₁.rd, g₁.wr]; exact in_word rP (by decide)) + (by rw [g₂.rd, g₂.wr, g₁.rd, g₁.wr]; exact in_word rQ (by decide)) + (by rw [g₂.wr, g₁.wr]; exact in_word wC (by decide)) fun s₃ g₃ => ?_ + have e₃ : ∀ r, r ≠ .eax → r ≠ .ecx → s₃.gpr r = s.gpr r := fun r h₁ h₂ => by rw [g₃.gpr r h₁ h₂, e₂ r h₁ h₂] + refine xw_ok (P := (s.gpr pb).setWidth 64 + BitVec.ofNat 64 pd + BitVec.ofNat 64 12) + (Q' := (s.gpr qb).setWidth 64 + BitVec.ofNat 64 qd + BitVec.ofNat 64 12) + (C := (s.gpr cb).setWidth 64 + BitVec.ofNat 64 cd + BitVec.ofNat 64 12) hq₁ hc₁ hc₂ + (by rw [e₃ _ hp₁ hp₂]; exact addr_word 12 fp (by decide)) + (by rw [e₃ _ hq₁ hq₂]; exact addr_word 12 fq (by decide)) + (by rw [e₃ _ hc₁ hc₂]; exact addr_word 12 fc (by decide)) + (by rw [g₃.rd, g₃.wr, g₂.rd, g₂.wr, g₁.rd, g₁.wr]; exact in_word rP (by decide)) + (by rw [g₃.rd, g₃.wr, g₂.rd, g₂.wr, g₁.rd, g₁.wr]; exact in_word rQ (by decide)) + (by rw [g₃.wr, g₂.wr, g₁.wr]; exact in_word wC (by decide)) fun s₄ g₄ => k s₄ ⟨?_, ?_, ?_, ?_⟩ + · intro r h₁ h₂; rw [g₄.gpr r h₁ h₂, e₃ r h₁ h₂] + · rw [g₄.mem, g₃.mem, g₂.mem, g₁.mem]; rfl + · rw [g₄.rd, g₃.rd, g₂.rd, g₁.rd] + · rw [g₄.wr, g₃.wr, g₂.wr, g₁.wr] + +/-- The block at `b + d` zeroed (`b` not `eax`). -/ +theorem zero4_ok {b : Reg} {d : Nat} {is : List Instr} {s : State} {Q : State → Prop} (hb : b ≠ .eax) + (fb : (s.gpr b).toNat + d + 16 ≤ 2 ^ 32) + (wB : Covers [⟨(s.gpr b).setWidth 64 + BitVec.ofNat 64 d, 16⟩] s.wr) + (k : ∀ s', (∀ r, r ≠ .eax → s'.gpr r = s.gpr r) → + s'.mem = Proof.Cmac.zero4 s.mem ((s.gpr b).setWidth 64 + BitVec.ofNat 64 d) → + s'.rd = s.rd → s'.wr = s.wr → WP isa (.block is) s' Q) : + WP isa (.block (zero4 b d ++ is)) s Q := by + rw [zero4_eq] + simp only [List.cons_append, List.nil_append] + refine wp_movi fun s₀ u₀ => ?_ + have b₀ : s₀.gpr b = s.gpr b := u₀.other _ hb + refine wp_store (a := (s.gpr b).setWidth 64 + BitVec.ofNat 64 d) (by rw [ea_at', b₀]; exact addr_eq (by omega)) + (by rw [u₀.wr]; exact in_word0 wB) fun s₁ u₁ => ?_ + refine wp_store (a := (s.gpr b).setWidth 64 + BitVec.ofNat 64 d + BitVec.ofNat 64 4) + (by rw [ea_at', u₁.gpr, b₀]; exact addr_word 4 fb (by decide)) + (by rw [u₁.wr, u₀.wr]; exact in_word wB (by decide)) fun s₂ u₂ => ?_ + refine wp_store (a := (s.gpr b).setWidth 64 + BitVec.ofNat 64 d + BitVec.ofNat 64 8) + (by rw [ea_at', u₂.gpr, u₁.gpr, b₀]; exact addr_word 8 fb (by decide)) + (by rw [u₂.wr, u₁.wr, u₀.wr]; exact in_word wB (by decide)) fun s₃ u₃ => ?_ + refine wp_store (a := (s.gpr b).setWidth 64 + BitVec.ofNat 64 d + BitVec.ofNat 64 12) + (by rw [ea_at', u₃.gpr, u₂.gpr, u₁.gpr, b₀]; exact addr_word 12 fb (by decide)) + (by rw [u₃.wr, u₂.wr, u₁.wr, u₀.wr]; exact in_word wB (by decide)) fun s₄ u₄ => k s₄ ?_ ?_ ?_ ?_ + · intro r hr; rw [u₄.gpr, u₃.gpr, u₂.gpr, u₁.gpr, u₀.other _ hr] + · rw [u₄.mem, u₃.mem, u₂.mem, u₁.mem, u₃.gpr, u₂.gpr, u₁.gpr, u₀.gpr, u₀.mem]; rfl + · rw [u₄.rd, u₃.rd, u₂.rd, u₁.rd, u₀.rd] + · rw [u₄.wr, u₃.wr, u₂.wr, u₁.wr, u₀.wr] + +end VG.Proof.CmacAes.X86 diff --git a/src/asm/x86/cmac_aes.rs b/src/asm/x86/cmac_aes.rs new file mode 100644 index 000000000..d0f93448d --- /dev/null +++ b/src/asm/x86/cmac_aes.rs @@ -0,0 +1,368 @@ +// @generated from lean/VerifiedGarbage/Artifacts.lean by lean/Emit.lean. DO NOT EDIT. +//! Verified `cmac_aes` functions for `x86`. +#![allow(dead_code)] + +/// The CMAC subkey generation (NIST SP 800-38B §6.1) for AES: writes `K1 ‖ K2` to `*subkeys`, where `L = CIPH_K(0¹²⁸)`, `K1 = L << 1` (XORed with `R₁₂₈ = 0¹²⁰10000111` if the leftmost bit of `L` is 1) and `K2` is `K1` doubled the same way. `CIPH_K` is AES (FIPS 197) with `rounds` rounds and the key schedule in the first `16 * (rounds + 1)` bytes of `*schedule`, as `vg_aes_expand_key` writes it. +/// +/// Contract: `VG.Spec.Cmac.aesSubkeysContract`. Constant time: only the pointers and `rounds` may affect timing, not the key schedule or the subkeys. +/// +/// This implementation encrypts each block with `vg_aes_ctr32`. +/// +/// # Safety +/// +/// * `schedule` must be valid for reads of 240 bytes. +/// * `subkeys` must be valid for reads and writes of 32 bytes. +/// * `scratch` must be valid for reads and writes of 2176 bytes. +/// * `rounds` must be 10, 12 or 14. +/// * The contents of `scratch` on return are unspecified. +/// * `subkeys` and `scratch` must not overlap each other, `schedule` or the arguments on the stack (distinct Rust objects never do). +/// * None of `schedule`, `subkeys` and `scratch` may overlap the return address on the stack or the 28 bytes of stack below it, or wrap around the end of the address space (no Rust object does). +#[unsafe(naked)] +pub(crate) unsafe extern "C" fn vg_cmac_aes_subkeys(schedule: *const [u8; 240], rounds: usize, subkeys: *mut [u8; 32], scratch: *mut [u64; 272]) { + core::arch::naked_asm!( + "mov eax, DWORD PTR [esp+16]", + "mov DWORD PTR [eax+2064], ebx", + "mov DWORD PTR [eax+2068], esi", + "mov DWORD PTR [eax+2072], edi", + "mov DWORD PTR [eax+2076], ebp", + "mov ebp, eax", + "mov ebx, DWORD PTR [esp+12]", + "mov eax, 0", + "mov DWORD PTR [ebp+2048], eax", + "mov DWORD PTR [ebp+2052], eax", + "mov DWORD PTR [ebp+2056], eax", + "mov DWORD PTR [ebp+2060], eax", + "mov eax, 0", + "mov DWORD PTR [ebx], eax", + "mov DWORD PTR [ebx+4], eax", + "mov DWORD PTR [ebx+8], eax", + "mov DWORD PTR [ebx+12], eax", + "mov eax, DWORD PTR [esp+4]", + "mov ecx, DWORD PTR [esp+8]", + "mov edx, ebp", + "add edx, 2048", + "mov edi, 1", + "push ebp", + "push edi", + "push ebx", + "push edx", + "push ecx", + "push eax", + "call {vg_aes_ctr32}", + "pop eax", + "pop eax", + "pop eax", + "pop eax", + "pop eax", + "pop eax", + "mov eax, DWORD PTR [ebx]", + "mov ecx, DWORD PTR [ebx+4]", + "mov edx, DWORD PTR [ebx+8]", + "mov esi, DWORD PTR [ebx+12]", + "bswap eax", + "bswap ecx", + "bswap edx", + "bswap esi", + "mov edi, eax", + "shr edi, 31", + "mov ebp, 0", + "sub ebp, edi", + "and ebp, 135", + "add eax, eax", + "mov edi, ecx", + "shr edi, 31", + "or eax, edi", + "add ecx, ecx", + "mov edi, edx", + "shr edi, 31", + "or ecx, edi", + "add edx, edx", + "mov edi, esi", + "shr edi, 31", + "or edx, edi", + "add esi, esi", + "xor esi, ebp", + "bswap eax", + "bswap ecx", + "bswap edx", + "bswap esi", + "mov DWORD PTR [ebx], eax", + "mov DWORD PTR [ebx+4], ecx", + "mov DWORD PTR [ebx+8], edx", + "mov DWORD PTR [ebx+12], esi", + "mov eax, DWORD PTR [ebx]", + "mov ecx, DWORD PTR [ebx+4]", + "mov edx, DWORD PTR [ebx+8]", + "mov esi, DWORD PTR [ebx+12]", + "bswap eax", + "bswap ecx", + "bswap edx", + "bswap esi", + "mov edi, eax", + "shr edi, 31", + "mov ebp, 0", + "sub ebp, edi", + "and ebp, 135", + "add eax, eax", + "mov edi, ecx", + "shr edi, 31", + "or eax, edi", + "add ecx, ecx", + "mov edi, edx", + "shr edi, 31", + "or ecx, edi", + "add edx, edx", + "mov edi, esi", + "shr edi, 31", + "or edx, edi", + "add esi, esi", + "xor esi, ebp", + "bswap eax", + "bswap ecx", + "bswap edx", + "bswap esi", + "mov DWORD PTR [ebx+16], eax", + "mov DWORD PTR [ebx+20], ecx", + "mov DWORD PTR [ebx+24], edx", + "mov DWORD PTR [ebx+28], esi", + "mov eax, DWORD PTR [esp+16]", + "mov ebx, DWORD PTR [eax+2064]", + "mov esi, DWORD PTR [eax+2068]", + "mov edi, DWORD PTR [eax+2072]", + "mov ebp, DWORD PTR [eax+2076]", + "ret", + vg_aes_ctr32 = sym super::aes::vg_aes_ctr32, + ) +} + +/// CMAC's chaining (NIST SP 800-38B §6.2 step 6) for AES, over whole blocks: replaces the block `C₀` at `*state` with `Cₙ`, where `Cᵢ = CIPH_K(Cᵢ₋₁ ⊕ Mᵢ)` for the `n` 16-byte blocks `M₁ … Mₙ` starting at `data`. `CIPH_K` is AES (FIPS 197) with `rounds` rounds and the key schedule in the first `16 * (rounds + 1)` bytes of `*schedule`, as `vg_aes_expand_key` writes it. +/// +/// Contract: `VG.Spec.Cmac.aesUpdateContract`. Constant time: only the pointers, `rounds` and `n` may affect timing, not the key schedule, the chaining value or the data. +/// +/// This implementation encrypts each block with `vg_aes_ctr32`. +/// +/// # Safety +/// +/// * `schedule` must be valid for reads of 240 bytes. +/// * `state` must be valid for reads and writes of 16 bytes. +/// * `data` must be valid for reads of `16 * n` bytes. +/// * `scratch` must be valid for reads and writes of 2176 bytes. +/// * `rounds` must be 10, 12 or 14. +/// * The contents of `scratch` on return are unspecified. +/// * `state` and `scratch` must not overlap each other, `schedule`, `data` or the arguments on the stack (distinct Rust objects never do). +/// * None of `schedule`, `state`, `data` and `scratch` may overlap the return address on the stack or the 28 bytes of stack below it, or wrap around the end of the address space (no Rust object does). +#[unsafe(naked)] +pub(crate) unsafe extern "C" fn vg_cmac_aes_update(schedule: *const [u8; 240], rounds: usize, state: *mut [u8; 16], data: *const [u8; 16], n: usize, scratch: *mut [u64; 272]) { + core::arch::naked_asm!( + "mov eax, DWORD PTR [esp+24]", + "mov DWORD PTR [eax+2064], ebx", + "mov DWORD PTR [eax+2068], esi", + "mov DWORD PTR [eax+2072], edi", + "mov DWORD PTR [eax+2076], ebp", + "mov esi, DWORD PTR [esp+16]", + "mov eax, DWORD PTR [esp+20]", + "test eax, eax", + "je 20f", + "22:", + "mov ebx, DWORD PTR [esp+12]", + "mov ebp, DWORD PTR [esp+24]", + "mov eax, DWORD PTR [ebx]", + "mov ecx, DWORD PTR [esi]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2048], eax", + "mov eax, DWORD PTR [ebx+4]", + "mov ecx, DWORD PTR [esi+4]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2052], eax", + "mov eax, DWORD PTR [ebx+8]", + "mov ecx, DWORD PTR [esi+8]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2056], eax", + "mov eax, DWORD PTR [ebx+12]", + "mov ecx, DWORD PTR [esi+12]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2060], eax", + "mov eax, 0", + "mov DWORD PTR [ebx], eax", + "mov DWORD PTR [ebx+4], eax", + "mov DWORD PTR [ebx+8], eax", + "mov DWORD PTR [ebx+12], eax", + "mov eax, DWORD PTR [esp+4]", + "mov ecx, DWORD PTR [esp+8]", + "mov edx, ebp", + "add edx, 2048", + "mov edi, 1", + "push ebp", + "push edi", + "push ebx", + "push edx", + "push ecx", + "push eax", + "call {vg_aes_ctr32}", + "pop eax", + "pop eax", + "pop eax", + "pop eax", + "pop eax", + "pop eax", + "add esi, 16", + "mov eax, DWORD PTR [esp+20]", + "add eax, eax", + "add eax, eax", + "add eax, eax", + "add eax, eax", + "add eax, DWORD PTR [esp+16]", + "cmp esi, eax", + "jne 22b", + "jmp 21f", + "20:", + "21:", + "mov eax, DWORD PTR [esp+24]", + "mov ebx, DWORD PTR [eax+2064]", + "mov esi, DWORD PTR [eax+2068]", + "mov edi, DWORD PTR [eax+2072]", + "mov ebp, DWORD PTR [eax+2076]", + "ret", + vg_aes_ctr32 = sym super::aes::vg_aes_ctr32, + ) +} + +/// Finishes an AES-CMAC computation (NIST SP 800-38B §6.2, with `Tlen = 128`): if the block at `*state` is the chaining value `Cₙ₋₁` of the message's blocks but the last (as `vg_cmac_aes_update` computes it from a zero block), and the `last_len` bytes at `last` are the message's last bytes `Mₙ*`, replaces it with the MAC `Cₙ = CIPH_K(Cₙ₋₁ ⊕ Mₙ)`, where `Mₙ = K1 ⊕ Mₙ*` if `last_len` is 16, and `Mₙ = K2 ⊕ (Mₙ* ‖ 10ʲ)` otherwise. `*key` is the 240 bytes `vg_aes_expand_key` writes the key schedule for `rounds` rounds to, followed by the subkeys `K1 ‖ K2` (as `vg_cmac_aes_subkeys` writes them). `last_len` is 0 only for the empty message. +/// +/// Contract: `VG.Spec.Cmac.aesFinalizeContract`. Constant time: only the pointers, `rounds` and `last_len` may affect timing, not the key schedule, the subkeys, the chaining value or the data. +/// +/// This implementation encrypts each block with `vg_aes_ctr32`. +/// +/// # Safety +/// +/// * `key` must be valid for reads of 272 bytes. +/// * `state` must be valid for reads and writes of 16 bytes. +/// * `last` must be valid for reads of `last_len` bytes. +/// * `scratch` must be valid for reads and writes of 2176 bytes. +/// * `rounds` must be 10, 12 or 14. +/// * `last_len` must be at most 16. +/// * The contents of `scratch` on return are unspecified. +/// * `state` and `scratch` must not overlap each other, `key`, `last` or the arguments on the stack (distinct Rust objects never do). +/// * None of `key`, `state`, `last` and `scratch` may overlap the return address on the stack or the 28 bytes of stack below it, or wrap around the end of the address space (no Rust object does). +#[unsafe(naked)] +pub(crate) unsafe extern "C" fn vg_cmac_aes_finalize(key: *const [u8; 272], rounds: usize, state: *mut [u8; 16], last: *const u8, last_len: usize, scratch: *mut [u64; 272]) { + core::arch::naked_asm!( + "mov eax, DWORD PTR [esp+24]", + "mov DWORD PTR [eax+2064], ebx", + "mov DWORD PTR [eax+2068], esi", + "mov DWORD PTR [eax+2072], edi", + "mov DWORD PTR [eax+2076], ebp", + "mov ebp, eax", + "mov ecx, DWORD PTR [esp+20]", + "cmp ecx, 16", + "je 20f", + "mov eax, 0", + "mov DWORD PTR [ebp+2048], eax", + "mov DWORD PTR [ebp+2052], eax", + "mov DWORD PTR [ebp+2056], eax", + "mov DWORD PTR [ebp+2060], eax", + "mov edi, ebp", + "add edi, 2048", + "mov esi, DWORD PTR [esp+16]", + "mov ecx, DWORD PTR [esp+20]", + "test ecx, ecx", + "je 22f", + "24:", + "movzx eax, BYTE PTR [esi]", + "mov BYTE PTR [edi], al", + "add esi, 1", + "add edi, 1", + "sub ecx, 1", + "jne 24b", + "jmp 23f", + "22:", + "23:", + "mov eax, 128", + "mov BYTE PTR [edi], al", + "mov edx, DWORD PTR [esp+4]", + "mov eax, DWORD PTR [ebp+2048]", + "mov ecx, DWORD PTR [edx+256]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2048], eax", + "mov eax, DWORD PTR [ebp+2052]", + "mov ecx, DWORD PTR [edx+260]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2052], eax", + "mov eax, DWORD PTR [ebp+2056]", + "mov ecx, DWORD PTR [edx+264]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2056], eax", + "mov eax, DWORD PTR [ebp+2060]", + "mov ecx, DWORD PTR [edx+268]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2060], eax", + "jmp 21f", + "20:", + "mov ebx, DWORD PTR [esp+16]", + "mov edx, DWORD PTR [esp+4]", + "mov eax, DWORD PTR [ebx]", + "mov ecx, DWORD PTR [edx+240]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2048], eax", + "mov eax, DWORD PTR [ebx+4]", + "mov ecx, DWORD PTR [edx+244]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2052], eax", + "mov eax, DWORD PTR [ebx+8]", + "mov ecx, DWORD PTR [edx+248]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2056], eax", + "mov eax, DWORD PTR [ebx+12]", + "mov ecx, DWORD PTR [edx+252]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2060], eax", + "21:", + "mov ebx, DWORD PTR [esp+12]", + "mov eax, DWORD PTR [ebp+2048]", + "mov ecx, DWORD PTR [ebx]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2048], eax", + "mov eax, DWORD PTR [ebp+2052]", + "mov ecx, DWORD PTR [ebx+4]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2052], eax", + "mov eax, DWORD PTR [ebp+2056]", + "mov ecx, DWORD PTR [ebx+8]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2056], eax", + "mov eax, DWORD PTR [ebp+2060]", + "mov ecx, DWORD PTR [ebx+12]", + "xor eax, ecx", + "mov DWORD PTR [ebp+2060], eax", + "mov eax, 0", + "mov DWORD PTR [ebx], eax", + "mov DWORD PTR [ebx+4], eax", + "mov DWORD PTR [ebx+8], eax", + "mov DWORD PTR [ebx+12], eax", + "mov eax, DWORD PTR [esp+4]", + "mov ecx, DWORD PTR [esp+8]", + "mov edx, ebp", + "add edx, 2048", + "mov edi, 1", + "push ebp", + "push edi", + "push ebx", + "push edx", + "push ecx", + "push eax", + "call {vg_aes_ctr32}", + "pop eax", + "pop eax", + "pop eax", + "pop eax", + "pop eax", + "pop eax", + "mov eax, DWORD PTR [esp+24]", + "mov ebx, DWORD PTR [eax+2064]", + "mov esi, DWORD PTR [eax+2068]", + "mov edi, DWORD PTR [eax+2072]", + "mov ebp, DWORD PTR [eax+2076]", + "ret", + vg_aes_ctr32 = sym super::aes::vg_aes_ctr32, + ) +} diff --git a/src/asm/x86/mod.rs b/src/asm/x86/mod.rs index 4d014beb6..5972dffb6 100644 --- a/src/asm/x86/mod.rs +++ b/src/asm/x86/mod.rs @@ -16,6 +16,9 @@ pub(crate) mod chacha20; #[rustfmt::skip] pub(crate) mod chacha20poly1305; +#[rustfmt::skip] +pub(crate) mod cmac_aes; + #[rustfmt::skip] pub(crate) mod ct; diff --git a/src/cmac/aes.rs b/src/cmac/aes.rs index 539826c16..086bd7a71 100644 --- a/src/cmac/aes.rs +++ b/src/cmac/aes.rs @@ -15,9 +15,15 @@ //! same verified CMAC code, calling `vg_aes_ctr32_aesni` rather than //! `vg_aes_ctr32` to encrypt each block. On AArch64, CPUs with the AES //! extension run `vg_aes_expand_key_aes` and the `_aes` CMAC functions, -//! calling `vg_aes_ctr32_aes`. ARMv7 has only the scalar implementation. +//! calling `vg_aes_ctr32_aes`. ARMv7 and x86 have only the scalar +//! implementation. -#![cfg(any(target_arch = "x86_64", target_arch = "aarch64", target_arch = "arm"))] +#![cfg(any( + target_arch = "x86_64", + target_arch = "aarch64", + target_arch = "arm", + target_arch = "x86" +))] use super::{InvalidKeyLength, InvalidMac}; use crate::arch::aes::vg_aes_expand_key; @@ -93,7 +99,7 @@ impl Backend { } /// The only implementation there is. - #[cfg(target_arch = "arm")] + #[cfg(any(target_arch = "arm", target_arch = "x86"))] fn select(_: Features) -> Backend { Backend::Scalar } @@ -357,7 +363,7 @@ mod tests { } /// The scalar implementation is the only one. - #[cfg(target_arch = "arm")] + #[cfg(any(target_arch = "arm", target_arch = "x86"))] #[test] fn select() { assert_eq!(Backend::select(Features::of(&[])), Backend::Scalar); diff --git a/tests/cavp/cmac_aes.rs b/tests/cavp/cmac_aes.rs index dfe7ba7d4..655dd59f0 100644 --- a/tests/cavp/cmac_aes.rs +++ b/tests/cavp/cmac_aes.rs @@ -1,7 +1,12 @@ //! AES-CMAC: every vector of the CMAC generation and verification files, //! for 128-, 192- and 256-bit keys (the MAC truncated to `Tlen` bytes). -#![cfg(any(target_arch = "x86_64", target_arch = "aarch64", target_arch = "arm"))] +#![cfg(any( + target_arch = "x86_64", + target_arch = "aarch64", + target_arch = "arm", + target_arch = "x86" +))] use verified_garbage::cmac::aes::AesCmac; diff --git a/tests/wycheproof/cmac_aes.rs b/tests/wycheproof/cmac_aes.rs index 135e3cdb1..3cb7b63ea 100644 --- a/tests/wycheproof/cmac_aes.rs +++ b/tests/wycheproof/cmac_aes.rs @@ -5,7 +5,12 @@ //! invalid one is either a modified tag, which `verify` must reject, or a //! key of a length AES does not take, which `new` must reject. -#![cfg(any(target_arch = "x86_64", target_arch = "aarch64", target_arch = "arm"))] +#![cfg(any( + target_arch = "x86_64", + target_arch = "aarch64", + target_arch = "arm", + target_arch = "x86" +))] use serde::Deserialize; use verified_garbage::cmac::InvalidKeyLength;