Implement verified Argon2 on x86-64

README.md

@@ -586,7 +586,7 @@ yours to keep:
 
 <td>✅</td>
 
-<td>❌</td>
+<td>✅</td>
 
 <td>❌</td>
 
@@ -602,7 +602,7 @@ yours to keep:
 
 <td>✅</td>
 
-<td>❌</td>
+<td>✅</td>
 
 <td>❌</td>
 
@@ -618,7 +618,7 @@ yours to keep:
 
 <td>✅</td>
 
-<td>❌</td>
+<td>✅</td>
 
 <td>❌</td>
 

bench/Cargo.toml

@@ -15,6 +15,12 @@ publish = false
 # `src/cpu.rs` and `ci/bench_arches.py`).
 verified-garbage = { path = "..", features = ["cpu-features-env"] }
 
+[features]
+# OpenSSL 3.2+ supplies Argon2; the benchmark runners use 3.0.
+# On a supported host, use `cargo bench --features openssl-argon2` and
+# `cargo test --features openssl-argon2 --test argon2` for the comparison.
+openssl-argon2 = []
+
 [dev-dependencies]
 criterion = { version = "0.8", default-features = false, features = ["cargo_bench_support"] }
 openssl = "0.10"

bench/benches/primitives/argon2.rs

@@ -0,0 +1,74 @@
+//! Complete Argon2 derivations, including allocation and initialization.
+//!
+//! OpenSSL supplies Argon2 from version 3.2; the runners use 3.0. Enable
+//! `openssl-argon2` on a supported host to benchmark it alongside this library.
+
+use criterion::Criterion;
+
+pub const USES: &[&str] = &["argon2", "blake2b"];
+
+#[cfg(target_arch = "x86_64")]
+pub fn bench(c: &mut Criterion) {
+    use std::hint::black_box;
+
+    use criterion::BenchmarkId;
+    use verified_garbage::argon2::{Variant, derive};
+
+    use crate::VG;
+    for (variant, name) in [
+        (Variant::Argon2d, "argon2d"),
+        (Variant::Argon2i, "argon2i"),
+        (Variant::Argon2id, "argon2id"),
+    ] {
+        let mut g = c.benchmark_group(name);
+        g.sample_size(10);
+        for memory in [1024u32, 16384] {
+            let mut out = [0u8; 32];
+            g.bench_function(BenchmarkId::new(VG, memory), |b| {
+                b.iter(|| {
+                    derive(
+                        variant,
+                        black_box(b"password"),
+                        black_box(b"saltsalt"),
+                        3,
+                        memory,
+                        1,
+                        1,
+                        b"",
+                        b"",
+                        &mut out,
+                    )
+                    .unwrap()
+                })
+            });
+            #[cfg(feature = "openssl-argon2")]
+            {
+                let openssl = match variant {
+                    Variant::Argon2d => openssl::kdf::argon2d,
+                    Variant::Argon2i => openssl::kdf::argon2i,
+                    Variant::Argon2id => openssl::kdf::argon2id,
+                };
+                g.bench_function(BenchmarkId::new(crate::OPENSSL, memory), |b| {
+                    b.iter(|| {
+                        openssl(
+                            None,
+                            black_box(b"password"),
+                            black_box(b"saltsalt"),
+                            None,
+                            None,
+                            3,
+                            1,
+                            memory,
+                            &mut out,
+                        )
+                        .unwrap()
+                    })
+                });
+            }
+        }
+        g.finish();
+    }
+}
+
+#[cfg(not(target_arch = "x86_64"))]
+pub fn bench(_: &mut Criterion) {}

bench/benches/primitives/main.rs

@@ -17,6 +17,7 @@ use openssl::pkey::PKey;
 use openssl::sign::Signer;
 
 mod aes_gcm;
+mod argon2;
 mod blake2b;
 mod blake2s;
 mod chacha20;
@@ -236,6 +237,7 @@ const BENCHES: &[Bench] = &[
     (poly1305::USES, poly1305::bench),
     (rc2_cbc::USES, rc2_cbc::bench),
     (triple_des_ecb::USES, triple_des_ecb::bench),
+    (argon2::USES, argon2::bench),
     (scrypt::USES, scrypt::bench),
     (sha1::USES, sha1::bench),
     (sha224::USES, sha224::bench),

bench/tests/argon2.rs

@@ -0,0 +1,69 @@
+//! Differential complete derivations against OpenSSL, including H′ boundaries.
+
+#![cfg(all(target_arch = "x86_64", feature = "openssl-argon2"))]
+
+use verified_garbage::argon2::{Variant, derive};
+
+type Oracle = fn(
+    Option<&openssl::lib_ctx::LibCtxRef>,
+    &[u8],
+    &[u8],
+    Option<&[u8]>,
+    Option<&[u8]>,
+    u32,
+    u32,
+    u32,
+    &mut [u8],
+) -> Result<(), openssl::error::ErrorStack>;
+
+#[test]
+fn matches_openssl() {
+    for (variant, oracle) in [
+        (Variant::Argon2d, openssl::kdf::argon2d as Oracle),
+        (Variant::Argon2i, openssl::kdf::argon2i),
+        (Variant::Argon2id, openssl::kdf::argon2id),
+    ] {
+        for (lanes, memory) in [(1, 8), (1, 9), (2, 16), (3, 25), (2, 1040)] {
+            for iterations in [1, 2] {
+                for length in [4, 32, 64, 65, 96, 128] {
+                    for (password, secret, ad) in [
+                        (&b""[..], &b""[..], &b""[..]),
+                        (&b"password"[..], &b"secret"[..], &b"associated data"[..]),
+                    ] {
+                        let mut expected = vec![0; length];
+                        oracle(
+                            None,
+                            password,
+                            b"saltsalt",
+                            Some(ad),
+                            Some(secret),
+                            iterations,
+                            lanes,
+                            memory,
+                            &mut expected,
+                        )
+                        .unwrap();
+                        let mut actual = vec![0; length];
+                        derive(
+                            variant,
+                            password,
+                            b"saltsalt",
+                            iterations,
+                            memory,
+                            lanes,
+                            1,
+                            secret,
+                            ad,
+                            &mut actual,
+                        )
+                        .unwrap();
+                        assert_eq!(
+                            actual, expected,
+                            "{variant:?}, lanes={lanes}, memory={memory}, passes={iterations}, length={length}"
+                        );
+                    }
+                }
+            }
+        }
+    }
+}

lean/VerifiedGarbage/Generic/Blake2b/X86_64/Argon2.lean

@@ -1,4 +1,4 @@
-import VerifiedGarbage.Proof.Argon2.X86_64.HPrime.Verified
+import VerifiedGarbage.Proof.Argon2.X86_64.DeriveVerified
 
 /-! # Argon2 H′ for every x86-64 BLAKE2b backend -/
 
@@ -16,6 +16,19 @@ def artifacts (v : Proof.Blake2.X86_64.Backend) : List Artifact := [
     stack := 16
     verified := Proof.Argon2.X86_64.HPrime.verified v
     spSafe := Proof.Argon2.X86_64.HPrime.spSafe v
+    features := v.features },
+  { Spec.Argon2.deriveApi with
+    name := Spec.Argon2.deriveApi.name ++ v.suffix
+    target := VG.X86_64.target
+    doc := Spec.Argon2.deriveApi.doc
+      (notes := ["Serial lane evaluation honors every positive worker limit. All hashing uses \
+        the selected BLAKE2b streaming backend, including H₀ and every H′ call."])
+    code := Impl.Argon2.X86_64.Derive.code (Spec.Argon2.hPrimeApi.name ++ v.suffix)
+      (Proof.Argon2.X86_64.HPrime.hash v)
+    contract := Spec.Argon2.deriveContract VG.X86_64.abi 344
+    stack := 344
+    verified := Proof.Argon2.X86_64.Derive.verified v _
+    spSafe := Proof.Argon2.X86_64.Derive.code_spSafe v _
     features := v.features }]
 
 end VG.Generic.Blake2b.X86_64.Argon2

lean/VerifiedGarbage/Impl/Argon2/X86_64/AddressCache.lean

@@ -0,0 +1,32 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressCalls
+
+/-! Cache one address block per 128 segment positions. Frame offset eight holds
+its one-based counter; initializing it to zero forces generation even when the
+first filled index is two. Only public counters control regeneration.
+-/
+
+namespace VG.Impl.Argon2.X86_64.AddressCache
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def check : List Instr := [
+  .mov .rax (.reg .r15), .shift .shr .rax 7, .alu .add .rax (.imm 1),
+  .alu .cmp .rax (.mem (at_ .rbp 8))]
+
+def save : List Instr := [.store (at_ .rbp 8) .rax]
+
+def select : Prog isa := .seq (.block check)
+  (.ite .e (.block []) (.seq (.block save) AddressCalls.code))
+
+def wordArgs : List Instr := [
+  .mov .rcx (.mem (at_ .rbp 248)), .mov .rax (.reg .r15), .alu .and .rax (.imm 127)]
+
+def wordRead : List Instr := [
+  .mov .rdi (.mem { base := .rcx, index := some .rax, scale := 8, disp := 6144 })]
+
+def word : Prog isa := .seq (.block wordArgs) (.block wordRead)
+
+def code : Prog isa := .seq select word
+
+end VG.Impl.Argon2.X86_64.AddressCache

lean/VerifiedGarbage/Impl/Argon2/X86_64/AddressCalls.lean

@@ -0,0 +1,37 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressHeader
+import VerifiedGarbage.Impl.Argon2.X86_64.ClearBlock
+import VerifiedGarbage.Spec.Argon2.Contract
+
+/-! Independent-address generation in the shared 16 KiB scratch allocation.
+G uses `[0,4096)`, temporary output `[4096,5120)`, input `[5120,6144)`,
+address output `[6144,7168)`, and the zero block `[7168,8192)`. Every stage
+reloads the scratch pointer from frame offset 248 after a compression call.
+-/
+
+namespace VG.Impl.Argon2.X86_64.AddressCalls
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def pointer (offset : Nat) : List Instr := [
+  .mov .rdi (.mem (at_ .rbp 248)), .alu .add .rdi (.imm (BitVec.ofNat 32 offset))]
+
+def args (x y out : Nat) : List Instr := [
+  .mov .rcx (.mem (at_ .rbp 248)),
+  .mov .rdi (.reg .rcx), .alu .add .rdi (.imm (BitVec.ofNat 32 x)),
+  .mov .rsi (.reg .rcx), .alu .add .rsi (.imm (BitVec.ofNat 32 y)),
+  .mov .rdx (.reg .rcx), .alu .add .rdx (.imm (BitVec.ofNat 32 out))]
+
+def stage (x y out : Nat) : Prog isa := .seq (.block (args x y out))
+  (.call Spec.Argon2.compressApi.name VG.Impl.Argon2.X86_64.compress)
+
+def calls : Prog isa := .seq (stage 7168 5120 4096) (stage 7168 4096 6144)
+
+def clearAt (offset : Nat) : Prog isa := .seq (.block (pointer offset)) ClearBlock.code
+
+def prepare : Prog isa := .seq (clearAt 5120) (.seq (clearAt 7168)
+  (.seq (.block (pointer 5120)) AddressHeader.code))
+
+def code : Prog isa := .seq prepare calls
+
+end VG.Impl.Argon2.X86_64.AddressCalls

lean/VerifiedGarbage/Impl/Argon2/X86_64/AddressHeader.lean

@@ -0,0 +1,31 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.Compress
+
+/-! Fill the first seven words of an independently generated address input.
+The input pointer is `rdi`; its remaining words were cleared once. The frame
+holds pass (0), address counter (8), passes (72), variant (112), blocks (240).
+Lane and slice remain in `rbx` and `r14`. The counter is supplied after the
+public address-generation loop advances it to its one-based value.
+-/
+
+namespace VG.Impl.Argon2.X86_64.AddressHeader
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def registerWord (i : Nat) (r : Reg) : List Instr := [.store (at_ .rdi (8 * i)) r]
+
+def frameWord (i offset : Nat) : List Instr :=
+  [.mov .rax (.mem (at_ .rbp offset)), .store (at_ .rdi (8 * i)) .rax]
+
+def frameOffset (i : Nat) : Nat :=
+  if i = 0 then 0 else if i = 3 then 240 else if i = 4 then 72 else if i = 5 then 112 else 8
+
+def field (i : Nat) : List Instr :=
+  if i = 1 then registerWord i .rbx else if i = 2 then registerWord i .r14
+  else frameWord i (frameOffset i)
+
+def fields (n : Nat) : List Instr := (List.range n).flatMap field
+
+def code : Prog isa := .block (fields 7)
+
+end VG.Impl.Argon2.X86_64.AddressHeader

lean/VerifiedGarbage/Impl/Argon2/X86_64/AddressMode.lean

@@ -0,0 +1,27 @@
+import VerifiedGarbage.TCB.X86_64.Isa
+import VerifiedGarbage.Impl.Argon2.X86_64.Compress
+
+/-! Determine the segment's address mode from public variant, pass and slice.
+The mask in `r10` is one for independent addressing and zero otherwise.
+-/
+
+namespace VG.Impl.Argon2.X86_64.AddressMode
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def kind : List Instr := [
+  .mov .rax (.mem (at_ .rbp 112)),
+  .mov .r10 (.reg .rax), .alu .xor .r10 (.imm 1), .alu .cmp .r10 (.imm 1), .alu .sbb .r10 (.reg .r10),
+  .mov .r8 (.reg .rax), .alu .xor .r8 (.imm 2), .alu .cmp .r8 (.imm 1), .alu .sbb .r8 (.reg .r8)]
+
+def pass : List Instr := [
+  .mov .r9 (.mem (at_ .rbp 0)), .alu .cmp .r9 (.imm 1), .alu .sbb .r9 (.reg .r9)]
+
+def slice : List Instr := [
+  .alu .cmp .r14 (.imm 2), .alu .sbb .r11 (.reg .r11),
+  .alu .and .r8 (.reg .r9), .alu .and .r8 (.reg .r11), .alu .or .r10 (.reg .r8), .alu .and .r10 (.imm 1)]
+
+def code : Prog isa := .seq (.block kind) (.seq (.block pass) (.block slice))
+
+end VG.Impl.Argon2.X86_64.AddressMode

lean/VerifiedGarbage/Impl/Argon2/X86_64/BlockAddress.lean

@@ -0,0 +1,20 @@
+import VerifiedGarbage.TCB.X86_64.Isa
+
+/-! Lane-major matrix addressing. The matrix base is in `r8`, the lane
+in `rax`, the column in `rcx`, and the lane length in `r12`. The resulting
+block pointer is returned in `rax`. Scalar multiplication and ten doublings
+work on the baseline ISA, including when the reference coordinates are secret.
+-/
+
+namespace VG.Impl.Argon2.X86_64.BlockAddress
+
+open VG.X86_64
+
+def flatten : List Instr := [.mul .r12, .alu .add .rax (.reg .rcx)]
+
+def scale : List Instr := List.replicate 10 (.alu .add .rax (.reg .rax))
+
+def code : Prog isa :=
+  .seq (.block flatten) (.seq (.block scale) (.block [.alu .add .rax (.reg .r8)]))
+
+end VG.Impl.Argon2.X86_64.BlockAddress

lean/VerifiedGarbage/Impl/Argon2/X86_64/ClearBlock.lean

@@ -0,0 +1,18 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.Compress
+
+/-! Clear one 1024-byte address-generation block. The destination in `rdi`
+is public; neither the old contents nor any input value affects the trace.
+-/
+
+namespace VG.Impl.Argon2.X86_64.ClearBlock
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def word (i : Nat) : List Instr := [.store (at_ .rdi (8 * i)) .rax]
+
+def words (n : Nat) : List Instr := (List.range n).flatMap word
+
+def code : Prog isa := .seq (.block [.mov .rax (.imm 0)]) (.block (words 128))
+
+end VG.Impl.Argon2.X86_64.ClearBlock