Repository navigation
clazel-crypto: verified CertificateVerify signatures (ECDSA P-256, RSA-PSS, Ed25519); stop offering rsa_pss_pss - #21
Merged
Conversation
RFC 8446 §4.2.3's rsa_pss_pss_sha256/384/512 (0x0809-0x080b) are for certificates whose key is an RSASSA-PSS key; verifying them needs an RFC 4055 RSASSA-PSS-params parser we do not have. Offer and accept only what the signature verifier (3.5f) checks: ecdsa_secp256r1_sha256, rsa_pss_rsae_sha256/384/512 and ed25519, plus RSA PKCS#1 v1.5 for certificate signatures only. Decided 2026-10-26. The implementation follows in the next commit. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Implements the previous commit's contract: the ClientHello's signature_algorithms list and the CertificateVerify scheme check drop rsa_pss_pss_sha256/384/512. The extension is 6 octets shorter (lemma_profile: 79 + SNI + cookie), and the expected wire bytes in tests/hello_client.rs follow. Whole-crate Verus: 2060 and 721 verified, 0 errors; cargo test -p clazel-tls: 86 passed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
src/signature_spec.rs: RFC 8446 §4.4.3 verification for the offered schemes, over the end-entity SubjectPublicKeyInfo parsed by clazel-x509: - ecdsa_secp256r1_sha256: id-ecPublicKey/secp256r1, uncompressed point, one DER Ecdsa-Sig-Value (clazel-der) with r, s padded to 32 octets; - rsa_pss_rsae_sha256/384/512: rsaEncryption, e = 65537, modulus of 2048/3072/4096/6144/8192 bits exactly, salt = digest length; - ed25519: id-Ed25519, absent parameters, 32-octet key, 64-octet sig; - everything else false. Modelling choices are listed at the top. src/axioms.rs: three new axioms wrapping libcrux-ecdsa, -rsa and -ed25519 verify (12 in total); rows for libcrux-ecdsa, -p256, -rsa and -ed25519 (verified-hacl, no unsafe). axioms.rs changed, so it needs a fresh review. The verified dispatcher follows. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The views of SubjectPublicKeyInfo, PublicKey and RsaPublicKey map pub fields one to one; closing them stopped other crates from relating a parsed key's fields to `parse_subject_public_key_info`'s spec, which clazel-crypto's signature verifier needs. No semantics change; whole- crate Verus passes with 0 errors. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
src/signature.rs: `verify(key, scheme, input, signature)`, proven equal to signature_spec::verify (33 verified, 0 errors for the crate). It parses the end-entity SPKI with clazel-x509 and the Ecdsa-Sig-Value with clazel-der, and calls only the three libcrux axioms. tests/signature.rs: RFC 8032 §7.1 TEST 1/2 (Ed25519), RFC 6979 A.2.5 (ECDSA P-256 SHA-256 "sample"), and our RSA-PSS fixtures for all three rsae schemes; every refusal the spec lists (trailing DER, 33-octet or negative r, r = 0, raw r||s, compressed or off-curve point, Ed25519 parameters, e = 3, a 2047-bit modulus, cross-scheme and unknown schemes). Full verifications are skipped under Miri; the parsing refusals run there. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The spec-review tracker (xtask/src/reviews.rs) finds files named spec.rs, so signature_spec.rs never showed as unreviewed. axioms.rs changes only in its paths to the moved module. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Under the identity key, R = identity and S = 0 verify for every message (RFC 8032 §5.1.7 is cofactorless and does not refuse it). The spec now refuses the seven y-coordinates libsodium does: the five of the points of order dividing 8, and p and p + 1. The implementation follows. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
is_small_order is proven equal to signature::spec::is_small_order. The test shows libcrux alone accepts the identity-key forgery for every message and the signature check refuses it, and that all eight canonical small-order encodings are refused. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
CI's mutation step fails a Verus crate with no mutations.json, and clazel-crypto had none (since #19). signature/examples.rs proves known answers about the spec's parsing and profile functions by evaluation: the key OIDs, the secp256r1 parameter decoded by clazel-der, pad32, the uncompressed point, Ecdsa-Sig-Value, the RSA moduli, the hash lengths and the small-order table against encodings computed from the curve. 31 mutations: 25 killed with certificates, 6 killed incidentally. Those six remove guards around the uninterpreted verifications, which no concrete example can evaluate; the exec proof and tests/signature.rs catch them, and they are not counted as coverage. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #19. This adds the signature half of
clazel-tls'sVerification: a verified dispatcher for every CertificateVerify scheme the client accepts.Commits
52590a4/a2bdc1c(clazel-tls): stop offeringrsa_pss_pss_sha256/384/512(0x0809–0x080b). Those schemes are for certificates whose key is an RSASSA-PSS key, and verifying them needs an RFC 4055 params parser we don't have. Alex decided on 2026-10-26 to offer only what we verify. The spec change is committed first, then the implementation. The extension is 6 octets shorter,lemma_profilechanges from 85 to 79, and the expected bytes intests/hello_client.rsfollow. Whole-crate Verus passes with 2060 and 721 verified, 0 errors.bd5217dcontract:src/signature_spec.rs(nowsrc/signature/spec.rs) holds RFC 8446 §4.4.3 verification over the end-entity SPKI, with every modelling choice listed at the top:It also adds 3 new axioms in
src/axioms.rs(12 in total) around libcrux-ecdsa, -rsa and -ed25519verify, and allowlist rows forlibcrux-ecdsa,-p256,-rsaand-ed25519, allverified-haclwith nounsafe.848e0d7(clazel-x509): open the SPKI exec views, so other crates can relate parsed fields to the spec. No semantics change, and whole-crate Verus passes. The identical commit is on clazel-x509: X.509 decoders and name matching (3.5b, partial), tier 0 #14 asc8646f8.2bb7a84dispatcher and tests:src/signature.rs, proven equal to the spec (crate: 33 verified, 0 errors). Parsing is ours, usingclazel-x509andclazel-der. The tests use RFC 8032 §7.1 TEST 1/2, RFC 6979 A.2.5, and our own RSA-PSS fixtures (provenance intests/fixtures/rsa-pss/SOURCE.md; public keys only). They exercise every refusal the spec lists.Local results
clazel-crypto: Verus gives 33 verified, 0 errors; tests give 19 passed, 0 failed; Miri ontests/signature.rsgives 2 passed and 5 ignored (the full verifications).cargo xtask checkpass, with 12 documented axioms.Needs before it lands
src/axioms.rsfound the three new axioms sound atsha256 18df935a…8636. Since then,3442a9fchanged only the module paths it names (crate::signature_spec::becamecrate::signature::spec::, 9 lines), so the file is nowd0cdbcdf…d479. A second fresh review confirmed the diff is path-only: the old file with that rename applied is byte-identical to the new one, every item the axioms name insignature/spec.rsis unchanged, and the count is still 12. The earlier soundness review carries over tod0cdbcdf…d479.Review follow-ups:
3442a9fmoves the files tosrc/signature/{spec,exec}.rs, so the spec-review tracker lists the spec as unreviewed.e80867c(spec) and646452a(exec + test) refuse small-order Ed25519 keys. Under the identity key, R = identity and S = 0 verify for every message, which RFC 8032 §5.1.7's cofactorless check allows. The refused y-coordinates are libsodium's seven: the five of the points of order dividing 8, plus p and p + 1. Mixed-order keys are not refused. The test shows that libcrux alone accepts the forgery and that our check refuses it, and it covers all 8 canonical encodings.Verifierimplementation itself, whosechainhalf is path validation (3.5b), and certificate-signature checks (PKCS#1 v1.5, ECDSA/SHA-384).CI note: CI's mutation step fails any Verus crate without a
mutations.json, andclazel-cryptohas had none since #19.4cff792adds one: 31 mutations ofsignature/spec.rs, 25 killed with certificates and 6 killed incidentally. #19 keeps failing that step by decision, because its crate has no spec of its own to mutate. Judge the crypto stack by this PR's CI.🤖 Generated with Claude Code