diff --git a/Cargo.lock b/Cargo.lock index 6c7e15e..e865e5b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -149,11 +149,16 @@ dependencies = [ name = "clazel-crypto" version = "0.0.0" dependencies = [ + "clazel-der", "clazel-tls", + "clazel-x509", "libcrux-chacha20poly1305", "libcrux-curve25519", + "libcrux-ecdsa", + "libcrux-ed25519", "libcrux-hkdf", "libcrux-hmac", + "libcrux-rsa", "libcrux-sha2", "vstd", ] @@ -753,6 +758,27 @@ dependencies = [ "libcrux-traits", ] +[[package]] +name = "libcrux-ecdsa" +version = "0.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "71554ed1831885ed1c972993cd022ef17dcb5eeb0560610326a6a268c0ed02b9" +dependencies = [ + "libcrux-p256", + "libcrux-sha2", +] + +[[package]] +name = "libcrux-ed25519" +version = "0.0.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "55de36c252a9fd97a202c03535deecbe988c525eb16901b2ea17ed99e737edc9" +dependencies = [ + "libcrux-hacl-rs", + "libcrux-macros", + "libcrux-sha2", +] + [[package]] name = "libcrux-hacl-rs" version = "0.0.6" @@ -806,6 +832,19 @@ dependencies = [ "syn 3.0.9", ] +[[package]] +name = "libcrux-p256" +version = "0.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7489aa205be22524e2f6ddbe006c0c4ff5f1dfc7c17b783e3d02f1cb2a01c605" +dependencies = [ + "libcrux-hacl-rs", + "libcrux-macros", + "libcrux-secrets", + "libcrux-sha2", + "libcrux-traits", +] + [[package]] name = "libcrux-platform" version = "0.0.4" @@ -825,6 +864,18 @@ dependencies = [ "libcrux-macros", ] +[[package]] +name = "libcrux-rsa" +version = "0.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "712e57d03eee2d5e4ced44aee1c475d6aae951ddf9395d709180a5df0c5be611" +dependencies = [ + "libcrux-hacl-rs", + "libcrux-macros", + "libcrux-sha2", + "libcrux-traits", +] + [[package]] name = "libcrux-secrets" version = "0.0.7" diff --git a/crates/clazel-crypto/Cargo.toml b/crates/clazel-crypto/Cargo.toml index f6eacb2..4901866 100644 --- a/crates/clazel-crypto/Cargo.toml +++ b/crates/clazel-crypto/Cargo.toml @@ -4,10 +4,13 @@ version = "0.0.0" edition.workspace = true license.workspace = true publish.workspace = true -description = "The libcrux providers for clazel-tls's cryptographic parameters: SHA-256, HMAC, HKDF, ChaCha20-Poly1305 and X25519." +description = "The libcrux providers for clazel-tls's cryptographic parameters: SHA-256, HMAC, HKDF, ChaCha20-Poly1305, X25519 and CertificateVerify signatures." [dependencies] clazel-tls = { path = "../clazel-tls" } +# The end-entity key is parsed with our own decoders (CLAUDE.md rule 8). +clazel-der = { path = "../clazel-der" } +clazel-x509 = { path = "../clazel-x509" } vstd = "=0.0.0-2026-10-04-0306" # Shipped cryptography (docs/DEPENDENCIES.md, class `shipped`; phase-3.md # items 3.0 and 3.5f). Pinned exactly: libcrux is pre-release (0.0.x), so @@ -18,6 +21,9 @@ libcrux-hmac = { version = "=0.0.9", default-features = false } libcrux-hkdf = { version = "=0.0.9", default-features = false } libcrux-chacha20poly1305 = { version = "=0.0.10", default-features = false } libcrux-curve25519 = { version = "=0.0.9", default-features = false } +libcrux-ecdsa = { version = "=0.0.9", default-features = false } +libcrux-rsa = { version = "=0.0.9", default-features = false } +libcrux-ed25519 = { version = "=0.0.10", default-features = false } # Verification tier (docs/VERIFICATION.md). The crate parses nothing; its # adapters are checked by Verus against clazel-tls's provider contracts, and diff --git a/crates/clazel-crypto/README.md b/crates/clazel-crypto/README.md index 5f98f6c..95e7337 100644 --- a/crates/clazel-crypto/README.md +++ b/crates/clazel-crypto/README.md @@ -19,6 +19,8 @@ independent). Its own code is the adapters, which Verus checks against | `Crypto::expand` | HKDF-Expand, RFC 5869 §2.3 | `libcrux_hkdf::sha2_256::expand` | | `traffic::provider::Factory` and `record::Aead` | ChaCha20-Poly1305, RFC 8439 §2.8 | `libcrux_chacha20poly1305::{encrypt, decrypt}` | | `hello::key_exchange::KeyExchange` | X25519, RFC 7748 | `libcrux_curve25519::{secret_to_public, ecdh}` | +| `auth::spec::Verification::signature` (CertificateVerify), as `signature::exec::verify` | ecdsa_secp256r1_sha256, rsa_pss_rsae_sha256/384/512, ed25519 (RFC 8446 §4.2.3) | `libcrux_ecdsa::p256::verify`, `libcrux_rsa::verify`, `libcrux_ed25519::verify` | +| Finished comparison (`Verifier::finished_equal`), as `compare::constant_time_eq` | RFC 8446 §4.4.4 | none: ours, proven, no data-dependent branch | ## The trust boundary @@ -46,10 +48,25 @@ Modelling choices: `unsafe`. The HMAC-SHA256 path calls only `libcrux-sha2`. The choice was made on 2026-10-26; see docs/DEPENDENCIES.md. +## Signature verification + +`signature::exec::verify(key, scheme, input, signature)` is proven equal to +`signature::spec::verify`. The end-entity key is its DER SubjectPublicKeyInfo, +parsed by `clazel-x509`, and an ECDSA signature's Ecdsa-Sig-Value is parsed by +`clazel-der`. Only the three verifications are libcrux's. What it accepts, and +everything it refuses, is listed at the top of `src/signature/spec.rs`: the +secp256r1 uncompressed point only, RSA keys with e = 65537 and a modulus of +exactly 2048/3072/4096/6144/8192 bits, and Ed25519 keys without parameters. +The `rsa_pss_pss_*` schemes are neither offered nor verified. + +Tests use RFC 8032 §7.1 (Ed25519) and RFC 6979 A.2.5 (ECDSA P-256) +vectors, and our own RSA-PSS fixtures in `tests/fixtures/rsa-pss` (see the +`SOURCE.md` there). + ## Not here -- Signature verification: ECDSA P-256, RSA-PSS and Ed25519 from libcrux, and - RSA PKCS#1 v1.5 from `clazel-pkcs1`. These come with certificate path - validation (3.5b). +- The `auth::verify::Verifier` implementation itself. Its `chain` half is + certificate path validation (3.5b). Certificate signatures (RSA PKCS#1 + v1.5 from `clazel-pkcs1`, and ECDSA with SHA-384) come with it. - Randomness: the caller supplies the X25519 private scalar. - Any side-channel claim beyond HACL\*'s. libcrux's README makes none for the extracted Rust, and this crate adds no secret-dependent branches. diff --git a/crates/clazel-crypto/mutations.json b/crates/clazel-crypto/mutations.json new file mode 100644 index 0000000..287383a --- /dev/null +++ b/crates/clazel-crypto/mutations.json @@ -0,0 +1,377 @@ +{ + "mutations": [ + { + "id": "ec-public-key-oid", + "file": "src/signature/spec.rs", + "find": "10045nat, 2nat, 1nat]", + "replace": "10045nat, 4nat, 1nat]", + "expect": "killed", + "reason": "id-ecPublicKey is 1.2.840.10045.2.1 (RFC 5480 §2.1.1); with arc 4 the real key OID is not recognised.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_oid_examples()", + "witness": "!is_ec_public_key(seq![1nat, 2nat, 840nat, 10045nat, 2nat, 1nat])" + } + }, + { + "id": "ed25519-oid", + "file": "src/signature/spec.rs", + "find": "101nat, 112nat]", + "replace": "101nat, 113nat]", + "expect": "killed", + "reason": "1.3.101.113 is id-Ed448 (RFC 8410 §3): Ed448 keys would be passed to Ed25519 verification and Ed25519 keys refused.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_oid_examples()", + "witness": "is_ed25519(seq![1nat, 3nat, 101nat, 113nat])" + } + }, + { + "id": "secp256r1-parameter-arc", + "file": "src/signature/spec.rs", + "find": "0x03u8, 0x01u8, 0x07u8]", + "replace": "0x03u8, 0x01u8, 0x22u8]", + "expect": "killed", + "reason": "Changes the last arc of the parameter from 7 to 34, so it no longer names secp256r1: the parameter must decode to 1.2.840.10045.3.1.7 (RFC 5480 §2.1.1.1).", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_secp256r1_parameter_example()", + "witness": "clazel_der::spec::read_oid(secp256r1_parameter(), 0, 10) == Some((seq![1nat, 2nat, 840nat, 10045nat, 3nat, 1nat, 34nat], 10nat))" + } + }, + { + "id": "pad32-zeros-after", + "file": "src/signature/spec.rs", + "find": "Seq::new((32 - m.len()) as nat, |i: int| 0u8) + m", + "replace": "m + Seq::new((32 - m.len()) as nat, |i: int| 0u8)", + "expect": "killed", + "reason": "Padding on the right multiplies r and s by a power of 256.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_pad32_example()", + "witness": "pad32(seq![0x01u8])[31] == 0u8" + } + }, + { + "id": "p256-compressed", + "file": "src/signature/spec.rs", + "find": "bits.len() == 65 && bits[0] == 0x04u8", + "replace": "bits.len() == 65 && bits[0] == 0x02u8", + "expect": "killed", + "reason": "0x04 marks the uncompressed point (RFC 5480 §2.2); with 0x02 the real key is refused.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_p256_point_examples()", + "witness": "p256_point(crate::signature::examples::ex_p256_spki(0x04u8, crate::signature::examples::ex_point())) is None" + } + }, + { + "id": "p256-length", + "file": "src/signature/spec.rs", + "find": "bits.len() == 65 && bits[0] == 0x04u8", + "replace": "bits.len() == 64 && bits[0] == 0x04u8", + "expect": "killed", + "reason": "The uncompressed point is 1 + 64 octets; at 64 the real key is refused.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_p256_point_examples()", + "witness": "p256_point(crate::signature::examples::ex_p256_spki(0x04u8, crate::signature::examples::ex_point())) is None" + } + }, + { + "id": "p256-subrange", + "file": "src/signature/spec.rs", + "find": "Some(bits.subrange(1, 65))", + "replace": "Some(bits.subrange(0, 64))", + "expect": "killed", + "reason": "X || Y starts after the 0x04 octet; from 0 the point handed to libcrux is shifted.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_p256_point_examples()", + "witness": "p256_point(crate::signature::examples::ex_p256_spki(0x04u8, crate::signature::examples::ex_point())).unwrap()[0] == 0x04u8" + } + }, + { + "id": "ecdsa-r-length", + "file": "src/signature/spec.rs", + "find": "!r_negative && re - rs <= 32", + "replace": "!r_negative && re - rs <= 31", + "expect": "killed", + "reason": "r may have 32 magnitude octets (r < n < 2^256); at 31 every r whose top octet is nonzero is refused.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_ecdsa_sig_value_examples()", + "witness": "ecdsa_sig_value(crate::signature::examples::ex_sig_max()) is None" + } + }, + { + "id": "ecdsa-s-length", + "file": "src/signature/spec.rs", + "find": "!s_negative && se - ss <= 32", + "replace": "!s_negative && se - ss <= 31", + "expect": "killed", + "reason": "s may have 32 magnitude octets, as r.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_ecdsa_sig_value_examples()", + "witness": "ecdsa_sig_value(crate::signature::examples::ex_sig_max()) is None" + } + }, + { + "id": "ecdsa-negative-r", + "file": "src/signature/spec.rs", + "find": "Some((r_negative, rs, re, after_r)) if !r_negative && re - rs <= 32", + "replace": "Some((r_negative, rs, re, after_r)) if re - rs <= 32", + "expect": "killed", + "reason": "r is a non-negative INTEGER (RFC 3279 §2.2.3); without the check -128 is read as the magnitude 0x80, a second encoding of r = 128.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_ecdsa_sig_value_examples()", + "witness": "ecdsa_sig_value(seq![0x30u8, 0x06, 0x02, 0x01, 0x80, 0x02, 0x01, 0x02]) is Some" + } + }, + { + "id": "ecdsa-nothing-after-s", + "file": "src/signature/spec.rs", + "find": "&& se - ss <= 32 && after_s == ce", + "replace": "&& se - ss <= 32", + "expect": "killed", + "reason": "The SEQUENCE holds exactly r and s; without the check a third INTEGER is ignored, a second encoding of one signature.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_ecdsa_sig_value_examples()", + "witness": "ecdsa_sig_value(seq![0x30u8, 0x09, 0x02, 0x01, 0x01, 0x02, 0x01, 0x02, 0x02, 0x01, 0x03]) is Some" + } + }, + { + "id": "ecdsa-nothing-after-sequence", + "file": "src/signature/spec.rs", + "find": "Some((cs, ce)) if ce == signature.len() =>", + "replace": "Some((cs, ce)) =>", + "expect": "killed", + "reason": "Nothing may follow the Ecdsa-Sig-Value; without the check trailing octets are ignored.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_ecdsa_sig_value_examples()", + "witness": "ecdsa_sig_value(seq![0x30u8, 0x06, 0x02, 0x01, 0x01, 0x02, 0x01, 0x02, 0x00]) is Some" + } + }, + { + "id": "ecdsa-r-from-s", + "file": "src/signature/spec.rs", + "find": "Some((pad32(signature.subrange(rs as int, re as int)),", + "replace": "Some((pad32(signature.subrange(ss as int, se as int)),", + "expect": "killed", + "reason": "r is the first INTEGER; reading s twice verifies (s, s).", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_ecdsa_sig_value_examples()", + "witness": "ecdsa_sig_value(crate::signature::examples::ex_sig_1_2()).unwrap().0[31] == 0x02u8" + } + }, + { + "id": "modulus-top-bit", + "file": "src/signature/spec.rs", + "find": "&& n[0] >= 0x80u8", + "replace": "&& n[0] >= 0x7fu8", + "expect": "killed", + "reason": "A first octet of 0x7f makes a 2047-bit modulus, which libcrux-rsa refuses as a 2048-bit one.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_modulus_ok_examples()", + "witness": "modulus_ok(Seq::new(256, |i: int| if i == 0 { 0x7fu8 } else { 0xffu8 }))" + } + }, + { + "id": "modulus-6144", + "file": "src/signature/spec.rs", + "find": "|| n.len() == 768 ||", + "replace": "|| n.len() == 767 ||", + "expect": "killed", + "reason": "6144 bits is 768 octets.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_modulus_ok_examples()", + "witness": "!modulus_ok(crate::signature::examples::ex_ones(768))" + } + }, + { + "id": "hash-len-sha384", + "file": "src/signature/spec.rs", + "find": "Hash::Sha384 => 48,", + "replace": "Hash::Sha384 => 32,", + "expect": "killed", + "reason": "SHA-384's digest, and so rsa_pss_rsae_sha384's salt, is 48 octets.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_hash_len_examples()", + "witness": "hash_len(Hash::Sha384) == 32" + } + }, + { + "id": "same-y-sign-bit", + "file": "src/signature/spec.rs", + "find": "&& key[31] & 0x7fu8 == y[31]", + "replace": "&& key[31] == y[31]", + "expect": "killed", + "reason": "Bit 255 is x's sign (RFC 8032 §5.1.2); compared, the negated small-order points are not refused.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_small_order_examples()", + "witness": "!same_y(crate::signature::examples::ex_key(0x00, 0x00, 0x80), small_order_y()[0])" + } + }, + { + "id": "same-y-prefix", + "file": "src/signature/spec.rs", + "find": "&& key.subrange(0, 31) =~= y.subrange(0, 31)", + "replace": "&& key.subrange(1, 31) =~= y.subrange(1, 31)", + "expect": "killed", + "reason": "Every octet but the last is compared; skipping the first, the identity key matches y = 0's entry.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_small_order_examples()", + "witness": "same_y(crate::signature::examples::ex_key(0x01, 0x00, 0x00), small_order_y()[0])" + } + }, + { + "id": "small-order-y-0", + "file": "src/signature/spec.rs", + "find": "// 0: (sqrt(-1), 0) and (-sqrt(-1), 0), order 4\n seq![\n 0x00u8", + "replace": "// 0: (sqrt(-1), 0) and (-sqrt(-1), 0), order 4\n seq![\n 0x02u8", + "expect": "killed", + "reason": "A wrong table entry lets that small-order key through; the entry must match the encoding computed from the curve.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_small_order_examples()", + "witness": "!same_y(crate::signature::examples::ex_key(0x00, 0x00, 0x00), small_order_y()[0])" + } + }, + { + "id": "small-order-y-1", + "file": "src/signature/spec.rs", + "find": "// 1: the identity (0, 1), order 1\n seq![\n 0x01u8", + "replace": "// 1: the identity (0, 1), order 1\n seq![\n 0x02u8", + "expect": "killed", + "reason": "A wrong table entry lets that small-order key through; the entry must match the encoding computed from the curve.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_small_order_examples()", + "witness": "!same_y(crate::signature::examples::ex_key(0x01, 0x00, 0x00), small_order_y()[1])" + } + }, + { + "id": "small-order-y-2", + "file": "src/signature/spec.rs", + "find": "// p - 1: (0, -1), order 2\n seq![\n 0xecu8", + "replace": "// p - 1: (0, -1), order 2\n seq![\n 0xebu8", + "expect": "killed", + "reason": "A wrong table entry lets that small-order key through; the entry must match the encoding computed from the curve.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_small_order_examples()", + "witness": "!same_y(crate::signature::examples::ex_key(0xec, 0xff, 0x7f), small_order_y()[2])" + } + }, + { + "id": "small-order-y-3", + "file": "src/signature/spec.rs", + "find": "// two of the order-8 points\n seq![\n 0x26u8", + "replace": "// two of the order-8 points\n seq![\n 0x27u8", + "expect": "killed", + "reason": "A wrong table entry lets that small-order key through; the entry must match the encoding computed from the curve.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_small_order_examples()", + "witness": "!same_y(crate::signature::examples::ex_order8_a(0x00), small_order_y()[3])" + } + }, + { + "id": "small-order-y-4", + "file": "src/signature/spec.rs", + "find": "// the other two order-8 points\n seq![\n 0xc7u8", + "replace": "// the other two order-8 points\n seq![\n 0xc6u8", + "expect": "killed", + "reason": "A wrong table entry lets that small-order key through; the entry must match the encoding computed from the curve.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_small_order_examples()", + "witness": "!same_y(crate::signature::examples::ex_order8_b(0x00), small_order_y()[4])" + } + }, + { + "id": "small-order-y-5", + "file": "src/signature/spec.rs", + "find": "// p: a non-canonical encoding of 0\n seq![\n 0xedu8", + "replace": "// p: a non-canonical encoding of 0\n seq![\n 0xefu8", + "expect": "killed", + "reason": "A wrong table entry lets that small-order key through; the entry must match the encoding computed from the curve.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_small_order_examples()", + "witness": "!same_y(crate::signature::examples::ex_key(0xed, 0xff, 0x7f), small_order_y()[5])" + } + }, + { + "id": "small-order-y-6", + "file": "src/signature/spec.rs", + "find": "// p + 1: a non-canonical encoding of 1\n seq![\n 0xeeu8", + "replace": "// p + 1: a non-canonical encoding of 1\n seq![\n 0xefu8", + "expect": "killed", + "reason": "A wrong table entry lets that small-order key through; the entry must match the encoding computed from the curve.", + "certificate": { + "file": "src/signature/certificates.rs", + "lemma": "crate::signature::examples::lemma_small_order_examples()", + "witness": "!same_y(crate::signature::examples::ex_key(0xee, 0xff, 0x7f), small_order_y()[6])" + } + }, + { + "id": "small-order-count", + "file": "src/signature/spec.rs", + "find": "0 <= i < small_order_y().len() && #[trigger]", + "replace": "0 <= i < 6 && #[trigger]", + "expect": "killed-incidentally", + "reason": "Leaves p + 1 out. The exec check's proof breaks; no example can evaluate the quantifier by compute_only." + }, + { + "id": "ed25519-small-order-guard", + "file": "src/signature/spec.rs", + "find": " && !is_small_order(spki.subject_public_key_bits)\n", + "replace": "", + "expect": "killed-incidentally", + "reason": "Accepts small-order keys again. It only removes a guard on the uninterpreted ed25519_verify, so no concrete theorem is false; the exec proof breaks and tests/signature.rs (ed25519_refuses_small_order_keys) catches it." + }, + { + "id": "ed25519-parameters", + "file": "src/signature/spec.rs", + "find": " && spki.algorithm.parameters_der is None\n", + "replace": "", + "expect": "killed-incidentally", + "reason": "Accepts Ed25519 keys with parameters (RFC 8410 §3 says absent). A guard on an uninterpreted verification: the exec proof breaks and tests/signature.rs catches it." + }, + { + "id": "rsa-exponent", + "file": "src/signature/spec.rs", + "find": "key.public_exponent_octets =~= seq![0x01u8, 0x00u8, 0x01u8]", + "replace": "key.public_exponent_octets =~= seq![0x03u8]", + "expect": "killed-incidentally", + "reason": "Passes e = 3 keys to libcrux-rsa, which verifies with 65537 only. A guard on an uninterpreted verification: the exec proof breaks and tests/signature.rs catches it." + }, + { + "id": "rsa-signature-length", + "file": "src/signature/spec.rs", + "find": "&& signature.len() == key.modulus_octets.len()\n", + "replace": "\n", + "expect": "killed-incidentally", + "reason": "Drops the length guard that keeps libcrux-rsa's precondition. The exec proof (and the axiom's requires) breaks." + }, + { + "id": "dispatch-ed25519", + "file": "src/signature/spec.rs", + "find": "if scheme == 0x0807 { ed25519(", + "replace": "if scheme == 0x0808 { ed25519(", + "expect": "killed-incidentally", + "reason": "Routes ed448 (0x0808) to Ed25519 and refuses ed25519. The exec dispatcher's proof breaks; tests/signature.rs verifies RFC 8032 under 0x0807." + } + ] +} diff --git a/crates/clazel-crypto/src/axioms.rs b/crates/clazel-crypto/src/axioms.rs index 27c4b91..282bfc4 100644 --- a/crates/clazel-crypto/src/axioms.rs +++ b/crates/clazel-crypto/src/axioms.rs @@ -195,4 +195,74 @@ pub fn x25519_shared(private_key: &[u8], peer_key: &[u8]) -> (out: Option (out: bool) + requires r.len() == 32, s.len() == 32, point.len() == 64, + ensures out == crate::signature::spec::ecdsa_p256_sha256_verify(message@, r@, s@, point@), +{ + if message.len() > MAX_INPUT { + std::process::abort(); + } + let (Ok(r), Ok(s), Ok(point)) = + (<[u8; 32]>::try_from(r), <[u8; 32]>::try_from(s), <[u8; 64]>::try_from(point)) else { + std::process::abort(); + }; + let signature = libcrux_ecdsa::p256::Signature::from_raw(r, s); + let public_key = libcrux_ecdsa::p256::PublicKey(point); + libcrux_ecdsa::p256::verify(libcrux_ecdsa::DigestAlgorithm::Sha256, message, &signature, + &public_key).is_ok() +} + +/// RSASSA-PSS verification with e = 65537, MGF1 over `hash`, and `salt_len`. +// AXIOM: libcrux-rsa 0.0.9 `verify(alg, &VarLenPublicKey(n), msg, salt_len, sig)` (e fixed to 65537) +// is Ok iff HACL's rsapss_pkey_verify is true; its other errors are excluded by `requires`. +#[verifier::external_body] +pub fn rsa_pss_verify(hash: crate::signature::spec::Hash, modulus: &[u8], message: &[u8], + salt_len: u32, signature: &[u8]) -> (out: bool) + requires + crate::signature::spec::modulus_ok(modulus@), + signature.len() == modulus.len(), + salt_len == crate::signature::spec::hash_len(hash), + ensures out == crate::signature::spec::rsa_pss_verify(hash, modulus@, message@, + salt_len as nat, signature@), +{ + if message.len() > MAX_INPUT { + std::process::abort(); + } + let alg = match hash { + crate::signature::spec::Hash::Sha256 => libcrux_rsa::DigestAlgorithm::Sha2_256, + crate::signature::spec::Hash::Sha384 => libcrux_rsa::DigestAlgorithm::Sha2_384, + crate::signature::spec::Hash::Sha512 => libcrux_rsa::DigestAlgorithm::Sha2_512, + }; + let Ok(key) = libcrux_rsa::VarLenPublicKey::try_from(modulus) else { + std::process::abort(); + }; + match libcrux_rsa::verify(alg, &key, message, salt_len, signature) { + Ok(()) => true, + Err(libcrux_rsa::Error::VerificationFailed) => false, + Err(_) => std::process::abort(), + } +} + +/// Ed25519 verification of `message` under a 32-octet key. +// AXIOM: libcrux-ed25519 0.0.10 `verify(payload, &[u8; 32], &[u8; 64])` is Ok iff HACL's +// ed25519 verify is true (verified-hacl); it errs otherwise only above u32::MAX octets. +#[verifier::external_body] +pub fn ed25519_verify(message: &[u8], key: &[u8], signature: &[u8]) -> (out: bool) + requires key.len() == 32, signature.len() == 64, + ensures out == crate::signature::spec::ed25519_verify(message@, key@, signature@), +{ + if message.len() > MAX_INPUT { + std::process::abort(); + } + let (Ok(key), Ok(signature)) = + (<&[u8; 32]>::try_from(key), <&[u8; 64]>::try_from(signature)) else { + std::process::abort(); + }; + libcrux_ed25519::verify(message, key, signature).is_ok() +} + } // verus! diff --git a/crates/clazel-crypto/src/lib.rs b/crates/clazel-crypto/src/lib.rs index b4e84f4..e3a0468 100644 --- a/crates/clazel-crypto/src/lib.rs +++ b/crates/clazel-crypto/src/lib.rs @@ -12,12 +12,14 @@ //! - [`provider`]: the adapters, checked by Verus against `clazel-tls`'s //! provider contracts. //! - [`compare`]: the timing-safe comparison for Finished values. +//! - [`signature`]: the CertificateVerify signature check (3.5b), whose key +//! parsing is ours and whose three verifications are axioms. //! //! The suite is the profile's only one, `TLS_CHACHA20_POLY1305_SHA256` with -//! X25519 (phase-3.md 3.0, cost 2). Signature verification and certificate -//! validation are separate (3.5b and 3.5c) and not here. +//! X25519 (phase-3.md 3.0, cost 2). Certificate validation (3.5c) is not here. pub mod axioms; pub mod compare; pub mod provider; +pub mod signature; pub mod spec; diff --git a/crates/clazel-crypto/src/signature/certificates.rs b/crates/clazel-crypto/src/signature/certificates.rs new file mode 100644 index 0000000..2d8b88d --- /dev/null +++ b/crates/clazel-crypto/src/signature/certificates.rs @@ -0,0 +1,13 @@ +//! The module that hosts the kill certificates of `mutations.json` +//! (xtask/src/mutate.rs adds one proof function here per certified +//! mutation, at run time, to a copy of the crate). It is empty on purpose: +//! a certificate is run alone in this module, and the evaluated examples in +//! [`super::examples`] (which a mutated spec makes fail) must not be in the +//! module being verified. + +#[allow(unused_imports)] +use super::spec::*; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! {} // verus! diff --git a/crates/clazel-crypto/src/signature/examples.rs b/crates/clazel-crypto/src/signature/examples.rs new file mode 100644 index 0000000..1f92c2b --- /dev/null +++ b/crates/clazel-crypto/src/signature/examples.rs @@ -0,0 +1,221 @@ +//! Known answers, evaluated: small cases of the signature check's parsing +//! and profile functions, with results written out from the RFCs or worked +//! out independently of [`super::spec`], proven by evaluating the spec +//! (`by (compute_only)`). They are facts about the spec itself and the +//! theorems the mutation certificates in `mutations.json` contradict. +//! +//! The three verifications are uninterpreted, so nothing here evaluates +//! one; the guards around them are covered by the exec proof and +//! tests/signature.rs (their mutations are `killed-incidentally`). + +#[allow(unused_imports)] +use super::spec::*; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +/// A SubjectPublicKeyInfo with the given algorithm and key bits. The fields +/// the signature check does not read are left empty. +pub open spec fn ex_spki(oid: Seq, parameters_der: Option>, unused_bits: u8, + bits: Seq) -> clazel_x509::spki::spec::SubjectPublicKeyInfo { + clazel_x509::spki::spec::SubjectPublicKeyInfo { + algorithm: clazel_x509::certificate::spec::AlgorithmIdentifier { oid, parameters_der }, + public_key: clazel_x509::spki::spec::PublicKey::Unsupported, + subject_public_key_unused_bits: unused_bits, + subject_public_key_bits: bits, + subject_public_key_tlv: Seq::empty(), + spki_der: Seq::empty(), + } +} + +/// An X || Y whose octets are 1, 2, ..., 64, so a shifted copy differs. +pub open spec fn ex_point() -> Seq { + Seq::new(64, |i: int| (i + 1) as u8) +} + +/// A secp256r1 key in uncompressed form, 0x04 || X || Y (RFC 5480 §2.2). +pub open spec fn ex_p256_spki(first: u8, point: Seq) -> clazel_x509::spki::spec::SubjectPublicKeyInfo { + ex_spki(seq![1nat, 2nat, 840nat, 10045nat, 2nat, 1nat], + Some(seq![0x06u8, 0x08u8, 0x2au8, 0x86u8, 0x48u8, 0xceu8, 0x3du8, 0x03u8, 0x01u8, 0x07u8]), + 0, seq![first] + point) +} + +/// RFC 5480 §2.1.1 and RFC 8410 §3: the key algorithm identifiers. +pub proof fn lemma_oid_examples() + ensures + is_ec_public_key(seq![1nat, 2nat, 840nat, 10045nat, 2nat, 1nat]), + // ecdsa-with-SHA256 (RFC 5758 §3.2) is a signature, not a key, OID. + !is_ec_public_key(seq![1nat, 2nat, 840nat, 10045nat, 4nat, 3nat, 2nat]), + is_ed25519(seq![1nat, 3nat, 101nat, 112nat]), + // id-Ed448 (RFC 8410 §3). + !is_ed25519(seq![1nat, 3nat, 101nat, 113nat]), +{ + assert(is_ec_public_key(seq![1nat, 2nat, 840nat, 10045nat, 2nat, 1nat])) by (compute_only); + assert(!is_ec_public_key(seq![1nat, 2nat, 840nat, 10045nat, 4nat, 3nat, 2nat])) by (compute_only); + assert(is_ed25519(seq![1nat, 3nat, 101nat, 112nat])) by (compute_only); + assert(!is_ed25519(seq![1nat, 3nat, 101nat, 113nat])) by (compute_only); +} + +/// RFC 5480 §2.1.1.1: the namedCurve parameter decodes, with our DER +/// decoder, to secp256r1's OBJECT IDENTIFIER 1.2.840.10045.3.1.7. +pub proof fn lemma_secp256r1_parameter_example() + ensures + clazel_der::spec::read_oid(secp256r1_parameter(), 0, 10) + == Some((seq![1nat, 2nat, 840nat, 10045nat, 3nat, 1nat, 7nat], 10nat)), +{ + assert(clazel_der::spec::read_oid(secp256r1_parameter(), 0, 10) + == Some((seq![1nat, 2nat, 840nat, 10045nat, 3nat, 1nat, 7nat], 10nat))) by (compute_only); +} + +/// Left-padding to 32 octets keeps the value: zeros go in front. +pub proof fn lemma_pad32_example() + ensures + pad32(seq![0x01u8]).len() == 32, + pad32(seq![0x01u8])[0] == 0u8, + pad32(seq![0x01u8])[31] == 0x01u8, +{ + assert(pad32(seq![0x01u8]).len() == 32) by (compute_only); + assert(pad32(seq![0x01u8])[0] == 0u8) by (compute_only); + assert(pad32(seq![0x01u8])[31] == 0x01u8) by (compute_only); +} + +/// RFC 5480 §2.2: only 0x04 || X || Y, 65 octets, with no unused bits. +pub proof fn lemma_p256_point_examples() + ensures + p256_point(ex_p256_spki(0x04u8, ex_point())) == Some(ex_point()), + // The compressed form, 0x02 || X. + p256_point(ex_p256_spki(0x02u8, ex_point().subrange(0, 32))) is None, + // A point one octet short. + p256_point(ex_p256_spki(0x04u8, ex_point().subrange(0, 63))) is None, +{ + assert(p256_point(ex_p256_spki(0x04u8, ex_point())) == Some(ex_point())) by (compute_only); + assert(p256_point(ex_p256_spki(0x02u8, ex_point().subrange(0, 32))) is None) by (compute_only); + assert(p256_point(ex_p256_spki(0x04u8, ex_point().subrange(0, 63))) is None) by (compute_only); +} + +/// Ecdsa-Sig-Value { r 1, s 2 } (RFC 3279 §2.2.3). +pub open spec fn ex_sig_1_2() -> Seq { + seq![0x30u8, 0x06, 0x02, 0x01, 0x01, 0x02, 0x01, 0x02] +} + +/// `n` octets of 0xff. +pub open spec fn ex_ones(n: nat) -> Seq { + Seq::new(n, |i: int| 0xffu8) +} + +/// Ecdsa-Sig-Value { r 2^256 - 1, s 2^256 - 1 }: 32 magnitude octets each, +/// after the 0x00 that keeps them positive. +pub open spec fn ex_sig_max() -> Seq { + seq![0x30u8, 0x46, 0x02, 0x21, 0x00] + ex_ones(32) + seq![0x02u8, 0x21, 0x00] + ex_ones(32) +} + +/// RFC 3279 §2.2.3 and the modelling choices: one SEQUENCE of two +/// non-negative INTEGERs of at most 32 magnitude octets, nothing after it. +pub proof fn lemma_ecdsa_sig_value_examples() + ensures + ecdsa_sig_value(ex_sig_1_2()) == Some((pad32(seq![0x01u8]), pad32(seq![0x02u8]))), + ecdsa_sig_value(ex_sig_max()) == Some((ex_ones(32), ex_ones(32))), + // r = -128. + ecdsa_sig_value(seq![0x30u8, 0x06, 0x02, 0x01, 0x80, 0x02, 0x01, 0x02]) is None, + // A third INTEGER. + ecdsa_sig_value(seq![0x30u8, 0x09, 0x02, 0x01, 0x01, 0x02, 0x01, 0x02, 0x02, 0x01, 0x03]) is None, + // An octet after the SEQUENCE. + ecdsa_sig_value(seq![0x30u8, 0x06, 0x02, 0x01, 0x01, 0x02, 0x01, 0x02, 0x00]) is None, +{ + assert(ecdsa_sig_value(ex_sig_1_2()) == Some((pad32(seq![0x01u8]), pad32(seq![0x02u8])))) + by (compute_only); + assert(ecdsa_sig_value(ex_sig_max()) == Some((ex_ones(32), ex_ones(32)))) by (compute_only); + assert(ecdsa_sig_value(seq![0x30u8, 0x06, 0x02, 0x01, 0x80, 0x02, 0x01, 0x02]) is None) + by (compute_only); + assert(ecdsa_sig_value(seq![0x30u8, 0x09, 0x02, 0x01, 0x01, 0x02, 0x01, 0x02, 0x02, 0x01, 0x03]) + is None) by (compute_only); + assert(ecdsa_sig_value(seq![0x30u8, 0x06, 0x02, 0x01, 0x01, 0x02, 0x01, 0x02, 0x00]) is None) + by (compute_only); +} + +/// libcrux-rsa 0.0.9's moduli: 2048 to 8192 bits, the top bit set. +pub proof fn lemma_modulus_ok_examples() + ensures + modulus_ok(ex_ones(256)), + modulus_ok(ex_ones(768)), + modulus_ok(Seq::new(256, |i: int| if i == 0 { 0x80u8 } else { 0u8 })), + // 2047 bits. + !modulus_ok(Seq::new(256, |i: int| if i == 0 { 0x7fu8 } else { 0xffu8 })), + // 2040 bits. + !modulus_ok(ex_ones(255)), +{ + assert(modulus_ok(ex_ones(256))) by (compute_only); + assert(modulus_ok(ex_ones(768))) by (compute_only); + assert(modulus_ok(Seq::new(256, |i: int| if i == 0 { 0x80u8 } else { 0u8 }))) by (compute_only); + assert(!modulus_ok(Seq::new(256, |i: int| if i == 0 { 0x7fu8 } else { 0xffu8 }))) by (compute_only); + assert(!modulus_ok(ex_ones(255))) by (compute_only); +} + +/// FIPS 180-4: the SHA-2 digest lengths, which RFC 8446 §4.2.3 makes the +/// PSS salt lengths. +pub proof fn lemma_hash_len_examples() + ensures + hash_len(Hash::Sha256) == 32, + hash_len(Hash::Sha384) == 48, + hash_len(Hash::Sha512) == 64, +{ +} + +/// 32 octets: `first`, then 30 of `middle`, then `last`. +pub open spec fn ex_key(first: u8, middle: u8, last: u8) -> Seq { + Seq::new(32, |i: int| if i == 0 { first } else if i == 31 { last } else { middle }) +} + +/// The encodings of edwards25519's eight points of order dividing 8, and +/// p and p + 1, computed from RFC 8032 §5.1's curve equation separately +/// from the table in the spec (they match libsodium's blocklist). +pub open spec fn ex_order8_a(sign: u8) -> Seq { + seq![0x26u8, 0xe8, 0x95, 0x8f, 0xc2, 0xb2, 0x27, 0xb0, 0x45, 0xc3, 0xf4, 0x89, 0xf2, 0xef, + 0x98, 0xf0, 0xd5, 0xdf, 0xac, 0x05, 0xd3, 0xc6, 0x33, 0x39, 0xb1, 0x38, 0x02, 0x88, + 0x6d, 0x53, 0xfc, 0x05 | sign] +} + +/// The other order-8 pair (see [`ex_order8_a`]). +pub open spec fn ex_order8_b(sign: u8) -> Seq { + seq![0xc7u8, 0x17, 0x6a, 0x70, 0x3d, 0x4d, 0xd8, 0x4f, 0xba, 0x3c, 0x0b, 0x76, 0x0d, 0x10, + 0x67, 0x0f, 0x2a, 0x20, 0x53, 0xfa, 0x2c, 0x39, 0xcc, 0xc6, 0x4e, 0xc7, 0xfd, 0x77, + 0x92, 0xac, 0x03, 0x7a | sign] +} + +/// Each small-order encoding matches its table entry, with either x sign +/// bit, and the identity is small-order. +pub proof fn lemma_small_order_examples() + ensures + same_y(ex_key(0x00, 0x00, 0x00), small_order_y()[0]), + same_y(ex_key(0x00, 0x00, 0x80), small_order_y()[0]), + same_y(ex_key(0x01, 0x00, 0x00), small_order_y()[1]), + same_y(ex_key(0x01, 0x00, 0x80), small_order_y()[1]), + same_y(ex_key(0xec, 0xff, 0x7f), small_order_y()[2]), + same_y(ex_order8_a(0x00), small_order_y()[3]), + same_y(ex_order8_a(0x80), small_order_y()[3]), + same_y(ex_order8_b(0x00), small_order_y()[4]), + same_y(ex_order8_b(0x80), small_order_y()[4]), + same_y(ex_key(0xed, 0xff, 0x7f), small_order_y()[5]), + same_y(ex_key(0xee, 0xff, 0x7f), small_order_y()[6]), + // The first octet counts: the identity is not y = 0. + !same_y(ex_key(0x01, 0x00, 0x00), small_order_y()[0]), + small_order_y().len() == 7, + is_small_order(ex_key(0x01, 0x00, 0x00)), +{ + assert(same_y(ex_key(0x00, 0x00, 0x00), small_order_y()[0])) by (compute_only); + assert(same_y(ex_key(0x00, 0x00, 0x80), small_order_y()[0])) by (compute_only); + assert(same_y(ex_key(0x01, 0x00, 0x00), small_order_y()[1])) by (compute_only); + assert(same_y(ex_key(0x01, 0x00, 0x80), small_order_y()[1])) by (compute_only); + assert(same_y(ex_key(0xec, 0xff, 0x7f), small_order_y()[2])) by (compute_only); + assert(same_y(ex_order8_a(0x00), small_order_y()[3])) by (compute_only); + assert(same_y(ex_order8_a(0x80), small_order_y()[3])) by (compute_only); + assert(same_y(ex_order8_b(0x00), small_order_y()[4])) by (compute_only); + assert(same_y(ex_order8_b(0x80), small_order_y()[4])) by (compute_only); + assert(same_y(ex_key(0xed, 0xff, 0x7f), small_order_y()[5])) by (compute_only); + assert(same_y(ex_key(0xee, 0xff, 0x7f), small_order_y()[6])) by (compute_only); + assert(!same_y(ex_key(0x01, 0x00, 0x00), small_order_y()[0])) by (compute_only); + assert(small_order_y().len() == 7) by (compute_only); +} + +} // verus! diff --git a/crates/clazel-crypto/src/signature/exec.rs b/crates/clazel-crypto/src/signature/exec.rs new file mode 100644 index 0000000..ff99d4f --- /dev/null +++ b/crates/clazel-crypto/src/signature/exec.rs @@ -0,0 +1,303 @@ +//! The executable CertificateVerify signature check, proven equal to +//! [`crate::signature::spec::verify`]. Parsing is ours (`clazel-x509`, +//! `clazel-der`); the three verifications are the axioms of +//! [`crate::axioms`]. +use crate::axioms; +use crate::signature::spec::Hash; +use clazel_der::decode as der; +use clazel_x509::spki::exec::{PublicKey, SubjectPublicKeyInfo}; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +/// id-ecPublicKey, 1.2.840.10045.2.1 (RFC 5480 §2.1.1). +fn is_ec_oid(oid: &[u64]) -> (r: bool) + ensures r == crate::signature::spec::is_ec_public_key(der::nats(oid@)), +{ + oid.len() == 6 + && oid.first() == Some(&1) + && oid.get(1) == Some(&2) + && oid.get(2) == Some(&840) + && oid.get(3) == Some(&10045) + && oid.get(4) == Some(&2) + && oid.get(5) == Some(&1) +} + +/// id-Ed25519, 1.3.101.112 (RFC 8410 §3). +fn is_ed25519_oid(oid: &[u64]) -> (r: bool) + ensures r == crate::signature::spec::is_ed25519(der::nats(oid@)), +{ + oid.len() == 4 + && oid.first() == Some(&1) + && oid.get(1) == Some(&3) + && oid.get(2) == Some(&101) + && oid.get(3) == Some(&112) +} + +/// The namedCurve secp256r1 parameter (RFC 5480 §2.1.1.1). +fn is_secp256r1_parameter(p: &[u8]) -> (r: bool) + ensures r == (p@ =~= crate::signature::spec::secp256r1_parameter()), +{ + p.len() == 10 + && p.first() == Some(&0x06) + && p.get(1) == Some(&0x08) + && p.get(2) == Some(&0x2a) + && p.get(3) == Some(&0x86) + && p.get(4) == Some(&0x48) + && p.get(5) == Some(&0xce) + && p.get(6) == Some(&0x3d) + && p.get(7) == Some(&0x03) + && p.get(8) == Some(&0x01) + && p.get(9) == Some(&0x07) +} + +/// `m` left-padded with zeros to 32 octets. +fn pad32(m: &[u8]) -> (out: Vec) + requires m.len() <= 32, + ensures out@ == crate::signature::spec::pad32(m@), out.len() == 32, +{ + // m.len() <= 32, so this is exact. + let zeros = 32usize.saturating_sub(m.len()); + let mut out: Vec = Vec::new(); + let mut k: usize = 0; + while k < zeros + invariant k <= zeros, zeros == 32 - m.len(), out@ =~= Seq::new(k as nat, |i: int| 0u8), + decreases zeros - k, + { + out.push(0); + // k < zeros <= 32, so this is exact. + k = k.saturating_add(1); + } + out.extend_from_slice(m); + proof { assert(out@ =~= crate::signature::spec::pad32(m@)); } + out +} + +/// RFC 5480 §2.2: the X || Y of an uncompressed secp256r1 key. +fn p256_point<'a>(spki: &SubjectPublicKeyInfo<'a>) -> (out: Option<&'a [u8]>) + ensures + match out { + Some(p) => crate::signature::spec::p256_point(spki@) == Some(p@), + None => crate::signature::spec::p256_point(spki@) is None, + }, +{ + let bits = spki.subject_public_key_bits; + let params_ok = match spki.algorithm.parameters_der { + Some(p) => is_secp256r1_parameter(p), + None => false, + }; + if is_ec_oid(spki.algorithm.oid.as_slice()) && params_ok + && spki.subject_public_key_unused_bits == 0 + && bits.len() == 65 && bits.first() == Some(&0x04) { + Some(vstd::slice::slice_subrange(bits, 1, 65)) + } else { + None + } +} + +/// RFC 3279 §2.2.3: r and s of one DER Ecdsa-Sig-Value, padded to 32. +fn ecdsa_sig_value(signature: &[u8]) -> (out: Option<(Vec, Vec)>) + ensures + match out { + Some((r, s)) => crate::signature::spec::ecdsa_sig_value(signature@) == Some((r@, s@)), + None => crate::signature::spec::ecdsa_sig_value(signature@) is None, + }, +{ + let (cs, ce) = der::expect_sequence(signature, 0, signature.len())?; + if ce != signature.len() { + return None; + } + let (r_negative, rs, re, after_r) = der::read_integer(signature, cs, ce)?; + // read_integer gives rs <= re and ss <= se, so these are exact. + if r_negative || re.saturating_sub(rs) > 32 { + return None; + } + let (s_negative, ss, se, after_s) = der::read_integer(signature, after_r, ce)?; + if s_negative || se.saturating_sub(ss) > 32 || after_s != ce { + return None; + } + let r = pad32(vstd::slice::slice_subrange(signature, rs, re)); + let s = pad32(vstd::slice::slice_subrange(signature, ss, se)); + Some((r, s)) +} + +/// ecdsa_secp256r1_sha256 (0x0403). +fn ecdsa_p256_sha256(spki: &SubjectPublicKeyInfo, input: &[u8], signature: &[u8]) -> (out: bool) + ensures out == crate::signature::spec::ecdsa_p256_sha256(spki@, input@, signature@), +{ + match (p256_point(spki), ecdsa_sig_value(signature)) { + (Some(point), Some((r, s))) => + axioms::ecdsa_p256_sha256_verify(input, r.as_slice(), s.as_slice(), point), + _ => false, + } +} + +/// The modulus sizes libcrux-rsa accepts, with the top bit set. +fn modulus_ok(n: &[u8]) -> (r: bool) + ensures r == crate::signature::spec::modulus_ok(n@), +{ + let len = n.len(); + (len == 256 || len == 384 || len == 512 || len == 768 || len == 1024) + && match n.first() { Some(&b) => b >= 0x80, None => false } +} + +/// rsa_pss_rsae_* (0x0804-0x0806). +fn rsa_pss_rsae(spki: &SubjectPublicKeyInfo, hash: Hash, input: &[u8], signature: &[u8]) -> (out: bool) + ensures out == crate::signature::spec::rsa_pss_rsae(spki@, hash, input@, signature@), +{ + match &spki.public_key { + PublicKey::Rsa(key) => { + let e = key.public_exponent_octets; + let n = key.modulus_octets; + let e_ok = e.len() == 3 && e.first() == Some(&1) && e.get(1) == Some(&0) + && e.get(2) == Some(&1); + proof { assert(e_ok == (e@ =~= seq![0x01u8, 0x00u8, 0x01u8])); } + if !e_ok || !modulus_ok(n) || signature.len() != n.len() { + return false; + } + let salt_len: u32 = match hash { + Hash::Sha256 => 32, + Hash::Sha384 => 48, + Hash::Sha512 => 64, + }; + axioms::rsa_pss_verify(hash, n, input, salt_len, signature) + }, + PublicKey::Unsupported => false, + } +} + +/// Whether `key`, ignoring its x sign bit, has y-coordinate `y`. +fn same_y(key: &[u8], y: &[u8]) -> (r: bool) + requires key.len() == 32, y.len() == 32, + ensures r == crate::signature::spec::same_y(key@, y@), +{ + let mut i: usize = 0; + while i < 31 + invariant i <= 31, key.len() == 32, y.len() == 32, + forall|j: int| 0 <= j < i ==> key@[j] == y@[j], + decreases 31 - i, + { + match (key.get(i), y.get(i)) { + (Some(a), Some(b)) if *a == *b => {}, + _ => { + proof { assert(key@.subrange(0, 31)[i as int] != y@.subrange(0, 31)[i as int]); } + return false; + }, + } + // i < 31, so this is exact. + i = i.saturating_add(1); + } + proof { assert(key@.subrange(0, 31) =~= y@.subrange(0, 31)); } + match (key.get(31), y.get(31)) { + (Some(a), Some(b)) => *a & 0x7f == *b, + _ => false, + } +} + +/// Whether the 32-octet `key` encodes a point of small order. +fn is_small_order(key: &[u8]) -> (r: bool) + requires key.len() == 32, + ensures r == crate::signature::spec::is_small_order(key@), +{ + // 0: (sqrt(-1), 0) and (-sqrt(-1), 0), order 4 + let y0: [u8; 32] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, + ]; + // 1: the identity (0, 1), order 1 + let y1: [u8; 32] = [ + 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, + ]; + // p - 1: (0, -1), order 2 + let y2: [u8; 32] = [ + 0xec, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, + 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, + 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, + 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x7f, + ]; + // two of the order-8 points + let y3: [u8; 32] = [ + 0x26, 0xe8, 0x95, 0x8f, 0xc2, 0xb2, 0x27, 0xb0, + 0x45, 0xc3, 0xf4, 0x89, 0xf2, 0xef, 0x98, 0xf0, + 0xd5, 0xdf, 0xac, 0x05, 0xd3, 0xc6, 0x33, 0x39, + 0xb1, 0x38, 0x02, 0x88, 0x6d, 0x53, 0xfc, 0x05, + ]; + // the other two order-8 points + let y4: [u8; 32] = [ + 0xc7, 0x17, 0x6a, 0x70, 0x3d, 0x4d, 0xd8, 0x4f, + 0xba, 0x3c, 0x0b, 0x76, 0x0d, 0x10, 0x67, 0x0f, + 0x2a, 0x20, 0x53, 0xfa, 0x2c, 0x39, 0xcc, 0xc6, + 0x4e, 0xc7, 0xfd, 0x77, 0x92, 0xac, 0x03, 0x7a, + ]; + // p: a non-canonical encoding of 0 + let y5: [u8; 32] = [ + 0xed, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, + 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, + 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, + 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x7f, + ]; + // p + 1: a non-canonical encoding of 1 + let y6: [u8; 32] = [ + 0xee, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, + 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, + 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, + 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x7f, + ]; + let r = same_y(key, y0.as_slice()) || same_y(key, y1.as_slice()) + || same_y(key, y2.as_slice()) || same_y(key, y3.as_slice()) + || same_y(key, y4.as_slice()) || same_y(key, y5.as_slice()) + || same_y(key, y6.as_slice()); + proof { + let ys = crate::signature::spec::small_order_y(); + assert(ys.len() == 7); + assert(y0@ =~= ys[0]); + assert(y1@ =~= ys[1]); + assert(y2@ =~= ys[2]); + assert(y3@ =~= ys[3]); + assert(y4@ =~= ys[4]); + assert(y5@ =~= ys[5]); + assert(y6@ =~= ys[6]); + } + r +} + +/// ed25519 (0x0807). +fn ed25519(spki: &SubjectPublicKeyInfo, input: &[u8], signature: &[u8]) -> (out: bool) + ensures out == crate::signature::spec::ed25519(spki@, input@, signature@), +{ + let key = spki.subject_public_key_bits; + if is_ed25519_oid(spki.algorithm.oid.as_slice()) + && spki.algorithm.parameters_der.is_none() + && spki.subject_public_key_unused_bits == 0 + && key.len() == 32 && signature.len() == 64 + && !is_small_order(key) { + axioms::ed25519_verify(input, key, signature) + } else { + false + } +} + +/// RFC 8446 §4.4.3: whether `signature` is a valid `scheme` signature of +/// `input` under the end-entity SubjectPublicKeyInfo `key`. +pub fn verify(key: &[u8], scheme: u16, input: &[u8], signature: &[u8]) -> (out: bool) + ensures out == crate::signature::spec::verify(key@, scheme, input@, signature@), +{ + match clazel_x509::spki::exec::parse_subject_public_key_info(key) { + None => false, + Some(spki) => + if scheme == 0x0403 { ecdsa_p256_sha256(&spki, input, signature) } + else if scheme == 0x0804 { rsa_pss_rsae(&spki, Hash::Sha256, input, signature) } + else if scheme == 0x0805 { rsa_pss_rsae(&spki, Hash::Sha384, input, signature) } + else if scheme == 0x0806 { rsa_pss_rsae(&spki, Hash::Sha512, input, signature) } + else if scheme == 0x0807 { ed25519(&spki, input, signature) } + else { false }, + } +} + +} // verus! diff --git a/crates/clazel-crypto/src/signature/mod.rs b/crates/clazel-crypto/src/signature/mod.rs new file mode 100644 index 0000000..18ca7b5 --- /dev/null +++ b/crates/clazel-crypto/src/signature/mod.rs @@ -0,0 +1,7 @@ +//! RFC 8446 §4.4.3 CertificateVerify signature verification. + +pub mod spec; + +pub mod certificates; +pub mod examples; +pub mod exec; diff --git a/crates/clazel-crypto/src/signature/spec.rs b/crates/clazel-crypto/src/signature/spec.rs new file mode 100644 index 0000000..ab0d143 --- /dev/null +++ b/crates/clazel-crypto/src/signature/spec.rs @@ -0,0 +1,268 @@ +//! RFC 8446 §4.4.3: verify a CertificateVerify signature with the +//! end-entity key, for the signature schemes this client offers (§4.2.3). +//! +//! Sources, by step: +//! - RFC 8446 §4.2.3, SignatureScheme: ecdsa_secp256r1_sha256 (0x0403), +//! rsa_pss_rsae_sha256/384/512 (0x0804-0x0806) and ed25519 (0x0807). +//! +//! - RFC 5480 §2.1.1 (id-ecPublicKey, namedCurve secp256r1) and §2.2 (the +//! ECPoint), ; RFC 3279 +//! §2.2.3 (Ecdsa-Sig-Value), . +//! - RFC 3279 §2.3.1 and RFC 8017 Appendix A.1.1 (rsaEncryption keys), via +//! `clazel_x509::spki`; RFC 8017 §8.1.2 RSASSA-PSS-VERIFY, with RFC 8446 +//! §4.2.3's MGF1 over the same hash and a salt as long as the digest. +//! - RFC 8410 §3 and §4 (id-Ed25519 keys); RFC 8032 §5.1.2 (point +//! encoding) and §5.1.7 (verification). The small-order points are those +//! of Chalkias, Garillot and Nikolaenko, "Taming the many EdDSAs" (2020), +//! . +//! +//! Modelling choices: +//! - `key` is the end-entity certificate's complete DER +//! SubjectPublicKeyInfo, the value chain validation hands to the signature +//! check. It is parsed with `clazel_x509::spki`, our own decoder. +//! - ECDSA: only id-ecPublicKey with the namedCurve secp256r1 parameter +//! (RFC 5480 §2.1.1.1; explicit curve parameters are refused) and only the +//! uncompressed point 0x04 || X || Y (RFC 5480 §2.2 requires support for +//! it; the compressed form is optional and refused). The signature is one +//! DER Ecdsa-Sig-Value with nothing after it; r and s are non-negative +//! DER INTEGERs of at most 32 magnitude octets, left-padded to 32. Their +//! range 1..n-1 and the point's validity are checked by libcrux. +//! - RSA-PSS (rsae): only rsaEncryption keys, as RFC 8446 §4.2.3 requires +//! for the rsae schemes. The public exponent must be 65537, the only one +//! libcrux-rsa 0.0.9 verifies with, and the modulus must be exactly 2048, +//! 3072, 4096, 6144 or 8192 bits (its first octet has the top bit set), +//! the only sizes it accepts. The signature is as long as the modulus. +//! Keys outside this profile are refused, never verified with another +//! exponent. +//! - rsa_pss_pss_* (0x0809-0x080b) are neither offered nor verified (see +//! `clazel_tls::hello::client_spec`). +//! - Ed25519: id-Ed25519 with absent parameters (RFC 8410 §3), a 32-octet +//! key in a BIT STRING with no unused bits, and a 64-octet signature. +//! A key of small order is refused, which RFC 8032 §5.1.7 does not +//! require: under the identity key, R = identity and S = 0 verify for +//! every message. Small order means the key's y-coordinate (its low 255 +//! bits, RFC 8032 §5.1.2) is one of the five that edwards25519's eight +//! points of order dividing 8 have, or p or p + 1, which libcrux refuses +//! as non-canonical but which are refused here too. Mixed-order keys +//! (a large-order point plus a small-order one) are not refused: they do +//! not let one signature verify every message. +//! - Any other scheme, key type or malformed input is `false`. +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +/// The SHA-2 function an RSA-PSS scheme uses for its digest and for MGF1. +#[derive(PartialEq, Eq, Clone, Copy)] +pub enum Hash { + /// SHA-256 (rsa_pss_rsae_sha256). + Sha256, + /// SHA-384 (rsa_pss_rsae_sha384). + Sha384, + /// SHA-512 (rsa_pss_rsae_sha512). + Sha512, +} + +/// The digest length of `hash`, which RFC 8446 §4.2.3 also makes the salt length. +pub open spec fn hash_len(hash: Hash) -> nat { + match hash { + Hash::Sha256 => 32, + Hash::Sha384 => 48, + Hash::Sha512 => 64, + } +} + +/// ECDSA P-256 with SHA-256 of `message` (FIPS 186-5 §6.4.2): `r` and `s` +/// are 32 octets, `point` is X || Y (64 octets). Uninterpreted: libcrux's. +pub uninterp spec fn ecdsa_p256_sha256_verify(message: Seq, r: Seq, s: Seq, + point: Seq) -> bool; + +/// RSASSA-PSS-VERIFY (RFC 8017 §8.1.2) with public exponent 65537, MGF1 +/// over `hash` and the given salt length. Uninterpreted: libcrux's. +pub uninterp spec fn rsa_pss_verify(hash: Hash, modulus: Seq, message: Seq, + salt_len: nat, signature: Seq) -> bool; + +/// Ed25519 verification (RFC 8032 §5.1.7) of `message` under the 32-octet +/// `key`. Uninterpreted: libcrux's. +pub uninterp spec fn ed25519_verify(message: Seq, key: Seq, signature: Seq) -> bool; + +/// id-ecPublicKey, 1.2.840.10045.2.1 (RFC 5480 §2.1.1). +pub open spec fn is_ec_public_key(oid: Seq) -> bool { + oid =~= seq![1nat, 2nat, 840nat, 10045nat, 2nat, 1nat] +} + +/// The DER of the namedCurve parameter secp256r1, OBJECT IDENTIFIER +/// 1.2.840.10045.3.1.7 (RFC 5480 §2.1.1.1). +pub open spec fn secp256r1_parameter() -> Seq { + seq![0x06u8, 0x08u8, 0x2au8, 0x86u8, 0x48u8, 0xceu8, 0x3du8, 0x03u8, 0x01u8, 0x07u8] +} + +/// id-Ed25519, 1.3.101.112 (RFC 8410 §3). +pub open spec fn is_ed25519(oid: Seq) -> bool { + oid =~= seq![1nat, 3nat, 101nat, 112nat] +} + +/// `m` left-padded with zero octets to 32 octets (`m` is at most 32). +pub open spec fn pad32(m: Seq) -> Seq { + Seq::new((32 - m.len()) as nat, |i: int| 0u8) + m +} + +/// RFC 5480 §2.2: the X || Y of a secp256r1 key in uncompressed form. +pub open spec fn p256_point(spki: clazel_x509::spki::spec::SubjectPublicKeyInfo) -> Option> { + let bits = spki.subject_public_key_bits; + if is_ec_public_key(spki.algorithm.oid) + && spki.algorithm.parameters_der == Some(secp256r1_parameter()) + && spki.subject_public_key_unused_bits == 0 + && bits.len() == 65 && bits[0] == 0x04u8 { + Some(bits.subrange(1, 65)) + } else { + None + } +} + +/// RFC 3279 §2.2.3: r and s of exactly one DER Ecdsa-Sig-Value, each a +/// non-negative INTEGER of at most 32 magnitude octets, padded to 32. +pub open spec fn ecdsa_sig_value(signature: Seq) -> Option<(Seq, Seq)> { + match clazel_der::spec::expect_sequence(signature, 0, signature.len()) { + Some((cs, ce)) if ce == signature.len() => + match clazel_der::spec::read_integer(signature, cs, ce) { + Some((r_negative, rs, re, after_r)) if !r_negative && re - rs <= 32 => + match clazel_der::spec::read_integer(signature, after_r, ce) { + Some((s_negative, ss, se, after_s)) if !s_negative && se - ss <= 32 && after_s == ce => + Some((pad32(signature.subrange(rs as int, re as int)), + pad32(signature.subrange(ss as int, se as int)))), + _ => None, + }, + _ => None, + }, + _ => None, + } +} + +/// ecdsa_secp256r1_sha256 (0x0403). +pub open spec fn ecdsa_p256_sha256(spki: clazel_x509::spki::spec::SubjectPublicKeyInfo, + input: Seq, signature: Seq) -> bool { + match (p256_point(spki), ecdsa_sig_value(signature)) { + (Some(point), Some((r, s))) => ecdsa_p256_sha256_verify(input, r, s, point), + _ => false, + } +} + +/// The RSA modulus sizes libcrux-rsa accepts, with the top bit of the +/// first octet set so the bit length is exactly 8 times the octet length. +pub open spec fn modulus_ok(n: Seq) -> bool { + (n.len() == 256 || n.len() == 384 || n.len() == 512 || n.len() == 768 || n.len() == 1024) + && n[0] >= 0x80u8 +} + +/// rsa_pss_rsae_sha256/384/512 (0x0804-0x0806). +pub open spec fn rsa_pss_rsae(spki: clazel_x509::spki::spec::SubjectPublicKeyInfo, hash: Hash, + input: Seq, signature: Seq) -> bool { + match spki.public_key { + clazel_x509::spki::spec::PublicKey::Rsa(key) => + key.public_exponent_octets =~= seq![0x01u8, 0x00u8, 0x01u8] + && modulus_ok(key.modulus_octets) + && signature.len() == key.modulus_octets.len() + && rsa_pss_verify(hash, key.modulus_octets, input, hash_len(hash), signature), + _ => false, + } +} + +/// The y-coordinates, as 32 little-endian octets with the sign bit clear, +/// of edwards25519's points of order 1, 2, 4 and 8, and the two values +/// at or above p that reduce to one of them. +pub open spec fn small_order_y() -> Seq> { + seq![ + // 0: (sqrt(-1), 0) and (-sqrt(-1), 0), order 4 + seq![ + 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, + 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, + 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, + 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, + ], + // 1: the identity (0, 1), order 1 + seq![ + 0x01u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, + 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, + 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, + 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, 0x00u8, + ], + // p - 1: (0, -1), order 2 + seq![ + 0xecu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, + 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, + 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, + 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0x7fu8, + ], + // two of the order-8 points + seq![ + 0x26u8, 0xe8u8, 0x95u8, 0x8fu8, 0xc2u8, 0xb2u8, 0x27u8, 0xb0u8, + 0x45u8, 0xc3u8, 0xf4u8, 0x89u8, 0xf2u8, 0xefu8, 0x98u8, 0xf0u8, + 0xd5u8, 0xdfu8, 0xacu8, 0x05u8, 0xd3u8, 0xc6u8, 0x33u8, 0x39u8, + 0xb1u8, 0x38u8, 0x02u8, 0x88u8, 0x6du8, 0x53u8, 0xfcu8, 0x05u8, + ], + // the other two order-8 points + seq![ + 0xc7u8, 0x17u8, 0x6au8, 0x70u8, 0x3du8, 0x4du8, 0xd8u8, 0x4fu8, + 0xbau8, 0x3cu8, 0x0bu8, 0x76u8, 0x0du8, 0x10u8, 0x67u8, 0x0fu8, + 0x2au8, 0x20u8, 0x53u8, 0xfau8, 0x2cu8, 0x39u8, 0xccu8, 0xc6u8, + 0x4eu8, 0xc7u8, 0xfdu8, 0x77u8, 0x92u8, 0xacu8, 0x03u8, 0x7au8, + ], + // p: a non-canonical encoding of 0 + seq![ + 0xedu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, + 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, + 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, + 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0x7fu8, + ], + // p + 1: a non-canonical encoding of 1 + seq![ + 0xeeu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, + 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, + 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, + 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0xffu8, 0x7fu8, + ], + ] +} + +/// Whether the encoded point `key` (RFC 8032 §5.1.2), ignoring its x sign +/// bit (bit 7 of the last octet), has y-coordinate `y`. +pub open spec fn same_y(key: Seq, y: Seq) -> bool { + key.len() == 32 && y.len() == 32 + && key.subrange(0, 31) =~= y.subrange(0, 31) + && key[31] & 0x7fu8 == y[31] +} + +/// Whether `key` encodes a point of small order (see the modelling choices). +pub open spec fn is_small_order(key: Seq) -> bool { + exists|i: int| 0 <= i < small_order_y().len() && #[trigger] same_y(key, small_order_y()[i]) +} + +/// ed25519 (0x0807). +pub open spec fn ed25519(spki: clazel_x509::spki::spec::SubjectPublicKeyInfo, input: Seq, + signature: Seq) -> bool { + is_ed25519(spki.algorithm.oid) + && spki.algorithm.parameters_der is None + && spki.subject_public_key_unused_bits == 0 + && spki.subject_public_key_bits.len() == 32 + && signature.len() == 64 + && !is_small_order(spki.subject_public_key_bits) + && ed25519_verify(input, spki.subject_public_key_bits, signature) +} + +/// RFC 8446 §4.4.3: whether `signature` is a valid `scheme` signature of +/// `input` under the end-entity SubjectPublicKeyInfo `key`. +pub open spec fn verify(key: Seq, scheme: u16, input: Seq, signature: Seq) -> bool { + match clazel_x509::spki::spec::parse_subject_public_key_info(key) { + None => false, + Some(spki) => + if scheme == 0x0403 { ecdsa_p256_sha256(spki, input, signature) } + else if scheme == 0x0804 { rsa_pss_rsae(spki, Hash::Sha256, input, signature) } + else if scheme == 0x0805 { rsa_pss_rsae(spki, Hash::Sha384, input, signature) } + else if scheme == 0x0806 { rsa_pss_rsae(spki, Hash::Sha512, input, signature) } + else if scheme == 0x0807 { ed25519(spki, input, signature) } + else { false }, + } +} + +} // verus! diff --git a/crates/clazel-crypto/tests/fixtures/rsa-pss/SOURCE.md b/crates/clazel-crypto/tests/fixtures/rsa-pss/SOURCE.md new file mode 100644 index 0000000..ef41387 --- /dev/null +++ b/crates/clazel-crypto/tests/fixtures/rsa-pss/SOURCE.md @@ -0,0 +1,30 @@ +# RSA-PSS CertificateVerify fixtures + +Generated for `tests/signature.rs` on 2026-10-26 with LibreSSL 3.3.6 (macOS). +There is no deterministic RFC test vector for RSASSA-PSS (the salt is random), +so these are our own. Only public keys and signatures are kept; the private +keys were discarded. + +- `msg.bin`: the 27-octet message `clazel rsa-pss test message`. +- `k2048.spki.der`: a 2048-bit rsaEncryption key, e = 65537. + `k2048.{sha256,sha384,sha512}.sig`: RSASSA-PSS signatures of `msg.bin` with + MGF1 over the same hash and a salt as long as the digest (RFC 8446 §4.2.3), + each checked with `openssl pkeyutl -verify` before being kept. +- `ke3.spki.der` / `ke3.sha256.sig`: a 2048-bit key with e = 3, signed the + same way. It must be refused: libcrux-rsa verifies only with e = 65537. +- `k2047.spki.der` / `k2047.sha256.sig`: a 2047-bit key (its modulus fills + 256 octets without the top bit set). It must be refused, too. + +To regenerate (new keys give new files, so update the tests' expectations): + +```sh +printf 'clazel rsa-pss test message' > msg.bin +openssl genpkey -algorithm RSA -pkeyopt rsa_keygen_bits:2048 -out k2048.pem +openssl genpkey -algorithm RSA -pkeyopt rsa_keygen_bits:2048 -pkeyopt rsa_keygen_pubexp:3 -out ke3.pem +openssl genpkey -algorithm RSA -pkeyopt rsa_keygen_bits:2047 -out k2047.pem +openssl pkey -in k2048.pem -pubout -outform DER -out k2048.spki.der # likewise ke3, k2047 +openssl dgst -sha256 -binary msg.bin > d256 +openssl pkeyutl -sign -in d256 -inkey k2048.pem -pkeyopt digest:sha256 \ + -pkeyopt rsa_padding_mode:pss -pkeyopt rsa_pss_saltlen:32 -pkeyopt rsa_mgf1_md:sha256 \ + -out k2048.sha256.sig # likewise 384/48, 512/64 +``` diff --git a/crates/clazel-crypto/tests/fixtures/rsa-pss/k2047.sha256.sig b/crates/clazel-crypto/tests/fixtures/rsa-pss/k2047.sha256.sig new file mode 100644 index 0000000..7ccad67 Binary files /dev/null and b/crates/clazel-crypto/tests/fixtures/rsa-pss/k2047.sha256.sig differ diff --git a/crates/clazel-crypto/tests/fixtures/rsa-pss/k2047.spki.der b/crates/clazel-crypto/tests/fixtures/rsa-pss/k2047.spki.der new file mode 100644 index 0000000..44ec94d Binary files /dev/null and b/crates/clazel-crypto/tests/fixtures/rsa-pss/k2047.spki.der differ diff --git a/crates/clazel-crypto/tests/fixtures/rsa-pss/k2048.sha256.sig b/crates/clazel-crypto/tests/fixtures/rsa-pss/k2048.sha256.sig new file mode 100644 index 0000000..25dedd8 Binary files /dev/null and b/crates/clazel-crypto/tests/fixtures/rsa-pss/k2048.sha256.sig differ diff --git a/crates/clazel-crypto/tests/fixtures/rsa-pss/k2048.sha384.sig b/crates/clazel-crypto/tests/fixtures/rsa-pss/k2048.sha384.sig new file mode 100644 index 0000000..2a7437e --- /dev/null +++ b/crates/clazel-crypto/tests/fixtures/rsa-pss/k2048.sha384.sig @@ -0,0 +1 @@ +28=^r%7ntkmBѕ*sUG ywCHJ2GPNwGegP[Y1nr$Ah4˗^ZGr[G-]m}zdzPo/7⋡Ї>onv|B/ ZڬO3c74FFnF RAm&Xz!Qi] @ۺlT+:{I"/E$1h|*i1<^ \ No newline at end of file diff --git a/crates/clazel-crypto/tests/fixtures/rsa-pss/k2048.sha512.sig b/crates/clazel-crypto/tests/fixtures/rsa-pss/k2048.sha512.sig new file mode 100644 index 0000000..67c7533 --- /dev/null +++ b/crates/clazel-crypto/tests/fixtures/rsa-pss/k2048.sha512.sig @@ -0,0 +1,2 @@ +KvpOO{kxsz/$ H< +8R#lc- nӟ7&Q͎~ NZ|/Jv{ϣ'"ڙrN7@+{X w3{֙<`~Xv1Ijҡ\+Ċ#xC`g2})i'5h{YY@`&7ag:mԇ%| \ No newline at end of file diff --git a/crates/clazel-crypto/tests/fixtures/rsa-pss/k2048.spki.der b/crates/clazel-crypto/tests/fixtures/rsa-pss/k2048.spki.der new file mode 100644 index 0000000..7456279 Binary files /dev/null and b/crates/clazel-crypto/tests/fixtures/rsa-pss/k2048.spki.der differ diff --git a/crates/clazel-crypto/tests/fixtures/rsa-pss/ke3.sha256.sig b/crates/clazel-crypto/tests/fixtures/rsa-pss/ke3.sha256.sig new file mode 100644 index 0000000..345dba5 Binary files /dev/null and b/crates/clazel-crypto/tests/fixtures/rsa-pss/ke3.sha256.sig differ diff --git a/crates/clazel-crypto/tests/fixtures/rsa-pss/ke3.spki.der b/crates/clazel-crypto/tests/fixtures/rsa-pss/ke3.spki.der new file mode 100644 index 0000000..b544322 Binary files /dev/null and b/crates/clazel-crypto/tests/fixtures/rsa-pss/ke3.spki.der differ diff --git a/crates/clazel-crypto/tests/fixtures/rsa-pss/msg.bin b/crates/clazel-crypto/tests/fixtures/rsa-pss/msg.bin new file mode 100644 index 0000000..58a1060 --- /dev/null +++ b/crates/clazel-crypto/tests/fixtures/rsa-pss/msg.bin @@ -0,0 +1 @@ +clazel rsa-pss test message \ No newline at end of file diff --git a/crates/clazel-crypto/tests/signature.rs b/crates/clazel-crypto/tests/signature.rs new file mode 100644 index 0000000..cf4d3b1 --- /dev/null +++ b/crates/clazel-crypto/tests/signature.rs @@ -0,0 +1,354 @@ +//! CertificateVerify signature checks (`clazel_crypto::signature::exec::verify`) +//! with the standards' own vectors where they exist: RFC 8032 §7.1 TEST 1 +//! and TEST 2 (Ed25519) and RFC 6979 A.2.5 (ECDSA P-256, SHA-256, message +//! "sample"). RSA-PSS has no deterministic vector; its fixtures are in +//! tests/fixtures/rsa-pss (see SOURCE.md there). Every refusal the spec's +//! modelling choices list is exercised. + +use clazel_crypto::signature::exec::verify; + +const ECDSA_P256_SHA256: u16 = 0x0403; +const RSA_PSS_RSAE_SHA256: u16 = 0x0804; +const RSA_PSS_RSAE_SHA384: u16 = 0x0805; +const RSA_PSS_RSAE_SHA512: u16 = 0x0806; +const ED25519: u16 = 0x0807; +const RSA_PSS_PSS_SHA256: u16 = 0x0809; + +type TestResult = Result<(), String>; + +fn hex(text: &str) -> Result, String> { + let digits: Vec = text.bytes().filter(|b| !b.is_ascii_whitespace()).collect(); + digits + .chunks(2) + .map(|pair| { + let pair = std::str::from_utf8(pair).map_err(|e| e.to_string())?; + u8::from_str_radix(pair, 16).map_err(|e| format!("{pair}: {e}")) + }) + .collect() +} + +/// A DER TLV with a short-form length (every value here is under 128 octets). +fn tlv(tag: u8, value: &[u8]) -> Result, String> { + let len = u8::try_from(value.len()).map_err(|e| e.to_string())?; + if len >= 0x80 { + return Err("long-form length not needed here".into()); + } + Ok([&[tag, len][..], value].concat()) +} + +/// A non-negative DER INTEGER with magnitude `m` (a sign octet if needed). +fn der_uint(m: &[u8]) -> Result, String> { + let needs_pad = m.first().is_some_and(|b| *b >= 0x80); + let value = if needs_pad { + [&[0u8][..], m].concat() + } else { + m.to_vec() + }; + tlv(0x02, &value) +} + +fn ecdsa_sig(r: &[u8], s: &[u8]) -> Result, String> { + tlv(0x30, &[der_uint(r)?, der_uint(s)?].concat()) +} + +fn p256_spki(point: &[u8]) -> Result, String> { + let algorithm = tlv( + 0x30, + &[ + tlv(0x06, &hex("2a8648ce3d0201")?)?, + tlv(0x06, &hex("2a8648ce3d030107")?)?, + ] + .concat(), + )?; + let key = tlv(0x03, &[&[0u8][..], point].concat())?; + tlv(0x30, &[algorithm, key].concat()) +} + +fn ed25519_spki(key: &[u8], with_null_parameters: bool) -> Result, String> { + let mut algorithm = tlv(0x06, &hex("2b6570")?)?; + if with_null_parameters { + algorithm.extend_from_slice(&[0x05, 0x00]); + } + let algorithm = tlv(0x30, &algorithm)?; + let key = tlv(0x03, &[&[0u8][..], key].concat())?; + tlv(0x30, &[algorithm, key].concat()) +} + +struct P256 { + spki: Vec, + point: Vec, + r: Vec, + s: Vec, +} + +/// RFC 6979 A.2.5: the key pair and the SHA-256 signature of "sample". +fn rfc_6979() -> Result { + let x = hex("60FED4BA255A9D31C961EB74C6356D68C049B8923B61FA6CE669622E60F29FB6")?; + let y = hex("7903FE1008B8BC99A41AE9E95628BC64F2F1B20C2D7E9F5177A3C294D4462299")?; + let point = [&[0x04u8][..], &x, &y].concat(); + Ok(P256 { + spki: p256_spki(&point)?, + point, + r: hex("EFD48B2AACB6A8FD1140DD9CD45E81D69D2C877B56AAF991C34D0EA84EAF3716")?, + s: hex("F7CB1C942D657C41D436C7A1B6E29F65F3E900DBB9AFF4064DC4AB2F843ACDA8")?, + }) +} + +#[test] +#[cfg_attr(miri, ignore = "full P-256 verifications are slow under Miri")] +fn ecdsa_p256_sha256_rfc_6979_a_2_5() -> TestResult { + let v = rfc_6979()?; + let sig = ecdsa_sig(&v.r, &v.s)?; + assert!(verify(&v.spki, ECDSA_P256_SHA256, b"sample", &sig)); + // Another message, another scheme number, a swapped r and s. + assert!(!verify(&v.spki, ECDSA_P256_SHA256, b"samplf", &sig)); + assert!(!verify(&v.spki, RSA_PSS_RSAE_SHA256, b"sample", &sig)); + assert!(!verify( + &v.spki, + ECDSA_P256_SHA256, + b"sample", + &ecdsa_sig(&v.s, &v.r)? + )); + Ok(()) +} + +#[test] +fn ecdsa_refuses_malformed_signatures() -> TestResult { + let v = rfc_6979()?; + let sig = ecdsa_sig(&v.r, &v.s)?; + // Trailing octets after the Ecdsa-Sig-Value. + let mut trailing = sig.clone(); + trailing.push(0); + assert!(!verify(&v.spki, ECDSA_P256_SHA256, b"sample", &trailing)); + // r with 33 magnitude octets (a leading 0x01 makes it too large). + let long_r = [&[0x01u8][..], &v.r].concat(); + assert!(!verify( + &v.spki, + ECDSA_P256_SHA256, + b"sample", + &ecdsa_sig(&long_r, &v.s)? + )); + // A negative r: the magnitude without its sign octet. + let negative = tlv(0x30, &[tlv(0x02, &v.r)?, der_uint(&v.s)?].concat())?; + assert!(!verify(&v.spki, ECDSA_P256_SHA256, b"sample", &negative)); + // r = 0 (libcrux checks 1 <= r < n). + assert!(!verify( + &v.spki, + ECDSA_P256_SHA256, + b"sample", + &ecdsa_sig(&[0], &v.s)? + )); + // Raw r || s instead of DER. + let raw = [v.r.clone(), v.s.clone()].concat(); + assert!(!verify(&v.spki, ECDSA_P256_SHA256, b"sample", &raw)); + Ok(()) +} + +#[test] +#[cfg_attr(miri, ignore = "P-256 point checks are slow under Miri")] +fn ecdsa_refuses_other_key_encodings() -> TestResult { + let v = rfc_6979()?; + let sig = ecdsa_sig(&v.r, &v.s)?; + // The compressed form of the same point (RFC 5480 §2.2 makes it optional). + let y_last = v.point.last().ok_or("empty point")?; + let prefix = if y_last % 2 == 0 { 0x02u8 } else { 0x03u8 }; + let x = v.point.get(1..33).ok_or("short point")?; + let compressed = p256_spki(&[&[prefix][..], x].concat())?; + assert!(!verify(&compressed, ECDSA_P256_SHA256, b"sample", &sig)); + // A point not on the curve (Y + 1). + let mut off_curve = v.point.clone(); + let last = off_curve.last_mut().ok_or("empty point")?; + *last ^= 1; + assert!(!verify( + &p256_spki(&off_curve)?, + ECDSA_P256_SHA256, + b"sample", + &sig + )); + Ok(()) +} + +#[test] +#[cfg_attr(miri, ignore = "full Ed25519 verifications are slow under Miri")] +fn ed25519_rfc_8032_tests_1_and_2() -> TestResult { + let key1 = hex("d75a980182b10ab7d54bfed3c964073a0ee172f3daa62325af021a68f707511a")?; + let sig1 = hex( + "e5564300c360ac729086e2cc806e828a84877f1eb8e5d974d873e06522490155 + 5fb8821590a33bacc61e39701cf9b46bd25bf5f0595bbe24655141438e7a100b", + )?; + let key2 = hex("3d4017c3e843895a92b70aa74d1b7ebc9c982ccf2ec4968cc0cd55f12af4660c")?; + let sig2 = hex( + "92a009a9f0d4cab8720e820b5f642540a2b27b5416503f8fb3762223ebdb69da + 085ac1e43e15996e458f3613d0f11d8c387b2eaeb4302aeeb00d291612bb0c00", + )?; + assert!(verify(&ed25519_spki(&key1, false)?, ED25519, b"", &sig1)); + assert!(verify( + &ed25519_spki(&key2, false)?, + ED25519, + &[0x72], + &sig2 + )); + // The other test's key, message or signature. + assert!(!verify( + &ed25519_spki(&key1, false)?, + ED25519, + &[0x72], + &sig2 + )); + assert!(!verify( + &ed25519_spki(&key2, false)?, + ED25519, + &[0x73], + &sig2 + )); + let mut tampered = sig1.clone(); + let first = tampered.first_mut().ok_or("empty signature")?; + *first ^= 1; + assert!(!verify( + &ed25519_spki(&key1, false)?, + ED25519, + b"", + &tampered + )); + // RFC 8410 §3: parameters must be absent. + assert!(!verify(&ed25519_spki(&key1, true)?, ED25519, b"", &sig1)); + // A signature of the wrong length, and the wrong scheme. + assert!(!verify( + &ed25519_spki(&key1, false)?, + ED25519, + b"", + sig1.get(..63).ok_or("short")? + )); + assert!(!verify( + &ed25519_spki(&key1, false)?, + ECDSA_P256_SHA256, + b"", + &sig1 + )); + Ok(()) +} + +/// The canonical encodings of edwards25519's eight points of order dividing +/// 8, computed independently from RFC 8032 §5.1's curve: each y below with +/// the x sign bit clear and, where x != 0, set. +const SMALL_ORDER_KEYS: [&str; 8] = [ + "0100000000000000000000000000000000000000000000000000000000000000", + "ecffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff7f", + "0000000000000000000000000000000000000000000000000000000000000000", + "0000000000000000000000000000000000000000000000000000000000000080", + "26e8958fc2b227b045c3f489f2ef98f0d5dfac05d3c63339b13802886d53fc05", + "26e8958fc2b227b045c3f489f2ef98f0d5dfac05d3c63339b13802886d53fc85", + "c7176a703d4dd84fba3c0b760d10670f2a2053fa2c39ccc64ec7fd7792ac037a", + "c7176a703d4dd84fba3c0b760d10670f2a2053fa2c39ccc64ec7fd7792ac03fa", +]; + +#[test] +#[cfg_attr(miri, ignore = "full Ed25519 verifications are slow under Miri")] +fn ed25519_refuses_small_order_keys() -> TestResult { + // Under the identity key, R = identity and S = 0 satisfy RFC 8032 + // §5.1.7's check for every message: libcrux alone accepts them, the + // signature check refuses them. + let identity = hex(SMALL_ORDER_KEYS.first().ok_or("table")?)?; + let forged = hex(&format!("01{}", "00".repeat(63)))?; + for message in [&b""[..], b"any message", &[0x72]] { + assert!(clazel_crypto::axioms::ed25519_verify( + message, &identity, &forged + )); + assert!(!verify( + &ed25519_spki(&identity, false)?, + ED25519, + message, + &forged + )); + } + for key in SMALL_ORDER_KEYS { + let key = hex(key)?; + assert!(!verify(&ed25519_spki(&key, false)?, ED25519, b"", &forged)); + } + Ok(()) +} + +fn fixture(name: &str) -> Result, String> { + let path = format!( + "{}/tests/fixtures/rsa-pss/{name}", + env!("CARGO_MANIFEST_DIR") + ); + std::fs::read(&path).map_err(|e| format!("{path}: {e}")) +} + +#[test] +#[cfg_attr(miri, ignore = "reads fixtures; RSA-2048 is slow under Miri")] +fn rsa_pss_rsae_sha256_384_512() -> TestResult { + let key = fixture("k2048.spki.der")?; + let message = fixture("msg.bin")?; + let sig256 = fixture("k2048.sha256.sig")?; + let sig384 = fixture("k2048.sha384.sig")?; + let sig512 = fixture("k2048.sha512.sig")?; + assert!(verify(&key, RSA_PSS_RSAE_SHA256, &message, &sig256)); + assert!(verify(&key, RSA_PSS_RSAE_SHA384, &message, &sig384)); + assert!(verify(&key, RSA_PSS_RSAE_SHA512, &message, &sig512)); + // Each signature under another hash's scheme. + assert!(!verify(&key, RSA_PSS_RSAE_SHA384, &message, &sig256)); + assert!(!verify(&key, RSA_PSS_RSAE_SHA256, &message, &sig512)); + // Another message, a flipped bit, a truncated signature. + assert!(!verify( + &key, + RSA_PSS_RSAE_SHA256, + b"another message", + &sig256 + )); + let mut tampered = sig256.clone(); + let last = tampered.last_mut().ok_or("empty signature")?; + *last ^= 1; + assert!(!verify(&key, RSA_PSS_RSAE_SHA256, &message, &tampered)); + assert!(!verify( + &key, + RSA_PSS_RSAE_SHA256, + &message, + sig256.get(1..).ok_or("short")? + )); + // rsa_pss_pss_* is not offered and never verified. + assert!(!verify(&key, RSA_PSS_PSS_SHA256, &message, &sig256)); + Ok(()) +} + +#[test] +#[cfg_attr(miri, ignore = "reads fixtures from disk")] +fn rsa_refuses_keys_outside_the_profile() -> TestResult { + let message = fixture("msg.bin")?; + // e = 3: refused, never verified with another exponent. + assert!(!verify( + &fixture("ke3.spki.der")?, + RSA_PSS_RSAE_SHA256, + &message, + &fixture("ke3.sha256.sig")? + )); + // A 2047-bit modulus. + assert!(!verify( + &fixture("k2047.spki.der")?, + RSA_PSS_RSAE_SHA256, + &message, + &fixture("k2047.sha256.sig")? + )); + Ok(()) +} + +#[test] +fn garbage_keys_and_unknown_schemes_are_refused() -> TestResult { + let v = rfc_6979()?; + let sig = ecdsa_sig(&v.r, &v.s)?; + assert!(!verify(&[], ECDSA_P256_SHA256, b"sample", &sig)); + assert!(!verify( + v.spki.get(1..).ok_or("short spki")?, + ECDSA_P256_SHA256, + b"sample", + &sig + )); + for scheme in [0x0000u16, 0x0401, 0x0503, 0x0808, 0x0809, 0xffff] { + assert!( + !verify(&v.spki, scheme, b"sample", &sig), + "scheme {scheme:#06x}" + ); + } + Ok(()) +} diff --git a/crates/clazel-tls/src/auth/exec.rs b/crates/clazel-tls/src/auth/exec.rs index 76286b0..57ff74b 100644 --- a/crates/clazel-tls/src/auth/exec.rs +++ b/crates/clazel-tls/src/auth/exec.rs @@ -170,7 +170,7 @@ pub fn signature_scheme(scheme: u16) -> (out: bool) ensures out == super::spec::signature_scheme(scheme), { scheme == 0x0403 || scheme == 0x0804 || scheme == 0x0805 || scheme == 0x0806 - || scheme == 0x0807 || scheme == 0x0809 || scheme == 0x080a || scheme == 0x080b + || scheme == 0x0807 } /// RFC 8446 §4.2: every parsed server response answers an actual offer. pub fn extensions_offered(es: &[Extension<'_>], offers: &[u16]) -> (out: bool) diff --git a/crates/clazel-tls/src/auth/spec.rs b/crates/clazel-tls/src/auth/spec.rs index a8cb33f..c33ea5d 100644 --- a/crates/clazel-tls/src/auth/spec.rs +++ b/crates/clazel-tls/src/auth/spec.rs @@ -165,10 +165,12 @@ pub open spec fn profile_extensions(es: Seq) -> bool es.len() == 0 || ((es[0] == 0 || es[0] == 10 || es[0] == 13 || es[0] == 43 || es[0] == 44 || es[0] == 50 || es[0] == 51) && profile_extensions(es.skip(1))) } -/// §4.4.3: permitted TLS 1.3 schemes in the selected library profile. +/// §4.4.3: permitted TLS 1.3 schemes in the selected library profile: +/// ecdsa_secp256r1_sha256, rsa_pss_rsae_sha256/384/512 and ed25519. The +/// rsa_pss_pss_* schemes are not offered (see hello::client_spec). pub open spec fn signature_scheme(scheme: u16) -> bool { scheme == 0x0403 || scheme == 0x0804 || scheme == 0x0805 || scheme == 0x0806 - || scheme == 0x0807 || scheme == 0x0809 || scheme == 0x080a || scheme == 0x080b + || scheme == 0x0807 } /// §4.2: EE responses must have been offered. Placement/body rules are parsed first. pub open spec fn extensions_offered(es: Seq, offers: Seq) -> bool diff --git a/crates/clazel-tls/src/hello/client.rs b/crates/clazel-tls/src/hello/client.rs index 0d84e9b..5513f61 100644 --- a/crates/clazel-tls/src/hello/client.rs +++ b/crates/clazel-tls/src/hello/client.rs @@ -33,7 +33,7 @@ pub fn signatures() -> (out: Vec) ensures out@ == super::client_spec::signatures(), { let out = vec![0x0403u16, 0x0804u16, 0x0805u16, 0x0806u16, 0x0807u16, - 0x0809u16, 0x080au16, 0x080bu16, 0x0401u16, 0x0501u16, 0x0601u16]; + 0x0401u16, 0x0501u16, 0x0601u16]; proof { assert(out@ =~= super::client_spec::signatures()); } out } diff --git a/crates/clazel-tls/src/hello/client_lemmas.rs b/crates/clazel-tls/src/hello/client_lemmas.rs index f27ab4b..3145511 100644 --- a/crates/clazel-tls/src/hello/client_lemmas.rs +++ b/crates/clazel-tls/src/hello/client_lemmas.rs @@ -87,11 +87,11 @@ pub proof fn lemma_profile(c: super::client_spec::Config, cookie: Seq) lemma_vec_len(c.public_key, 65535); lemma_vec_len(crate::spec::write_key_share(crate::spec::KeyShare { group: 29, key_exchange: c.public_key }), 65535); assert(key.len() == 38); - assert(crate::spec::write_signature_schemes(super::client_spec::signatures()).len() == 24) by (compute_only); + assert(crate::spec::write_signature_schemes(super::client_spec::signatures()).len() == 18) by (compute_only); let es = super::client_spec::extensions(c, cookie); reveal_with_fuel(extension_len, 8); lemma_extensions_len(es); - assert(extension_len(es) == 85 + (if c.send_sni { c.host.len() + 9 } else { 0 }) + assert(extension_len(es) == 79 + (if c.send_sni { c.host.len() + 9 } else { 0 }) + (if cookie.len() == 0 { 0 } else { cookie.len() + 4 })); assert forall|i: int| 0 <= i < es.len() implies (#[trigger] es[i]).data.len() <= 65535 by { if c.send_sni { if i == 0 {} else if i == 1 {} else if i == 2 {} else if i == 3 {} else if i == 4 {} } diff --git a/crates/clazel-tls/src/hello/client_spec.rs b/crates/clazel-tls/src/hello/client_spec.rs index a6a9e07..854cffc 100644 --- a/crates/clazel-tls/src/hello/client_spec.rs +++ b/crates/clazel-tls/src/hello/client_spec.rs @@ -15,6 +15,9 @@ //! The record driver must implement Appendix D.4's dummy CCS rules later. //! - Signature schemes include TLS 1.3 schemes and RSA PKCS#1 for certificate //! signatures only. The auth machine already excludes PKCS#1 in CV. +//! rsa_pss_pss_* (0x0809-0x080b, certificates with an RSASSA-PSS key) are +//! not offered: verifying them needs an RFC 4055 RSASSA-PSS-params parser, +//! and we offer only what the signature verifier accepts. //! - HRR cookie extension_data is capped at 4098 bytes (4096-byte cookie), //! a resource policy, so ClientHello2's extension vector stays representable. //! - The controller is consumed on receive. A fatal error discards it; @@ -52,7 +55,7 @@ pub open spec fn config_ok(c: Config) -> bool { /// §4.2.3: schemes offered for CV and certificate signatures. pub open spec fn signatures() -> Seq { seq![0x0403u16, 0x0804u16, 0x0805u16, 0x0806u16, 0x0807u16, - 0x0809u16, 0x080au16, 0x080bu16, 0x0401u16, 0x0501u16, 0x0601u16] + 0x0401u16, 0x0501u16, 0x0601u16] } /// §4.2.2: an absent initial cookie or a structurally valid bounded retry cookie. pub open spec fn cookie_ok(cookie: Seq) -> bool { diff --git a/crates/clazel-tls/tests/hello_client.rs b/crates/clazel-tls/tests/hello_client.rs index 55d08cb..420a6db 100644 --- a/crates/clazel-tls/tests/hello_client.rs +++ b/crates/clazel-tls/tests/hello_client.rs @@ -344,10 +344,10 @@ fn expected_sni(host: &[u8]) -> Vec { fn expected_signatures() -> Vec { let schemes = [ - 0x0403u16, 0x0804, 0x0805, 0x0806, 0x0807, 0x0809, 0x080a, 0x080b, 0x0401, 0x0501, 0x0601, + 0x0403u16, 0x0804, 0x0805, 0x0806, 0x0807, 0x0401, 0x0501, 0x0601, ]; let mut data = Vec::new(); - data.extend_from_slice(&22u16.to_be_bytes()); + data.extend_from_slice(&16u16.to_be_bytes()); for scheme in schemes { data.extend_from_slice(&scheme.to_be_bytes()); } diff --git a/crates/clazel-x509/src/spki/exec.rs b/crates/clazel-x509/src/spki/exec.rs index 1c2e302..527d596 100644 --- a/crates/clazel-x509/src/spki/exec.rs +++ b/crates/clazel-x509/src/spki/exec.rs @@ -104,7 +104,7 @@ pub struct RsaPublicKey<'a> { impl View for RsaPublicKey<'_> { type V = super::spec::RsaPublicKey; - closed spec fn view(&self) -> Self::V { + open spec fn view(&self) -> Self::V { Self::V { encoded_der: self.encoded_der@, modulus_der: self.modulus_der@, @@ -125,7 +125,7 @@ pub enum PublicKey<'a> { impl View for PublicKey<'_> { type V = super::spec::PublicKey; - closed spec fn view(&self) -> Self::V { + open spec fn view(&self) -> Self::V { match self { PublicKey::Rsa(key) => super::spec::PublicKey::Rsa(key@), PublicKey::Unsupported => super::spec::PublicKey::Unsupported, @@ -151,7 +151,7 @@ pub struct SubjectPublicKeyInfo<'a> { impl View for SubjectPublicKeyInfo<'_> { type V = super::spec::SubjectPublicKeyInfo; - closed spec fn view(&self) -> Self::V { + open spec fn view(&self) -> Self::V { Self::V { algorithm: crate::certificate::contract::view_algorithm_identifier(&self.algorithm), public_key: self.public_key@, diff --git a/docs/DEPENDENCIES.md b/docs/DEPENDENCIES.md index b35ca03..fed5623 100644 --- a/docs/DEPENDENCIES.md +++ b/docs/DEPENDENCIES.md @@ -130,6 +130,10 @@ Changing a row is a reviewable act. Adding one means saying why below. | const-oid | 0.10.2 | test | `der`'s OBJECT IDENTIFIER type (the `oid` feature). No dependencies with default features off. | | libcrux-chacha20poly1305 | 0.0.10 | shipped | libcrux, badge `verified-hacl` (safe Rust from proven HACL* code), no `unsafe`. ChaCha20-Poly1305 (RFC 8439): the record AEAD (`traffic::provider::Factory`). Used by `clazel-crypto` (src/axioms.rs). | | libcrux-curve25519 | 0.0.9 | shipped | libcrux, badge `verified-hacl` (safe Rust from proven HACL* code), no `unsafe`. X25519 (RFC 7748): `hello::key_exchange::KeyExchange`. Used by `clazel-crypto` (src/axioms.rs). | +| libcrux-ecdsa | 0.0.9 | shipped | libcrux, badge `verified-hacl` (safe Rust from proven HACL* code), no `unsafe`. ECDSA P-256 with SHA-256 (FIPS 186-5): `ecdsa_secp256r1_sha256` CertificateVerify signatures. Only `p256::verify` with raw r, s and the point coordinates X and Y is called; its DER signature helpers are not (we parse Ecdsa-Sig-Value with `clazel-der`, CLAUDE.md rule 8). Default features off, so `rand` is not reached. Used by `clazel-crypto` (src/axioms.rs). | +| libcrux-p256 | 0.0.9 | shipped | libcrux, badge `verified-hacl`, no `unsafe`. The P-256 field and point arithmetic and HACL's `ecdsa_verif_p256_sha2`, required by `libcrux-ecdsa`. | +| libcrux-rsa | 0.0.9 | shipped | libcrux, badge `verified-hacl`, no `unsafe`. RSASSA-PSS verification (RFC 8017 §8.1.2) with the public exponent fixed to 65537: `rsa_pss_rsae_sha256/384/512` CertificateVerify signatures. It has no PKCS#1 v1.5, which `clazel-pkcs1` provides. Used by `clazel-crypto` (src/axioms.rs). | +| libcrux-ed25519 | 0.0.10 | shipped | libcrux, badge `verified-hacl`, no `unsafe`. Ed25519 verification (RFC 8032 §5.1.7): `ed25519` CertificateVerify signatures. Its optional `rand_core` and `tls_codec` are not enabled. Used by `clazel-crypto` (src/axioms.rs). | | libcrux-hacl-rs | 0.0.6 | shipped | Support crate of libcrux: The F*/Low* runtime support every HACL-derived libcrux crate links (bignum, fstar and lowstar shims). Badge `pre-verification`; no compiled `unsafe` (the one `mem::zeroed` in `util/memzero0.rs` is commented out, which also makes its `memzero` a no-op: HACL's zeroisation of temporaries does not happen). | | libcrux-hkdf | 0.0.9 | shipped | libcrux, badge `verified-hacl` (safe Rust from proven HACL* code), no `unsafe`. HKDF-SHA256 (RFC 5869): `Crypto::extract` and `Crypto::expand`. Used by `clazel-crypto` (src/axioms.rs). | | libcrux-hmac | 0.0.9 | shipped | libcrux, badge `verified-hacl` (safe Rust from proven HACL* code), no `unsafe`. HMAC-SHA256 (RFC 2104): `Crypto::hmac`. Its non-optional `libcrux-sha3` dependency is for HMAC-SHA3 types we never use (see `libcrux-sha3`). Used by `clazel-crypto` (src/axioms.rs). |