Add hax→ProVerif symbolic analysis for protocol-minimal

.github/workflows/proverif.yml

@@ -0,0 +1,38 @@
+name: proverif
+
+# Engine-free symbolic-analysis lane: runs ProVerif against the COMMITTED
+# extraction snapshot (proofs/proverif/extraction/lib.pvl) plus the vendored
+# support libraries. It does NOT build the hax ProVerif backend, so it stays fast
+# and portable — only a `proverif` binary is needed. Re-extraction (which needs the
+# hax-proverif opam switch) is a manual step: `make proverif-extract`.
+
+on: [push, pull_request]
+
+permissions:
+  contents: read
+
+jobs:
+  proverif:
+    name: ProVerif symbolic model (engine-free)
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check out
+        uses: actions/checkout@a81bbbf8298c0fa03ea29cdc473d45769f953675 # v4.1.1
+        with:
+          persist-credentials: false
+
+      - name: Set up OCaml (for ProVerif)
+        uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3
+        with:
+          ocaml-compiler: "5.3"
+
+      - name: Install ProVerif
+        run: opam install -y proverif
+
+      - name: Verify committed model snapshot (engine-free)
+        run: opam exec -- python3 proofs/proverif/hax.py reconstruct-proverif
+        working-directory: securedrop-protocol/protocol-minimal
+
+      - name: Check ProVerif verdicts against committed EXPECTPV
+        run: opam exec -- make proverif-check
+        working-directory: securedrop-protocol/protocol-minimal

securedrop-protocol/Cargo.toml

@@ -19,4 +19,7 @@ authors = ["SecureDrop Team <securedrop@freedom.press>"]
 license = "GPL-3.0"
 
 [workspace.lints.rust]
-unexpected_cfgs = { level = "warn", check-cfg = ["cfg(hax)"] }
+# `cfg(hax_backend_proverif)` is set only by hax during `cargo hax into proverif`
+# (it gates the ProVerif-specific annotations). Normal builds, `cargo test`, and
+# `into fstar` never set it, so those lanes strip the gated annotations entirely.
+unexpected_cfgs = { level = "warn", check-cfg = ["cfg(hax)", "cfg(hax_backend_proverif)"] }

securedrop-protocol/protocol-minimal/Makefile

@@ -52,6 +52,15 @@ verify:  # Internal/CI: Type-check and verify extracted proofs.
 	# Verify:
 	$(MAKE) -C $(PROOF_DIR) ADMIT_MODULES="$(HAX_ADMITS)" all-keep-going
 
+.PHONY: proverif-check
+proverif-check:  ## Verify the ProVerif (symbolic) model against committed verdicts (engine-free; needs `proverif`).
+	python3 proofs/proverif/hax.py reconstruct-proverif
+	python3 proofs/proverif/hax.py check-proverif
+
+.PHONY: proverif-extract
+proverif-extract:  ## Re-extract the ProVerif model from Rust (needs the hax-proverif opam switch).
+	python3 proofs/proverif/hax.py extract-proverif
+
 .PHONY: hax-lib-version
 hax-lib-version:  # Internal: Query Cargo for the hax-lib version.
 	@cargo pkgid hax-lib 2>/dev/null | sed 's/.*@//'

securedrop-protocol/protocol-minimal/proofs/fstar/extraction/Securedrop_protocol_minimal.Sign.fst

@@ -423,6 +423,9 @@ let impl_SigningKey__new
     <:
     (v_R & Core_models.Result.t_Result t_SigningKey Anyhow.t_Error)
 
+let impl_SigningKey__as_bytes (self: t_SigningKey) : t_Array u8 (mk_usize 32) =
+  impl_SigningSecretKey__as_bytes self.f_sk
+
 /// Sign `msg` in domain `D`, returning a `Signature<D>`.
 /// The actual preimage is `len(tag) || tag || msg` where `tag = D::TAG`.
 let impl_SigningKey__sign
@@ -432,18 +435,16 @@ let impl_SigningKey__sign
       (msg: t_Slice u8)
     : t_Signature v_D =
   let preimage:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = tagged_preimage #v_D msg in
+  let sk:t_Array u8 (mk_usize 32) = impl_SigningKey__as_bytes self in
   let bytes:t_Array u8 (mk_usize 64) =
     Securedrop_protocol_minimal.Primitives.Provider.Ed25519.sign (Alloc.Vec.impl_1__as_slice preimage
 
         <:
         t_Slice u8)
-      (impl_SigningSecretKey__as_bytes self.f_sk <: t_Array u8 (mk_usize 32))
+      sk
   in
   impl_7__from_bytes #v_D bytes
 
-let impl_SigningKey__as_bytes (self: t_SigningKey) : t_Array u8 (mk_usize 32) =
-  impl_SigningSecretKey__as_bytes self.f_sk
-
 let impl_SigningKey__from_seed (seed: t_Array u8 (mk_usize 32)) : t_SigningKey =
   let pk:t_Array u8 (mk_usize 32) = Rust_primitives.Hax.repeat (mk_u8 0) (mk_usize 32) in
   let pk:t_Array u8 (mk_usize 32) =
@@ -466,6 +467,7 @@ let impl_VerifyingKey__verify
       (sig: t_Signature v_D)
     : Core_models.Result.t_Result Prims.unit Anyhow.t_Error =
   let preimage:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = tagged_preimage #v_D msg in
+  let sig_bytes:t_Array u8 (mk_usize 64) = impl_7__as_bytes #v_D sig in
   Core_models.Result.impl__map_err #Prims.unit
     #Anyhow.t_Error
     #Anyhow.t_Error
@@ -475,7 +477,7 @@ let impl_VerifyingKey__verify
           <:
           t_Slice u8)
         (impl_VerifyingKey__as_bytes self <: t_Array u8 (mk_usize 32))
-        sig.f_bytes
+        sig_bytes
       <:
       Core_models.Result.t_Result Prims.unit Anyhow.t_Error)
     (fun temp_0_ ->