From 3a7a56c4e51b4712ecd0a836902bee06d5614963 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Fri, 7 Aug 2026 09:22:58 +0200 Subject: [PATCH] =?UTF-8?q?config:=20fips205-slhdsa-verified=20entry=20?= =?UTF-8?q?=E2=80=94=20certificates=20and=20cones=20measured=20from=20its?= =?UTF-8?q?=20manifest?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit First slh_dsa-kind repo. The 11 certificate names and every per-certificate cone are GENERATED from the repositorys own pinned AUDIT-MANIFEST.txt, not hand-typed; the apex resolves to kernel-3 plus the five verify-path oracles. Exclusions carry TRUSTED-BASE items 2/9/10 into the leaf: hash oracles assumed, signing/keygen out of scope, everything above the extraction root (including the pure/prehash domain-separator byte) uncovered, the deployed bridge a 137-case differential test. Dry-run green: 11/11 proven+clean at d44b70d8, attestation signed verified-dalek-serial. Co-Authored-By: Claude Opus 4.8 --- examples/repos.yaml | 53 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/examples/repos.yaml b/examples/repos.yaml index dfca475..622132c 100644 --- a/examples/repos.yaml +++ b/examples/repos.yaml @@ -221,3 +221,56 @@ repos: LTLAcc.take_append_drop: [] LTLAcc.take_drop_prefix: ["propext", "Classical.choice", "Quot.sound"] LTLAcc.take_take_le: ["propext", "Quot.sound"] + + - name: fips205-slhdsa-verified + url: https://github.com/saymrwulf/fips205-slhdsa-verified.git + kind: slh_dsa + verification_dir: verification + verified_backend: verify-mono/sha2-128s + env_script: ~/aeneas-toolchain/env.sh + lean_project_dir: $AENEAS_HOME/backends/lean + lean_guard: verification/lean-guard + backend_warning: >- + proved subject is the private verify_mono facade; the bridge to the + deployed generic pk.verify() is a 137-case differential test, not a + machine-checked refinement (TRUSTED-BASE item 9) + known_exclusions: + - the five verify-path hash oracles h_msg/f/h/t_l/t_len (assumed, not proven against FIPS 180-4) + - signing and key generation (out of extraction scope entirely) + - "everything above the extraction root: M' assembly, the pure/prehash domain-separator byte, ctx length bound, deserialization (TRUSTED-BASE item 10)" + - the base_2b inner loop (threaded opaquely, no certificate) + - parameter sets other than SLH-DSA-SHA2-128s + - compiler correctness and side channels + axiom_imports: + - Proofs.ApexSpec + - Proofs.ChainSpec + - Proofs.ForsInnerSpec + - Proofs.ForsOuterSpec + - Proofs.HtSpec + - Proofs.InputPrepSpec + - Proofs.WotsSpec + - Proofs.XmssSpec + certificates: + - fips205.base2b_outer_loop_eq + - fips205.chain_free_loop_eq + - fips205.fors_inner_loop_eq + - fips205.fors_outer_loop_eq + - fips205.ht_loop_eq + - fips205.slh_verify_128s_accepts_iff + - fips205.to_byte_loop_eq + - fips205.to_int_loop_eq + - fips205.wots_csum_loop_eq + - fips205.wots_loop1_eq + - fips205.xmss_loop_eq + certificate_axioms: + fips205.base2b_outer_loop_eq: ["Classical.choice", "Quot.sound", "propext"] + fips205.chain_free_loop_eq: ["Classical.choice", "Quot.sound", "propext", "verify_mono.oracle.f"] + fips205.fors_inner_loop_eq: ["Classical.choice", "Quot.sound", "propext", "verify_mono.oracle.h"] + fips205.fors_outer_loop_eq: ["Classical.choice", "Quot.sound", "propext", "verify_mono.oracle.f", "verify_mono.oracle.h"] + fips205.ht_loop_eq: ["Classical.choice", "Quot.sound", "propext", "verify_mono.oracle.f", "verify_mono.oracle.h", "verify_mono.oracle.t_l"] + fips205.slh_verify_128s_accepts_iff: ["Classical.choice", "Quot.sound", "propext", "verify_mono.oracle.f", "verify_mono.oracle.h", "verify_mono.oracle.h_msg", "verify_mono.oracle.t_l", "verify_mono.oracle.t_len"] + fips205.to_byte_loop_eq: ["Classical.choice", "Quot.sound", "propext"] + fips205.to_int_loop_eq: ["Classical.choice", "Quot.sound", "propext"] + fips205.wots_csum_loop_eq: ["Classical.choice", "Quot.sound", "propext"] + fips205.wots_loop1_eq: ["Classical.choice", "Quot.sound", "propext", "verify_mono.oracle.f"] + fips205.xmss_loop_eq: ["Classical.choice", "Quot.sound", "propext", "verify_mono.oracle.h"]