diff --git a/ci/bench_arches.py b/ci/bench_arches.py index da0356174..2cd598bb4 100644 --- a/ci/bench_arches.py +++ b/ci/bench_arches.py @@ -47,7 +47,7 @@ "arm": { "os": "ubuntu-24.04-arm", "image": "ghcr.io/pyca/cryptography-runner-ubuntu-rolling:armv7l", - "options": "--env RUSTUP_HOME=/root/.rustup", + "options": "--env RUSTUP_HOME=/tmp/verified-garbage-rustup", }, } diff --git a/lean/VerifiedGarbage/Artifacts/HmacSha256/X86.lean b/lean/VerifiedGarbage/Artifacts/HmacSha256/X86.lean deleted file mode 100644 index 00a38a089..000000000 --- a/lean/VerifiedGarbage/Artifacts/HmacSha256/X86.lean +++ /dev/null @@ -1,37 +0,0 @@ -import VerifiedGarbage.TCB.X86.Target -import VerifiedGarbage.Proof.Hmac.X86.Init - -/-! -# HMAC-SHA-256 (RFC 2104) 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. --/ - -namespace VG.Artifacts.HmacSha256.X86 - -def artifacts : List Artifact := [ - { Spec.Hmac.initSha256Api with - target := X86.target - doc := Spec.Hmac.initSha256Api.doc - code := Impl.Hmac.X86.init - contract := Spec.Hmac.initSha256Contract X86.abi 20 - stack := 20 - verified := Proof.Hmac.X86.Init.init_verified - spSafe := Code.all_of_allInstrs (by lit_decide) }, - { Spec.Hmac.finalizeSha256OutApi with - target := X86.target - doc := Spec.Hmac.finalizeSha256OutApi.doc - code := Impl.Hmac.X86.finalize - contract := Spec.Hmac.finalizeSha256OutContract X86.abi 20 - stack := 20 - verified := Proof.Hmac.X86.Finalize.finalize_verified - spSafe := Code.all_of_allInstrs (by lit_decide) }] - -end VG.Artifacts.HmacSha256.X86 diff --git a/lean/VerifiedGarbage/Artifacts/Pbkdf2Sha256/X86.lean b/lean/VerifiedGarbage/Artifacts/Pbkdf2Sha256/X86.lean deleted file mode 100644 index 0ab9167a6..000000000 --- a/lean/VerifiedGarbage/Artifacts/Pbkdf2Sha256/X86.lean +++ /dev/null @@ -1,29 +0,0 @@ -import VerifiedGarbage.TCB.X86.Target -import VerifiedGarbage.Impl.Pbkdf2.X86 -import VerifiedGarbage.Proof.Pbkdf2.X86.Iterate - -/-! -# The PBKDF2-HMAC-SHA-256 iteration (RFC 8018) 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. --/ - -namespace VG.Artifacts.Pbkdf2Sha256.X86 - -def artifacts : List Artifact := [ - { Spec.Pbkdf2.iterateSha256Api with - target := X86.target - doc := Spec.Pbkdf2.iterateSha256Api.doc - code := Impl.Pbkdf2.X86.iterate - contract := Spec.Pbkdf2.iterateSha256Contract X86.abi 20 - stack := 20 - verified := Proof.Pbkdf2.X86.iterate_verified }] - -end VG.Artifacts.Pbkdf2Sha256.X86 diff --git a/lean/VerifiedGarbage/Artifacts/Sha256/X86.lean b/lean/VerifiedGarbage/Artifacts/Sha256/X86.lean index 5680fe16c..dfb56e549 100644 --- a/lean/VerifiedGarbage/Artifacts/Sha256/X86.lean +++ b/lean/VerifiedGarbage/Artifacts/Sha256/X86.lean @@ -17,35 +17,12 @@ against the contract. namespace VG.Artifacts.Sha256.X86 def artifacts : List Artifact := [ - { Spec.Sha256.compressApi with - target := X86.target - doc := Spec.Sha256.compressApi.doc - code := Impl.Sha256.X86.compress - contract := Spec.Sha256.compressContract X86.abi - verified := Proof.Sha256.X86.Shared.compress - spSafe := Code.all_of_allInstrs (by lit_decide) }, { Spec.Sha256.initApi with target := X86.target doc := Spec.Sha256.initApi.doc code := Impl.Sha256.X86.Stream.init contract := Spec.Sha256.initContract X86.abi verified := Proof.Sha256.X86.Shared.init - spSafe := Code.all_of_allInstrs (by lit_decide) }, - { Spec.Sha256.updateApi with - target := X86.target - doc := Spec.Sha256.updateApi.doc - code := Impl.Sha256.X86.Stream.update - contract := Spec.Sha256.updateContract X86.abi 20 - stack := 20 - verified := Proof.Sha256.X86.Shared.update - spSafe := Code.all_of_allInstrs (by lit_decide) }, - { Spec.Sha256.finalizeApi with - target := X86.target - doc := Spec.Sha256.finalizeApi.doc - code := Impl.Sha256.X86.Stream.finalize - contract := Spec.Sha256.finalizeContract X86.abi 20 - stack := 20 - verified := Proof.Sha256.X86.Shared.finalize spSafe := Code.all_of_allInstrs (by lit_decide) }] end VG.Artifacts.Sha256.X86 diff --git a/lean/VerifiedGarbage/Generic/Sha256/X86/Hmac.lean b/lean/VerifiedGarbage/Generic/Sha256/X86/Hmac.lean new file mode 100644 index 000000000..f45cd9fb7 --- /dev/null +++ b/lean/VerifiedGarbage/Generic/Sha256/X86/Hmac.lean @@ -0,0 +1,30 @@ +import VerifiedGarbage.TCB.X86.Target +import VerifiedGarbage.Proof.Sha256.X86.Variants.Interface + +/-! Generic hmac registrations for every x86 SHA-256 backend. -/ + +namespace VG.Generic.Sha256.X86.Hmac + +def artifacts (v : Proof.Sha256.X86.Variants.Backend) : List Artifact := [ + { Spec.Hmac.initSha256Api with + name := Spec.Hmac.initSha256Api.name ++ v.suffix + target := X86.target + doc := Spec.Hmac.initSha256Api.doc + code := Impl.Hmac.Sha256.X86.init v.cmpN v.cmpC + contract := Spec.Hmac.initSha256Contract X86.abi 20 + stack := 20 + verified := Proof.Hmac.Sha256.X86.Init.verified v.cmp v.cmpSp v.cmpStack v.initCt + spSafe := v.initSp + features := v.features }, + { Spec.Hmac.finalizeSha256OutApi with + name := Spec.Hmac.finalizeSha256OutApi.name ++ v.suffix + target := X86.target + doc := Spec.Hmac.finalizeSha256OutApi.doc + code := Impl.Hmac.Sha256.X86.finalize v.cmpN v.cmpC + contract := Spec.Hmac.finalizeSha256OutContract X86.abi 20 + stack := 20 + verified := Proof.Hmac.Sha256.X86.Finalize.verified v.cmp v.cmpSp v.cmpStack v.finHashSp v.finHashStack v.finCt + spSafe := v.finSp + features := v.features }] + +end VG.Generic.Sha256.X86.Hmac diff --git a/lean/VerifiedGarbage/Generic/Sha256/X86/Pbkdf2.lean b/lean/VerifiedGarbage/Generic/Sha256/X86/Pbkdf2.lean new file mode 100644 index 000000000..96cf19592 --- /dev/null +++ b/lean/VerifiedGarbage/Generic/Sha256/X86/Pbkdf2.lean @@ -0,0 +1,20 @@ +import VerifiedGarbage.TCB.X86.Target +import VerifiedGarbage.Proof.Sha256.X86.Variants.Interface + +/-! Generic PBKDF2 iteration registration for every x86 SHA-256 backend. -/ +namespace VG.Generic.Sha256.X86.Pbkdf2 + +def artifacts (v : Proof.Sha256.X86.Variants.Backend) : List Artifact := [ + { Spec.Pbkdf2.iterateSha256Api with + name := Spec.Pbkdf2.iterateSha256Api.name ++ v.suffix + target := X86.target + doc := Spec.Pbkdf2.iterateSha256Api.doc + code := Impl.Pbkdf2.Sha256.X86.iterate v.cmpN v.cmpC + contract := Spec.Pbkdf2.iterateSha256Contract X86.abi 20 + writeArgs := true + stack := 20 + verified := Proof.Pbkdf2.Sha256.X86.verified v.cmp v.cmpSp v.cmpStack v.iterCt + spSafe := v.iterSp + features := v.features }] + +end VG.Generic.Sha256.X86.Pbkdf2 diff --git a/lean/VerifiedGarbage/Generic/Sha256/X86/Stream.lean b/lean/VerifiedGarbage/Generic/Sha256/X86/Stream.lean new file mode 100644 index 000000000..085ce82de --- /dev/null +++ b/lean/VerifiedGarbage/Generic/Sha256/X86/Stream.lean @@ -0,0 +1,22 @@ +import VerifiedGarbage.TCB.X86.Target +import VerifiedGarbage.Proof.Sha256.X86.Variants.Interface + +/-! Generic stream registrations for every x86 SHA-256 backend. -/ + +namespace VG.Generic.Sha256.X86.Stream + +def artifacts (v : Proof.Sha256.X86.Variants.Backend) : List Artifact := v.functions.map fun f => + { f.api with + name := f.api.name ++ v.suffix + target := X86.target + doc := f.api.doc + code := f.code + contract := f.contract + stack := f.stack + verified := f.verified + ofSig := f.ofSig + ofApi := f.ofApi + spSafe := f.spSafe + features := v.features } + +end VG.Generic.Sha256.X86.Stream diff --git a/lean/VerifiedGarbage/Impl/Hmac/Sha256/X86.lean b/lean/VerifiedGarbage/Impl/Hmac/Sha256/X86.lean new file mode 100644 index 000000000..9357f2088 --- /dev/null +++ b/lean/VerifiedGarbage/Impl/Hmac/Sha256/X86.lean @@ -0,0 +1,48 @@ +import VerifiedGarbage.Impl.Hmac.X86 +import VerifiedGarbage.Impl.MdStream.X86 + +/-! SHA-256's efficient x86 HMAC bodies, generic over compression. -/ +namespace VG.Impl.Hmac.Sha256.X86 +open VG.X86 +open VG.Impl.Sha256.X86 (at_) +open VG.Impl.Sha256.X86.Stream (save restore) +open VG.Impl.Hmac.X86 (h0 keyLoop padLoop opadWord bswapWord copyWord padWords) + +def compressBuf (name : String) (code : Prog isa) (b : Reg) : Prog isa := + .seq (.block [.mov .eax (.reg b), .alu .add .eax (.imm 32)]) (Impl.MdStream.X86.compressAt name code b .ebp) + +def init (name : String) (code : Prog isa) : Prog isa := + .seq (.block ([.mov .eax (.mem (at_ .esp 20))] ++ save .eax ++ + [.mov .ebp (.reg .eax), .mov .ebx (.mem (at_ .esp 4)), .mov .esi (.mem (at_ .esp 8))] ++ + h0 .ebx ++ h0 .esi ++ + [.mov .edi (.mem (at_ .esp 12)), .mov .ecx (.mem (at_ .esp 16)), .mov .edx (.reg .ebx), + .alu .add .edx (.imm 32), .alu .test .ecx (.reg .ecx)])) + (.seq (.ite .e (.block []) keyLoop) + (.seq (.block [.mov .eax (.reg .ebx), .alu .add .eax (.imm 96), .mov .ecx (.imm 0x36), + .alu .cmp .edx (.reg .eax)]) + (.seq (.ite .e (.block []) padLoop) + (.seq (.block ((List.range 16).flatMap opadWord)) + (.seq (compressBuf name code .ebx) + (.seq (compressBuf name code .esi) + (.block (.mov .eax (.reg .ebp) :: restore .eax)))))))) + +def finalizeHash (name : String) (code : Prog isa) : Prog isa := + match Impl.MdStream.X86.finalize Impl.Sha256.X86.Stream.params name code with + | .seq a (.seq b (.seq c _)) => .seq a (.seq b c) + | p => p + +def finalize (name : String) (code : Prog isa) : Prog isa := + .seq (.block [.mov .edx (.mem (at_ .esp 24)), .mov .ecx (.mem (at_ .esp 8)), .store (at_ .edx 176) .ecx, + .mov .ecx (.mem (at_ .esp 12)), .store (at_ .esp 8) .ecx, + .mov .ecx (.mem (at_ .esp 16)), .store (at_ .esp 12) .ecx, + .mov .ecx (.mem (at_ .esp 20)), .store (at_ .esp 16) .ecx, .store (at_ .esp 20) .edx]) + (.seq (finalizeHash name code) + -- The inner digest into the inner buffer, and the outer hash value into the inner state. + (.seq (.block ((List.range 8).flatMap (bswapWord .ebx .ebx 0 32) ++ .mov .edx (.mem (at_ .ebp 176)) :: + (List.range 8).flatMap (copyWord .edx .ebx 0 0) ++ padWords ++ + [.mov .eax (.reg .ebx), .alu .add .eax (.imm 32)])) + (.seq (Impl.MdStream.X86.compressAt name code .ebx .ebp) + (.block (.mov .eax (.mem (at_ .ebp 136)) :: (List.range 8).flatMap (bswapWord .ebx .eax 0 0) ++ + .mov .eax (.reg .ebp) :: restore .eax))))) + +end VG.Impl.Hmac.Sha256.X86 diff --git a/lean/VerifiedGarbage/Impl/Pbkdf2/Sha256/X86.lean b/lean/VerifiedGarbage/Impl/Pbkdf2/Sha256/X86.lean new file mode 100644 index 000000000..1ac84a977 --- /dev/null +++ b/lean/VerifiedGarbage/Impl/Pbkdf2/Sha256/X86.lean @@ -0,0 +1,20 @@ +import VerifiedGarbage.Impl.Pbkdf2.X86 +import VerifiedGarbage.Impl.MdStream.X86 + +/-! PBKDF2-SHA-256's two-compression iteration, generic over compression. -/ +namespace VG.Impl.Pbkdf2.Sha256.X86 +open VG.X86 +open VG.Impl.Pbkdf2.X86 (load atBlock digest xorW prologue epilogue) + +def body (name : String) (code : Prog isa) : Prog isa := + .seq (.block (load 0 ++ atBlock)) + (.seq (Impl.MdStream.X86.compressAt name code .ebx .ebp) + (.seq (.block (digest ++ load 96 ++ atBlock)) + (.seq (Impl.MdStream.X86.compressAt name code .ebx .ebp) + (.block (digest ++ (List.range 8).flatMap xorW ++ [.alu .sub .edi (.imm 1)]))))) + +def iterate (name : String) (code : Prog isa) : Prog isa := + .seq (.block prologue) + (.seq (.ite .e (.block []) (.loop (body name code) .ne)) (.block epilogue)) + +end VG.Impl.Pbkdf2.Sha256.X86 diff --git a/lean/VerifiedGarbage/Proof/Hmac/Sha256/X86/Finalize.lean b/lean/VerifiedGarbage/Proof/Hmac/Sha256/X86/Finalize.lean new file mode 100644 index 000000000..e18b3b848 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Hmac/Sha256/X86/Finalize.lean @@ -0,0 +1,303 @@ +import VerifiedGarbage.Proof.Hmac.X86.Finalize +import VerifiedGarbage.Proof.Sha256.X86.Stream.FinalizeVariant +import VerifiedGarbage.Impl.Hmac.Sha256.X86 + +/-! The efficient SHA-256 HMAC finalizer, proved for any compressor. -/ +namespace VG.Proof.Hmac.Sha256.X86.Finalize +open VG VG.X86 VG.Impl.Hmac.X86 +open VG.Impl.Sha256.X86 (at_) +open VG.Impl.Sha256.X86.Stream (compressAt restore saved) +open VG.Proof.Sha256.X86 (contains_offset) +open VG.Proof.Sha256.X86.Stream +open VG.Proof.Sha256.Stream (writeBytes writeBytes_frame writeBytes_append repr_congr compressList_append + hash_one lenBytes rest) +open VG.Proof.Hmac.X86 +open VG.Proof.Hmac.Common (bytesAt_length) +open VG.Spec.Sha256 (HashValue stateAt blockAt compress parseBlock bytesAt wordBytes Repr) +open VG.Proof.Sha256 (countX86) +open VG.Spec.Hmac (xorPad ipad opad hmacBlockKey sha256) +open VG.Proof.Hmac (countFinalizeX86) + +open VG.Proof.Hmac.X86.Finalize +variable {name : String} {code : Prog isa} + (hv : Verified X86.target code Proof.Sha256.compressX86) + (hnosp : NoSp code) (hstack : stackUse code = 0) + +theorem finalizeHash_eq : Impl.Hmac.Sha256.X86.finalizeHash name code = .seq (.block (([.mov .eax (.mem (at_ .esp 20))] : List Instr) ++ + VG.Impl.Sha256.X86.Stream.save .eax ++ + ([.mov .ebp (.reg .eax), .mov .ebx (.mem (at_ .esp 4)), + .mov .ecx (.mem (at_ .esp 8)), .store (at_ .ebp 128) .ecx, + .mov .ecx (.mem (at_ .esp 12)), .store (at_ .ebp 132) .ecx, + .mov .ecx (.mem (at_ .esp 16)), .store (at_ .ebp 136) .ecx, + .mov .edi (.mem (at_ .esp 8)), .alu .and .edi (.imm 63), + .mov .edx (.reg .ebx), .alu .add .edx (.reg .edi), .mov .ecx (.imm 0x80), + .store8 (at_ .edx 32) .cl, .alu .add .edi (.imm 1), + .mov .esi (.imm 0), .alu .cmp .edi (.imm 57)] : List Instr))) + (.seq (.ite .ae (.block [.mov .esi (.imm 1)]) (.block [])) + (.loop (VG.Impl.MdStream.X86.finalizeBody VG.Impl.Sha256.X86.Stream.params name code) .e)) := rfl + +include hv hnosp hstack + +theorem hash_ok {s : State} (hp : SPre s) : WP isa (Impl.Hmac.Sha256.X86.finalizeHash name code) s (SDone s) := by + rw [finalizeHash_eq, ← VG.Proof.Sha256.X86.Stream.Finalize.seq_assoc] + refine WP.seq (WP.mono (VG.Proof.Sha256.X86.Stream.Finalize.prologue_ok hp) fun s₁ ⟨k, hL⟩ => ?_) + refine WP.loop (M := isa) (fun i s' => ∃ n, VG.Proof.Sha256.X86.Stream.Finalize.LInv s i n s') ?_ k s₁ ⟨_, hL⟩ + rintro i s' ⟨n, hL⟩ + refine WP.mono (VG.Proof.Sha256.X86.Stream.Finalize.body_of hv hnosp hstack hp hL) fun s'' h => ?_ + rcases h with ⟨he, hD⟩ | ⟨he, rfl, hL'⟩ + · exact .inl ⟨he, hD⟩ + · exact .inr ⟨he, 0, by omega_nat, 0, hL'⟩ + +theorem comp_of {s₀ s : State} (hp : Pre s₀) (hrd : s.rd = s₀.rd) (hwr : s.wr = s₀.wr) + (hsp : s.gpr .esp = esp₀ s₀) (hebx : s.gpr .ebx = inn s₀) (hebp : s.gpr .ebp = scr s₀) + (heax : s.gpr .eax = inn s₀ + 32) {Q : State → Prop} + (hQ : ∀ s', s'.rd = s.rd → s'.wr = s.wr → (∀ r ∈ calleeSaved, s'.gpr r = s.gpr r) → + Frame [⟨inA s₀, 32⟩, ⟨scA s₀, 112⟩, stkR s₀] s.mem s'.mem → + stateAt s'.mem (inA s₀) = + compress (stateAt s.mem (inA s₀)) (blockAt s.mem (inA s₀ + BitVec.ofNat 64 32)) → Q s') : + WP isa (Impl.MdStream.X86.compressAt name code .ebx .ebp) s Q := by + have fi := hp.in_fit + have fs := hp.scr_fit + have fsp := hp.sp_fit + have hb := blk_eq hp + have s32 : Region.Sub ⟨inA s₀, 32⟩ (inR s₀) := Region.sub_prefix (by omega_nat) + have s112 : Region.Sub ⟨scA s₀, 112⟩ (scR s₀) := Region.sub_prefix (by omega_nat) + have b64 : Region.Sub ⟨(inn s₀ + 32).setWidth 64, 64⟩ (inR s₀) := by rw [hb]; exact sub_offset (by omega_nat) (by omega_nat) + refine compressAt_of hv hnosp hstack (st := inn s₀) (scr := scr s₀) (blk := inn s₀ + 32) (E := esp₀ s₀) + (by decide) (by decide) (by decide) (by decide) hsp hebx hebp heax hp.sp_lo + (by omega_nat) (by rw [show (inn s₀ + 32).toNat = (inn s₀).toNat + 32 by + rw [BitVec.toNat_add]; exact Nat.mod_eq_of_lt (by simp; omega_nat)]; omega_nat) (by omega_nat) + ((hp.in_scr.sub_left s32).sub_right s112) ?_ ((hp.in_scr.sub_left b64).sub_right s112) + (hp.stk_in.sub_right s32) (hp.stk_scr.sub_right s112) (hp.stk_in.sub_right b64) ?_ ?_ ?_ + · rw [hb] + intro a h₁ h₂ + simp only [Region.Contains] at h₁ h₂ + have := sep_off (inA s₀) (d := 32) (e := 0) (n := 64) (k := 32) (by omega_nat) (by omega_nat) (by omega_nat) a + (by omega_nat) (by simp at h₂ ⊢; omega_nat) + exact this + · apply Covers.of_sub + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + subst hr + exact ⟨inR s₀, by simp [hrd, hwr, hp.wr], 32, hb, by simp⟩ + · apply Covers.of_sub + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl + · exact ⟨inR s₀, by simp [hwr, hp.wr], 0, by simp, by simp⟩ + · exact ⟨scR s₀, by simp [hwr, hp.wr], 0, by simp, by simp⟩ + · intro s' h₁ h₂ h₃ h₄ h₇ + rw [hb] at h₇ + exact hQ s' h₁ h₂ h₃ h₄ h₇ + +/-! ## Writing the MAC -/ + +variable (hfSp : NoSp (Impl.Hmac.Sha256.X86.finalizeHash name code)) + (hfStack : stackUse (Impl.Hmac.Sha256.X86.finalizeHash name code) = 20) +include hfSp hfStack + +theorem correct {s₀ : State} (hp : Pre s₀) : + WP isa (Impl.Hmac.Sha256.X86.finalize name code) s₀ fun s' => abiPreserved s₀ s' ∧ Proof.Hmac.finalizeSha256X86.post s₀ s' := by + have fi := hp.in_fit + have fs := hp.scr_fit + have fsp := hp.sp_fit + unfold Impl.Hmac.Sha256.X86.finalize + refine WP.seq (WP.mono (pro_ok hp) fun s₁ h₁ => ?_) + have sp₁ : s₁.gpr .esp = esp₀ s₀ := h₁.gpr _ (by decide) (by decide) + have s160 : Region.Sub ⟨scA s₀, 160⟩ (scR s₀) := Region.sub_prefix (by omega_nat) + have a20 : Region.Sub ⟨addr (esp₀ s₀) 4, 20⟩ (argR s₀) := Region.sub_prefix (by omega_nat) + have finSub : ∀ r ∈ finW s₀ ++ [stkR s₀], ∃ r' ∈ allR s₀, Region.Sub r r' := by + intro r hr + simp only [finW, 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 + · exact ⟨inR s₀, by simp, fun _ h => h⟩ + · exact ⟨outR s₀, by simp, fun _ h => h⟩ + · exact ⟨scR s₀, by simp, s160⟩ + · exact ⟨argR s₀, by simp, a20⟩ + · exact ⟨stkR s₀, by simp, fun _ h => h⟩ + refine WP.seq (WP.narrowSp (hash_ok hv hnosp hstack (narrow_pre hp h₁)) ?_ ?_ hfSp + (by rw [hfStack, sp₁]; exact hp.sp_lo) fun sD rdD wrD frD hD => ?_) + · rw [h₁.rd, h₁.wr, hp.rd, hp.wr] + apply Covers.of_sub + intro r hr + simp only [List.nil_append, finW, List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · exact ⟨inR s₀, by simp, 0, by simp, by simp⟩ + · exact ⟨outR s₀, by simp, 0, by simp, by simp⟩ + · exact ⟨scR s₀, by simp, 0, by simp, by simp⟩ + · exact ⟨argR s₀, by simp, 0, by simp, by simp⟩ + · rw [h₁.wr, hp.wr] + apply Covers.of_sub + intro r hr + simp only [finW, List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · exact ⟨inR s₀, by simp, 0, by simp, by simp⟩ + · exact ⟨outR s₀, by simp, 0, by simp, by simp⟩ + · exact ⟨scR s₀, by simp, 0, by simp, by simp⟩ + · exact ⟨argR s₀, by simp, 0, by simp, by simp⟩ + rw [hfStack, sp₁] at frD + obtain ⟨hC, hHash⟩ := hD + have e3 : VG.Proof.Sha256.X86.Stream.Finalize.out (narrow s₀ s₁) = out s₀ := narrow_arg hp h₁ (by omega_nat) + have e4 : VG.Proof.Sha256.X86.Stream.Finalize.scr (narrow s₀ s₁) = scr s₀ := narrow_arg hp h₁ (by omega_nat) + have outpD : sD.mem.readW (addr (scr s₀) 136) 32 = out s₀ := by + have := hC.outp; rw [e4, e3] at this; exact this + have savedD : ∀ p ∈ saved, sD.mem.readW (addr (scr s₀) p.2) 32 = s₀.gpr p.1 := by + intro p hp' + have := hC.saved p hp' + rw [e4] at this + refine this.trans ?_ + show s₁.gpr p.1 = s₀.gpr p.1 + simp only [saved, List.mem_cons, List.not_mem_nil, or_false] at hp' + rcases hp' with rfl | rfl | rfl | rfl <;> exact h₁.gpr _ (by decide) (by decide) + have ebxD : sD.gpr .ebx = inn s₀ := hC.ebx.trans (narrow_arg hp h₁ (i := 0) (by omega_nat)) + have ebpD : sD.gpr .ebp = scr s₀ := hC.ebp.trans (narrow_arg hp h₁ (i := 4) (by omega_nat)) + have spD : sD.gpr .esp = esp₀ s₀ := hC.esp.trans sp₁ + have rdD' : sD.rd = s₀.rd := rdD.trans h₁.rd + have wrD' : sD.wr = s₀.wr := wrD.trans h₁.wr + -- `scratch[176..180)`, where `outer` is, lies outside what `finalizeHash` writes. + have w176 : ∀ r ∈ finW s₀ ++ [stkR s₀], Region.Disjoint ⟨addr (scr s₀) 176, 4⟩ r := by + have hs : Region.Sub ⟨addr (scr s₀) 176, 4⟩ (scR s₀) := hp.scr_sub (by omega_nat) + intro r hr + simp only [finW, 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 + · exact (hp.in_scr.symm.sub_left hs) + · exact (hp.out_scr.symm.sub_left hs) + · rw [addr_eq (by omega_nat)]; exact Offset.disjoint_base _ (by omega_nat) (by omega_nat) + · exact (hp.a_scr.symm.sub_left hs).sub_right a20 + · exact hp.stk_scr.symm.sub_left hs + have ouD : sD.mem.readW (addr (scr s₀) 176) 32 = ou s₀ := by + rw [frD.readW (Region.contains_self _ _) w176 (by decide), h₁.mem, proMem_176 hp] + refine WP.seq (WP.mono (mid_ok hp ⟨rdD', wrD', ebxD, ebpD, spD, ouD⟩) fun s₃ h₃ => ?_) + have sp₃ : s₃.gpr .esp = esp₀ s₀ := by rw [h₃.gpr _ (by decide) (by decide) (by decide), spD] + refine WP.seq (comp_of hv hnosp hstack hp h₃.rd h₃.wr sp₃ (by rw [h₃.gpr _ (by decide) (by decide) (by decide), ebxD]) + (by rw [h₃.gpr _ (by decide) (by decide) (by decide), ebpD]) h₃.eax fun s₄ rd₄ wr₄ cs₄ fr₄ st₄ => ?_) + -- Words of the scratch space that neither the middle block nor the compression writes. + have keep : ∀ d, 112 ≤ d → d + 4 ≤ 160 → + s₄.mem.readW (addr (scr s₀) d) 32 = sD.mem.readW (addr (scr s₀) d) 32 := by + intro d h₁ h₂ + have hs : Region.Sub ⟨addr (scr s₀) d, 4⟩ (scR s₀) := hp.scr_sub (by omega_nat) + rw [fr₄.readW (Region.contains_self _ _) ?_ (by decide), h₃.mem, + (midMem_frame sD.mem).readW (Region.contains_self _ _) ?_ (by decide)] + · intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl + · exact hp.in_scr.symm.sub_left hs + · exact hp.a_scr.symm.sub_left hs + · intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact (hp.in_scr.symm.sub_left hs).sub_right (Region.sub_prefix (by omega_nat)) + · rw [addr_eq (by omega_nat)]; exact Offset.disjoint_base _ (by omega_nat) (by omega_nat) + · exact hp.stk_scr.symm.sub_left hs + have csD : ∀ r ∈ calleeSaved, s₄.gpr r = sD.gpr r := fun r hr => by + rw [cs₄ r hr, h₃.gpr r ?_ ?_ ?_] <;> + · simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl | rfl <;> decide + refine WP.mono (out_ok hp (rd₄.trans h₃.rd) (wr₄.trans h₃.wr) (by rw [csD _ (by decide), ebxD]) + (by rw [csD _ (by decide), ebpD]) (by rw [csD _ (by decide), spD]) + (by rw [keep 136 (by omega_nat) (by omega_nat)]; exact outpD) + fun p hp' => ?_) fun s' ⟨rd', wr', cs', m'⟩ => ?_ + · have hd : 112 ≤ p.2 ∧ p.2 + 4 ≤ 128 := by + simp only [saved, List.mem_cons, List.not_mem_nil, or_false] at hp' + rcases hp' with rfl | rfl | rfl | rfl <;> simp + rw [keep p.2 hd.1 (by omega_nat)] + exact savedD p hp' + -- Everything written is within our regions. + have f1 : Frame (allR s₀) s₀.mem s₁.mem := by rw [h₁.mem]; exact (proMem_frame hp).mono (by simp) + have f2 : Frame (allR s₀) s₁.mem sD.mem := frD.sub finSub + have f3 : Frame (allR s₀) sD.mem s₃.mem := by rw [h₃.mem]; exact (midMem_frame sD.mem).mono (by simp) + have f4 : Frame (allR s₀) s₃.mem s₄.mem := by + refine fr₄.sub fun r hr => ?_ + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact ⟨inR s₀, by simp, Region.sub_prefix (by omega_nat)⟩ + · exact ⟨scR s₀, by simp, Region.sub_prefix (by omega_nat)⟩ + · exact ⟨stkR s₀, by simp, fun _ h => h⟩ + have f5 : Frame (allR s₀) s₄.mem s'.mem := by + rw [m'] + refine (writeBytes_frame (R := outR s₀) _ _ _ ?_).mono (by simp) + rw [beWords_length]; exact contains_offset (by omega_nat) (by omega_nat) + have F : Frame (allR s₀) s₀.mem s'.mem := f1.trans (f2.trans (f3.trans (f4.trans f5))) + refine ⟨⟨cs', F.readW (r := retR s₀) (Region.contains_self _ _) ?_ (by decide)⟩, ?_⟩ + · intro r hr + simp only [allR, List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl | rfl + exacts [hp.ret_in, hp.ret_out, hp.ret_scr, ret_a hp, ret_stk hp] + intro k0 text hk hin hcnt hout + -- The inner digest. + have e0 : VG.Proof.Sha256.X86.Stream.Finalize.st (narrow s₀ s₁) = inn s₀ := narrow_arg hp h₁ (by omega_nat) + have oD : ∀ r ∈ allR s₀, (ouR s₀).Disjoint r := by + intro r hr + simp only [allR, List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl | rfl + exacts [hp.o_in, hp.o_out, hp.o_scr, hp.o_a, hp.stk_ou.symm] + have hR₀ : VG.Proof.Sha256.X86.Stream.Finalize.R₀ (narrow s₀ s₁) (xorPad k0 ipad ++ text) := by + refine ⟨?_, ?_⟩ + · show Repr s₁.mem ((VG.Proof.Sha256.X86.Stream.Finalize.st (narrow s₀ s₁)).setWidth 64) _ + rw [e0] + refine repr_congr (fun i hi => ?_) hin + rw [h₁.mem] + refine frame_bytes (proMem_frame hp) (R := inR s₀) (fun r hr => ?_) (by simp) hi + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl + exacts [hp.in_scr, hp.a_in.symm] + · show countX86 (narrow s₀ s₁) = _ + simp only [countX86] + rw [narrow_arg hp h₁ (i := 2) (by omega_nat), narrow_arg hp h₁ (i := 1) (by omega_nat)] + simp only [List.getD_cons_succ, List.getD_cons_zero, List.length_append, xorPad_length, hk] + exact hcnt + have hdig : Spec.Sha256.hash (xorPad k0 ipad ++ text) = beWords sD.mem (inn s₀) 0 8 := by + have e0A : VG.Proof.Sha256.X86.Stream.Finalize.stA (narrow s₀ s₁) = inA s₀ := by + show (VG.Proof.Sha256.X86.Stream.Finalize.st (narrow s₀ s₁)).setWidth 64 = _ + rw [e0] + rw [hHash _ hR₀, beWords_stateAt _ (by omega_nat), e0A, State.withRegions_mem] + -- The outer hash value. + have hou : stateAt s₃.mem (inA s₀) = Spec.Sha256.compressList Spec.Sha256.H0 (xorPad k0 opad) 1 := by + rw [h₃.mem, midMem_state, + VG.Proof.Sha256.Stream.stateAt_congr (mem := s₀.mem) fun i hi => + frame_bytes (f1.trans f2) (R := ouR s₀) oD (by simp) (by simp; omega_nat), + hout.1, xorPad_length, hk] + -- The block after it. + have hblk : blockAt s₃.mem (inA s₀ + BitVec.ofNat 64 32) = + parseBlock fun t => (beWords sD.mem (inn s₀) 0 8 ++ padBytes).getD t 0 := by + have hb := midMem_block (s₀ := s₀) sD.mem + rw [← h₃.mem] at hb + exact VG.Proof.Sha256.Stream.parseBlock_congr fun k hk => bytesAt_getD hb (by omega_nat) + -- The MAC. + have hmac : bytesAt s'.mem (outA s₀) 32 = beWords s₄.mem (inn s₀) 0 8 := by + rw [m', show outA s₀ + BitVec.ofNat 64 0 = outA s₀ by simp] + have := VG.Proof.Hmac.Common.bytesAt_writeBytes_self s₄.mem (outA s₀) + (beWords s₄.mem (inn s₀) 0 8) (by rw [beWords_length]; omega_nat) + rw [beWords_length] at this + simpa only [Nat.reduceMul] using this + show bytesAt s'.mem (outA s₀) 32 = _ + rw [hmac, beWords_stateAt _ (by omega_nat), st₄, hou, hblk] + simp only [hmacBlockKey, sha256] + rw [hdig, outer_hash hk (beWords_length _ _ _ _)] + + +local macro "narrow" loc:(Lean.Parser.Tactic.location)? : tactic => + `(tactic| simp only [Proof.Hmac.finalizeSha256X86, Proof.Hmac.countFinalizeX86, + VG.Proof.Hmac.X86.Finalize.finalizeWide, VG.Proof.Hmac.X86.Finalize.narrowWr, VG.X86.arg_withRegions, VG.X86.argAddr_withRegions, + VG.X86.State.withRegions_gpr, VG.X86.State.withRegions_mem, VG.X86.State.withRegions_rd, + VG.X86.State.withRegions_wr] $(loc)?) + +theorem verified + (hct : ConstantTime isa Proof.Hmac.finalizeSha256X86.pre Proof.Hmac.finalizeSha256X86.pub + (Impl.Hmac.Sha256.X86.finalize name code)) : + Verified X86.target (Impl.Hmac.Sha256.X86.finalize name code) (Spec.Hmac.finalizeSha256OutContract X86.abi 20) := + have hsat := finalizeWide_implies.sat_left + (Verified.widen (Verified.of_correct (fun s hs => by + obtain ⟨t, s', he, h⟩ := correct hv hnosp hstack hfSp hfStack (pre_of hs) + exact ⟨t, s', he, h⟩) hct + (.refl (hsat.elim fun s hs => ⟨_, finalizeWide_pre s hs⟩))) + narrowWr finalizeWide_pre + (fun _ h => by + obtain ⟨_, h₂, _⟩ := h + rw [h₂] + exact .cons (Region.prefix_of_ble rfl) (.cons (Region.prefix_of_ble rfl) + (.cons (Region.prefix_of_ble rfl) (.cons (Region.prefix_of_ble rfl) .nil)))) + (fun _ _ _ h => by narrow at h ⊢; exact h) + (fun _ _ _ _ h => by narrow; exact h) hsat).of_implies finalizeWide_implies + +end VG.Proof.Hmac.Sha256.X86.Finalize diff --git a/lean/VerifiedGarbage/Proof/Hmac/Sha256/X86/Init.lean b/lean/VerifiedGarbage/Proof/Hmac/Sha256/X86/Init.lean new file mode 100644 index 000000000..9cce6df1e --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Hmac/Sha256/X86/Init.lean @@ -0,0 +1,260 @@ +import VerifiedGarbage.Proof.Hmac.X86.Init +import VerifiedGarbage.Proof.Sha256.X86.Stream.CompressAt +import VerifiedGarbage.Impl.Hmac.Sha256.X86 + +/-! The efficient SHA-256 HMAC initializer, proved for any compressor. -/ +namespace VG.Proof.Hmac.Sha256.X86.Init +open VG VG.X86 VG.Impl.Hmac.X86 +open VG.Impl.Sha256.X86 (at_) +open VG.Impl.Sha256.X86.Stream (compressAt save restore saved) +open VG.Proof.Sha256.X86 (contains_offset) +open VG.Proof.Sha256.X86.Stream +open VG.Proof.Sha256.Stream (writeBytes writeBytes_frame writeBytes_append repr_congr) +open VG.Proof.Hmac.X86 +open VG.Proof.Hmac.Common (bytesAt_length writeState stateAt_writeState) +open VG.Spec.Sha256 (HashValue stateAt blockAt compress bytesAt Repr H0) +open VG.Spec.Hmac (xorPad ipad opad blockKey sha256) + +open VG.Proof.Hmac.X86.Init +variable {name : String} {code : Prog isa} + (hv : Verified X86.target code Proof.Sha256.compressX86) + (hnosp : NoSp code) (hstack : stackUse code = 0) +include hv hnosp hstack + +theorem compBuf_of {s₀ s : State} (hp : Pre s₀) {b : Reg} {x : BitVec 32} (hx : x = inn s₀ ∨ x = ou s₀) + (hb : b = .ebx ∨ b = .esi) (hrd : s.rd = s₀.rd) (hwr : s.wr = s₀.wr) (hbx : s.gpr b = x) + (hebp : s.gpr .ebp = scr s₀) (hsp : s.gpr .esp = esp₀ s₀) {Q : State → Prop} + (hQ : ∀ s', s'.rd = s₀.rd → s'.wr = s₀.wr → (∀ r ∈ calleeSaved, s'.gpr r = s.gpr r) → + Frame [⟨x.setWidth 64, 32⟩, ⟨scA s₀, 112⟩, stkR s₀] s.mem s'.mem → + stateAt s'.mem (x.setWidth 64) = + compress (stateAt s.mem (x.setWidth 64)) (blockAt s.mem (x.setWidth 64 + 32)) → Q s') : + WP isa (Impl.Hmac.Sha256.X86.compressBuf name code b) s Q := by + have fs := hp.scr_fit + have fsp := hp.sp_fit + obtain ⟨fx, dS, dK, hm⟩ : x.toNat + 96 ≤ 2 ^ 32 ∧ Region.Disjoint ⟨x.setWidth 64, 96⟩ (scR s₀) ∧ + (stkR s₀).Disjoint ⟨x.setWidth 64, 96⟩ ∧ (⟨x.setWidth 64, 96⟩ : Region) ∈ s₀.wr := by + rcases hx with rfl | rfl + · exact ⟨hp.in_fit, hp.i_s, hp.stk_i, by simp [hp.wr]⟩ + · exact ⟨hp.ou_fit, hp.o_s, hp.stk_o, by simp [hp.wr]⟩ + have hb' : b ≠ .eax := by rcases hb with rfl | rfl <;> decide + unfold Impl.Hmac.Sha256.X86.compressBuf + refine WP.seq (wp_mov fun s₃ u₃ => wp_addi fun s₄ u₄ => WP.block_nil ?_) + have g₄ : ∀ r, r ≠ .eax → s₄.gpr r = s.gpr r := fun r h => by rw [u₄.other r h, u₃.other r h] + have m₄ : s₄.mem = s.mem := by rw [u₄.mem, u₃.mem] + have rd₄ : s₄.rd = s₀.rd := by rw [u₄.rd, u₃.rd, hrd] + have wr₄ : s₄.wr = s₀.wr := by rw [u₄.wr, u₃.wr, hwr] + have eax₄ : s₄.gpr .eax = x + 32 := by rw [u₄.gpr, u₃.gpr, hbx] + have hbA : (x + 32).setWidth 64 = x.setWidth 64 + 32 := addr_eq (x := x) (k := 32) (by omega_nat) + have s32 : Region.Sub ⟨x.setWidth 64, 32⟩ ⟨x.setWidth 64, 96⟩ := sub32 _ + have s112 : Region.Sub ⟨scA s₀, 112⟩ (scR s₀) := Region.sub_prefix (by omega_nat) + have b64 : Region.Sub ⟨(x + 32).setWidth 64, 64⟩ ⟨x.setWidth 64, 96⟩ := by + rw [hbA]; exact sub_offset (off := 32) (by omega_nat) (by omega_nat) + refine compressAt_of hv hnosp hstack (st := x) (scr := scr s₀) (blk := x + 32) (E := esp₀ s₀) + (by rcases hb with rfl | rfl <;> decide) (by decide) (by rcases hb with rfl | rfl <;> decide) (by decide) + (by rw [g₄ _ (by decide), hsp]) (by rw [g₄ _ hb', hbx]) (by rw [g₄ _ (by decide), hebp]) eax₄ hp.sp_lo + (by omega_nat) (by rw [show (x + 32).toNat = x.toNat + 32 by + rw [BitVec.toNat_add]; exact Nat.mod_eq_of_lt (by simp; omega_nat)]; omega_nat) (by omega_nat) + ((dS.sub_left s32).sub_right s112) ?_ ((dS.sub_left b64).sub_right s112) + (dK.sub_right s32) (hp.stk_s.sub_right s112) (dK.sub_right b64) ?_ ?_ ?_ + · rw [hbA]; exact Offset.disjoint_base _ (d := 32) (by omega_nat) (by omega_nat) + · rw [rd₄, wr₄] + apply Covers.of_sub + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + subst hr + exact ⟨_, List.mem_append_right _ hm, 32, hbA, by simp⟩ + · rw [wr₄] + apply Covers.of_sub + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl + · exact ⟨_, hm, 0, by simp, by simp⟩ + · exact ⟨scR s₀, by simp [hp.wr], 0, by simp, by simp⟩ + · intro s' h₁ h₂ h₃ h₅ h₇ + rw [m₄] at h₅ h₇ + refine hQ s' (h₁.trans rd₄) (h₂.trans wr₄) (fun r hr => by + rw [h₃ r hr, g₄ r (by + simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl | rfl <;> decide)]) h₅ ?_ + rw [h₇, hbA] + +/-! ## Epilogue -/ + +theorem correct {s₀ : State} (hp : Pre s₀) : + WP isa (Impl.Hmac.Sha256.X86.init name code) s₀ fun s' => abiPreserved s₀ s' ∧ Proof.Hmac.initSha256X86.post s₀ s' := by + have hkl := hp.kl_le + have fi := hp.in_fit + have fo := hp.ou_fit + have fs := hp.scr_fit + unfold Impl.Hmac.Sha256.X86.init + refine WP.seq (WP.mono (prologue_ok hp) fun s₁ ⟨h₁, z₁⟩ => ?_) + -- The key. + refine WP.seq (WP.mono (Q := Buf s₀ (kl s₀)) ?_ fun s₂ h₂ => ?_) + · refine WP.ite (decide (kl s₀ = 0)) (by simp [eval, z₁]) (fun hb => WP.block_nil ?_) + (fun hb => key_loop_ok hp h₁ ?_) + · rw [of_decide_eq_true hb]; exact h₁.toBuf + · have := of_decide_eq_false hb; omega_nat + -- The padding. + refine WP.seq (wp_mov fun s₃ u₃ => wp_addi fun s₄ u₄ => wp_movi fun s₅ u₅ => + wp_cmp fun s₆ f₆ _ z₆ => WP.block_nil ?_) + have k₆ : ∀ r, r ≠ .eax → r ≠ .ecx → s₆.gpr r = s₂.gpr r := fun r h h' => by + rw [f₆.gpr, u₅.other r h', u₄.other r h, u₃.other r h] + have eax₆ : s₆.gpr .eax = inn s₀ + 96 := by + rw [f₆.gpr, u₅.other _ (by decide), u₄.gpr, u₃.gpr, h₂.ebx] + have hP : Pad s₀ (kl s₀) s₆ := + ⟨⟨h₂.j_le, by rw [f₆.rd, u₅.rd, u₄.rd, u₃.rd, h₂.rd], by rw [f₆.wr, u₅.wr, u₄.wr, u₃.wr, h₂.wr], + by rw [k₆ _ (by decide) (by decide), h₂.ebx], by rw [k₆ _ (by decide) (by decide), h₂.esi], + by rw [k₆ _ (by decide) (by decide), h₂.ebp], by rw [k₆ _ (by decide) (by decide), h₂.esp], + by rw [k₆ _ (by decide) (by decide), h₂.edx], by rw [f₆.mem, u₅.mem, u₄.mem, u₃.mem]; exact h₂.mem⟩, + eax₆, by rw [f₆.gpr, u₅.gpr]⟩ + have hz : s₆.zf = some (decide (kl s₀ = 64)) := by + rw [z₆, ← f₆.gpr, k₆ _ (by decide) (by decide), h₂.edx, eax₆, cmp_end _ hkl] + refine WP.seq (WP.mono (Q := Buf s₀ 64) ?_ fun s₇ h₇ => ?_) + · refine WP.ite (decide (kl s₀ = 64)) (by simp [eval, hz]) (fun hb => WP.block_nil ?_) + (fun hb => pad_loop_ok hp hP ?_) + · rw [← of_decide_eq_true hb]; exact hP.toBuf + · have := of_decide_eq_false hb; omega_nat + -- The outer buffer. + have hbufI : bytesAt s₇.mem (inA s₀ + 32) 64 = xorPad (K0 s₀) ipad := by + rw [h₇.mem.buf, List.take_of_length_le (by rw [K0_length s₀ hp])]; rfl + refine WP.seq ?_ + rw [← List.append_nil ((List.range 16).flatMap opadWord)] + refine xorWords_ok 16 [] s₇ _ h₇.ebx h₇.esi (by omega_nat) (by omega_nat) + (fun k hk => ⟨inR s₀, by simp [h₇.rd, h₇.wr, hp.wr], hp.in_in (by omega_nat) (by omega_nat)⟩) + (fun k hk => ⟨ouR s₀, by simp [h₇.wr, hp.wr], hp.ou_in (by omega_nat) (by omega_nat)⟩) + (hp.i_o.sep (contains_offset (by omega_nat) (by omega_nat)) (contains_offset (by omega_nat) (by omega_nat))) + fun s₈ g₈ rd₈ wr₈ m₈ => WP.block_nil ?_ + set ob := (bytesAt s₇.mem (inA s₀ + BitVec.ofNat 64 32) (4 * 16)).map (· ^^^ (0x6a : Byte)) with hob + have hobl : ob.length = 64 := by simp [ob, bytesAt_length] + have hob' : ob = xorPad (K0 s₀) opad := by + rw [hob, show 4 * 16 = 64 from rfl, show inA s₀ + BitVec.ofNat 64 32 = inA s₀ + 32 from rfl, hbufI, + xorPad_6a] + let bO : Region := ⟨ouA s₀ + BitVec.ofNat 64 32, 64⟩ + have sO : Region.Sub bO (ouR s₀) := sub_offset (by omega_nat) (by omega_nat) + have F₈ : Frame [bO] s₇.mem s₈.mem := by + rw [m₈]; exact writeBytes_frame _ _ _ (by rw [hobl]; exact Region.contains_self _ _) + have bOd : ∀ R : Region, R.Disjoint (ouR s₀) → ∀ r ∈ [bO], R.Disjoint r := fun R h r hr => by + simp only [List.mem_singleton] at hr; subst hr; exact h.sub_right sO + have stI₈ : stateAt s₈.mem (inA s₀) = H0 := by + rw [← h₇.mem.stI] + exact Proof.Sha256.Stream.stateAt_congr fun i hi => + frame_bytes F₈ (R := ⟨inA s₀, 32⟩) (bOd _ (hp.i_o.sub_left (sub32 _))) (by simp) hi + have bI₈ : bytesAt s₈.mem (inA s₀ + 32) 64 = xorPad (K0 s₀) ipad := by + rw [← hbufI] + exact Proof.Sha256.Stream.bytesAt_congr fun i hi => + frame_bytes F₈ (R := ⟨inA s₀ + 32, 64⟩) + (bOd _ (hp.i_o.sub_left (sub_offset (off := 32) (by omega_nat) (by omega_nat)))) (by simp) hi + have stO₈ : stateAt s₈.mem (ouA s₀) = H0 := by + rw [← h₇.mem.stO] + refine Proof.Sha256.Stream.stateAt_congr fun i hi => frame_bytes F₈ (R := ⟨ouA s₀, 32⟩) ?_ (by simp) hi + simp only [List.mem_singleton]; rintro r rfl + exact Offset.base_disjoint _ (e := 32) (by omega_nat) (by have := hp.ou_fit; omega_nat) + have bO₈ : bytesAt s₈.mem (ouA s₀ + 32) 64 = xorPad (K0 s₀) opad := by + rw [m₈, ← hob'] + have := VG.Proof.Hmac.Common.bytesAt_writeBytes_self s₇.mem (ouA s₀ + BitVec.ofNat 64 32) ob (by omega_nat) + rw [hobl] at this + exact this + have sv₈ : Saved s₀ s₈.mem := saved_frame h₇.mem.saved F₈ fun d h₁ h₂ r hr => by + simp only [List.mem_singleton] at hr; subst hr; exact save_disj hp (hp.o_s.sub_left sO) d h₁ h₂ + have f₈ : Frame [inR s₀, ouR s₀, scR s₀] s₀.mem s₈.mem := + h₇.mem.frame.trans (F₈.sub fun r hr => by + simp only [List.mem_singleton] at hr; subst hr; exact ⟨ouR s₀, by simp, sO⟩) + -- The inner block. + refine WP.seq (compBuf_of hv hnosp hstack hp (x := inn s₀) (.inl rfl) (b := .ebx) (.inl rfl) (by rw [rd₈, h₇.rd]) + (by rw [wr₈, h₇.wr]) (by rw [g₈ _ (by decide), h₇.ebx]) (by rw [g₈ _ (by decide), h₇.ebp]) + (by rw [g₈ _ (by decide), h₇.esp]) fun s₉ rd₉ wr₉ cs₉ fr₉ st₉ => ?_) + have hI₉ : Repr s₉.mem (inA s₀) (xorPad (K0 s₀) ipad) := + VG.Proof.Hmac.Common.repr_block stI₈ bI₈ (by simp [xorPad, K0_length s₀ hp]) st₉ + have dO : ∀ r ∈ [(⟨inA s₀, 32⟩ : Region), ⟨scA s₀, 112⟩, stkR s₀], Region.Disjoint (ouR s₀) r := by + simp only [List.mem_cons, List.not_mem_nil, or_false] + rintro r (rfl | rfl | rfl) + · exact hp.i_o.symm.sub_right (sub32 _) + · exact hp.o_s.sub_right (Region.sub_prefix (by omega_nat)) + · exact hp.stk_o.symm + have stO₉ : stateAt s₉.mem (ouA s₀) = H0 := by + rw [← stO₈] + exact Proof.Sha256.Stream.stateAt_congr fun i hi => + frame_bytes fr₉ (R := ⟨ouA s₀, 32⟩) (fun r hr => (dO r hr).sub_left (sub32 _)) (by simp) hi + have bO₉ : bytesAt s₉.mem (ouA s₀ + 32) 64 = xorPad (K0 s₀) opad := by + rw [← bO₈] + exact Proof.Sha256.Stream.bytesAt_congr fun i hi => + frame_bytes fr₉ (R := ⟨ouA s₀ + 32, 64⟩) + (fun r hr => (dO r hr).sub_left (sub_offset (off := 32) (by omega_nat) (by omega_nat))) (by simp) hi + have sv₉ : Saved s₀ s₉.mem := saved_frame sv₈ fr₉ fun d h₁ h₂ r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact save_disj hp (hp.i_s.sub_left (sub32 _)) d h₁ h₂ + · exact save_disj112 hp d h₁ h₂ + · exact save_disj hp hp.stk_s d h₁ h₂ + have f₉ : Frame (allR s₀) s₀.mem s₉.mem := (f₈.mono (by simp)).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 + · exact ⟨inR s₀, by simp, sub32 _⟩ + · exact ⟨scR s₀, by simp, Region.sub_prefix (by omega_nat)⟩ + · exact ⟨stkR s₀, by simp, fun _ h => h⟩) + have cs₉' : ∀ r ∈ calleeSaved, s₉.gpr r = s₇.gpr r := fun r hr => by + rw [cs₉ r hr, g₈ r (callee_ne_eax hr)] + -- The outer block. + refine WP.seq (compBuf_of hv hnosp hstack hp (x := ou s₀) (.inr rfl) (b := .esi) (.inr rfl) rd₉ wr₉ + (by rw [cs₉' _ (by decide), h₇.esi]) (by rw [cs₉' _ (by decide), h₇.ebp]) + (by rw [cs₉' _ (by decide), h₇.esp]) fun s₁₀ rd₁₀ wr₁₀ cs₁₀ fr₁₀ st₁₀ => ?_) + have hO : Repr s₁₀.mem (ouA s₀) (xorPad (K0 s₀) opad) := + VG.Proof.Hmac.Common.repr_block stO₉ bO₉ (by simp [xorPad, K0_length s₀ hp]) st₁₀ + have hI : Repr s₁₀.mem (inA s₀) (xorPad (K0 s₀) ipad) := by + refine repr_congr (fun i hi => frame_bytes fr₁₀ (R := inR s₀) ?_ (by simp) hi) hI₉ + simp only [List.mem_cons, List.not_mem_nil, or_false] + rintro r (rfl | rfl | rfl) + · exact hp.i_o.sub_right (sub32 _) + · exact hp.i_s.sub_right (Region.sub_prefix (by omega_nat)) + · exact hp.stk_i.symm + have sv₁₀ : Saved s₀ s₁₀.mem := saved_frame sv₉ fr₁₀ fun d h₁ h₂ r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact save_disj hp (hp.o_s.sub_left (sub32 _)) d h₁ h₂ + · exact save_disj112 hp d h₁ h₂ + · exact save_disj hp hp.stk_s d h₁ h₂ + have f₁₀ : Frame (allR s₀) s₀.mem s₁₀.mem := 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 + · exact ⟨ouR s₀, by simp, sub32 _⟩ + · exact ⟨scR s₀, by simp, Region.sub_prefix (by omega_nat)⟩ + · exact ⟨stkR s₀, by simp, fun _ h => h⟩) + have cs₁₀' : ∀ r ∈ calleeSaved, s₁₀.gpr r = s₇.gpr r := fun r hr => by rw [cs₁₀ r hr, cs₉' r hr] + -- Epilogue. + refine WP.mono (epilogue_ok hp rd₁₀ wr₁₀ (by rw [cs₁₀' _ (by decide), h₇.ebp]) + (by rw [cs₁₀' _ (by decide), h₇.esp]) sv₁₀) fun s' ⟨m', cs'⟩ => ⟨⟨cs', ?_⟩, ?_⟩ + · rw [m'] + refine f₁₀.readW (r := retR s₀) (Region.contains_self _ _) ?_ (by decide) + intro r hr + simp only [allR, List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl | rfl + exacts [hp.ret_i, hp.ret_o, hp.ret_s, ret_a hp, ret_stk hp] + · show Repr s'.mem (inA s₀) (xorPad (blockKey sha256 (bytesAt s₀.mem (kA s₀) (kl s₀))) ipad) ∧ + Repr s'.mem (ouA s₀) (xorPad (blockKey sha256 (bytesAt s₀.mem (kA s₀) (kl s₀))) opad) + rw [blockKey_eq hp, m'] + exact ⟨hI, hO⟩ + +local macro "narrow" loc:(Lean.Parser.Tactic.location)? : tactic => + `(tactic| simp only [Proof.Hmac.initSha256X86, VG.Proof.Hmac.X86.Init.initWide, VG.Proof.Hmac.X86.Init.narrowWr, VG.X86.arg_withRegions, VG.X86.argAddr_withRegions, + VG.X86.State.withRegions_gpr, VG.X86.State.withRegions_mem, VG.X86.State.withRegions_rd, + VG.X86.State.withRegions_wr] $(loc)?) + +theorem verified + (hct : ConstantTime isa Proof.Hmac.initSha256X86.pre Proof.Hmac.initSha256X86.pub + (Impl.Hmac.Sha256.X86.init name code)) : + Verified X86.target (Impl.Hmac.Sha256.X86.init name code) (Spec.Hmac.initSha256Contract X86.abi 20) := + have hsat := initWide_implies.sat_left + (Verified.widen (Verified.of_correct (fun s hs => by + obtain ⟨t, s', he, h⟩ := correct hv hnosp hstack (pre_of hs) + exact ⟨t, s', he, h⟩) hct + (.refl (hsat.elim fun s hs => ⟨_, initWide_pre s hs⟩))) + narrowWr initWide_pre + (fun _ h => by + obtain ⟨_, _, h₃, _⟩ := h + rw [h₃] + exact .cons (Region.prefix_of_ble rfl) (.cons (Region.prefix_of_ble rfl) + (.cons (Region.prefix_of_ble rfl) (.cons (Region.prefix_of_ble rfl) .nil)))) + (fun _ _ _ h => by narrow at h ⊢; exact h) + (fun _ _ _ _ h => by narrow; exact h) hsat).of_implies initWide_implies + +end VG.Proof.Hmac.Sha256.X86.Init diff --git a/lean/VerifiedGarbage/Proof/Hmac/X86/Finalize.lean b/lean/VerifiedGarbage/Proof/Hmac/X86/Finalize.lean index cb7289a6e..c5f2e435c 100644 --- a/lean/VerifiedGarbage/Proof/Hmac/X86/Finalize.lean +++ b/lean/VerifiedGarbage/Proof/Hmac/X86/Finalize.lean @@ -15,7 +15,9 @@ import VerifiedGarbage.Proof.Framework.OmegaLit /-! # HMAC-SHA-256 on x86 (32-bit): `finalize` -Untrusted: everything here is checked by Lean. Lemmas `init` uses too, then +Untrusted: everything here is checked by Lean. The compressor-dependent +correctness proof is generic in `Proof/Hmac/Sha256/X86/Finalize.lean`; this module keeps +the shared memory, state and scalar constant-time facts. Lemmas `init` uses too, then `finalize`. -/ @@ -546,17 +548,6 @@ theorem finalizeHash_nosp : NoSp finalizeHash := NoSp.of_all (by lit_decide) theorem finalizeHash_stack : stackUse finalizeHash = 20 := by lit_decide -/-- `vg_sha256_finalize` up to writing the digest, from its precondition. -/ -theorem hash_ok {s : State} (hp : SPre s) : WP isa finalizeHash s (SDone s) := by - rw [finalizeHash_eq, ← VG.Proof.Sha256.X86.Stream.Finalize.seq_assoc] - refine WP.seq (WP.mono (VG.Proof.Sha256.X86.Stream.Finalize.prologue_ok hp) fun s₁ ⟨k, hL⟩ => ?_) - refine WP.loop (M := isa) (fun i s' => ∃ n, VG.Proof.Sha256.X86.Stream.Finalize.LInv s i n s') ?_ k s₁ ⟨_, hL⟩ - rintro i s' ⟨n, hL⟩ - refine WP.mono (VG.Proof.Sha256.X86.Stream.Finalize.body_ok hp hL) fun s'' h => ?_ - rcases h with ⟨he, hD⟩ | ⟨he, rfl, hL'⟩ - · exact .inl ⟨he, hD⟩ - · exact .inr ⟨he, 0, by omega_nat, 0, hL'⟩ - /-- The state after the prologue, with the permissions of `vg_sha256_finalize`. -/ abbrev narrow (s₀ s : State) : State := s.withRegions [] (finW s₀) @@ -864,50 +855,6 @@ theorem blk_eq {s₀ : State} (hp : Pre s₀) : (inn s₀ + 32).setWidth 64 = in show addr (inn s₀) 32 = _ exact addr_eq (by have := hp.in_fit; omega_nat) -theorem comp_ok {s₀ s : State} (hp : Pre s₀) (hrd : s.rd = s₀.rd) (hwr : s.wr = s₀.wr) - (hsp : s.gpr .esp = esp₀ s₀) (hebx : s.gpr .ebx = inn s₀) (hebp : s.gpr .ebp = scr s₀) - (heax : s.gpr .eax = inn s₀ + 32) {Q : State → Prop} - (hQ : ∀ s', s'.rd = s.rd → s'.wr = s.wr → (∀ r ∈ calleeSaved, s'.gpr r = s.gpr r) → - Frame [⟨inA s₀, 32⟩, ⟨scA s₀, 112⟩, stkR s₀] s.mem s'.mem → - stateAt s'.mem (inA s₀) = - compress (stateAt s.mem (inA s₀)) (blockAt s.mem (inA s₀ + BitVec.ofNat 64 32)) → Q s') : - WP isa (compressAt .ebx .ebp) s Q := by - have fi := hp.in_fit - have fs := hp.scr_fit - have fsp := hp.sp_fit - have hb := blk_eq hp - have s32 : Region.Sub ⟨inA s₀, 32⟩ (inR s₀) := Region.sub_prefix (by omega_nat) - have s112 : Region.Sub ⟨scA s₀, 112⟩ (scR s₀) := Region.sub_prefix (by omega_nat) - have b64 : Region.Sub ⟨(inn s₀ + 32).setWidth 64, 64⟩ (inR s₀) := by rw [hb]; exact sub_offset (by omega_nat) (by omega_nat) - refine compressAt_ok (st := inn s₀) (scr := scr s₀) (blk := inn s₀ + 32) (E := esp₀ s₀) - (by decide) (by decide) (by decide) (by decide) hsp hebx hebp heax hp.sp_lo - (by omega_nat) (by rw [show (inn s₀ + 32).toNat = (inn s₀).toNat + 32 by - rw [BitVec.toNat_add]; exact Nat.mod_eq_of_lt (by simp; omega_nat)]; omega_nat) (by omega_nat) - ((hp.in_scr.sub_left s32).sub_right s112) ?_ ((hp.in_scr.sub_left b64).sub_right s112) - (hp.stk_in.sub_right s32) (hp.stk_scr.sub_right s112) (hp.stk_in.sub_right b64) ?_ ?_ ?_ - · rw [hb] - intro a h₁ h₂ - simp only [Region.Contains] at h₁ h₂ - have := sep_off (inA s₀) (d := 32) (e := 0) (n := 64) (k := 32) (by omega_nat) (by omega_nat) (by omega_nat) a - (by omega_nat) (by simp at h₂ ⊢; omega_nat) - exact this - · apply Covers.of_sub - intro r hr - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - subst hr - exact ⟨inR s₀, by simp [hrd, hwr, hp.wr], 32, hb, by simp⟩ - · apply Covers.of_sub - intro r hr - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl - · exact ⟨inR s₀, by simp [hwr, hp.wr], 0, by simp, by simp⟩ - · exact ⟨scR s₀, by simp [hwr, hp.wr], 0, by simp, by simp⟩ - · intro s' h₁ h₂ h₃ h₄ h₇ - rw [hb] at h₇ - exact hQ s' h₁ h₂ h₃ h₄ h₇ - -/-! ## Writing the MAC -/ - theorem out_ok {s₀ s : State} (hp : Pre s₀) (hrd : s.rd = s₀.rd) (hwr : s.wr = s₀.wr) (hebx : s.gpr .ebx = inn s₀) (hebp : s.gpr .ebp = scr s₀) (hsp : s.gpr .esp = esp₀ s₀) (hout : s.mem.readW (addr (scr s₀) 136) 32 = out s₀) @@ -996,186 +943,6 @@ theorem outer_hash {k0 d : List Byte} (hk : k0.length = 64) (hd : d.length = 32) rw [hr, hlb, padBytes_eq] simp only [List.append_assoc] -theorem correct {s₀ : State} (hp : Pre s₀) : - WP isa finalize s₀ fun s' => abiPreserved s₀ s' ∧ Proof.Hmac.finalizeSha256X86.post s₀ s' := by - have fi := hp.in_fit - have fs := hp.scr_fit - have fsp := hp.sp_fit - unfold finalize - refine WP.seq (WP.mono (pro_ok hp) fun s₁ h₁ => ?_) - have sp₁ : s₁.gpr .esp = esp₀ s₀ := h₁.gpr _ (by decide) (by decide) - have s160 : Region.Sub ⟨scA s₀, 160⟩ (scR s₀) := Region.sub_prefix (by omega_nat) - have a20 : Region.Sub ⟨addr (esp₀ s₀) 4, 20⟩ (argR s₀) := Region.sub_prefix (by omega_nat) - have finSub : ∀ r ∈ finW s₀ ++ [stkR s₀], ∃ r' ∈ allR s₀, Region.Sub r r' := by - intro r hr - simp only [finW, 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 - · exact ⟨inR s₀, by simp, fun _ h => h⟩ - · exact ⟨outR s₀, by simp, fun _ h => h⟩ - · exact ⟨scR s₀, by simp, s160⟩ - · exact ⟨argR s₀, by simp, a20⟩ - · exact ⟨stkR s₀, by simp, fun _ h => h⟩ - refine WP.seq (WP.narrowSp (hash_ok (narrow_pre hp h₁)) ?_ ?_ finalizeHash_nosp - (by rw [finalizeHash_stack, sp₁]; exact hp.sp_lo) fun sD rdD wrD frD hD => ?_) - · rw [h₁.rd, h₁.wr, hp.rd, hp.wr] - apply Covers.of_sub - intro r hr - simp only [List.nil_append, finW, List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl | rfl - · exact ⟨inR s₀, by simp, 0, by simp, by simp⟩ - · exact ⟨outR s₀, by simp, 0, by simp, by simp⟩ - · exact ⟨scR s₀, by simp, 0, by simp, by simp⟩ - · exact ⟨argR s₀, by simp, 0, by simp, by simp⟩ - · rw [h₁.wr, hp.wr] - apply Covers.of_sub - intro r hr - simp only [finW, List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl | rfl - · exact ⟨inR s₀, by simp, 0, by simp, by simp⟩ - · exact ⟨outR s₀, by simp, 0, by simp, by simp⟩ - · exact ⟨scR s₀, by simp, 0, by simp, by simp⟩ - · exact ⟨argR s₀, by simp, 0, by simp, by simp⟩ - rw [finalizeHash_stack, sp₁] at frD - obtain ⟨hC, hHash⟩ := hD - have e3 : VG.Proof.Sha256.X86.Stream.Finalize.out (narrow s₀ s₁) = out s₀ := narrow_arg hp h₁ (by omega_nat) - have e4 : VG.Proof.Sha256.X86.Stream.Finalize.scr (narrow s₀ s₁) = scr s₀ := narrow_arg hp h₁ (by omega_nat) - have outpD : sD.mem.readW (addr (scr s₀) 136) 32 = out s₀ := by - have := hC.outp; rw [e4, e3] at this; exact this - have savedD : ∀ p ∈ saved, sD.mem.readW (addr (scr s₀) p.2) 32 = s₀.gpr p.1 := by - intro p hp' - have := hC.saved p hp' - rw [e4] at this - refine this.trans ?_ - show s₁.gpr p.1 = s₀.gpr p.1 - simp only [saved, List.mem_cons, List.not_mem_nil, or_false] at hp' - rcases hp' with rfl | rfl | rfl | rfl <;> exact h₁.gpr _ (by decide) (by decide) - have ebxD : sD.gpr .ebx = inn s₀ := hC.ebx.trans (narrow_arg hp h₁ (i := 0) (by omega_nat)) - have ebpD : sD.gpr .ebp = scr s₀ := hC.ebp.trans (narrow_arg hp h₁ (i := 4) (by omega_nat)) - have spD : sD.gpr .esp = esp₀ s₀ := hC.esp.trans sp₁ - have rdD' : sD.rd = s₀.rd := rdD.trans h₁.rd - have wrD' : sD.wr = s₀.wr := wrD.trans h₁.wr - -- `scratch[176..180)`, where `outer` is, lies outside what `finalizeHash` writes. - have w176 : ∀ r ∈ finW s₀ ++ [stkR s₀], Region.Disjoint ⟨addr (scr s₀) 176, 4⟩ r := by - have hs : Region.Sub ⟨addr (scr s₀) 176, 4⟩ (scR s₀) := hp.scr_sub (by omega_nat) - intro r hr - simp only [finW, 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 - · exact (hp.in_scr.symm.sub_left hs) - · exact (hp.out_scr.symm.sub_left hs) - · rw [addr_eq (by omega_nat)]; exact Offset.disjoint_base _ (by omega_nat) (by omega_nat) - · exact (hp.a_scr.symm.sub_left hs).sub_right a20 - · exact hp.stk_scr.symm.sub_left hs - have ouD : sD.mem.readW (addr (scr s₀) 176) 32 = ou s₀ := by - rw [frD.readW (Region.contains_self _ _) w176 (by decide), h₁.mem, proMem_176 hp] - refine WP.seq (WP.mono (mid_ok hp ⟨rdD', wrD', ebxD, ebpD, spD, ouD⟩) fun s₃ h₃ => ?_) - have sp₃ : s₃.gpr .esp = esp₀ s₀ := by rw [h₃.gpr _ (by decide) (by decide) (by decide), spD] - refine WP.seq (comp_ok hp h₃.rd h₃.wr sp₃ (by rw [h₃.gpr _ (by decide) (by decide) (by decide), ebxD]) - (by rw [h₃.gpr _ (by decide) (by decide) (by decide), ebpD]) h₃.eax fun s₄ rd₄ wr₄ cs₄ fr₄ st₄ => ?_) - -- Words of the scratch space that neither the middle block nor the compression writes. - have keep : ∀ d, 112 ≤ d → d + 4 ≤ 160 → - s₄.mem.readW (addr (scr s₀) d) 32 = sD.mem.readW (addr (scr s₀) d) 32 := by - intro d h₁ h₂ - have hs : Region.Sub ⟨addr (scr s₀) d, 4⟩ (scR s₀) := hp.scr_sub (by omega_nat) - rw [fr₄.readW (Region.contains_self _ _) ?_ (by decide), h₃.mem, - (midMem_frame sD.mem).readW (Region.contains_self _ _) ?_ (by decide)] - · intro r hr - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl - · exact hp.in_scr.symm.sub_left hs - · exact hp.a_scr.symm.sub_left hs - · intro r hr - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl - · exact (hp.in_scr.symm.sub_left hs).sub_right (Region.sub_prefix (by omega_nat)) - · rw [addr_eq (by omega_nat)]; exact Offset.disjoint_base _ (by omega_nat) (by omega_nat) - · exact hp.stk_scr.symm.sub_left hs - have csD : ∀ r ∈ calleeSaved, s₄.gpr r = sD.gpr r := fun r hr => by - rw [cs₄ r hr, h₃.gpr r ?_ ?_ ?_] <;> - · simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl | rfl | rfl <;> decide - refine WP.mono (out_ok hp (rd₄.trans h₃.rd) (wr₄.trans h₃.wr) (by rw [csD _ (by decide), ebxD]) - (by rw [csD _ (by decide), ebpD]) (by rw [csD _ (by decide), spD]) - (by rw [keep 136 (by omega_nat) (by omega_nat)]; exact outpD) - fun p hp' => ?_) fun s' ⟨rd', wr', cs', m'⟩ => ?_ - · have hd : 112 ≤ p.2 ∧ p.2 + 4 ≤ 128 := by - simp only [saved, List.mem_cons, List.not_mem_nil, or_false] at hp' - rcases hp' with rfl | rfl | rfl | rfl <;> simp - rw [keep p.2 hd.1 (by omega_nat)] - exact savedD p hp' - -- Everything written is within our regions. - have f1 : Frame (allR s₀) s₀.mem s₁.mem := by rw [h₁.mem]; exact (proMem_frame hp).mono (by simp) - have f2 : Frame (allR s₀) s₁.mem sD.mem := frD.sub finSub - have f3 : Frame (allR s₀) sD.mem s₃.mem := by rw [h₃.mem]; exact (midMem_frame sD.mem).mono (by simp) - have f4 : Frame (allR s₀) s₃.mem s₄.mem := by - refine fr₄.sub fun r hr => ?_ - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl - · exact ⟨inR s₀, by simp, Region.sub_prefix (by omega_nat)⟩ - · exact ⟨scR s₀, by simp, Region.sub_prefix (by omega_nat)⟩ - · exact ⟨stkR s₀, by simp, fun _ h => h⟩ - have f5 : Frame (allR s₀) s₄.mem s'.mem := by - rw [m'] - refine (writeBytes_frame (R := outR s₀) _ _ _ ?_).mono (by simp) - rw [beWords_length]; exact contains_offset (by omega_nat) (by omega_nat) - have F : Frame (allR s₀) s₀.mem s'.mem := f1.trans (f2.trans (f3.trans (f4.trans f5))) - refine ⟨⟨cs', F.readW (r := retR s₀) (Region.contains_self _ _) ?_ (by decide)⟩, ?_⟩ - · intro r hr - simp only [allR, List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl | rfl | rfl - exacts [hp.ret_in, hp.ret_out, hp.ret_scr, ret_a hp, ret_stk hp] - intro k0 text hk hin hcnt hout - -- The inner digest. - have e0 : VG.Proof.Sha256.X86.Stream.Finalize.st (narrow s₀ s₁) = inn s₀ := narrow_arg hp h₁ (by omega_nat) - have oD : ∀ r ∈ allR s₀, (ouR s₀).Disjoint r := by - intro r hr - simp only [allR, List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl | rfl | rfl - exacts [hp.o_in, hp.o_out, hp.o_scr, hp.o_a, hp.stk_ou.symm] - have hR₀ : VG.Proof.Sha256.X86.Stream.Finalize.R₀ (narrow s₀ s₁) (xorPad k0 ipad ++ text) := by - refine ⟨?_, ?_⟩ - · show Repr s₁.mem ((VG.Proof.Sha256.X86.Stream.Finalize.st (narrow s₀ s₁)).setWidth 64) _ - rw [e0] - refine repr_congr (fun i hi => ?_) hin - rw [h₁.mem] - refine frame_bytes (proMem_frame hp) (R := inR s₀) (fun r hr => ?_) (by simp) hi - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl - exacts [hp.in_scr, hp.a_in.symm] - · show countX86 (narrow s₀ s₁) = _ - simp only [countX86] - rw [narrow_arg hp h₁ (i := 2) (by omega_nat), narrow_arg hp h₁ (i := 1) (by omega_nat)] - simp only [List.getD_cons_succ, List.getD_cons_zero, List.length_append, xorPad_length, hk] - exact hcnt - have hdig : Spec.Sha256.hash (xorPad k0 ipad ++ text) = beWords sD.mem (inn s₀) 0 8 := by - have e0A : VG.Proof.Sha256.X86.Stream.Finalize.stA (narrow s₀ s₁) = inA s₀ := by - show (VG.Proof.Sha256.X86.Stream.Finalize.st (narrow s₀ s₁)).setWidth 64 = _ - rw [e0] - rw [hHash _ hR₀, beWords_stateAt _ (by omega_nat), e0A, State.withRegions_mem] - -- The outer hash value. - have hou : stateAt s₃.mem (inA s₀) = Spec.Sha256.compressList Spec.Sha256.H0 (xorPad k0 opad) 1 := by - rw [h₃.mem, midMem_state, - VG.Proof.Sha256.Stream.stateAt_congr (mem := s₀.mem) fun i hi => - frame_bytes (f1.trans f2) (R := ouR s₀) oD (by simp) (by simp; omega_nat), - hout.1, xorPad_length, hk] - -- The block after it. - have hblk : blockAt s₃.mem (inA s₀ + BitVec.ofNat 64 32) = - parseBlock fun t => (beWords sD.mem (inn s₀) 0 8 ++ padBytes).getD t 0 := by - have hb := midMem_block (s₀ := s₀) sD.mem - rw [← h₃.mem] at hb - exact VG.Proof.Sha256.Stream.parseBlock_congr fun k hk => bytesAt_getD hb (by omega_nat) - -- The MAC. - have hmac : bytesAt s'.mem (outA s₀) 32 = beWords s₄.mem (inn s₀) 0 8 := by - rw [m', show outA s₀ + BitVec.ofNat 64 0 = outA s₀ by simp] - have := VG.Proof.Hmac.Common.bytesAt_writeBytes_self s₄.mem (outA s₀) - (beWords s₄.mem (inn s₀) 0 8) (by rw [beWords_length]; omega_nat) - rw [beWords_length] at this - simpa only [Nat.reduceMul] using this - show bytesAt s'.mem (outA s₀) 32 = _ - rw [hmac, beWords_stateAt _ (by omega_nat), st₄, hou, hblk] - simp only [hmacBlockKey, sha256] - rw [hdig, outer_hash hk (beWords_length _ _ _ _)] - - /-! ## Constant time -/ /-- The initial taint: `esp + 4` is the base of the (public) arguments, whose @@ -1281,12 +1048,6 @@ def sat : State where rd := [⟨0x1100, 96⟩] wr := [⟨0x1000, 96⟩, ⟨0x2000, 32⟩, ⟨0x3000, 240⟩, ⟨0x4004, 24⟩] -theorem finalize_correct (s : State) (hs : Proof.Hmac.finalizeSha256X86.pre s) : - ∃ t s', Exec isa finalize s t s' ∧ abiPreserved s s' ∧ - Proof.Hmac.finalizeSha256X86.post s s' := by - obtain ⟨t, s', he, h⟩ := correct (pre_of hs) - exact ⟨t, s', he, h⟩ - /-- What the analysis forgets wherever the hint records a taint (`taint_decide_weaken`): the public words of `inner` and `out` (data, never addresses), the count in `scratch[128..136)` (only data too), and the @@ -1368,20 +1129,4 @@ theorem finalizeWide_implies : X86.argBytes] [a0, a1, a4, a5, e, esp] using wideSat -/-- The proof is written against `finalizeSha256X86`, widened to the shared -contract's scratch. -/ -theorem finalize_verified : - Verified X86.target Impl.Hmac.X86.finalize (Spec.Hmac.finalizeSha256OutContract X86.abi 20) := - have hsat := finalizeWide_implies.sat_left - (Verified.widen (Verified.of_correct finalize_correct finalize_ct - (.refl (hsat.elim fun s hs => ⟨_, finalizeWide_pre s hs⟩))) - narrowWr finalizeWide_pre - (fun _ h => by - obtain ⟨_, h₂, _⟩ := h - rw [h₂] - exact .cons (Region.prefix_of_ble rfl) (.cons (Region.prefix_of_ble rfl) - (.cons (Region.prefix_of_ble rfl) (.cons (Region.prefix_of_ble rfl) .nil)))) - (fun _ _ _ h => by narrow at h ⊢; exact h) - (fun _ _ _ _ h => by narrow; exact h) hsat).of_implies finalizeWide_implies - end VG.Proof.Hmac.X86.Finalize diff --git a/lean/VerifiedGarbage/Proof/Hmac/X86/Init.lean b/lean/VerifiedGarbage/Proof/Hmac/X86/Init.lean index 32f4a2ff6..8325d4306 100644 --- a/lean/VerifiedGarbage/Proof/Hmac/X86/Init.lean +++ b/lean/VerifiedGarbage/Proof/Hmac/X86/Init.lean @@ -8,14 +8,16 @@ import VerifiedGarbage.Proof.Framework.OmegaLit /-! # HMAC-SHA-256 on x86 (32-bit): `init` -Untrusted: everything here is checked by Lean. The prologue saves our +Untrusted: everything here is checked by Lean. The compressor-dependent +correctness proof is generic in `Proof/Hmac/Sha256/X86/Init.lean`; this module keeps +the shared memory, state and scalar constant-time facts. The prologue saves our caller's registers in `scratch[112..128)` and stores `H⁽⁰⁾` in both states; the key loop and the pad loop then fill the inner buffer with `K₀ ⊕ ipad` a byte at a time (invariant `Buf`: `j` bytes written, `edx` at byte `j`), the outer buffer is computed from it a word at a time (`xorWords_ok`), and each buffer is compressed by calling the compression function -(`compBuf_ok`, via `compressAt_ok`, using the 20 bytes below `esp`), after which each state represents its -block (`Common.repr_block`). +through the generic proof, using the 20 bytes below `esp`. Each state then +represents its block (`Common.repr_block`). -/ namespace VG.Proof.Hmac.X86.Init @@ -693,65 +695,6 @@ theorem xorPad_6a (k : List Byte) : (xorPad k ipad).map (· ^^^ 0x6a) = xorPad k /-! ## The compressions -/ -theorem compBuf_ok {s₀ s : State} (hp : Pre s₀) {b : Reg} {x : BitVec 32} (hx : x = inn s₀ ∨ x = ou s₀) - (hb : b = .ebx ∨ b = .esi) (hrd : s.rd = s₀.rd) (hwr : s.wr = s₀.wr) (hbx : s.gpr b = x) - (hebp : s.gpr .ebp = scr s₀) (hsp : s.gpr .esp = esp₀ s₀) {Q : State → Prop} - (hQ : ∀ s', s'.rd = s₀.rd → s'.wr = s₀.wr → (∀ r ∈ calleeSaved, s'.gpr r = s.gpr r) → - Frame [⟨x.setWidth 64, 32⟩, ⟨scA s₀, 112⟩, stkR s₀] s.mem s'.mem → - stateAt s'.mem (x.setWidth 64) = - compress (stateAt s.mem (x.setWidth 64)) (blockAt s.mem (x.setWidth 64 + 32)) → Q s') : - WP isa (compressBuf b) s Q := by - have fs := hp.scr_fit - have fsp := hp.sp_fit - obtain ⟨fx, dS, dK, hm⟩ : x.toNat + 96 ≤ 2 ^ 32 ∧ Region.Disjoint ⟨x.setWidth 64, 96⟩ (scR s₀) ∧ - (stkR s₀).Disjoint ⟨x.setWidth 64, 96⟩ ∧ (⟨x.setWidth 64, 96⟩ : Region) ∈ s₀.wr := by - rcases hx with rfl | rfl - · exact ⟨hp.in_fit, hp.i_s, hp.stk_i, by simp [hp.wr]⟩ - · exact ⟨hp.ou_fit, hp.o_s, hp.stk_o, by simp [hp.wr]⟩ - have hb' : b ≠ .eax := by rcases hb with rfl | rfl <;> decide - unfold compressBuf - refine WP.seq (wp_mov fun s₃ u₃ => wp_addi fun s₄ u₄ => WP.block_nil ?_) - have g₄ : ∀ r, r ≠ .eax → s₄.gpr r = s.gpr r := fun r h => by rw [u₄.other r h, u₃.other r h] - have m₄ : s₄.mem = s.mem := by rw [u₄.mem, u₃.mem] - have rd₄ : s₄.rd = s₀.rd := by rw [u₄.rd, u₃.rd, hrd] - have wr₄ : s₄.wr = s₀.wr := by rw [u₄.wr, u₃.wr, hwr] - have eax₄ : s₄.gpr .eax = x + 32 := by rw [u₄.gpr, u₃.gpr, hbx] - have hbA : (x + 32).setWidth 64 = x.setWidth 64 + 32 := addr_eq (x := x) (k := 32) (by omega_nat) - have s32 : Region.Sub ⟨x.setWidth 64, 32⟩ ⟨x.setWidth 64, 96⟩ := sub32 _ - have s112 : Region.Sub ⟨scA s₀, 112⟩ (scR s₀) := Region.sub_prefix (by omega_nat) - have b64 : Region.Sub ⟨(x + 32).setWidth 64, 64⟩ ⟨x.setWidth 64, 96⟩ := by - rw [hbA]; exact sub_offset (off := 32) (by omega_nat) (by omega_nat) - refine compressAt_ok (st := x) (scr := scr s₀) (blk := x + 32) (E := esp₀ s₀) - (by rcases hb with rfl | rfl <;> decide) (by decide) (by rcases hb with rfl | rfl <;> decide) (by decide) - (by rw [g₄ _ (by decide), hsp]) (by rw [g₄ _ hb', hbx]) (by rw [g₄ _ (by decide), hebp]) eax₄ hp.sp_lo - (by omega_nat) (by rw [show (x + 32).toNat = x.toNat + 32 by - rw [BitVec.toNat_add]; exact Nat.mod_eq_of_lt (by simp; omega_nat)]; omega_nat) (by omega_nat) - ((dS.sub_left s32).sub_right s112) ?_ ((dS.sub_left b64).sub_right s112) - (dK.sub_right s32) (hp.stk_s.sub_right s112) (dK.sub_right b64) ?_ ?_ ?_ - · rw [hbA]; exact Offset.disjoint_base _ (d := 32) (by omega_nat) (by omega_nat) - · rw [rd₄, wr₄] - apply Covers.of_sub - intro r hr - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - subst hr - exact ⟨_, List.mem_append_right _ hm, 32, hbA, by simp⟩ - · rw [wr₄] - apply Covers.of_sub - intro r hr - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl - · exact ⟨_, hm, 0, by simp, by simp⟩ - · exact ⟨scR s₀, by simp [hp.wr], 0, by simp, by simp⟩ - · intro s' h₁ h₂ h₃ h₅ h₇ - rw [m₄] at h₅ h₇ - refine hQ s' (h₁.trans rd₄) (h₂.trans wr₄) (fun r hr => by - rw [h₃ r hr, g₄ r (by - simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl | rfl | rfl <;> decide)]) h₅ ?_ - rw [h₇, hbA] - -/-! ## Epilogue -/ - theorem epilogue_ok {s₀ s : State} (hp : Pre s₀) (hrd : s.rd = s₀.rd) (hwr : s.wr = s₀.wr) (hebp : s.gpr .ebp = scr s₀) (hsp : s.gpr .esp = esp₀ s₀) (hsv : Saved s₀ s.mem) : WP isa (.block (.mov .eax (.reg .ebp) :: restore .eax)) s fun s' => @@ -796,160 +739,6 @@ theorem callee_ne_eax {r : Reg} (hr : r ∈ calleeSaved) : r ≠ .eax := by simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr rcases hr with rfl | rfl | rfl | rfl | rfl <;> decide -theorem correct {s₀ : State} (hp : Pre s₀) : - WP isa init s₀ fun s' => abiPreserved s₀ s' ∧ Proof.Hmac.initSha256X86.post s₀ s' := by - have hkl := hp.kl_le - have fi := hp.in_fit - have fo := hp.ou_fit - have fs := hp.scr_fit - unfold init - refine WP.seq (WP.mono (prologue_ok hp) fun s₁ ⟨h₁, z₁⟩ => ?_) - -- The key. - refine WP.seq (WP.mono (Q := Buf s₀ (kl s₀)) ?_ fun s₂ h₂ => ?_) - · refine WP.ite (decide (kl s₀ = 0)) (by simp [eval, z₁]) (fun hb => WP.block_nil ?_) - (fun hb => key_loop_ok hp h₁ ?_) - · rw [of_decide_eq_true hb]; exact h₁.toBuf - · have := of_decide_eq_false hb; omega_nat - -- The padding. - refine WP.seq (wp_mov fun s₃ u₃ => wp_addi fun s₄ u₄ => wp_movi fun s₅ u₅ => - wp_cmp fun s₆ f₆ _ z₆ => WP.block_nil ?_) - have k₆ : ∀ r, r ≠ .eax → r ≠ .ecx → s₆.gpr r = s₂.gpr r := fun r h h' => by - rw [f₆.gpr, u₅.other r h', u₄.other r h, u₃.other r h] - have eax₆ : s₆.gpr .eax = inn s₀ + 96 := by - rw [f₆.gpr, u₅.other _ (by decide), u₄.gpr, u₃.gpr, h₂.ebx] - have hP : Pad s₀ (kl s₀) s₆ := - ⟨⟨h₂.j_le, by rw [f₆.rd, u₅.rd, u₄.rd, u₃.rd, h₂.rd], by rw [f₆.wr, u₅.wr, u₄.wr, u₃.wr, h₂.wr], - by rw [k₆ _ (by decide) (by decide), h₂.ebx], by rw [k₆ _ (by decide) (by decide), h₂.esi], - by rw [k₆ _ (by decide) (by decide), h₂.ebp], by rw [k₆ _ (by decide) (by decide), h₂.esp], - by rw [k₆ _ (by decide) (by decide), h₂.edx], by rw [f₆.mem, u₅.mem, u₄.mem, u₃.mem]; exact h₂.mem⟩, - eax₆, by rw [f₆.gpr, u₅.gpr]⟩ - have hz : s₆.zf = some (decide (kl s₀ = 64)) := by - rw [z₆, ← f₆.gpr, k₆ _ (by decide) (by decide), h₂.edx, eax₆, cmp_end _ hkl] - refine WP.seq (WP.mono (Q := Buf s₀ 64) ?_ fun s₇ h₇ => ?_) - · refine WP.ite (decide (kl s₀ = 64)) (by simp [eval, hz]) (fun hb => WP.block_nil ?_) - (fun hb => pad_loop_ok hp hP ?_) - · rw [← of_decide_eq_true hb]; exact hP.toBuf - · have := of_decide_eq_false hb; omega_nat - -- The outer buffer. - have hbufI : bytesAt s₇.mem (inA s₀ + 32) 64 = xorPad (K0 s₀) ipad := by - rw [h₇.mem.buf, List.take_of_length_le (by rw [K0_length s₀ hp])]; rfl - refine WP.seq ?_ - rw [← List.append_nil ((List.range 16).flatMap opadWord)] - refine xorWords_ok 16 [] s₇ _ h₇.ebx h₇.esi (by omega_nat) (by omega_nat) - (fun k hk => ⟨inR s₀, by simp [h₇.rd, h₇.wr, hp.wr], hp.in_in (by omega_nat) (by omega_nat)⟩) - (fun k hk => ⟨ouR s₀, by simp [h₇.wr, hp.wr], hp.ou_in (by omega_nat) (by omega_nat)⟩) - (hp.i_o.sep (contains_offset (by omega_nat) (by omega_nat)) (contains_offset (by omega_nat) (by omega_nat))) - fun s₈ g₈ rd₈ wr₈ m₈ => WP.block_nil ?_ - set ob := (bytesAt s₇.mem (inA s₀ + BitVec.ofNat 64 32) (4 * 16)).map (· ^^^ (0x6a : Byte)) with hob - have hobl : ob.length = 64 := by simp [ob, bytesAt_length] - have hob' : ob = xorPad (K0 s₀) opad := by - rw [hob, show 4 * 16 = 64 from rfl, show inA s₀ + BitVec.ofNat 64 32 = inA s₀ + 32 from rfl, hbufI, - xorPad_6a] - let bO : Region := ⟨ouA s₀ + BitVec.ofNat 64 32, 64⟩ - have sO : Region.Sub bO (ouR s₀) := sub_offset (by omega_nat) (by omega_nat) - have F₈ : Frame [bO] s₇.mem s₈.mem := by - rw [m₈]; exact writeBytes_frame _ _ _ (by rw [hobl]; exact Region.contains_self _ _) - have bOd : ∀ R : Region, R.Disjoint (ouR s₀) → ∀ r ∈ [bO], R.Disjoint r := fun R h r hr => by - simp only [List.mem_singleton] at hr; subst hr; exact h.sub_right sO - have stI₈ : stateAt s₈.mem (inA s₀) = H0 := by - rw [← h₇.mem.stI] - exact Proof.Sha256.Stream.stateAt_congr fun i hi => - frame_bytes F₈ (R := ⟨inA s₀, 32⟩) (bOd _ (hp.i_o.sub_left (sub32 _))) (by simp) hi - have bI₈ : bytesAt s₈.mem (inA s₀ + 32) 64 = xorPad (K0 s₀) ipad := by - rw [← hbufI] - exact Proof.Sha256.Stream.bytesAt_congr fun i hi => - frame_bytes F₈ (R := ⟨inA s₀ + 32, 64⟩) - (bOd _ (hp.i_o.sub_left (sub_offset (off := 32) (by omega_nat) (by omega_nat)))) (by simp) hi - have stO₈ : stateAt s₈.mem (ouA s₀) = H0 := by - rw [← h₇.mem.stO] - refine Proof.Sha256.Stream.stateAt_congr fun i hi => frame_bytes F₈ (R := ⟨ouA s₀, 32⟩) ?_ (by simp) hi - simp only [List.mem_singleton]; rintro r rfl - exact Offset.base_disjoint _ (e := 32) (by omega_nat) (by have := hp.ou_fit; omega_nat) - have bO₈ : bytesAt s₈.mem (ouA s₀ + 32) 64 = xorPad (K0 s₀) opad := by - rw [m₈, ← hob'] - have := VG.Proof.Hmac.Common.bytesAt_writeBytes_self s₇.mem (ouA s₀ + BitVec.ofNat 64 32) ob (by omega_nat) - rw [hobl] at this - exact this - have sv₈ : Saved s₀ s₈.mem := saved_frame h₇.mem.saved F₈ fun d h₁ h₂ r hr => by - simp only [List.mem_singleton] at hr; subst hr; exact save_disj hp (hp.o_s.sub_left sO) d h₁ h₂ - have f₈ : Frame [inR s₀, ouR s₀, scR s₀] s₀.mem s₈.mem := - h₇.mem.frame.trans (F₈.sub fun r hr => by - simp only [List.mem_singleton] at hr; subst hr; exact ⟨ouR s₀, by simp, sO⟩) - -- The inner block. - refine WP.seq (compBuf_ok hp (x := inn s₀) (.inl rfl) (b := .ebx) (.inl rfl) (by rw [rd₈, h₇.rd]) - (by rw [wr₈, h₇.wr]) (by rw [g₈ _ (by decide), h₇.ebx]) (by rw [g₈ _ (by decide), h₇.ebp]) - (by rw [g₈ _ (by decide), h₇.esp]) fun s₉ rd₉ wr₉ cs₉ fr₉ st₉ => ?_) - have hI₉ : Repr s₉.mem (inA s₀) (xorPad (K0 s₀) ipad) := - VG.Proof.Hmac.Common.repr_block stI₈ bI₈ (by simp [xorPad, K0_length s₀ hp]) st₉ - have dO : ∀ r ∈ [(⟨inA s₀, 32⟩ : Region), ⟨scA s₀, 112⟩, stkR s₀], Region.Disjoint (ouR s₀) r := by - simp only [List.mem_cons, List.not_mem_nil, or_false] - rintro r (rfl | rfl | rfl) - · exact hp.i_o.symm.sub_right (sub32 _) - · exact hp.o_s.sub_right (Region.sub_prefix (by omega_nat)) - · exact hp.stk_o.symm - have stO₉ : stateAt s₉.mem (ouA s₀) = H0 := by - rw [← stO₈] - exact Proof.Sha256.Stream.stateAt_congr fun i hi => - frame_bytes fr₉ (R := ⟨ouA s₀, 32⟩) (fun r hr => (dO r hr).sub_left (sub32 _)) (by simp) hi - have bO₉ : bytesAt s₉.mem (ouA s₀ + 32) 64 = xorPad (K0 s₀) opad := by - rw [← bO₈] - exact Proof.Sha256.Stream.bytesAt_congr fun i hi => - frame_bytes fr₉ (R := ⟨ouA s₀ + 32, 64⟩) - (fun r hr => (dO r hr).sub_left (sub_offset (off := 32) (by omega_nat) (by omega_nat))) (by simp) hi - have sv₉ : Saved s₀ s₉.mem := saved_frame sv₈ fr₉ fun d h₁ h₂ r hr => by - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl - · exact save_disj hp (hp.i_s.sub_left (sub32 _)) d h₁ h₂ - · exact save_disj112 hp d h₁ h₂ - · exact save_disj hp hp.stk_s d h₁ h₂ - have f₉ : Frame (allR s₀) s₀.mem s₉.mem := (f₈.mono (by simp)).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 - · exact ⟨inR s₀, by simp, sub32 _⟩ - · exact ⟨scR s₀, by simp, Region.sub_prefix (by omega_nat)⟩ - · exact ⟨stkR s₀, by simp, fun _ h => h⟩) - have cs₉' : ∀ r ∈ calleeSaved, s₉.gpr r = s₇.gpr r := fun r hr => by - rw [cs₉ r hr, g₈ r (callee_ne_eax hr)] - -- The outer block. - refine WP.seq (compBuf_ok hp (x := ou s₀) (.inr rfl) (b := .esi) (.inr rfl) rd₉ wr₉ - (by rw [cs₉' _ (by decide), h₇.esi]) (by rw [cs₉' _ (by decide), h₇.ebp]) - (by rw [cs₉' _ (by decide), h₇.esp]) fun s₁₀ rd₁₀ wr₁₀ cs₁₀ fr₁₀ st₁₀ => ?_) - have hO : Repr s₁₀.mem (ouA s₀) (xorPad (K0 s₀) opad) := - VG.Proof.Hmac.Common.repr_block stO₉ bO₉ (by simp [xorPad, K0_length s₀ hp]) st₁₀ - have hI : Repr s₁₀.mem (inA s₀) (xorPad (K0 s₀) ipad) := by - refine repr_congr (fun i hi => frame_bytes fr₁₀ (R := inR s₀) ?_ (by simp) hi) hI₉ - simp only [List.mem_cons, List.not_mem_nil, or_false] - rintro r (rfl | rfl | rfl) - · exact hp.i_o.sub_right (sub32 _) - · exact hp.i_s.sub_right (Region.sub_prefix (by omega_nat)) - · exact hp.stk_i.symm - have sv₁₀ : Saved s₀ s₁₀.mem := saved_frame sv₉ fr₁₀ fun d h₁ h₂ r hr => by - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl - · exact save_disj hp (hp.o_s.sub_left (sub32 _)) d h₁ h₂ - · exact save_disj112 hp d h₁ h₂ - · exact save_disj hp hp.stk_s d h₁ h₂ - have f₁₀ : Frame (allR s₀) s₀.mem s₁₀.mem := 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 - · exact ⟨ouR s₀, by simp, sub32 _⟩ - · exact ⟨scR s₀, by simp, Region.sub_prefix (by omega_nat)⟩ - · exact ⟨stkR s₀, by simp, fun _ h => h⟩) - have cs₁₀' : ∀ r ∈ calleeSaved, s₁₀.gpr r = s₇.gpr r := fun r hr => by rw [cs₁₀ r hr, cs₉' r hr] - -- Epilogue. - refine WP.mono (epilogue_ok hp rd₁₀ wr₁₀ (by rw [cs₁₀' _ (by decide), h₇.ebp]) - (by rw [cs₁₀' _ (by decide), h₇.esp]) sv₁₀) fun s' ⟨m', cs'⟩ => ⟨⟨cs', ?_⟩, ?_⟩ - · rw [m'] - refine f₁₀.readW (r := retR s₀) (Region.contains_self _ _) ?_ (by decide) - intro r hr - simp only [allR, List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl | rfl | rfl - exacts [hp.ret_i, hp.ret_o, hp.ret_s, ret_a hp, ret_stk hp] - · show Repr s'.mem (inA s₀) (xorPad (blockKey sha256 (bytesAt s₀.mem (kA s₀) (kl s₀))) ipad) ∧ - Repr s'.mem (ouA s₀) (xorPad (blockKey sha256 (bytesAt s₀.mem (kA s₀) (kl s₀))) opad) - rw [blockKey_eq hp, m'] - exact ⟨hI, hO⟩ - /-! ## Constant time -/ /-- The initial taint: `esp + 4` is the base of the (public) arguments, whose @@ -1048,11 +837,6 @@ def sat : State where rd := [⟨0x1200, 0⟩] wr := [⟨0x1000, 96⟩, ⟨0x1100, 96⟩, ⟨0x3000, 160⟩, ⟨0x4004, 20⟩] -theorem init_correct (s : State) (hs : Proof.Hmac.initSha256X86.pre s) : - ∃ t s', Exec isa init s t s' ∧ abiPreserved s s' ∧ Proof.Hmac.initSha256X86.post s s' := by - obtain ⟨t, s', he, h⟩ := correct (pre_of hs) - exact ⟨t, s', he, h⟩ - theorem init_ct : ConstantTime isa Proof.Hmac.initSha256X86.pre Proof.Hmac.initSha256X86.pub init := VG.Taint.constantTime (A := taint) τ₀ (fun _ _ h₁ h₂ hp => agree₀ h₁ h₂ hp) (by taint_decide) @@ -1116,20 +900,4 @@ theorem initWide_implies : initWide.Implies (Spec.Hmac.initSha256Contract X86.ab Proof.Hmac.initSha256X86, X86.abi, X86.argSlots, X86.argVal, X86.argBytes] [a0, a1, a2, a3, a4, e, esp] using wideSat -/-- The proof is written against `initSha256X86`, widened to the shared -contract's scratch. -/ -theorem init_verified : - Verified X86.target Impl.Hmac.X86.init (Spec.Hmac.initSha256Contract X86.abi 20) := - have hsat := initWide_implies.sat_left - (Verified.widen (Verified.of_correct init_correct init_ct - (.refl (hsat.elim fun s hs => ⟨_, initWide_pre s hs⟩))) - narrowWr initWide_pre - (fun _ h => by - obtain ⟨_, _, h₃, _⟩ := h - rw [h₃] - exact .cons (Region.prefix_of_ble rfl) (.cons (Region.prefix_of_ble rfl) - (.cons (Region.prefix_of_ble rfl) (.cons (Region.prefix_of_ble rfl) .nil)))) - (fun _ _ _ h => by narrow at h ⊢; exact h) - (fun _ _ _ _ h => by narrow; exact h) hsat).of_implies initWide_implies - end VG.Proof.Hmac.X86.Init diff --git a/lean/VerifiedGarbage/Proof/Pbkdf2/Sha256/X86.lean b/lean/VerifiedGarbage/Proof/Pbkdf2/Sha256/X86.lean new file mode 100644 index 000000000..53a283219 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Pbkdf2/Sha256/X86.lean @@ -0,0 +1,207 @@ +import VerifiedGarbage.Proof.Pbkdf2.X86.Iterate +import VerifiedGarbage.Proof.Sha256.X86.Stream.CompressAt +import VerifiedGarbage.Impl.Pbkdf2.Sha256.X86 + +/-! PBKDF2-SHA-256's direct-compression loop, proved once for any backend. -/ +namespace VG.Proof.Pbkdf2.Sha256.X86 +open VG VG.X86 +open VG.Proof.Pbkdf2.X86 +open VG.Proof.Sha256.X86.Stream +open VG.Impl.Pbkdf2.X86 (digest) +open VG.Proof.Pbkdf2.Memory (frame_bytesAt blockAt_eq xorBytes_length digest_self add_ofNat contains_base) +open VG.Proof.Sha256.Stream (writeBytes writeBytes_frame) +open VG.Proof.Hmac.Common (bytesAt_writeBytes_self bytesAt_writeBytes_sep bytesAt_length) +open VG.Spec.Sha256 (stateAt compress blockAt bytesAt) +variable {name : String} {code : Prog isa} + (hv : Verified X86.target code Proof.Sha256.compressX86) + (hnosp : NoSp code) (hstack : stackUse code = 0) +include hv hnosp hstack + +theorem cmp_of {s₀ : State} (hp : Pre s₀) {s : State} (h : Regs s₀ s) + (hax : s.gpr .eax = scr s₀ + BitVec.ofNat 32 192) {Q : State → Prop} + (k : ∀ s', Keep s₀ s s' → + stateAt s'.mem (tA s₀) = compress (stateAt s.mem (tA s₀)) (blockAt s.mem (blkA s₀)) → Q s') : + WP isa (Impl.MdStream.X86.compressAt name code .ebx .ebp) s Q := by + have := hp.scr_fit; have := hp.t_fit + have ea : (scr s₀ + BitVec.ofNat 32 192).setWidth 64 = blkA s₀ := addr_off (len := 256) hp.scr_fit (by omega) + have et : (scr s₀ + BitVec.ofNat 32 192).toNat = (scr s₀).toNat + 192 := by + rw [BitVec.toNat_add, BitVec.toNat_ofNat]; omega + have hsc : scR s₀ ∈ s.wr := by simp [h.wr, hp.wr] + have htr : tR s₀ ∈ s.wr := by simp [h.wr, hp.wr] + have b64 : Region.Sub ⟨(scr s₀ + BitVec.ofNat 32 192).setWidth 64, 64⟩ (sR s₀ 192 64) := by + rw [ea]; exact fun _ h => h + refine compressAt_of hv hnosp hstack (st := tP s₀) (scr := scr s₀) (blk := scr s₀ + BitVec.ofNat 32 192) (E := esp₀ s₀) + (by decide) (by decide) (by decide) (by decide) h.esp h.ebx h.ebp hax hp.sp_lo (by omega) + (by rw [et]; omega) (by omega) (hp.t_s.sub_right (cmp_sub s₀)) + ((hp.t_s.sub_right (scr_sub s₀ (o := 192) (n := 64) (by omega))).symm.sub_left b64) + ((scr_disj0 s₀ (a := 192) (m := 64) (by omega) (by omega)).sub_left b64) + hp.stk_t (hp.stk_s.sub_right (cmp_sub s₀)) (hp.stk_s.sub_right fun a ha => scr_sub s₀ (o := 192) (n := 64) (by omega) a (b64 a ha)) ?_ ?_ + fun s' hrd hwr hcs hf hst => k s' ⟨hrd, hwr, fun r hr => hcs r (by + simp only [kept, List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl | rfl <;> simp [calleeSaved]), hf⟩ (by rw [hst, ea]) + · rw [ea] + refine Covers.of_sub fun r hr => ?_ + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + subst hr + exact ⟨scR s₀, List.mem_append_right _ hsc, 192, rfl, by simp⟩ + · 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 + · exact ⟨tR s₀, htr, 0, by simp, by simp⟩ + · exact ⟨scR s₀, hsc, 0, by simp, by simp⟩ + +theorem body_ok {s₀ : State} (hp : Pre s₀) {r : Nat} {s : State} (h : Inv s₀ (r + 1) s) : + WP isa (Impl.Pbkdf2.Sha256.X86.body name code) s fun s' => VG.X86.eval .ne s' = some (r != 0) ∧ Inv s₀ r s' := by + have := hp.scr_fit + unfold Impl.Pbkdf2.Sha256.X86.body + have hU : ∀ {m : Mem}, Frame [tR s₀, cmpR s₀, stkR s₀] s.mem m → + bytesAt m (blkA s₀) 32 = bytesAt s.mem (blkA s₀) 32 := + fun hf => frame_bytesAt hf (blk_disj hp) (by omega) + have hpad : ∀ {m : Mem}, Frame (bodyR s₀) s.mem m → bytesAt m (blkA s₀ + 32) 32 = pad96 := by + intro m hf + rw [show blkA s₀ + 32 = scA s₀ + BitVec.ofNat 64 224 by + change scA s₀ + 192 + 32 = scA s₀ + BitVec.ofNat 64 224 + rw [BitVec.add_assoc]; rfl, ← h.pad] + exact frame_bytesAt hf (body_disj hp (o := 224) (n := 32) (.inr (Nat.le_refl _)) (by omega)) (by omega) + -- The inner hash. + refine WP.seq ?_ + refine load_ok hp h.toRegs (o := 0) (by omega) fun s₁ k₁ e₁ => ?_ + refine atBlock_ok (rest := []) (h.toRegs.keep k₁) fun s₂ k₂ m₂ x₂ => WP.block_nil ?_ + have h₂ := (h.toRegs.keep k₁).keep k₂ + refine WP.seq (cmp_of hv hnosp hstack hp h₂ x₂ fun s₃ k₃ e₃ => ?_) + rw [m₂, e₁, blockAt_eq (hpad (frame_body k₁.frame (by simp))), hU k₁.frame] at e₃ + -- The outer hash. + have h₃ := h₂.keep k₃ + refine WP.seq ?_ + refine digest_ok hp h₃ fun s₄ h₄ g₄ f₄ m₄ => ?_ + refine load_ok hp h₄ (o := 96) (by omega) fun s₅ k₅ e₅ => ?_ + refine atBlock_ok (rest := []) (h₄.keep k₅) fun s₆ k₆ m₆ x₆ => WP.block_nil ?_ + have h₆ := (h₄.keep k₅).keep k₆ + have f₃₄ : Frame (bodyR s₀) s.mem s₄.mem := + (frame_body ((k₁.trans k₂).trans k₃).frame (by simp)).trans (frame_body f₄ (by simp)) + refine WP.seq (cmp_of hv hnosp hstack hp h₆ x₆ fun s₇ k₇ e₇ => ?_) + have hX : bytesAt s₅.mem (blkA s₀) 32 = Pbkdf2.digest (stateAt s₃.mem (tA s₀)) := by + rw [frame_bytesAt (p := blkA s₀) (n := 32) k₅.frame (blk_disj hp) (by omega), m₄, digest_self] + rw [m₆, e₅, blockAt_eq (hpad (f₃₄.trans (frame_body k₅.frame (by simp)))), hX, e₃] at e₇ + -- The digest, `T ← T ⊕ U` and the count. + have h₇ := h₆.keep k₇ + refine digest_ok hp h₇ fun s₈ h₈ g₈ f₈ m₈ => ?_ + refine xor_ok (p := scr s₀) (by omega) 8 (Nat.le_refl _) _ s₈ _ h₈.ebp + (fun j hj => InRegions.right (by rw [add_ofNat]; exact in_scr hp h₈.wr (a := 192 + 4 * j) (n := 4) (by omega))) + (fun j hj => by rw [add_ofNat]; exact in_scr hp h₈.wr (a := 160 + 4 * j) (n := 4) (by omega)) + fun s₉ g₉ rd₉ wr₉ m₉ => ?_ + rw [show 4 * 8 = 32 from rfl] at m₉ + have f₉ : Frame [sR s₀ 160 32] s₈.mem s₉.mem := by + rw [m₉] + exact writeBytes_frame _ _ _ (contains_base (by rw [xorBytes_length _ _ (by simp [bytesAt]), bytesAt_length])) + have h₉ := h₈.write (fun r hr => g₉ r (by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl <;> decide)) rd₉ wr₉ (R := scR s₀) (by simp) + (f₉.sub fun r hr => by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + subst hr; exact ⟨scR s₀, by simp, scr_sub s₀ (by omega)⟩) + refine wp_subi fun s₁₀ u₁₀ z₁₀ => WP.block_nil ?_ + have h₁₀ := h₉.write (fun r hr => u₁₀.other r (by + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl <;> decide)) u₁₀.rd u₁₀.wr (R := tR s₀) (by simp) + (by rw [u₁₀.mem]; exact Frame.refl _ _) + have xedi : s₉.gpr .edi = BitVec.ofNat 32 (r + 1) := by + rw [g₉ _ (by decide), g₈ _ (by decide), k₇.gpr _ (by simp [kept]), k₆.gpr _ (by simp [kept]), + k₅.gpr _ (by simp [kept]), g₄ _ (by decide), k₃.gpr _ (by simp [kept]), k₂.gpr _ (by simp [kept]), + k₁.gpr _ (by simp [kept]), h.edi] + have hlt : r + 1 < 2 ^ 32 := by have := h.le; have := (arg s₀ 2).isLt; simp only [nn] at *; omega + have e₁₀ : s₉.gpr .edi - 1 = BitVec.ofNat 32 r := by + rw [xedi, show (1 : BitVec 32) = BitVec.ofNat 32 1 from rfl, sub_ofNat (by omega), Nat.add_sub_cancel] + have fb : Frame (bodyR s₀) s.mem s₁₀.mem := by + rw [u₁₀.mem] + exact f₃₄.trans (frame_body ((k₅.trans k₆).trans k₇).frame (by simp)) |>.trans (frame_body f₈ (by simp)) + |>.trans (frame_body f₉ (by simp)) + have f₈' : Frame [tR s₀, cmpR s₀, stkR s₀, sR s₀ 192 32] s.mem s₈.mem := + (((k₁.trans k₂).trans k₃).frame.mono (by simp)) |>.trans (f₄.mono (by simp)) + |>.trans ((((k₅.trans k₆).trans k₇).frame).mono (by simp)) |>.trans (f₈.mono (by simp)) + have hT : bytesAt s₈.mem (TA s₀) 32 = bytesAt s.mem (TA s₀) 32 := + frame_bytesAt f₈' (T_disj hp) (by omega) + have hU₈ : bytesAt s₈.mem (blkA s₀) 32 = stepM s₀ (bytesAt s.mem (blkA s₀) 32) := by + rw [m₈, digest_self, e₇]; rfl + have hsep : Mem.Sep (blkA s₀) 32 (TA s₀) + (Spec.Pbkdf2.xorBytes (bytesAt s₈.mem (TA s₀) 32) (bytesAt s₈.mem (blkA s₀) 32)).length := by + rw [xorBytes_length _ _ (by simp [bytesAt]), bytesAt_length] + exact Region.Disjoint.sep (scr_disj s₀ (a := 192) (m := 32) (b := 160) (n := 32) (by omega) (by omega) + (by omega)) (contains_base (Nat.le_refl _)) (contains_base (Nat.le_refl _)) + have hU₁₀ : bytesAt s₁₀.mem (blkA s₀) 32 = stepM s₀ (bytesAt s.mem (blkA s₀) 32) := by + rw [u₁₀.mem, m₉, bytesAt_writeBytes_sep _ _ hsep (by omega), hU₈] + have hT₁₀ : bytesAt s₁₀.mem (TA s₀) 32 = + Spec.Pbkdf2.xorBytes (bytesAt s.mem (TA s₀) 32) (stepM s₀ (bytesAt s.mem (blkA s₀) 32)) := by + have := bytesAt_writeBytes_self s₈.mem (TA s₀) + (Spec.Pbkdf2.xorBytes (bytesAt s₈.mem (TA s₀) 32) (bytesAt s₈.mem (blkA s₀) 32)) + (by rw [xorBytes_length _ _ (by simp [bytesAt]), bytesAt_length]; omega) + rw [xorBytes_length _ _ (by simp [bytesAt]), bytesAt_length] at this + rw [u₁₀.mem, m₉, this, hT, hU₈] + have hle : r ≤ nn s₀ := by have := h.le; omega + refine ⟨?_, { h₁₀ with edi := ?_, saved := h.saved.frame hp fb, pad := ?_, le := hle, val := ?_ }⟩ + · rw [eval_ne, z₁₀, e₁₀, ofNat_beq_zero (by omega)] + cases r <;> rfl + · rw [u₁₀.gpr, e₁₀] + · rw [← h.pad] + exact frame_bytesAt fb (body_disj hp (o := 224) (n := 32) (.inr (Nat.le_refl _)) (by omega)) (by omega) + · rw [h.val, hU₁₀, hT₁₀]; rfl + +theorem loop_ok {s₀ : State} (hp : Pre s₀) {n : Nat} {s : State} (h : Inv s₀ n s) + (hz : s.zf = some (decide (n = 0))) : + WP isa (.ite .e (.block []) (.loop (Impl.Pbkdf2.Sha256.X86.body name code) .ne)) s (Inv s₀ 0) := by + refine WP.ite (decide (n = 0)) (by show s.zf = _; rw [hz]) (fun hb => ?_) (fun hb => ?_) + · obtain rfl : n = 0 := by simpa using hb + exact WP.block_nil h + · obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by simp at hb; omega⟩ + refine WP.loop (fun m s => Inv s₀ (m + 1) s) (fun m s hs => WP.mono (body_ok hv hnosp hstack hp hs) fun s' ⟨he, hi⟩ => ?_) m s h + cases m with + | zero => exact .inl ⟨he, hi⟩ + | succ m => exact .inr ⟨he, m, by omega, hi⟩ + +/-- Prologue and epilogue are unchanged; the loop calls this compressor. -/ +theorem correct {s₀ : State} (hp : Pre s₀) : + WP isa (Impl.Pbkdf2.Sha256.X86.iterate name code) s₀ (Post s₀) := by + unfold Impl.Pbkdf2.Sha256.X86.iterate + refine WP.seq (WP.mono (prologue_ok hp) fun s₁ ⟨h₁, z₁⟩ => ?_) + exact WP.seq (WP.mono (loop_ok hv hnosp hstack hp h₁ z₁) fun s₂ h₂ => epilogue_ok hp h₂) + +local macro "narrow" loc:(Lean.Parser.Tactic.location)? : tactic => + `(tactic| simp only [Proof.Pbkdf2.iterateSha256X86, VG.Proof.Pbkdf2.X86.iterateWide, + VG.Proof.Pbkdf2.X86.narrowRd, VG.Proof.Pbkdf2.X86.narrowWr, VG.X86.arg_withRegions, + VG.X86.argAddr_withRegions, VG.X86.State.withRegions_gpr, VG.X86.State.withRegions_mem, + VG.X86.State.withRegions_rd, VG.X86.State.withRegions_wr] $(loc)?) + +theorem verified + (hct : ConstantTime isa Proof.Pbkdf2.iterateSha256X86.pre + Proof.Pbkdf2.iterateSha256X86.pub (Impl.Pbkdf2.Sha256.X86.iterate name code)) : + Verified X86.target (Impl.Pbkdf2.Sha256.X86.iterate name code) (Spec.Pbkdf2.iterateSha256Contract X86.abi 20) := + have hsat := iterateWide_implies.sat_left + (Verified.narrowTo (Verified.of_correct (fun s hs => by + obtain ⟨t, s', he, h⟩ := correct hv hnosp hstack (pre_of hs) + exact ⟨t, s', he, h⟩) hct (.refl ⟨sat, sat_pre⟩)) + narrowRd narrowWr iterateWide_pre + (fun _ h => by + obtain ⟨h₁, h₂, _⟩ := h + rw [h₁, h₂] + refine Covers.of_sub fun r hr => ?_ + simp only [narrowRd, narrowWr, 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 + · exact ⟨_, List.mem_append_left _ List.mem_cons_self, 0, by simp, by simp⟩ + · exact ⟨_, List.mem_append_left _ (List.mem_cons_of_mem _ List.mem_cons_self), 0, by simp, by simp⟩ + · exact ⟨_, List.mem_append_right _ (List.mem_cons_of_mem _ (List.mem_cons_of_mem _ List.mem_cons_self)), + 0, by simp, by simp⟩ + · exact ⟨_, List.mem_append_right _ List.mem_cons_self, 0, by simp, by simp⟩ + · exact ⟨_, List.mem_append_right _ (List.mem_cons_of_mem _ List.mem_cons_self), 0, by simp, by simp⟩) + (fun _ h => by + obtain ⟨_, h₂, _⟩ := h + rw [h₂] + refine Covers.of_sub fun r hr => ?_ + simp only [narrowWr, List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl + · exact ⟨_, List.mem_cons_self, 0, by simp, by simp⟩ + · exact ⟨_, List.mem_cons_of_mem _ List.mem_cons_self, 0, by simp, by simp⟩) + (fun _ _ _ h => by narrow at h ⊢; exact h) + (fun _ _ _ _ h => by narrow; exact h) hsat).of_implies iterateWide_implies + +end VG.Proof.Pbkdf2.Sha256.X86 diff --git a/lean/VerifiedGarbage/Proof/Pbkdf2/X86/Body.lean b/lean/VerifiedGarbage/Proof/Pbkdf2/X86/Body.lean index 3fb2aee70..26c370f19 100644 --- a/lean/VerifiedGarbage/Proof/Pbkdf2/X86/Body.lean +++ b/lean/VerifiedGarbage/Proof/Pbkdf2/X86/Body.lean @@ -96,110 +96,4 @@ structure Inv (s₀ : State) (r : Nat) (s : State) : Prop extends Regs s₀ s wh val : Spec.Pbkdf2.iterate (stepM s₀) (nn s₀) (bytesAt s₀.mem (uA s₀) 32) (bytesAt s₀.mem (tA s₀) 32) = Spec.Pbkdf2.iterate (stepM s₀) r (bytesAt s.mem (blkA s₀) 32) (bytesAt s.mem (TA s₀) 32) -theorem body_ok {s₀ : State} (hp : Pre s₀) {r : Nat} {s : State} (h : Inv s₀ (r + 1) s) : - WP isa body s fun s' => VG.X86.eval .ne s' = some (r != 0) ∧ Inv s₀ r s' := by - have := hp.scr_fit - unfold body - have hU : ∀ {m : Mem}, Frame [tR s₀, cmpR s₀, stkR s₀] s.mem m → - bytesAt m (blkA s₀) 32 = bytesAt s.mem (blkA s₀) 32 := - fun hf => frame_bytesAt hf (blk_disj hp) (by omega) - have hpad : ∀ {m : Mem}, Frame (bodyR s₀) s.mem m → bytesAt m (blkA s₀ + 32) 32 = pad96 := by - intro m hf - rw [show blkA s₀ + 32 = scA s₀ + BitVec.ofNat 64 224 by bv_omega, ← h.pad] - exact frame_bytesAt hf (body_disj hp (o := 224) (n := 32) (.inr (Nat.le_refl _)) (by omega)) (by omega) - -- The inner hash. - refine WP.seq ?_ - refine load_ok hp h.toRegs (o := 0) (by omega) fun s₁ k₁ e₁ => ?_ - refine atBlock_ok (rest := []) (h.toRegs.keep k₁) fun s₂ k₂ m₂ x₂ => WP.block_nil ?_ - have h₂ := (h.toRegs.keep k₁).keep k₂ - refine WP.seq (cmp_ok hp h₂ x₂ fun s₃ k₃ e₃ => ?_) - rw [m₂, e₁, blockAt_eq (hpad (frame_body k₁.frame (by simp))), hU k₁.frame] at e₃ - -- The outer hash. - have h₃ := h₂.keep k₃ - refine WP.seq ?_ - refine digest_ok hp h₃ fun s₄ h₄ g₄ f₄ m₄ => ?_ - refine load_ok hp h₄ (o := 96) (by omega) fun s₅ k₅ e₅ => ?_ - refine atBlock_ok (rest := []) (h₄.keep k₅) fun s₆ k₆ m₆ x₆ => WP.block_nil ?_ - have h₆ := (h₄.keep k₅).keep k₆ - have f₃₄ : Frame (bodyR s₀) s.mem s₄.mem := - (frame_body ((k₁.trans k₂).trans k₃).frame (by simp)).trans (frame_body f₄ (by simp)) - refine WP.seq (cmp_ok hp h₆ x₆ fun s₇ k₇ e₇ => ?_) - have hX : bytesAt s₅.mem (blkA s₀) 32 = Pbkdf2.digest (stateAt s₃.mem (tA s₀)) := by - rw [frame_bytesAt (p := blkA s₀) (n := 32) k₅.frame (blk_disj hp) (by omega), m₄, digest_self] - rw [m₆, e₅, blockAt_eq (hpad (f₃₄.trans (frame_body k₅.frame (by simp)))), hX, e₃] at e₇ - -- The digest, `T ← T ⊕ U` and the count. - have h₇ := h₆.keep k₇ - refine digest_ok hp h₇ fun s₈ h₈ g₈ f₈ m₈ => ?_ - refine xor_ok (p := scr s₀) (by omega) 8 (Nat.le_refl _) _ s₈ _ h₈.ebp - (fun j hj => InRegions.right (by rw [add_ofNat]; exact in_scr hp h₈.wr (a := 192 + 4 * j) (n := 4) (by omega))) - (fun j hj => by rw [add_ofNat]; exact in_scr hp h₈.wr (a := 160 + 4 * j) (n := 4) (by omega)) - fun s₉ g₉ rd₉ wr₉ m₉ => ?_ - rw [show 4 * 8 = 32 from rfl] at m₉ - have f₉ : Frame [sR s₀ 160 32] s₈.mem s₉.mem := by - rw [m₉] - exact writeBytes_frame _ _ _ (contains_base (by rw [xorBytes_length _ _ (by simp [bytesAt]), bytesAt_length])) - have h₉ := h₈.write (fun r hr => g₉ r (by - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl | rfl <;> decide)) rd₉ wr₉ (R := scR s₀) (by simp) - (f₉.sub fun r hr => by - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - subst hr; exact ⟨scR s₀, by simp, scr_sub s₀ (by omega)⟩) - refine wp_subi fun s₁₀ u₁₀ z₁₀ => WP.block_nil ?_ - have h₁₀ := h₉.write (fun r hr => u₁₀.other r (by - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl | rfl <;> decide)) u₁₀.rd u₁₀.wr (R := tR s₀) (by simp) - (by rw [u₁₀.mem]; exact Frame.refl _ _) - have xedi : s₉.gpr .edi = BitVec.ofNat 32 (r + 1) := by - rw [g₉ _ (by decide), g₈ _ (by decide), k₇.gpr _ (by simp [kept]), k₆.gpr _ (by simp [kept]), - k₅.gpr _ (by simp [kept]), g₄ _ (by decide), k₃.gpr _ (by simp [kept]), k₂.gpr _ (by simp [kept]), - k₁.gpr _ (by simp [kept]), h.edi] - have hlt : r + 1 < 2 ^ 32 := by have := h.le; have := (arg s₀ 2).isLt; simp only [nn] at *; omega - have e₁₀ : s₉.gpr .edi - 1 = BitVec.ofNat 32 r := by - rw [xedi, show (1 : BitVec 32) = BitVec.ofNat 32 1 from rfl, sub_ofNat (by omega), Nat.add_sub_cancel] - have fb : Frame (bodyR s₀) s.mem s₁₀.mem := by - rw [u₁₀.mem] - exact f₃₄.trans (frame_body ((k₅.trans k₆).trans k₇).frame (by simp)) |>.trans (frame_body f₈ (by simp)) - |>.trans (frame_body f₉ (by simp)) - have f₈' : Frame [tR s₀, cmpR s₀, stkR s₀, sR s₀ 192 32] s.mem s₈.mem := - (((k₁.trans k₂).trans k₃).frame.mono (by simp)) |>.trans (f₄.mono (by simp)) - |>.trans ((((k₅.trans k₆).trans k₇).frame).mono (by simp)) |>.trans (f₈.mono (by simp)) - have hT : bytesAt s₈.mem (TA s₀) 32 = bytesAt s.mem (TA s₀) 32 := - frame_bytesAt f₈' (T_disj hp) (by omega) - have hU₈ : bytesAt s₈.mem (blkA s₀) 32 = stepM s₀ (bytesAt s.mem (blkA s₀) 32) := by - rw [m₈, digest_self, e₇]; rfl - have hsep : Mem.Sep (blkA s₀) 32 (TA s₀) - (Spec.Pbkdf2.xorBytes (bytesAt s₈.mem (TA s₀) 32) (bytesAt s₈.mem (blkA s₀) 32)).length := by - rw [xorBytes_length _ _ (by simp [bytesAt]), bytesAt_length] - exact Region.Disjoint.sep (scr_disj s₀ (a := 192) (m := 32) (b := 160) (n := 32) (by omega) (by omega) - (by omega)) (contains_base (Nat.le_refl _)) (contains_base (Nat.le_refl _)) - have hU₁₀ : bytesAt s₁₀.mem (blkA s₀) 32 = stepM s₀ (bytesAt s.mem (blkA s₀) 32) := by - rw [u₁₀.mem, m₉, bytesAt_writeBytes_sep _ _ hsep (by omega), hU₈] - have hT₁₀ : bytesAt s₁₀.mem (TA s₀) 32 = - Spec.Pbkdf2.xorBytes (bytesAt s.mem (TA s₀) 32) (stepM s₀ (bytesAt s.mem (blkA s₀) 32)) := by - have := bytesAt_writeBytes_self s₈.mem (TA s₀) - (Spec.Pbkdf2.xorBytes (bytesAt s₈.mem (TA s₀) 32) (bytesAt s₈.mem (blkA s₀) 32)) - (by rw [xorBytes_length _ _ (by simp [bytesAt]), bytesAt_length]; omega) - rw [xorBytes_length _ _ (by simp [bytesAt]), bytesAt_length] at this - rw [u₁₀.mem, m₉, this, hT, hU₈] - have hle : r ≤ nn s₀ := by have := h.le; omega - refine ⟨?_, { h₁₀ with edi := ?_, saved := h.saved.frame hp fb, pad := ?_, le := hle, val := ?_ }⟩ - · rw [eval_ne, z₁₀, e₁₀, ofNat_beq_zero (by omega)] - cases r <;> rfl - · rw [u₁₀.gpr, e₁₀] - · rw [← h.pad] - exact frame_bytesAt fb (body_disj hp (o := 224) (n := 32) (.inr (Nat.le_refl _)) (by omega)) (by omega) - · rw [h.val, hU₁₀, hT₁₀]; rfl - -theorem loop_ok {s₀ : State} (hp : Pre s₀) {n : Nat} {s : State} (h : Inv s₀ n s) - (hz : s.zf = some (decide (n = 0))) : - WP isa (.ite .e (.block []) (.loop body .ne)) s (Inv s₀ 0) := by - refine WP.ite (decide (n = 0)) (by show s.zf = _; rw [hz]) (fun hb => ?_) (fun hb => ?_) - · obtain rfl : n = 0 := by simpa using hb - exact WP.block_nil h - · obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by simp at hb; omega⟩ - refine WP.loop (fun m s => Inv s₀ (m + 1) s) (fun m s hs => WP.mono (body_ok hp hs) fun s' ⟨he, hi⟩ => ?_) m s h - cases m with - | zero => exact .inl ⟨he, hi⟩ - | succ m => exact .inr ⟨he, m, by omega, hi⟩ - end VG.Proof.Pbkdf2.X86 diff --git a/lean/VerifiedGarbage/Proof/Pbkdf2/X86/Common.lean b/lean/VerifiedGarbage/Proof/Pbkdf2/X86/Common.lean index 56f55c9f2..05fb036ce 100644 --- a/lean/VerifiedGarbage/Proof/Pbkdf2/X86/Common.lean +++ b/lean/VerifiedGarbage/Proof/Pbkdf2/X86/Common.lean @@ -10,8 +10,8 @@ import VerifiedGarbage.Impl.Pbkdf2.X86 Untrusted: everything here is checked by Lean. The same structure as the ARMv7 proof (`VG.Proof.Pbkdf2.Arm`), with the same target-independent memory lemmas (`VG.Proof.Pbkdf2.Memory`). Each step is two calls -of `vg_sha256_compress`, used as a black box through its proof -(`compressAt_ok`, from the streaming SHA-256 proof), each using the 20 bytes +of the selected compression backend, used as a black box through the +generic proof in `Proof/Pbkdf2/Sha256/X86.lean`, each using the 20 bytes below `esp`. The hash value being compressed is `t`, and `T` is kept in `scratch[160..192)`. -/ @@ -74,7 +74,7 @@ open VG.Impl.Sha256.X86.Stream (compressAt saved) open VG.Impl.Hmac.X86 (bswapWord copyWord) open VG.Proof.Sha256.X86 (contains_offset) open VG.Proof.Sha256.X86.Stream (Upd Mupd Fupd wp_mov wp_movi wp_movm wp_store wp_addi ea_at sub_offset - addr_toNat compressAt_ok stk_eq) + addr_toNat stk_eq) open VG.Proof.Hmac.X86 (copyWords_ok bswapWords_ok) open VG.Proof.Hmac.X86.Finalize (beWords_stateAt) open VG.Proof.Hmac.Common (bytesAt_length bytesAt_writeBytes_sep bytesAt_add extractLsb'_read) @@ -316,40 +316,6 @@ theorem atBlock_ok {s₀ : State} {s : State} (h : Regs s₀ s) {rest : List Ins fun r hr => by rw [u₂.other r (ne r hr), u₁.other r (ne r hr)], by rw [u₂.mem, u₁.mem]; exact Frame.refl _ _⟩ (by rw [u₂.mem, u₁.mem]) (by rw [u₂.gpr, u₁.gpr, h.ebp]; rfl) -/-- Compressing the block into the hash value in `t`. -/ -theorem cmp_ok {s₀ : State} (hp : Pre s₀) {s : State} (h : Regs s₀ s) - (hax : s.gpr .eax = scr s₀ + BitVec.ofNat 32 192) {Q : State → Prop} - (k : ∀ s', Keep s₀ s s' → - stateAt s'.mem (tA s₀) = compress (stateAt s.mem (tA s₀)) (blockAt s.mem (blkA s₀)) → Q s') : - WP isa (compressAt .ebx .ebp) s Q := by - have := hp.scr_fit; have := hp.t_fit - have ea : (scr s₀ + BitVec.ofNat 32 192).setWidth 64 = blkA s₀ := addr_off (len := 256) hp.scr_fit (by omega) - have et : (scr s₀ + BitVec.ofNat 32 192).toNat = (scr s₀).toNat + 192 := by - rw [BitVec.toNat_add, BitVec.toNat_ofNat]; omega - have hsc : scR s₀ ∈ s.wr := by simp [h.wr, hp.wr] - have htr : tR s₀ ∈ s.wr := by simp [h.wr, hp.wr] - have b64 : Region.Sub ⟨(scr s₀ + BitVec.ofNat 32 192).setWidth 64, 64⟩ (sR s₀ 192 64) := by - rw [ea]; exact fun _ h => h - refine compressAt_ok (st := tP s₀) (scr := scr s₀) (blk := scr s₀ + BitVec.ofNat 32 192) (E := esp₀ s₀) - (by decide) (by decide) (by decide) (by decide) h.esp h.ebx h.ebp hax hp.sp_lo (by omega) - (by rw [et]; omega) (by omega) (hp.t_s.sub_right (cmp_sub s₀)) - ((hp.t_s.sub_right (scr_sub s₀ (o := 192) (n := 64) (by omega))).symm.sub_left b64) - ((scr_disj0 s₀ (a := 192) (m := 64) (by omega) (by omega)).sub_left b64) - hp.stk_t (hp.stk_s.sub_right (cmp_sub s₀)) (hp.stk_s.sub_right fun a ha => scr_sub s₀ (o := 192) (n := 64) (by omega) a (b64 a ha)) ?_ ?_ - fun s' hrd hwr hcs hf hst => k s' ⟨hrd, hwr, fun r hr => hcs r (by - simp only [kept, List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl | rfl | rfl <;> simp [calleeSaved]), hf⟩ (by rw [hst, ea]) - · rw [ea] - refine Covers.of_sub fun r hr => ?_ - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - subst hr - exact ⟨scR s₀, List.mem_append_right _ hsc, 192, rfl, by simp⟩ - · 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 - · exact ⟨tR s₀, htr, 0, by simp, by simp⟩ - · exact ⟨scR s₀, hsc, 0, by simp, by simp⟩ - /-! ## The digest into the block -/ /-- The digest of the hash value in `t` into the block. -/ diff --git a/lean/VerifiedGarbage/Proof/Pbkdf2/X86/Iterate.lean b/lean/VerifiedGarbage/Proof/Pbkdf2/X86/Iterate.lean index 076051728..f7ac32988 100644 --- a/lean/VerifiedGarbage/Proof/Pbkdf2/X86/Iterate.lean +++ b/lean/VerifiedGarbage/Proof/Pbkdf2/X86/Iterate.lean @@ -6,8 +6,10 @@ import VerifiedGarbage.Spec.Pbkdf2.Contract /-! # PBKDF2-HMAC-SHA-256's iteration on x86 (32-bit) -Untrusted: everything here is checked by Lean. The prologue, the epilogue, -and `Verified`. Constant time is proven by the taint analysis: the argument +Untrusted: everything here is checked by Lean. The compressor-dependent +correctness proof is generic in `Proof/Pbkdf2/Sha256/X86.lean`; this module keeps +the shared prologue, epilogue, contract and scalar constant-time facts. +Constant time is proven by the taint analysis: the argument words holding `t` and `scratch` are the bases of the two writable regions, and the code keeps them in `ebx` and `ebp` across the calls, so the registers `vg_sha256_compress` saves in its scratch space and restores are @@ -406,11 +408,6 @@ theorem epilogue_ok {s₀ : State} (hp : Pre s₀) {s : State} (h : Inv s₀ 0 s /-! ## Correctness -/ -theorem correct {s₀ : State} (hp : Pre s₀) : WP isa iterate s₀ (Post s₀) := by - unfold iterate - refine WP.seq (WP.mono (prologue_ok hp) fun s₁ ⟨h₁, z₁⟩ => ?_) - exact WP.seq (WP.mono (loop_ok hp h₁ z₁) fun s₂ h₂ => epilogue_ok hp h₂) - /-! ## Constant time -/ /-- The initial taint: the stack arguments are public, the words holding `t` @@ -495,11 +492,6 @@ theorem sat_pre : Proof.Pbkdf2.iterateSha256X86.pre sat := by simp only [Region.Contains, sat] at h₁ h₂ bv_omega -theorem iterate_correct (s : State) (hs : Proof.Pbkdf2.iterateSha256X86.pre s) : - ∃ t s', Exec isa iterate s t s' ∧ abiPreserved s s' ∧ Proof.Pbkdf2.iterateSha256X86.post s s' := by - obtain ⟨t, s', he, h⟩ := correct (pre_of hs) - exact ⟨t, s', he, h⟩ - theorem iterate_ct : ConstantTime isa Proof.Pbkdf2.iterateSha256X86.pre Proof.Pbkdf2.iterateSha256X86.pub iterate := VG.Taint.constantTime (A := taint) τ₀ (fun _ _ h₁ h₂ hp => agree₀ h₁ h₂ hp) (by taint_decide) @@ -566,35 +558,4 @@ theorem iterateWide_implies : iterateWide.Implies (Spec.Pbkdf2.iterateSha256Cont Proof.Pbkdf2.iterateSha256X86, X86.abi, X86.argSlots, X86.argVal, X86.argBytes] [a0, a1, a2, a3, a4, e, esp] using wideSat -/-- The proof is written against `iterateSha256X86`, widened to the shared -contract's scratch and to writable arguments. -/ -theorem iterate_verified : - Verified X86.target Impl.Pbkdf2.X86.iterate (Spec.Pbkdf2.iterateSha256Contract X86.abi 20) := - have hsat := iterateWide_implies.sat_left - (Verified.narrowTo (Verified.of_correct iterate_correct iterate_ct (.refl ⟨sat, sat_pre⟩)) - narrowRd narrowWr iterateWide_pre - (fun _ h => by - obtain ⟨h₁, h₂, _⟩ := h - rw [h₁, h₂] - refine Covers.of_sub fun r hr => ?_ - simp only [narrowRd, narrowWr, 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 - · exact ⟨_, List.mem_append_left _ List.mem_cons_self, 0, by simp, by simp⟩ - · exact ⟨_, List.mem_append_left _ (List.mem_cons_of_mem _ List.mem_cons_self), 0, by simp, by simp⟩ - · exact ⟨_, List.mem_append_right _ (List.mem_cons_of_mem _ (List.mem_cons_of_mem _ List.mem_cons_self)), - 0, by simp, by simp⟩ - · exact ⟨_, List.mem_append_right _ List.mem_cons_self, 0, by simp, by simp⟩ - · exact ⟨_, List.mem_append_right _ (List.mem_cons_of_mem _ List.mem_cons_self), 0, by simp, by simp⟩) - (fun _ h => by - obtain ⟨_, h₂, _⟩ := h - rw [h₂] - refine Covers.of_sub fun r hr => ?_ - simp only [narrowWr, List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl - · exact ⟨_, List.mem_cons_self, 0, by simp, by simp⟩ - · exact ⟨_, List.mem_cons_of_mem _ List.mem_cons_self, 0, by simp, by simp⟩) - (fun _ _ _ h => by narrow at h ⊢; exact h) - (fun _ _ _ _ h => by narrow; exact h) hsat).of_implies iterateWide_implies - end VG.Proof.Pbkdf2.X86 diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86/Shared.lean b/lean/VerifiedGarbage/Proof/Sha256/X86/Shared.lean index b5e3848f5..98d5a4d79 100644 --- a/lean/VerifiedGarbage/Proof/Sha256/X86/Shared.lean +++ b/lean/VerifiedGarbage/Proof/Sha256/X86/Shared.lean @@ -338,9 +338,9 @@ theorem compressWide_verified (hsat : ∃ s, compressWide.pre s) : (fun _ _ _ _ h => by narrow; exact h) hsat /-- `update` only reads its arguments. -/ -theorem updateWide_verified (hsat : ∃ s, updateWide.pre s) : - Verified X86.target Impl.Sha256.X86.Stream.update updateWide := - Verified.narrowTo Proof.Sha256.X86.Stream.Update.update_verified +theorem updateWide_of {code : Prog isa} (hv : Verified X86.target code Proof.Sha256.updateX86) + (hsat : ∃ s, updateWide.pre s) : Verified X86.target code updateWide := + Verified.narrowTo hv (fun s => [⟨(arg s 3).setWidth 64, (arg s 4).toNat⟩, ⟨argAddr s 0, 24⟩]) (fun s => [⟨(arg s 0).setWidth 64, 96⟩, ⟨(arg s 5).setWidth 64, 160⟩]) (fun _ h => by @@ -372,9 +372,9 @@ theorem updateWide_verified (hsat : ∃ s, updateWide.pre s) : (fun _ _ _ h => by narrow at h ⊢; exact h) (fun _ _ _ _ h => by narrow; exact h) hsat -theorem finalizeWide_verified (hsat : ∃ s, finalizeWide.pre s) : - Verified X86.target Impl.Sha256.X86.Stream.finalize finalizeWide := - Verified.widen Proof.Sha256.X86.Stream.Finalize.finalize_verified +theorem finalizeWide_of {code : Prog isa} (hv : Verified X86.target code Proof.Sha256.finalizeX86) + (hsat : ∃ s, finalizeWide.pre s) : Verified X86.target code finalizeWide := + Verified.widen hv (fun s => [⟨(arg s 0).setWidth 64, 96⟩, ⟨(arg s 3).setWidth 64, 32⟩, ⟨(arg s 4).setWidth 64, 160⟩, ⟨argAddr s 0, 20⟩]) (fun _ h => by @@ -427,7 +427,7 @@ theorem updateWide_implies : updateWide.Implies (Spec.Sha256.updateContract X86. theorem update : Verified X86.target Impl.Sha256.X86.Stream.update (Spec.Sha256.updateContract X86.abi 20) := - (updateWide_verified updateWide_implies.sat_left).of_implies updateWide_implies + (updateWide_of Proof.Sha256.X86.Stream.Update.update_verified updateWide_implies.sat_left).of_implies updateWide_implies theorem finalizeWide_implies : finalizeWide.Implies (Spec.Sha256.finalizeContract X86.abi 20) := by contract_implies [Spec.Sha256.finalizeContract, Spec.Sha256.finalizeSig, finalizeWide, @@ -438,6 +438,6 @@ theorem finalizeWide_implies : finalizeWide.Implies (Spec.Sha256.finalizeContrac theorem finalize : Verified X86.target Impl.Sha256.X86.Stream.finalize (Spec.Sha256.finalizeContract X86.abi 20) := - (finalizeWide_verified finalizeWide_implies.sat_left).of_implies finalizeWide_implies + (finalizeWide_of Proof.Sha256.X86.Stream.Finalize.finalize_verified finalizeWide_implies.sat_left).of_implies finalizeWide_implies end VG.Proof.Sha256.X86.Shared diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Common.lean b/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Common.lean index 2c8b503cb..c2665e095 100644 --- a/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Common.lean +++ b/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Common.lean @@ -10,7 +10,9 @@ import VerifiedGarbage.Proof.Framework.Offset /-! # Streaming SHA-256 on x86 (32-bit): common lemmas -Untrusted: everything here is checked by Lean. Per-instruction WP rules that +Untrusted: everything here is checked by Lean. The compressor-dependent +correctness proof is generic in `Proof/Sha256/X86/Stream/CompressAt.lean`; this module keeps +the shared memory, state and scalar constant-time facts. Per-instruction WP rules that expose only what changes, the call of the compression function (`compressAt`), and arithmetic on 32-bit values. -/ @@ -234,101 +236,6 @@ theorem within {r : Region} {rs' : List Region} (r' : Region) (hr' : r' ∈ rs') ∃ r' ∈ rs', ∃ o, r.base = r'.base + BitVec.ofNat 64 o ∧ o + r.len ≤ r'.len := ⟨r', hr', o, hb, hl⟩ -/-- Compressing the block at `eax` (`blk`) into the hash value at `st` (in -register `sr`), with the scratch space at `scr` (in register `cr`): a call of -`vg_sha256_compress(st, blk, 1, scr)` in a frame of its arguments, which -uses the 20 bytes below `esp` (`E`) and writes only there, the hash value -and the first 112 bytes of the scratch space. -/ -theorem compressAt_ok {sr cr : Reg} (hsr : sr ≠ .esp) (hcr : cr ≠ .esp) (hsr' : sr ≠ .ecx) - (hcr' : cr ≠ .ecx) {s : State} {st scr blk E : BitVec 32} - (hesp : s.gpr .esp = E) (hS : s.gpr sr = st) (hC : s.gpr cr = scr) (heax : s.gpr .eax = blk) - (hE : 20 ≤ E.toNat) (f₀ : st.toNat + 32 ≤ 2 ^ 32) (f₁ : blk.toNat + 64 ≤ 2 ^ 32) - (f₃ : scr.toNat + 112 ≤ 2 ^ 32) - (d₁ : Region.Disjoint ⟨st.setWidth 64, 32⟩ ⟨scr.setWidth 64, 112⟩) - (d₂ : Region.Disjoint ⟨blk.setWidth 64, 64⟩ ⟨st.setWidth 64, 32⟩) - (d₃ : Region.Disjoint ⟨blk.setWidth 64, 64⟩ ⟨scr.setWidth 64, 112⟩) - (dS : Region.Disjoint (below E 20) ⟨st.setWidth 64, 32⟩) - (dC : Region.Disjoint (below E 20) ⟨scr.setWidth 64, 112⟩) - (dB : Region.Disjoint (below E 20) ⟨blk.setWidth 64, 64⟩) - (hc : Covers [⟨blk.setWidth 64, 64⟩] (s.rd ++ s.wr)) - (hw : Covers [⟨st.setWidth 64, 32⟩, ⟨scr.setWidth 64, 112⟩] s.wr) - {Q : State → Prop} - (hQ : ∀ s', s'.rd = s.rd → s'.wr = s.wr → (∀ r ∈ calleeSaved, s'.gpr r = s.gpr r) → - Frame [⟨st.setWidth 64, 32⟩, ⟨scr.setWidth 64, 112⟩, below E 20] s.mem s'.mem → - stateAt s'.mem (st.setWidth 64) = - compress (stateAt s.mem (st.setWidth 64)) (blockAt s.mem (blk.setWidth 64)) → Q s') : - WP isa (compressAt sr cr) s Q := by - unfold compressAt - refine WP.seq (WP.cons (s' := s.setReg .ecx 1) rfl (WP.block_nil ?_)) - set s₁ := s.setReg .ecx 1 with hs₁ - have g₁ : ∀ r, r ≠ .ecx → s₁.gpr r = s.gpr r := fun r h => by simp [hs₁, State.setReg, h] - have fit : 4 * [cr, Reg.ecx, .eax, sr].length + 4 ≤ (s₁.gpr .esp).toNat := by - rw [g₁ _ (by decide), hesp]; simp only [List.length_cons, List.length_nil]; omega - have hrs : Reg.esp ∉ [cr, Reg.ecx, .eax, sr] := by simp [Ne.symm hsr, Ne.symm hcr] - set sE := (pushed [cr, Reg.ecx, .eax, sr] s₁).callEntry with hsE - have a0 : arg sE 0 = st := by rw [hsE, callEntry_arg fit hrs (by simp)]; simp [g₁ _ hsr', hS] - have a1 : arg sE 1 = blk := by rw [hsE, callEntry_arg fit hrs (by simp)]; simp [g₁ Reg.eax (by decide), heax] - have a2 : arg sE 2 = 1 := by rw [hsE, callEntry_arg fit hrs (by simp)]; simp [hs₁, State.setReg] - have a3 : arg sE 3 = scr := by rw [hsE, callEntry_arg fit hrs (by simp)]; simp [g₁ _ hcr', hC] - have eA : argAddr sE 0 = (E - BitVec.ofNat 32 16).setWidth 64 := by - rw [hsE, callEntry_argAddr0, g₁ _ (by decide), hesp]; rfl - have eSp : sE.gpr .esp = E - BitVec.ofNat 32 20 := by - rw [hsE, callEntry_esp', g₁ _ (by decide), hesp]; rfl - have b16 : Region.Sub (below E 16) (below E 20) := below_sub (by omega) hE - have r4 : Region.Sub ⟨(E - BitVec.ofNat 32 20).setWidth 64, 4⟩ (below E 20) := by - have := below_inner (sp := E) (a := 4) (b := 20) (k := 16) (by omega) hE - rw [show E - BitVec.ofNat 32 20 = E - BitVec.ofNat 32 16 - BitVec.ofNat 32 4 by - rw [← VG.Offset.sub_add_eq]; rfl] - exact this - have hesp₁ : s₁.gpr .esp = E := by rw [g₁ _ (by decide), hesp] - refine WP.callWith (k := Proof.Sha256.compressX86) compress_verified.1 compress_nosp (by simp) hrs - (by rw [compress_stack, hesp₁]; simp only [List.length_cons, List.length_nil]; omega) - (rd := [⟨blk.setWidth 64, 64 * (1 : BitVec 32).toNat⟩, ⟨argAddr sE 0, 16⟩]) - (wr := [⟨st.setWidth 64, 32⟩, ⟨scr.setWidth 64, 112⟩]) - ⟨?_, ?_, ?_⟩ fun s' rd' wr' cs' f' ⟨s₂, m₂, post⟩ => ?_ - · rw [← hsE] - simp only [Proof.Sha256.compressX86, State.withRegions_rd, State.withRegions_wr, State.withRegions_gpr, - arg_withRegions, argAddr_withRegions, a0, a1, a2, a3, eA, eSp] - refine ⟨trivial, trivial, d₁, d₂, d₃, dS.sub_left b16, dC.sub_left b16, - dS.sub_left r4, dC.sub_left r4, f₀, by simpa using f₁, f₃, ?_⟩ - rw [sub_toNat hE]; have := E.isLt; omega - · rw [hesp₁] - 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 - · obtain ⟨r', hr', hc'⟩ := hc a n ⟨_, List.mem_singleton_self _, by simpa using hcn⟩ - exact InRegions_append_cons.mpr (.inr ⟨r', hr', hc'⟩) - · refine InRegions_append_cons.mpr (.inl ?_) - rw [eA] at hcn - simp only [Region.Contains] at hcn ⊢ - simpa using hcn - · obtain ⟨r', hr', hc'⟩ := hw a n ⟨_, by simp, hcn⟩ - exact InRegions_append_cons.mpr (.inr ⟨r', List.mem_append_right _ hr', hc'⟩) - · obtain ⟨r', hr', hc'⟩ := hw a n ⟨_, by simp, hcn⟩ - exact InRegions_append_cons.mpr (.inr ⟨r', List.mem_append_right _ hr', hc'⟩) - · rw [hesp₁] - intro a n ⟨r, hr, hcn⟩ - obtain ⟨r', hr', hc'⟩ := hw a n ⟨r, hr, hcn⟩ - exact ⟨r', List.mem_cons_of_mem _ hr', hc'⟩ - · rw [compress_stack, hesp₁] at f' - have hsE' : Frame [below E 20] s.mem sE.mem := by - have := callEntry_frame fit hrs - rw [hesp₁] at this; exact this - rw [← hsE] at post - simp only [Proof.Sha256.compressX86, arg_withRegions, State.withRegions_mem, a0, a1, a2, m₂, - show (1 : BitVec 32).toNat = 1 from rfl, compressBlocks_one] at post - rw [hs₁] at f' - refine hQ s' rd' wr' (fun r hr => ?_) (by simpa [State.setReg] using f') ?_ - · rw [cs' r hr, g₁ r (by simp [calleeSaved] at hr; rcases hr with rfl | rfl | rfl | rfl | rfl <;> decide)] - · have e₁ : stateAt sE.mem (st.setWidth 64) = stateAt s.mem (st.setWidth 64) := - Proof.Sha256.Stream.stateAt_congr fun i hi => - hsE'.bytes (R := ⟨st.setWidth 64, 32⟩) (by simpa using dS.symm) (by simp) hi - have e₂ : blockAt sE.mem (blk.setWidth 64) = blockAt s.mem (blk.setWidth 64) := by - simp only [blockAt] - exact Proof.Sha256.Stream.parseBlock_congr fun k hk => - hsE'.bytes (R := ⟨blk.setWidth 64, 64⟩) (by simpa using dB.symm) (by simp) hk - rw [post, e₁, e₂] - /-! ## Arithmetic -/ theorem ofNat_beq_zero {k : Nat} (h : k < 2 ^ 32) : (BitVec.ofNat 32 k == 0) = decide (k = 0) := by diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/CompressAt.lean b/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/CompressAt.lean new file mode 100644 index 000000000..7734252ec --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/CompressAt.lean @@ -0,0 +1,108 @@ +import VerifiedGarbage.Proof.Sha256.X86.Stream.Common +import VerifiedGarbage.Impl.MdStream.X86 +import VerifiedGarbage.Proof.Framework.X86.RegUpd + +/-! The framed single-block compression proof, independent of backend. -/ +namespace VG.Proof.Sha256.X86.Stream +open VG.X86 +open VG.X86.RegUpd +open VG.Spec.Sha256 (stateAt compress blockAt) +variable {name : String} {code : Prog isa} + (hv : Verified X86.target code Proof.Sha256.compressX86) + (hnosp : NoSp code) (hstack : stackUse code = 0) +include hv hnosp hstack + +theorem compressAt_of {sr cr : Reg} (hsr : sr ≠ .esp) (hcr : cr ≠ .esp) (hsr' : sr ≠ .ecx) + (hcr' : cr ≠ .ecx) {s : State} {st scr blk E : BitVec 32} + (hesp : s.gpr .esp = E) (hS : s.gpr sr = st) (hC : s.gpr cr = scr) (heax : s.gpr .eax = blk) + (hE : 20 ≤ E.toNat) (f₀ : st.toNat + 32 ≤ 2 ^ 32) (f₁ : blk.toNat + 64 ≤ 2 ^ 32) + (f₃ : scr.toNat + 112 ≤ 2 ^ 32) + (d₁ : Region.Disjoint ⟨st.setWidth 64, 32⟩ ⟨scr.setWidth 64, 112⟩) + (d₂ : Region.Disjoint ⟨blk.setWidth 64, 64⟩ ⟨st.setWidth 64, 32⟩) + (d₃ : Region.Disjoint ⟨blk.setWidth 64, 64⟩ ⟨scr.setWidth 64, 112⟩) + (dS : Region.Disjoint (below E 20) ⟨st.setWidth 64, 32⟩) + (dC : Region.Disjoint (below E 20) ⟨scr.setWidth 64, 112⟩) + (dB : Region.Disjoint (below E 20) ⟨blk.setWidth 64, 64⟩) + (hc : Covers [⟨blk.setWidth 64, 64⟩] (s.rd ++ s.wr)) + (hw : Covers [⟨st.setWidth 64, 32⟩, ⟨scr.setWidth 64, 112⟩] s.wr) + {Q : State → Prop} + (hQ : ∀ s', s'.rd = s.rd → s'.wr = s.wr → (∀ r ∈ calleeSaved, s'.gpr r = s.gpr r) → + Frame [⟨st.setWidth 64, 32⟩, ⟨scr.setWidth 64, 112⟩, below E 20] s.mem s'.mem → + stateAt s'.mem (st.setWidth 64) = + compress (stateAt s.mem (st.setWidth 64)) (blockAt s.mem (blk.setWidth 64)) → Q s') : + WP isa (Impl.MdStream.X86.compressAt name code sr cr) s Q := by + unfold Impl.MdStream.X86.compressAt Impl.MdStream.X86.compressWith + refine WP.seq (WP.cons (s' := s.setReg .ecx 1) rfl (WP.block_nil ?_)) + set s₁ := s.setReg .ecx 1 with hs₁ + have g₁ : ∀ r, r ≠ .ecx → s₁.gpr r = s.gpr r := fun r h => by rw [hs₁, gpr_setReg_of_ne s 1 h] + have fit : 4 * [cr, Reg.ecx, .eax, sr].length + 4 ≤ (s₁.gpr .esp).toNat := by + rw [g₁ _ (by decide), hesp]; simp only [List.length_cons, List.length_nil]; omega + have hrs : Reg.esp ∉ [cr, Reg.ecx, .eax, sr] := by simp [Ne.symm hsr, Ne.symm hcr] + set sE := (pushed [cr, Reg.ecx, .eax, sr] s₁).callEntry with hsE + have a0 : arg sE 0 = st := by rw [hsE, callEntry_arg fit hrs (by simp)]; simp [g₁ _ hsr', hS] + have a1 : arg sE 1 = blk := by rw [hsE, callEntry_arg fit hrs (by simp)]; simp [g₁ Reg.eax (by decide), heax] + have a2 : arg sE 2 = 1 := by rw [hsE, callEntry_arg fit hrs (by simp)]; change s₁.gpr .ecx = 1; rw [hs₁, gpr_setReg_self] + have a3 : arg sE 3 = scr := by rw [hsE, callEntry_arg fit hrs (by simp)]; simp [g₁ _ hcr', hC] + have eA : argAddr sE 0 = (E - BitVec.ofNat 32 16).setWidth 64 := by + rw [hsE, callEntry_argAddr0, g₁ _ (by decide), hesp]; rfl + have eSp : sE.gpr .esp = E - BitVec.ofNat 32 20 := by + rw [hsE, callEntry_esp', g₁ _ (by decide), hesp]; rfl + have b16 : Region.Sub (below E 16) (below E 20) := below_sub (by omega) hE + have r4 : Region.Sub ⟨(E - BitVec.ofNat 32 20).setWidth 64, 4⟩ (below E 20) := by + have := below_inner (sp := E) (a := 4) (b := 20) (k := 16) (by omega) hE + rw [show E - BitVec.ofNat 32 20 = E - BitVec.ofNat 32 16 - BitVec.ofNat 32 4 by + rw [← VG.Offset.sub_add_eq]; rfl] + exact this + have hesp₁ : s₁.gpr .esp = E := by rw [g₁ _ (by decide), hesp] + refine WP.callWith (k := Proof.Sha256.compressX86) hv.1 hnosp (by simp) hrs + (by rw [hstack, hesp₁]; simp only [List.length_cons, List.length_nil]; omega) + (rd := [⟨blk.setWidth 64, 64 * (1 : BitVec 32).toNat⟩, ⟨argAddr sE 0, 16⟩]) + (wr := [⟨st.setWidth 64, 32⟩, ⟨scr.setWidth 64, 112⟩]) + ⟨?_, ?_, ?_⟩ fun s' rd' wr' cs' f' ⟨s₂, m₂, post⟩ => ?_ + · rw [← hsE] + simp only [Proof.Sha256.compressX86, State.withRegions_rd, State.withRegions_wr, State.withRegions_gpr, + arg_withRegions, argAddr_withRegions, a0, a1, a2, a3, eA, eSp] + refine ⟨trivial, trivial, d₁, d₂, d₃, dS.sub_left b16, dC.sub_left b16, + dS.sub_left r4, dC.sub_left r4, f₀, by simpa using f₁, f₃, ?_⟩ + rw [sub_toNat hE]; have := E.isLt; omega + · rw [hesp₁] + 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 + · obtain ⟨r', hr', hc'⟩ := hc a n ⟨_, List.mem_singleton_self _, by simpa using hcn⟩ + exact InRegions_append_cons.mpr (.inr ⟨r', hr', hc'⟩) + · refine InRegions_append_cons.mpr (.inl ?_) + rw [eA] at hcn + simp only [Region.Contains] at hcn ⊢ + simpa using hcn + · obtain ⟨r', hr', hc'⟩ := hw a n ⟨_, by simp, hcn⟩ + exact InRegions_append_cons.mpr (.inr ⟨r', List.mem_append_right _ hr', hc'⟩) + · obtain ⟨r', hr', hc'⟩ := hw a n ⟨_, by simp, hcn⟩ + exact InRegions_append_cons.mpr (.inr ⟨r', List.mem_append_right _ hr', hc'⟩) + · rw [hesp₁] + intro a n ⟨r, hr, hcn⟩ + obtain ⟨r', hr', hc'⟩ := hw a n ⟨r, hr, hcn⟩ + exact ⟨r', List.mem_cons_of_mem _ hr', hc'⟩ + · rw [hstack, hesp₁] at f' + have hsE' : Frame [below E 20] s.mem sE.mem := by + have := callEntry_frame fit hrs + rw [hesp₁] at this; exact this + rw [← hsE] at post + simp only [Proof.Sha256.compressX86, arg_withRegions, State.withRegions_mem, a0, a1, a2, m₂, + show (1 : BitVec 32).toNat = 1 from rfl, compressBlocks_one] at post + rw [hs₁] at f' + refine hQ s' rd' wr' (fun r hr => ?_) (by + change Frame [⟨st.setWidth 64, 32⟩, ⟨scr.setWidth 64, 112⟩, below E 20] s.mem s'.mem at f' + exact f') ?_ + · rw [cs' r hr, g₁ r (by simp [calleeSaved] at hr; rcases hr with rfl | rfl | rfl | rfl | rfl <;> decide)] + · have e₁ : stateAt sE.mem (st.setWidth 64) = stateAt s.mem (st.setWidth 64) := + Proof.Sha256.Stream.stateAt_congr fun i hi => + hsE'.bytes (R := ⟨st.setWidth 64, 32⟩) (by simpa using dS.symm) (by simp) hi + have e₂ : blockAt sE.mem (blk.setWidth 64) = blockAt s.mem (blk.setWidth 64) := by + simp only [blockAt] + exact Proof.Sha256.Stream.parseBlock_congr fun k hk => + hsE'.bytes (R := ⟨blk.setWidth 64, 64⟩) (by simpa using dB.symm) (by simp) hk + rw [post, e₁, e₂] + + +end VG.Proof.Sha256.X86.Stream diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Finalize.lean b/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Finalize.lean index cdc1302ec..f5e30e628 100644 --- a/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Finalize.lean +++ b/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Finalize.lean @@ -4,14 +4,13 @@ import VerifiedGarbage.Proof.Sha256.X86.Contract /-! # Streaming SHA-256 on x86 (32-bit): the loop of `finalize` -Untrusted: everything here is checked by Lean. `finalize` itself is verified -by the generic proof (`Proof/Sha256/X86/Shared.lean`); HMAC-SHA256 on x86 -(`Proof/Hmac/X86/`), whose `finalize` reuses its code, and SHA-512 on x86 -use the pieces here: its prologue and loop body (`prologue_ok`, `body_ok`), -with `state` in `ebx`, `scratch` in `ebp`, the buffered bytes in `edi`, -whether the block being padded is not the last in `esi`, and `count` and -`out` in `scratch[128..140)`. Each compression calls the compression -function (`compressAt_ok`), which uses the 20 bytes below `esp`. +Untrusted: everything here is checked by Lean. The compressor-dependent +correctness proof is generic in `Proof/Sha256/X86/Stream/FinalizeVariant.lean`. +This module keeps the shared memory, state, prologue and scalar constant-time +facts used by the generic proof, HMAC-SHA256 and SHA-512 on x86. +The state is in `ebx`, scratch in `ebp`, buffered bytes in `edi`, and the +padding-loop flag in `esi`; count and output are in `scratch[128..140)`. +Each compression call uses the 20 bytes below `esp`. -/ namespace VG.Proof.Sha256.X86.Stream.Finalize @@ -277,65 +276,6 @@ theorem zero_ok {s₀ : State} (hp : Pre s₀) {sI : State} (hC : Common s₀ sI /-! ## One block -/ /-- The compression of the buffer. -/ -theorem compress_buf {s₀ : State} (hp : Pre s₀) {s : State} (hC : Common s₀ s) - (heax : s.gpr .eax = st s₀ + BitVec.ofNat 32 32) {Q : State → Prop} - (hQ : ∀ s', Common s₀ s' → (∀ r ∈ calleeSaved, s'.gpr r = s.gpr r) → - stateAt s'.mem (stA s₀) = compress (stateAt s.mem (stA s₀)) (blockAt s.mem (stA s₀ + 32)) → Q s') : - WP isa (compressAt .ebx .ebp) s Q := by - have hst := hp.st_fit; have hsc := hp.scr_fit; have hsp := hp.sp_fit - have e32 : Region.Sub ⟨stA s₀, 32⟩ (stR s₀) := Region.sub_prefix (by omega) - have e112 : Region.Sub ⟨scA s₀, 112⟩ (scR s₀) := Region.sub_prefix (by omega) - have hb : (st s₀ + BitVec.ofNat 32 32).setWidth 64 = stA s₀ + BitVec.ofNat 64 32 := addr_eq (by omega) - have eb : Region.Sub ⟨(st s₀ + BitVec.ofNat 32 32).setWidth 64, 64⟩ (stR s₀) := by - rw [hb]; exact sub_offset (by omega) (by omega) - refine compressAt_ok (st := st s₀) (scr := scr s₀) (blk := st s₀ + BitVec.ofNat 32 32) (E := esp₀ s₀) - (by decide) (by decide) (by decide) (by decide) hC.esp hC.ebx hC.ebp heax hp.sp_lo (by omega) - (by rw [BitVec.toNat_add, toNat_ofNat_lt (by omega), Nat.mod_eq_of_lt (by omega)]; omega) (by omega) - ((hp.st_scr.sub_left e32).sub_right e112) ?_ ((hp.st_scr.sub_left eb).sub_right e112) - (hp.stk_st.sub_right e32) (hp.stk_scr.sub_right e112) (hp.stk_st.sub_right eb) ?_ ?_ ?_ - · rw [hb]; exact Offset.disjoint_base _ (Nat.le_refl _) (by omega) - · rw [hC.rd, hC.wr, hp.rd, hp.wr] - apply Covers.of_sub - intro r hr - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - subst hr - exact ⟨stR s₀, by simp, 32, hb, by simp⟩ - · rw [hC.wr, hp.wr] - apply Covers.of_sub - intro r hr - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl - · exact ⟨stR s₀, by simp, 0, by simp, by simp⟩ - · exact ⟨scR s₀, by simp, 0, by simp, by simp⟩ - · intro s' hrd hwr hcs hf hstate - have cs : ∀ r ∈ calleeSaved, s'.gpr r = s.gpr r := hcs - have word : ∀ d, 112 ≤ d → d + 4 ≤ 160 → - s'.mem.readW (addr (scr s₀) d) 32 = s.mem.readW (addr (scr s₀) d) 32 := by - intro d h₁ h₂ - refine hf.readW (r := ⟨addr (scr s₀) d, 4⟩) (Region.contains_self _ _) ?_ (by decide) - intro r hr - 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 (hp.scr_sub h₂)).sub_right e32 - · rw [addr_eq (by omega)]; exact Offset.disjoint_base _ (by omega) (by omega) - · exact hp.stk_scr.symm.sub_left (hp.scr_sub h₂) - refine hQ s' ⟨hrd.trans hC.rd, hwr.trans hC.wr, by rw [cs _ (by decide)]; exact hC.ebx, - by rw [cs _ (by decide)]; exact hC.ebp, by rw [cs _ (by decide)]; exact hC.esp, - hC.frame.trans (hf.sub ?_), fun p hp' => ?_, by rw [word 128 (by omega) (by omega)]; exact hC.lo, - by rw [word 132 (by omega) (by omega)]; exact hC.hi, by rw [word 136 (by omega) (by omega)]; exact hC.outp⟩ - hcs (by rw [hstate, show (st s₀ + BitVec.ofNat 32 32).setWidth 64 = stA s₀ + 32 from hb]) - · intro r hr - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl - · exact ⟨stR s₀, by simp, e32⟩ - · exact ⟨scR s₀, by simp, e112⟩ - · exact ⟨stkR s₀, by simp, fun _ h => h⟩ - · have hd : 112 ≤ p.2 ∧ p.2 + 4 ≤ 128 := by - simp only [VG.Impl.Sha256.X86.Stream.saved, List.mem_cons, List.not_mem_nil, or_false] at hp' - rcases hp' with rfl | rfl | rfl | rfl <;> simp - rw [word p.2 hd.1 (by omega)] - exact hC.saved p hp' - theorem times8 (x : BitVec 32) : x + x + (x + x) + (x + x + (x + x)) = x <<< 3 := by apply BitVec.eq_of_toNat_eq simp only [BitVec.toNat_add, BitVec.toNat_shiftLeft, Nat.shiftLeft_eq] @@ -424,151 +364,6 @@ theorem regs3 {r : Reg} (hr : r ∈ [Reg.ebx, .ebp, .esp]) : r ≠ .eax ∧ r simp only [List.mem_cons, List.not_mem_nil, or_false] at hr rcases hr with rfl | rfl | rfl <;> decide -theorem body_ok {s₀ : State} (hp : Pre s₀) {k n : Nat} {s : State} (h : LInv s₀ k n s) : - WP isa finalizeBody s (Step s₀ k) := by - have hk := h.k_le; have hn := h.n_le; have hst := hp.st_fit - have hC := h.toCommon - unfold finalizeBody - -- `eax := 64` or `56`: the end of the zeros. - refine WP.seq (wp_movi fun s₁ u₁ => wp_test fun s₂ f₂ z₂ => WP.block_nil ?_) - have hz₂ : s₂.zf = some (decide (k = 0)) := by - rw [z₂, u₁.other _ (by decide), h.esi, BitVec.and_self, ofNat_beq_zero (by omega)] - refine WP.seq (WP.mono (Q := fun (s₃ : State) => s₃.gpr .eax = BitVec.ofNat 32 (56 + 8 * k) ∧ - (∀ r, r ≠ .eax → s₃.gpr r = s.gpr r) ∧ s₃.mem = s.mem ∧ s₃.rd = s.rd ∧ s₃.wr = s.wr) ?_ - fun s₃ ⟨heax₃, g₃, m₃, rd₃, wr₃⟩ => ?_) - · refine WP.ite (decide (k = 0)) (by show s₂.zf = _; rw [hz₂]) (fun hb => ?_) (fun hb => ?_) - · simp only [decide_eq_true_eq] at hb; subst hb - refine wp_movi fun s₃ u₃ => WP.block_nil ⟨by rw [u₃.gpr]; rfl, fun r hr => ?_, ?_, ?_, ?_⟩ - · rw [u₃.other r hr, f₂.gpr, u₁.other r hr] - · rw [u₃.mem, f₂.mem, u₁.mem] - · rw [u₃.rd, f₂.rd, u₁.rd] - · rw [u₃.wr, f₂.wr, u₁.wr] - · simp only [decide_eq_false_iff_not] at hb - refine WP.block_nil ⟨by rw [f₂.gpr, u₁.gpr, show k = 1 by omega]; rfl, fun r hr => ?_, ?_, ?_, ?_⟩ - · rw [f₂.gpr, u₁.other r hr] - · rw [f₂.mem, u₁.mem] - · rw [f₂.rd, u₁.rd] - · rw [f₂.wr, u₁.wr] - -- `ecx := 0; eax -= edi`: zero the rest of the buffer, up to `lim`. - have hC₃ : Common s₀ s₃ := hC.of_gpr (fun r hr => g₃ r (regs3 hr).1) m₃ rd₃ wr₃ - refine WP.seq (wp_movi fun s₄ u₄ => wp_sub fun s₅ u₅ z₅ => WP.block_nil ?_) - have hC₄ : Common s₀ s₄ := hC₃.of_gpr (fun r hr => u₄.other r (regs3 hr).2.1) u₄.mem u₄.rd u₄.wr - have hecx₄ : s₄.gpr .ecx = 0 := u₄.gpr - have hedi₄ : s₄.gpr .edi = BitVec.ofNat 32 n := by rw [u₄.other _ (by decide), g₃ _ (by decide), h.edi] - have heax₅ : s₅.gpr .eax = BitVec.ofNat 32 (56 + 8 * k - n) := by - rw [u₅.gpr, u₄.other _ (by decide), heax₃, hedi₄, sub_ofNat (a := 56 + 8 * k) (b := n) (by omega)] - have hZ : Zero s₀ s₄ n (56 + 8 * k) 0 s₅ := by - refine ⟨Nat.zero_le _, fun r hr => u₅.other r ?_, u₅.rd, u₅.wr, - by rw [u₅.other _ (by decide), hedi₄, Nat.add_zero], by rw [heax₅, Nat.sub_zero], - by rw [u₅.mem, List.replicate_zero, writeBytes_nil]⟩ - simp only [List.mem_cons, List.not_mem_nil, or_false] at hr - rcases hr with rfl | rfl | rfl | rfl | rfl <;> decide - have hz₅ : s₅.zf = some (decide (56 + 8 * k - n = 0)) := by - rw [z₅, ← u₅.gpr, heax₅, ofNat_beq_zero (by omega)] - refine WP.seq (WP.mono (zero_ok hp hC₄ hecx₄ (by omega) hn hZ hz₅) fun s₆ hZ₆ => ?_) - have hm₄ : s₄.mem = s.mem := by rw [u₄.mem, m₃] - have hf₆ : Frame [stR s₀] s₄.mem s₆.mem := by - rw [hZ₆.mem]; exact buf_frame _ (by simp only [List.length_replicate]; omega) - obtain ⟨hfr₆, hsv₆, hlo₆, hhi₆, hout₆⟩ := hC₄.frame_keep hp (hf₆.mono (by simp)) - have hC₆ : Common s₀ s₆ := ⟨hZ₆.rd.trans hC₄.rd, hZ₆.wr.trans hC₄.wr, by rw [hZ₆.keep _ (by simp), hC₄.ebx], - by rw [hZ₆.keep _ (by simp), hC₄.ebp], by rw [hZ₆.keep _ (by simp), hC₄.esp], hfr₆, hsv₆, hlo₆, hhi₆, hout₆⟩ - have hst₆ : stateAt s₆.mem (stA s₀) = stateAt s.mem (stA s₀) := by - rw [hZ₆.mem, hm₄] - apply stateAt_congr - intro i hi - rw [st_add] - exact writeBytes_before _ _ _ (by omega) (by simp only [List.length_replicate]; omega) - have hby₆ : bytesAt s₆.mem (stA s₀ + 32) (56 + 8 * k) = - bytesAt s.mem (stA s₀ + 32) n ++ List.replicate (56 + 8 * k - n) 0 := by - rw [hZ₆.mem, hm₄, ← bytesAt_writeBytes _ _ _ _ (by simp only [List.length_replicate]; omega)] - congr 1; simp only [List.length_replicate]; omega - have hesi₆ : s₆.gpr .esi = BitVec.ofNat 32 k := by - rw [hZ₆.keep _ (by simp), u₄.other _ (by decide), g₃ _ (by decide), h.esi] - -- In the last block, the length. - refine WP.seq (wp_test fun s₇ f₇ z₇ => WP.block_nil ?_) - have hC₇ : Common s₀ s₇ := hC₆.of_gpr (fun r _ => by rw [f₇.gpr]) f₇.mem f₇.rd f₇.wr - have hz₇ : s₇.zf = some (decide (k = 0)) := by - rw [z₇, hesi₆, BitVec.and_self, ofNat_beq_zero (by omega)] - have hesi₇ : s₇.gpr .esi = BitVec.ofNat 32 k := by rw [f₇.gpr, hesi₆] - refine WP.seq (WP.mono (Q := fun (s₈ : State) => Common s₀ s₈ ∧ s₈.gpr .esi = BitVec.ofNat 32 k ∧ - stateAt s₈.mem (stA s₀) = stateAt s.mem (stA s₀) ∧ - ∀ m, R₀ s₀ m → bytesAt s₈.mem (stA s₀ + 32) 64 = bytesAt s.mem (stA s₀ + 32) n ++ - (if k = 1 then List.replicate (64 - n) 0 else List.replicate (56 - n) 0 ++ lenBytes m)) ?_ - fun s₈ ⟨hC₈, hesi₈, hst₈, hby₈⟩ => ?_) - · refine WP.ite (decide (k = 0)) (by show s₇.zf = _; rw [hz₇]) (fun hb => ?_) (fun hb => ?_) - · simp only [decide_eq_true_eq] at hb; subst hb - refine WP.mono (len_ok hp hC₇) fun s₈ ⟨g₈, rd₈, wr₈, m₈⟩ => ?_ - have hfL : Frame [stR s₀] s₇.mem s₈.mem := by - rw [m₈]; exact buf_frame _ (by simp [lenL, wordBytes]) - obtain ⟨hfr, hsv, hlo, hhi, hout⟩ := hC₇.frame_keep hp (hfL.mono (by simp)) - refine ⟨⟨rd₈.trans hC₇.rd, wr₈.trans hC₇.wr, by rw [g₈ _ (by decide) (by decide) (by decide), hC₇.ebx], - by rw [g₈ _ (by decide) (by decide) (by decide), hC₇.ebp], - by rw [g₈ _ (by decide) (by decide) (by decide), hC₇.esp], hfr, hsv, hlo, hhi, hout⟩, - by rw [g₈ _ (by decide) (by decide) (by decide), hesi₇], ?_, fun m hm => ?_⟩ - · rw [m₈, ← hst₆, ← f₇.mem] - apply stateAt_congr - intro i hi - rw [st_add] - exact writeBytes_before _ _ _ (by omega) (by simp [lenL, wordBytes]) - · simp only [show ¬ ((0 : Nat) = 1) by decide, ite_false] - have e := bytesAt_writeBytes s₇.mem (stA s₀ + 32) 56 (lenL s₀) (by simp [lenL, wordBytes]) - simp only [lenL, List.length_append, show ∀ w, (wordBytes w).length = 4 from fun _ => rfl] at e - rw [m₈, e, f₇.mem, hby₆, ← lenBytes_halves _ _ m hm.2] - simp [List.append_assoc] - · simp only [decide_eq_false_iff_not] at hb - have hk1 : k = 1 := by omega - subst hk1 - refine WP.block_nil ⟨hC₇, hesi₇, by rw [f₇.mem, hst₆], fun m _ => ?_⟩ - rw [f₇.mem, hby₆]; simp - -- Compress the block. - refine WP.seq (WP.mono (args_ok hC₈) fun s₉ ⟨hC₉, g₉, heax₉, hf₉⟩ => ?_) - refine WP.seq (compress_buf hp hC₉ heax₉ fun s₁₀ hC₁₀ cs₁₀ hst₁₀ => ?_) - have hesi₁₀ : s₁₀.gpr .esi = BitVec.ofNat 32 k := by - rw [cs₁₀ _ (by decide), g₉ _ (by decide), hesi₈] - have hbyte : ∀ i, i < 96 → s₉.mem (stA s₀ + BitVec.ofNat 64 i) = s₈.mem (stA s₀ + BitVec.ofNat 64 i) := - fun i hi => frame_bytes hf₉ (R := stR s₀) (by simpa using hp.a_st.symm) (by simp) hi - have hblk : ∀ m, R₀ s₀ m → blockAt s₉.mem (stA s₀ + 32) = parseBlock fun t => - (bytesAt s.mem (stA s₀ + 32) n ++ - (if k = 1 then List.replicate (64 - n) 0 else List.replicate (56 - n) 0 ++ lenBytes m)).getD t 0 := by - intro m hm - apply parseBlock_congr - intro t ht - rw [show stA s₀ + 32 + BitVec.ofNat 64 t = stA s₀ + BitVec.ofNat 64 (32 + t) by - simp only [BitVec.ofNat_add]; rw [BitVec.add_assoc]; rfl, hbyte _ (by omega), - ← show stA s₀ + 32 + BitVec.ofNat 64 t = stA s₀ + BitVec.ofNat 64 (32 + t) by - simp only [BitVec.ofNat_add]; rw [BitVec.add_assoc]; rfl] - exact bytesAt_getD (hby₈ m hm) ht - have hst₉ : stateAt s₉.mem (stA s₀) = stateAt s₈.mem (stA s₀) := - stateAt_congr fun i hi => hbyte i (by omega) - -- Next block, if any. - refine wp_movi fun s₁₁ u₁₁ => wp_subi fun s₁₂ u₁₂ z₁₂ => WP.block_nil ?_ - have hC₁₂ : Common s₀ s₁₂ := hC₁₀.of_gpr (fun r hr => by - rw [u₁₂.other r (regs3 hr).2.2.2.2, u₁₁.other r (regs3 hr).2.2.2.1]) (by rw [u₁₂.mem, u₁₁.mem]) - (by rw [u₁₂.rd, u₁₁.rd]) (by rw [u₁₂.wr, u₁₁.wr]) - have hz : s₁₂.zf = some (decide (k = 1)) := by - rw [z₁₂, u₁₁.other _ (by decide), hesi₁₀, lit32 1, sub_beq (a := k) (b := 1) (by omega) (by omega)] - have hst : ∀ m, R₀ s₀ m → stateAt s₁₂.mem (stA s₀) = compress (stateAt s.mem (stA s₀)) (parseBlock fun t => - (bytesAt s.mem (stA s₀ + 32) n ++ - (if k = 1 then List.replicate (64 - n) 0 else List.replicate (56 - n) 0 ++ lenBytes m)).getD t 0) := by - intro m hm - rw [u₁₂.mem, u₁₁.mem, hst₁₀, hst₉, hst₈, hblk m hm] - by_cases hk1 : k = 1 - · subst hk1 - refine .inr ⟨by show s₁₂.zf = _; rw [hz]; rfl, rfl, ⟨hC₁₂, by omega, by omega, ?_, ?_, fun m hm => ?_⟩⟩ - · rw [u₁₂.other _ (by decide), u₁₁.gpr]; rfl - · rw [u₁₂.gpr, u₁₁.other _ (by decide), hesi₁₀]; rfl - · rw [h.hash m hm] - simp only [ite_true, show ¬ (0 = 1) by decide, ite_false, Fin1, Fin0, hst m hm] - simp [bytesAt] - · have hk0 : k = 0 := by omega - subst hk0 - refine .inl ⟨by show s₁₂.zf = _; rw [hz]; rfl, hC₁₂, fun m hm => ?_⟩ - rw [h.hash m hm, hst m hm] - simp only [show ¬ (0 = 1) by decide, ite_false, Fin0, List.append_assoc] - -/-! ## Prologue -/ - -/-- The memory after saving our caller's registers and copying `count` and `out` to scratch. -/ def proMem (s₀ : State) : Mem := ((((((s₀.mem.writeW (addr (scr s₀) 112) (s₀.gpr .ebx)).writeW (addr (scr s₀) 116) (s₀.gpr .esi)).writeW (addr (scr s₀) 120) (s₀.gpr .edi)).writeW (addr (scr s₀) 124) (s₀.gpr .ebp)).writeW diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/FinalizeVariant.lean b/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/FinalizeVariant.lean new file mode 100644 index 000000000..4e17873e1 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/FinalizeVariant.lean @@ -0,0 +1,218 @@ +import VerifiedGarbage.Proof.Sha256.X86.Stream.Finalize +import VerifiedGarbage.Proof.Sha256.X86.Stream.CompressAt + +/-! SHA-256's padding loop, independent of compression backend. -/ +namespace VG.Proof.Sha256.X86.Stream.Finalize +open VG VG.X86 +open VG.Proof.Sha256.X86.Stream +open VG.Proof.Sha256.Stream +open VG.Spec.Sha256 (stateAt blockAt compress bytesAt HashValue wordBytes parseBlock) +variable {name : String} {code : Prog isa} + (hv : Verified X86.target code Proof.Sha256.compressX86) + (hnosp : NoSp code) (hstack : stackUse code = 0) +include hv hnosp hstack + +theorem compress_buf_of {s₀ : State} (hp : Pre s₀) {s : State} (hC : Common s₀ s) + (heax : s.gpr .eax = st s₀ + BitVec.ofNat 32 32) {Q : State → Prop} + (hQ : ∀ s', Common s₀ s' → (∀ r ∈ calleeSaved, s'.gpr r = s.gpr r) → + stateAt s'.mem (stA s₀) = compress (stateAt s.mem (stA s₀)) (blockAt s.mem (stA s₀ + 32)) → Q s') : + WP isa (Impl.MdStream.X86.compressAt name code .ebx .ebp) s Q := by + have hst := hp.st_fit; have hsc := hp.scr_fit; have hsp := hp.sp_fit + have e32 : Region.Sub ⟨stA s₀, 32⟩ (stR s₀) := Region.sub_prefix (by omega) + have e112 : Region.Sub ⟨scA s₀, 112⟩ (scR s₀) := Region.sub_prefix (by omega) + have hb : (st s₀ + BitVec.ofNat 32 32).setWidth 64 = stA s₀ + BitVec.ofNat 64 32 := addr_eq (by omega) + have eb : Region.Sub ⟨(st s₀ + BitVec.ofNat 32 32).setWidth 64, 64⟩ (stR s₀) := by + rw [hb]; exact sub_offset (by omega) (by omega) + refine compressAt_of hv hnosp hstack (st := st s₀) (scr := scr s₀) (blk := st s₀ + BitVec.ofNat 32 32) (E := esp₀ s₀) + (by decide) (by decide) (by decide) (by decide) hC.esp hC.ebx hC.ebp heax hp.sp_lo (by omega) + (by rw [BitVec.toNat_add, toNat_ofNat_lt (by omega), Nat.mod_eq_of_lt (by omega)]; omega) (by omega) + ((hp.st_scr.sub_left e32).sub_right e112) ?_ ((hp.st_scr.sub_left eb).sub_right e112) + (hp.stk_st.sub_right e32) (hp.stk_scr.sub_right e112) (hp.stk_st.sub_right eb) ?_ ?_ ?_ + · rw [hb]; exact Offset.disjoint_base _ (Nat.le_refl _) (by omega) + · rw [hC.rd, hC.wr, hp.rd, hp.wr] + apply Covers.of_sub + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + subst hr + exact ⟨stR s₀, by simp, 32, hb, by simp⟩ + · rw [hC.wr, hp.wr] + apply Covers.of_sub + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl + · exact ⟨stR s₀, by simp, 0, by simp, by simp⟩ + · exact ⟨scR s₀, by simp, 0, by simp, by simp⟩ + · intro s' hrd hwr hcs hf hstate + have cs : ∀ r ∈ calleeSaved, s'.gpr r = s.gpr r := hcs + have word : ∀ d, 112 ≤ d → d + 4 ≤ 160 → + s'.mem.readW (addr (scr s₀) d) 32 = s.mem.readW (addr (scr s₀) d) 32 := by + intro d h₁ h₂ + refine hf.readW (r := ⟨addr (scr s₀) d, 4⟩) (Region.contains_self _ _) ?_ (by decide) + intro r hr + 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 (hp.scr_sub h₂)).sub_right e32 + · rw [addr_eq (by omega)]; exact Offset.disjoint_base _ (by omega) (by omega) + · exact hp.stk_scr.symm.sub_left (hp.scr_sub h₂) + refine hQ s' ⟨hrd.trans hC.rd, hwr.trans hC.wr, by rw [cs _ (by decide)]; exact hC.ebx, + by rw [cs _ (by decide)]; exact hC.ebp, by rw [cs _ (by decide)]; exact hC.esp, + hC.frame.trans (hf.sub ?_), fun p hp' => ?_, by rw [word 128 (by omega) (by omega)]; exact hC.lo, + by rw [word 132 (by omega) (by omega)]; exact hC.hi, by rw [word 136 (by omega) (by omega)]; exact hC.outp⟩ + hcs (by rw [hstate, show (st s₀ + BitVec.ofNat 32 32).setWidth 64 = stA s₀ + 32 from hb]) + · intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact ⟨stR s₀, by simp, e32⟩ + · exact ⟨scR s₀, by simp, e112⟩ + · exact ⟨stkR s₀, by simp, fun _ h => h⟩ + · have hd : 112 ≤ p.2 ∧ p.2 + 4 ≤ 128 := by + simp only [VG.Impl.Sha256.X86.Stream.saved, List.mem_cons, List.not_mem_nil, or_false] at hp' + rcases hp' with rfl | rfl | rfl | rfl <;> simp + rw [word p.2 hd.1 (by omega)] + exact hC.saved p hp' + +theorem body_of {s₀ : State} (hp : Pre s₀) {k n : Nat} {s : State} (h : LInv s₀ k n s) : + WP isa (Impl.MdStream.X86.finalizeBody Impl.Sha256.X86.Stream.params name code) s (Step s₀ k) := by + have hk := h.k_le; have hn := h.n_le; have hst := hp.st_fit + have hC := h.toCommon + unfold Impl.MdStream.X86.finalizeBody + change WP isa _ _ _ + -- `eax := 64` or `56`: the end of the zeros. + refine WP.seq (wp_movi fun s₁ u₁ => wp_test fun s₂ f₂ z₂ => WP.block_nil ?_) + have hz₂ : s₂.zf = some (decide (k = 0)) := by + rw [z₂, u₁.other _ (by decide), h.esi, BitVec.and_self, ofNat_beq_zero (by omega)] + refine WP.seq (WP.mono (Q := fun (s₃ : State) => s₃.gpr .eax = BitVec.ofNat 32 (56 + 8 * k) ∧ + (∀ r, r ≠ .eax → s₃.gpr r = s.gpr r) ∧ s₃.mem = s.mem ∧ s₃.rd = s.rd ∧ s₃.wr = s.wr) ?_ + fun s₃ ⟨heax₃, g₃, m₃, rd₃, wr₃⟩ => ?_) + · refine WP.ite (decide (k = 0)) (by show s₂.zf = _; rw [hz₂]) (fun hb => ?_) (fun hb => ?_) + · simp only [decide_eq_true_eq] at hb; subst hb + refine wp_movi fun s₃ u₃ => WP.block_nil ⟨by rw [u₃.gpr]; rfl, fun r hr => ?_, ?_, ?_, ?_⟩ + · rw [u₃.other r hr, f₂.gpr, u₁.other r hr] + · rw [u₃.mem, f₂.mem, u₁.mem] + · rw [u₃.rd, f₂.rd, u₁.rd] + · rw [u₃.wr, f₂.wr, u₁.wr] + · simp only [decide_eq_false_iff_not] at hb + refine WP.block_nil ⟨by rw [f₂.gpr, u₁.gpr, show k = 1 by omega]; rfl, fun r hr => ?_, ?_, ?_, ?_⟩ + · rw [f₂.gpr, u₁.other r hr] + · rw [f₂.mem, u₁.mem] + · rw [f₂.rd, u₁.rd] + · rw [f₂.wr, u₁.wr] + -- `ecx := 0; eax -= edi`: zero the rest of the buffer, up to `lim`. + have hC₃ : Common s₀ s₃ := hC.of_gpr (fun r hr => g₃ r (regs3 hr).1) m₃ rd₃ wr₃ + refine WP.seq (wp_movi fun s₄ u₄ => wp_sub fun s₅ u₅ z₅ => WP.block_nil ?_) + have hC₄ : Common s₀ s₄ := hC₃.of_gpr (fun r hr => u₄.other r (regs3 hr).2.1) u₄.mem u₄.rd u₄.wr + have hecx₄ : s₄.gpr .ecx = 0 := u₄.gpr + have hedi₄ : s₄.gpr .edi = BitVec.ofNat 32 n := by rw [u₄.other _ (by decide), g₃ _ (by decide), h.edi] + have heax₅ : s₅.gpr .eax = BitVec.ofNat 32 (56 + 8 * k - n) := by + rw [u₅.gpr, u₄.other _ (by decide), heax₃, hedi₄, sub_ofNat (a := 56 + 8 * k) (b := n) (by omega)] + have hZ : Zero s₀ s₄ n (56 + 8 * k) 0 s₅ := by + refine ⟨Nat.zero_le _, fun r hr => u₅.other r ?_, u₅.rd, u₅.wr, + by rw [u₅.other _ (by decide), hedi₄, Nat.add_zero], by rw [heax₅, Nat.sub_zero], + by rw [u₅.mem, List.replicate_zero, writeBytes_nil]⟩ + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl | rfl <;> decide + have hz₅ : s₅.zf = some (decide (56 + 8 * k - n = 0)) := by + rw [z₅, ← u₅.gpr, heax₅, ofNat_beq_zero (by omega)] + refine WP.seq (WP.mono (zero_ok hp hC₄ hecx₄ (by omega) hn hZ hz₅) fun s₆ hZ₆ => ?_) + have hm₄ : s₄.mem = s.mem := by rw [u₄.mem, m₃] + have hf₆ : Frame [stR s₀] s₄.mem s₆.mem := by + rw [hZ₆.mem]; exact buf_frame _ (by simp only [List.length_replicate]; omega) + obtain ⟨hfr₆, hsv₆, hlo₆, hhi₆, hout₆⟩ := hC₄.frame_keep hp (hf₆.mono (by simp)) + have hC₆ : Common s₀ s₆ := ⟨hZ₆.rd.trans hC₄.rd, hZ₆.wr.trans hC₄.wr, by rw [hZ₆.keep _ (by simp), hC₄.ebx], + by rw [hZ₆.keep _ (by simp), hC₄.ebp], by rw [hZ₆.keep _ (by simp), hC₄.esp], hfr₆, hsv₆, hlo₆, hhi₆, hout₆⟩ + have hst₆ : stateAt s₆.mem (stA s₀) = stateAt s.mem (stA s₀) := by + rw [hZ₆.mem, hm₄] + apply stateAt_congr + intro i hi + rw [st_add] + exact writeBytes_before _ _ _ (by omega) (by simp only [List.length_replicate]; omega) + have hby₆ : bytesAt s₆.mem (stA s₀ + 32) (56 + 8 * k) = + bytesAt s.mem (stA s₀ + 32) n ++ List.replicate (56 + 8 * k - n) 0 := by + rw [hZ₆.mem, hm₄, ← bytesAt_writeBytes _ _ _ _ (by simp only [List.length_replicate]; omega)] + congr 1; simp only [List.length_replicate]; omega + have hesi₆ : s₆.gpr .esi = BitVec.ofNat 32 k := by + rw [hZ₆.keep _ (by simp), u₄.other _ (by decide), g₃ _ (by decide), h.esi] + -- In the last block, the length. + refine WP.seq (wp_test fun s₇ f₇ z₇ => WP.block_nil ?_) + have hC₇ : Common s₀ s₇ := hC₆.of_gpr (fun r _ => by rw [f₇.gpr]) f₇.mem f₇.rd f₇.wr + have hz₇ : s₇.zf = some (decide (k = 0)) := by + rw [z₇, hesi₆, BitVec.and_self, ofNat_beq_zero (by omega)] + have hesi₇ : s₇.gpr .esi = BitVec.ofNat 32 k := by rw [f₇.gpr, hesi₆] + refine WP.seq (WP.mono (Q := fun (s₈ : State) => Common s₀ s₈ ∧ s₈.gpr .esi = BitVec.ofNat 32 k ∧ + stateAt s₈.mem (stA s₀) = stateAt s.mem (stA s₀) ∧ + ∀ m, R₀ s₀ m → bytesAt s₈.mem (stA s₀ + 32) 64 = bytesAt s.mem (stA s₀ + 32) n ++ + (if k = 1 then List.replicate (64 - n) 0 else List.replicate (56 - n) 0 ++ lenBytes m)) ?_ + fun s₈ ⟨hC₈, hesi₈, hst₈, hby₈⟩ => ?_) + · refine WP.ite (decide (k = 0)) (by show s₇.zf = _; rw [hz₇]) (fun hb => ?_) (fun hb => ?_) + · simp only [decide_eq_true_eq] at hb; subst hb + refine WP.mono (len_ok hp hC₇) fun s₈ ⟨g₈, rd₈, wr₈, m₈⟩ => ?_ + have hfL : Frame [stR s₀] s₇.mem s₈.mem := by + rw [m₈]; exact buf_frame _ (by simp [lenL, wordBytes]) + obtain ⟨hfr, hsv, hlo, hhi, hout⟩ := hC₇.frame_keep hp (hfL.mono (by simp)) + refine ⟨⟨rd₈.trans hC₇.rd, wr₈.trans hC₇.wr, by rw [g₈ _ (by decide) (by decide) (by decide), hC₇.ebx], + by rw [g₈ _ (by decide) (by decide) (by decide), hC₇.ebp], + by rw [g₈ _ (by decide) (by decide) (by decide), hC₇.esp], hfr, hsv, hlo, hhi, hout⟩, + by rw [g₈ _ (by decide) (by decide) (by decide), hesi₇], ?_, fun m hm => ?_⟩ + · rw [m₈, ← hst₆, ← f₇.mem] + apply stateAt_congr + intro i hi + rw [st_add] + exact writeBytes_before _ _ _ (by omega) (by simp [lenL, wordBytes]) + · simp only [show ¬ ((0 : Nat) = 1) by decide, ite_false] + have e := bytesAt_writeBytes s₇.mem (stA s₀ + 32) 56 (lenL s₀) (by simp [lenL, wordBytes]) + simp only [lenL, List.length_append, show ∀ w, (wordBytes w).length = 4 from fun _ => rfl] at e + rw [m₈, e, f₇.mem, hby₆, ← lenBytes_halves _ _ m hm.2] + simp [List.append_assoc] + · simp only [decide_eq_false_iff_not] at hb + have hk1 : k = 1 := by omega + subst hk1 + refine WP.block_nil ⟨hC₇, hesi₇, by rw [f₇.mem, hst₆], fun m _ => ?_⟩ + rw [f₇.mem, hby₆]; simp + -- Compress the block. + refine WP.seq (WP.mono (args_ok hC₈) fun s₉ ⟨hC₉, g₉, heax₉, hf₉⟩ => ?_) + refine WP.seq (compress_buf_of hv hnosp hstack hp hC₉ heax₉ fun s₁₀ hC₁₀ cs₁₀ hst₁₀ => ?_) + have hesi₁₀ : s₁₀.gpr .esi = BitVec.ofNat 32 k := by + rw [cs₁₀ _ (by decide), g₉ _ (by decide), hesi₈] + have hbyte : ∀ i, i < 96 → s₉.mem (stA s₀ + BitVec.ofNat 64 i) = s₈.mem (stA s₀ + BitVec.ofNat 64 i) := + fun i hi => frame_bytes hf₉ (R := stR s₀) (by simpa using hp.a_st.symm) (by simp) hi + have hblk : ∀ m, R₀ s₀ m → blockAt s₉.mem (stA s₀ + 32) = parseBlock fun t => + (bytesAt s.mem (stA s₀ + 32) n ++ + (if k = 1 then List.replicate (64 - n) 0 else List.replicate (56 - n) 0 ++ lenBytes m)).getD t 0 := by + intro m hm + apply parseBlock_congr + intro t ht + rw [show stA s₀ + 32 + BitVec.ofNat 64 t = stA s₀ + BitVec.ofNat 64 (32 + t) by + simp only [BitVec.ofNat_add]; rw [BitVec.add_assoc]; rfl, hbyte _ (by omega), + ← show stA s₀ + 32 + BitVec.ofNat 64 t = stA s₀ + BitVec.ofNat 64 (32 + t) by + simp only [BitVec.ofNat_add]; rw [BitVec.add_assoc]; rfl] + exact bytesAt_getD (hby₈ m hm) ht + have hst₉ : stateAt s₉.mem (stA s₀) = stateAt s₈.mem (stA s₀) := + stateAt_congr fun i hi => hbyte i (by omega) + -- Next block, if any. + refine wp_movi fun s₁₁ u₁₁ => wp_subi fun s₁₂ u₁₂ z₁₂ => WP.block_nil ?_ + have hC₁₂ : Common s₀ s₁₂ := hC₁₀.of_gpr (fun r hr => by + rw [u₁₂.other r (regs3 hr).2.2.2.2, u₁₁.other r (regs3 hr).2.2.2.1]) (by rw [u₁₂.mem, u₁₁.mem]) + (by rw [u₁₂.rd, u₁₁.rd]) (by rw [u₁₂.wr, u₁₁.wr]) + have hz : s₁₂.zf = some (decide (k = 1)) := by + rw [z₁₂, u₁₁.other _ (by decide), hesi₁₀, lit32 1, sub_beq (a := k) (b := 1) (by omega) (by omega)] + have hst : ∀ m, R₀ s₀ m → stateAt s₁₂.mem (stA s₀) = compress (stateAt s.mem (stA s₀)) (parseBlock fun t => + (bytesAt s.mem (stA s₀ + 32) n ++ + (if k = 1 then List.replicate (64 - n) 0 else List.replicate (56 - n) 0 ++ lenBytes m)).getD t 0) := by + intro m hm + rw [u₁₂.mem, u₁₁.mem, hst₁₀, hst₉, hst₈, hblk m hm] + by_cases hk1 : k = 1 + · subst hk1 + refine .inr ⟨by show s₁₂.zf = _; rw [hz]; rfl, rfl, ⟨hC₁₂, by omega, by omega, ?_, ?_, fun m hm => ?_⟩⟩ + · rw [u₁₂.other _ (by decide), u₁₁.gpr]; rfl + · rw [u₁₂.gpr, u₁₁.other _ (by decide), hesi₁₀]; rfl + · rw [h.hash m hm] + simp only [ite_true, show ¬ (0 = 1) by decide, ite_false, Fin1, Fin0, hst m hm] + simp [bytesAt] + · have hk0 : k = 0 := by omega + subst hk0 + refine .inl ⟨by show s₁₂.zf = _; rw [hz]; rfl, hC₁₂, fun m hm => ?_⟩ + rw [h.hash m hm, hst m hm] + simp only [show ¬ (0 = 1) by decide, ite_false, Fin0, List.append_assoc] + + +end VG.Proof.Sha256.X86.Stream.Finalize diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Variant.lean b/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Variant.lean new file mode 100644 index 000000000..824da9bd9 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Variant.lean @@ -0,0 +1,37 @@ +import VerifiedGarbage.Proof.Sha256.X86.Shared + +/-! +# Streaming SHA-256 parameterized by compression on x86 + +The functional and ABI proofs hold once for every verified compression +function. Each backend supplies constant-time certificates for its emitted +streaming code, checked against the same streaming contracts. +-/ +namespace VG.Proof.Sha256.X86.Stream + +open VG.X86 +open VG.Proof.MdStream VG.Proof.MdStream.X86 + +variable {name : String} {code : Prog isa} + (hcomp : CalleeOk (P := params) md code) +include hcomp + +/-- Any verified compressor gives the same SHA-256 update contract. -/ +theorem update_of (ct : ConstantTime isa (updK (P := params) md 160).pre + (updK (P := params) md 160).pub (Impl.MdStream.X86.update params name code)) : + Verified X86.target (Impl.MdStream.X86.update params name code) Proof.Sha256.updateX86 := by + have h := MdStream.X86.Update.verified (name := name) dims hcomp ct + exact Verified.of_implies h + ⟨fun _ h => h, fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr hc, + fun _ _ _ _ h => h, h.2.2⟩ + +/-- Any verified compressor gives the same SHA-256 finalization contract. -/ +theorem finalize_of (ct : ConstantTime isa (finK (P := params) md 160).pre + (finK (P := params) md 160).pub (Impl.MdStream.X86.finalize params name code)) : + Verified X86.target (Impl.MdStream.X86.finalize params name code) Proof.Sha256.finalizeX86 := by + have h := MdStream.X86.Finalize.verified (name := name) dims shape hcomp ct + exact Verified.of_implies h + ⟨fun _ h => h, fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr trivial hc, + fun _ _ _ _ h => h, h.2.2⟩ + +end VG.Proof.Sha256.X86.Stream diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86/Variants/Interface.lean b/lean/VerifiedGarbage/Proof/Sha256/X86/Variants/Interface.lean new file mode 100644 index 000000000..5398c471c --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Sha256/X86/Variants/Interface.lean @@ -0,0 +1,50 @@ +import VerifiedGarbage.Proof.Hmac.Sha256.X86.Init +import VerifiedGarbage.Proof.Hmac.Sha256.X86.Finalize +import VerifiedGarbage.Proof.Pbkdf2.Sha256.X86 +import VerifiedGarbage.Proof.Sha256.X86.Stream.Variant +import VerifiedGarbage.TCB.Artifact + +/-! +# SHA-256 backends on x86 + +A backend is registered once. The emitter applies every generic construction +to it, so adding compression acceleration also emits the corresponding SHA, +HMAC, and PBKDF2 callers. +-/ +namespace VG.Proof.Sha256.X86.Variants + +open VG.X86 + +structure StreamFn where + api : Api + code : Prog isa + contract : Contract isa + stack : Nat := 0 + verified : Verified X86.target code contract + ofSig : ∃ pre post leak, + contract = api.sig.contract X86.abi pre post api.writeArgs stack leak + ofApi : api.contracts.elim True fun f => contract = f X86.abi stack + spSafe : code.all (fun i => !isa.writesSp i) = true + +structure Backend where + cmpN : String + cmpC : Prog isa + cmp : Verified X86.target cmpC Proof.Sha256.compressX86 + cmpSp : NoSp cmpC + cmpStack : stackUse cmpC = 0 + initCt : ConstantTime isa Proof.Hmac.initSha256X86.pre Proof.Hmac.initSha256X86.pub + (Impl.Hmac.Sha256.X86.init cmpN cmpC) + finCt : ConstantTime isa Proof.Hmac.finalizeSha256X86.pre Proof.Hmac.finalizeSha256X86.pub + (Impl.Hmac.Sha256.X86.finalize cmpN cmpC) + finHashSp : NoSp (Impl.Hmac.Sha256.X86.finalizeHash cmpN cmpC) + finHashStack : stackUse (Impl.Hmac.Sha256.X86.finalizeHash cmpN cmpC) = 20 + iterCt : ConstantTime isa Proof.Pbkdf2.iterateSha256X86.pre + Proof.Pbkdf2.iterateSha256X86.pub (Impl.Pbkdf2.Sha256.X86.iterate cmpN cmpC) + suffix : String + features : List String + functions : List StreamFn + initSp : (Impl.Hmac.Sha256.X86.init cmpN cmpC).all (fun i => !isa.writesSp i) = true + finSp : (Impl.Hmac.Sha256.X86.finalize cmpN cmpC).all (fun i => !isa.writesSp i) = true + iterSp : (Impl.Pbkdf2.Sha256.X86.iterate cmpN cmpC).all (fun i => !isa.writesSp i) = true + +end VG.Proof.Sha256.X86.Variants diff --git a/lean/VerifiedGarbage/Variants/Sha256/X86/Scalar.lean b/lean/VerifiedGarbage/Variants/Sha256/X86/Scalar.lean new file mode 100644 index 000000000..1fa02c1ea --- /dev/null +++ b/lean/VerifiedGarbage/Variants/Sha256/X86/Scalar.lean @@ -0,0 +1,61 @@ +import VerifiedGarbage.Proof.Sha256.X86.Variants.Interface +import VerifiedGarbage.Proof.Framework.X86.Lit + +/-! Scalar SHA-256 is one backend; its generic callers are emitted with it. -/ +namespace VG.Variants.Sha256.X86.Scalar + +open VG.X86 + +materialize_code sha256HInit := Impl.Hmac.Sha256.X86.init "vg_sha256_compress" Impl.Sha256.X86.compress +materialize_code sha256HFinalize := Impl.Hmac.Sha256.X86.finalize "vg_sha256_compress" Impl.Sha256.X86.compress +materialize_code sha256HIterate := Impl.Pbkdf2.Sha256.X86.iterate "vg_sha256_compress" Impl.Sha256.X86.compress + +/-- Generic registration preserves every scalar construction instruction. -/ +theorem scalar_code_unchanged : + Impl.Hmac.Sha256.X86.init "vg_sha256_compress" Impl.Sha256.X86.compress = Impl.Hmac.X86.init ∧ + Impl.Hmac.Sha256.X86.finalize "vg_sha256_compress" Impl.Sha256.X86.compress = Impl.Hmac.X86.finalize ∧ + Impl.Pbkdf2.Sha256.X86.iterate "vg_sha256_compress" Impl.Sha256.X86.compress = Impl.Pbkdf2.X86.iterate := + ⟨rfl, rfl, rfl⟩ + +def variant : Proof.Sha256.X86.Variants.Backend where + cmpN := "vg_sha256_compress" + cmpC := Impl.Sha256.X86.compress + cmp := Proof.Sha256.X86.compress_verified + cmpSp := NoSp.of_all (by lit_decide) + cmpStack := by lit_decide + initCt := Proof.Hmac.X86.Init.init_ct + finCt := Proof.Hmac.X86.Finalize.finalize_ct + finHashSp := Proof.Hmac.X86.Finalize.finalizeHash_nosp + finHashStack := Proof.Hmac.X86.Finalize.finalizeHash_stack + iterCt := Proof.Pbkdf2.X86.iterate_ct + suffix := "" + features := [] + functions := [ + { api := Spec.Sha256.compressApi + code := Impl.Sha256.X86.compress + contract := Spec.Sha256.compressContract X86.abi + verified := Proof.Sha256.X86.Shared.compress + ofSig := ⟨_, _, _, rfl⟩ + ofApi := rfl + spSafe := Code.all_of_allInstrs (by lit_decide) }, + { api := Spec.Sha256.updateApi + code := Impl.Sha256.X86.Stream.update + contract := Spec.Sha256.updateContract X86.abi 20 + stack := 20 + verified := Proof.Sha256.X86.Shared.update + ofSig := ⟨_, _, _, rfl⟩ + ofApi := rfl + spSafe := Code.all_of_allInstrs (by lit_decide) }, + { api := Spec.Sha256.finalizeApi + code := Impl.Sha256.X86.Stream.finalize + contract := Spec.Sha256.finalizeContract X86.abi 20 + stack := 20 + verified := Proof.Sha256.X86.Shared.finalize + ofSig := ⟨_, _, _, rfl⟩ + ofApi := rfl + spSafe := Code.all_of_allInstrs (by lit_decide) }] + initSp := Code.all_of_allInstrs (by lit_decide) + finSp := Code.all_of_allInstrs (by lit_decide) + iterSp := Code.all_of_allInstrs (by lit_decide) + +end VG.Variants.Sha256.X86.Scalar diff --git a/src/asm/x86/sha256.rs b/src/asm/x86/sha256.rs index 022b57806..c8a1f786c 100644 --- a/src/asm/x86/sha256.rs +++ b/src/asm/x86/sha256.rs @@ -2,6 +2,39 @@ //! Verified `sha256` functions for `x86`. #![allow(dead_code)] +/// Starts a SHA-256 computation: makes the streaming state `*state` represent the empty message. +/// +/// Contract: `VG.Spec.Sha256.initContract`. The streaming state is the hash value followed by a buffered partial block (`VG.Spec.Sha256.Repr`). +/// +/// # Safety +/// +/// * `state` must be valid for reads and writes of 96 bytes. +/// * `state` must not overlap the arguments on the stack (distinct Rust objects never do). +/// * `state` must not overlap the return address on the stack, or wrap around the end of the address space (no Rust object does). +#[unsafe(naked)] +pub(crate) unsafe extern "C" fn vg_sha256_init(state: *mut [u8; 96]) { + core::arch::naked_asm!( + "mov eax, DWORD PTR [esp+4]", + "mov ecx, 1779033703", + "mov DWORD PTR [eax], ecx", + "mov ecx, -1150833019", + "mov DWORD PTR [eax+4], ecx", + "mov ecx, 1013904242", + "mov DWORD PTR [eax+8], ecx", + "mov ecx, -1521486534", + "mov DWORD PTR [eax+12], ecx", + "mov ecx, 1359893119", + "mov DWORD PTR [eax+16], ecx", + "mov ecx, -1694144372", + "mov DWORD PTR [eax+20], ecx", + "mov ecx, 528734635", + "mov DWORD PTR [eax+24], ecx", + "mov ecx, 1541459225", + "mov DWORD PTR [eax+28], ecx", + "ret", + ) +} + /// The SHA-256 compression function (FIPS 180-4 §6.2.2): updates the hash value `*state` with the `n` 64-byte blocks starting at `blocks`, in order. /// /// Contract: `VG.Spec.Sha256.compressContract`. Constant time: only the pointers and `n` may affect timing, not the hash value or the blocks. @@ -3364,39 +3397,6 @@ pub(crate) unsafe extern "C" fn vg_sha256_compress(state: *mut [u32; 8], blocks: ) } -/// Starts a SHA-256 computation: makes the streaming state `*state` represent the empty message. -/// -/// Contract: `VG.Spec.Sha256.initContract`. The streaming state is the hash value followed by a buffered partial block (`VG.Spec.Sha256.Repr`). -/// -/// # Safety -/// -/// * `state` must be valid for reads and writes of 96 bytes. -/// * `state` must not overlap the arguments on the stack (distinct Rust objects never do). -/// * `state` must not overlap the return address on the stack, or wrap around the end of the address space (no Rust object does). -#[unsafe(naked)] -pub(crate) unsafe extern "C" fn vg_sha256_init(state: *mut [u8; 96]) { - core::arch::naked_asm!( - "mov eax, DWORD PTR [esp+4]", - "mov ecx, 1779033703", - "mov DWORD PTR [eax], ecx", - "mov ecx, -1150833019", - "mov DWORD PTR [eax+4], ecx", - "mov ecx, 1013904242", - "mov DWORD PTR [eax+8], ecx", - "mov ecx, -1521486534", - "mov DWORD PTR [eax+12], ecx", - "mov ecx, 1359893119", - "mov DWORD PTR [eax+16], ecx", - "mov ecx, -1694144372", - "mov DWORD PTR [eax+20], ecx", - "mov ecx, 528734635", - "mov DWORD PTR [eax+24], ecx", - "mov ecx, 1541459225", - "mov DWORD PTR [eax+28], ecx", - "ret", - ) -} - /// Absorbs data into a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`. /// /// Contract: `VG.Spec.Sha256.updateContract`. Constant time: only the pointers, `count` and `len` may affect timing, not the state or the data. diff --git a/src/hmac/sha256.rs b/src/hmac/sha256.rs index 133d408ec..6dcf8ff28 100644 --- a/src/hmac/sha256.rs +++ b/src/hmac/sha256.rs @@ -119,8 +119,11 @@ impl HmacHash for Sha256 { // `key.len()` bytes and `scratch` for reads and writes of 608 bytes; // they are distinct objects, so they do not overlap each other or the // call's stack frame, nor wrap around the address space. + let init = match state.backend { + Sha256Backend::Scalar => vg_hmac_sha256_init, + }; unsafe { - vg_hmac_sha256_init( + init( &mut state.inner, &mut state.outer, key.as_ptr(), @@ -162,8 +165,11 @@ impl HmacHash for Sha256 { // frame, nor wrap around the address space. `state.inner` represents // `(K₀ ⊕ ipad) ‖ text`, of `state.count` bytes, and `state.outer` // represents `K₀ ⊕ opad`. + let finalize = match state.backend { + Sha256Backend::Scalar => vg_hmac_sha256_finalize, + }; unsafe { - vg_hmac_sha256_finalize( + finalize( &mut state.inner, &state.outer, state.count, diff --git a/src/pbkdf2/sha256.rs b/src/pbkdf2/sha256.rs index 869fec991..0d33fe99e 100644 --- a/src/pbkdf2/sha256.rs +++ b/src/pbkdf2/sha256.rs @@ -39,7 +39,7 @@ use crate::arch::pbkdf2_sha256::{ #[cfg(target_arch = "aarch64")] use crate::arch::pbkdf2_sha256::{VG_PBKDF2_HMAC_SHA256_SHA2_FEATURES, vg_pbkdf2_hmac_sha256_sha2}; use crate::hashes::sha256::Sha256; -#[cfg(any(target_arch = "x86_64", target_arch = "aarch64"))] +#[cfg(not(target_arch = "arm"))] use crate::hashes::sha256::Sha256Backend; #[cfg(any(target_arch = "x86_64", target_arch = "aarch64"))] @@ -72,7 +72,19 @@ fn iterate(key: &[u8; 192], u: &[u8; 32], n: u32, t: &mut [u8; 32]) { // stack below it (on x86), nor wrap around the address // space. `key` holds the streaming states for `K₀ ⊕ ipad` and `K₀ ⊕ opad` // that `vg_hmac_sha256_init` left. - unsafe { vg_pbkdf2_hmac_sha256_iterate(key, u, n, t, &mut scratch) }; + #[cfg(target_arch = "arm")] + unsafe { + vg_pbkdf2_hmac_sha256_iterate(key, u, n, t, &mut scratch) + }; + #[cfg(target_arch = "x86")] + { + let iterate = match Sha256Backend::select(crate::cpu::detected()) { + Sha256Backend::Scalar => vg_pbkdf2_hmac_sha256_iterate, + }; + // SAFETY: the buffers satisfy the contract described above; selecting + // the hash backend also selects every PBKDF2 caller of that backend. + unsafe { iterate(key, u, n, t, &mut scratch) }; + } } #[cfg(any(target_arch = "arm", target_arch = "x86"))]