diff --git a/Cargo.lock b/Cargo.lock index bfa58ef..6c7e15e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,12 +2,47 @@ # It is not intended for manual editing. version = 4 +[[package]] +name = "aho-corasick" +version = "1.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c982642fa9e8606056828ee9a8505737230110bb1099153c79efe865c59d12ba" +dependencies = [ + "memchr", +] + +[[package]] +name = "autocfg" +version = "1.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53" + [[package]] name = "base64" version = "0.22.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "72b3254f16251a8381aa12e40e3c4d2f0199f8c6508fbecb9d91f575e0fbb8c6" +[[package]] +name = "bindgen" +version = "0.72.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "993776b509cfb49c750f11b8f07a46fa23e0a1386ffc01fb1e7d343efc387895" +dependencies = [ + "bitflags", + "cexpr", + "clang-sys", + "itertools", + "log", + "prettyplease", + "proc-macro2", + "quote", + "regex", + "rustc-hash", + "shlex 1.3.0", + "syn 2.0.119", +] + [[package]] name = "bitflags" version = "2.13.2" @@ -23,6 +58,12 @@ dependencies = [ "generic-array", ] +[[package]] +name = "bumpalo" +version = "3.20.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72f5acc6cb2ba439de613abc23857ec3d78374d8ed5ac84e9d11336e87da8649" + [[package]] name = "cc" version = "1.10.0" @@ -30,7 +71,16 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "86e055fa6e3e40ad6187ba25b6855eeb635d5271f8e0f0e1e9a5826b8d75bea0" dependencies = [ "find-msvc-tools", - "shlex", + "shlex 2.0.1", +] + +[[package]] +name = "cexpr" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6fac387a98bb7c37292057cffc56d62ecb629900026402633ae9160df93a8766" +dependencies = [ + "nom", ] [[package]] @@ -39,6 +89,28 @@ version = "1.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4e7648175b45a9a48536d676f68d918270699102aa8dab5496df06904c914600" +[[package]] +name = "chacha20" +version = "0.10.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "65c35e4b699c7e15ccbe7ee35c005e4fc0a278d22238a2857e6ce2dadeda1b06" +dependencies = [ + "cfg-if", + "cpufeatures 0.3.1", + "rand_core", +] + +[[package]] +name = "clang-sys" +version = "1.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "157a8ba7b480713b56f4c09fd13fc3e0a22a5dfab8097ba61cbc5feef950788a" +dependencies = [ + "glob", + "libc", + "libloading", +] + [[package]] name = "clazel" version = "0.0.0" @@ -73,6 +145,19 @@ dependencies = [ "vstd", ] +[[package]] +name = "clazel-crypto" +version = "0.0.0" +dependencies = [ + "clazel-tls", + "libcrux-chacha20poly1305", + "libcrux-curve25519", + "libcrux-hkdf", + "libcrux-hmac", + "libcrux-sha2", + "vstd", +] + [[package]] name = "clazel-der" version = "0.0.0" @@ -300,6 +385,17 @@ dependencies = [ "url", ] +[[package]] +name = "core-models" +version = "0.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ee3344d349528f449816cfa85e558c439bdca5a6d8a738cfb21e69f0b2b1952f" +dependencies = [ + "hax-lib 0.3.7", + "pastey", + "rand", +] + [[package]] name = "cpufeatures" version = "0.2.17" @@ -309,6 +405,27 @@ dependencies = [ "libc", ] +[[package]] +name = "cpufeatures" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5ca28b0ae3115b884660db4118d803791fd6756b6e88f39c0f3f7859060d7566" +dependencies = [ + "libc", +] + +[[package]] +name = "crabgrind" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "035c801dc4b418e1d857a6536dc88b4d1929c7a1fd163389766e18d322d34a84" +dependencies = [ + "bindgen", + "cc", + "pkg-config", + "rustversion", +] + [[package]] name = "crypto-common" version = "0.1.7" @@ -348,6 +465,12 @@ dependencies = [ "litrs", ] +[[package]] +name = "either" +version = "1.19.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0e9c71c2167ca323c882b99918929403426e2373ea17242ff5653e0d5e1058be" + [[package]] name = "encoding_rs" version = "0.8.35" @@ -378,6 +501,30 @@ dependencies = [ "percent-encoding", ] +[[package]] +name = "futures-core" +version = "0.3.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "92d699e522242e69e3003b94ecc1f960f3a5e015aa7c5d7486e65ad01dd94f5e" + +[[package]] +name = "futures-task" +version = "0.3.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cd417de3d1d015fc3bfd2b1ea46dfc7bab72ef86f1cc7cc9c78e728b34a6d1fd" + +[[package]] +name = "futures-util" +version = "0.3.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0d50a92467f8ba5dd6e3ee5d4bd04d73ab2e4e1c44474a0674821dfce14b79bc" +dependencies = [ + "futures-core", + "futures-task", + "pin-project-lite", + "slab", +] + [[package]] name = "generic-array" version = "0.14.7" @@ -399,12 +546,103 @@ dependencies = [ "wasi", ] +[[package]] +name = "getrandom" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "300e883d756b2e4ec94e02791f39b04b522276138852cfc41d9fb7e904106099" +dependencies = [ + "cfg-if", + "libc", + "r-efi", + "rand_core", +] + +[[package]] +name = "glob" +version = "0.3.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e4eba85ea1d0a966a983acd07deee566e67395d2d96b6fb39e62b5a833f1eb0b" + [[package]] name = "hashbrown" version = "0.17.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a" +[[package]] +name = "hax-lib" +version = "0.3.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "01a33cb227f97ee5c419064c31d7c55a7d895f28d8019ccdadc311cc036500c4" +dependencies = [ + "hax-lib-macros 0.3.7", + "num-bigint", + "num-traits", +] + +[[package]] +name = "hax-lib" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fb3bfcfc915e894c331662e4ac76706b777a5956535ea24535f4df30da04b1bf" +dependencies = [ + "hax-lib-macros 0.4.2", + "num-bigint", + "num-traits", +] + +[[package]] +name = "hax-lib-macros" +version = "0.3.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "28da835a5f153e9f3d0cc1f42ee605a1cfa9093c93348193793d60a1b0908b51" +dependencies = [ + "hax-lib-macros-types 0.3.7", + "proc-macro-error2", + "proc-macro2", + "quote", + "syn 2.0.119", +] + +[[package]] +name = "hax-lib-macros" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6e9010990fcba1d1494047fa433a433be0a5df23653a9784c739f7bba270272e" +dependencies = [ + "hax-lib-macros-types 0.4.2", + "proc-macro2", + "quote", + "syn 2.0.119", +] + +[[package]] +name = "hax-lib-macros-types" +version = "0.3.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eed327e9a28d6ee018a4a9ba842d4ee27e378c8a591d2beb6f42f32b24a02fcb" +dependencies = [ + "proc-macro2", + "quote", + "serde", + "serde_json", + "uuid", +] + +[[package]] +name = "hax-lib-macros-types" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e053e3a5aeb92df47b07323180c5088edc488ca49883a234f6c73255c54cc520" +dependencies = [ + "proc-macro2", + "quote", + "serde", + "serde_json", + "uuid", +] + [[package]] name = "httparse" version = "1.10.1" @@ -458,18 +696,188 @@ version = "0.19.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a588916bfdfd92e71cacef98a63d9b1f0d74d6599980d11894290e7ddefffcf7" +[[package]] +name = "itertools" +version = "0.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186" +dependencies = [ + "either", +] + [[package]] name = "itoa" version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" +[[package]] +name = "js-sys" +version = "0.3.106" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7883d941dae510fb2d978fc3fe018c71c9e2892fd38854de3e8b92c2e5ad9cc5" +dependencies = [ + "cfg-if", + "futures-util", + "wasm-bindgen", +] + [[package]] name = "libc" version = "0.2.190" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ce5d3ddc6d3fa000eb1536d85e147bfe31aacaba692ed6a876f95cb7c855be78" +[[package]] +name = "libcrux-chacha20poly1305" +version = "0.0.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2ae27cbc4917bfd7759d7db19ea6dcf0279f195431942b59ff113aa34a2140a3" +dependencies = [ + "libcrux-hacl-rs", + "libcrux-macros", + "libcrux-poly1305", + "libcrux-secrets", + "libcrux-traits", +] + +[[package]] +name = "libcrux-curve25519" +version = "0.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5e78d0f36b23bcf258792dcc3a948fc628cb195950afa7b9a954250714688cfd" +dependencies = [ + "libcrux-hacl-rs", + "libcrux-macros", + "libcrux-secrets", + "libcrux-traits", +] + +[[package]] +name = "libcrux-hacl-rs" +version = "0.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "27ce64ead37fc67c1039fdbcf1e8c97044e6a644cb3d1f79060b5c9ac8fdfe0a" +dependencies = [ + "libcrux-macros", +] + +[[package]] +name = "libcrux-hkdf" +version = "0.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5d061b72fb31bcb77940e379b3df170389c5f372a604f755c097fac9a870cc43" +dependencies = [ + "libcrux-hacl-rs", + "libcrux-hmac", + "libcrux-secrets", +] + +[[package]] +name = "libcrux-hmac" +version = "0.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1b454775ca55f79559f4dbc03b9896d46d929f11041d1c71c14501f0c1b97d75" +dependencies = [ + "libcrux-hacl-rs", + "libcrux-macros", + "libcrux-sha2", + "libcrux-sha3", + "libcrux-traits", +] + +[[package]] +name = "libcrux-intrinsics" +version = "0.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "de82722c9c7419a311e84ee902e9643a15e39a6fcaade87f21e94f8d0f30fa70" +dependencies = [ + "core-models", + "hax-lib 0.4.2", +] + +[[package]] +name = "libcrux-macros" +version = "0.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2afdd4da30d6e23f76bd6f3ad61be5c773720349eef3e791f8b79cfea3fe1436" +dependencies = [ + "quote", + "syn 3.0.9", +] + +[[package]] +name = "libcrux-platform" +version = "0.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8bf8bee8c35d34867a3762d6ee7b74e8523a882855c3cfce30484e9554342206" +dependencies = [ + "libc", +] + +[[package]] +name = "libcrux-poly1305" +version = "0.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d727ee28ee0d5d2661daa5f2f47965cd3489a0ac9130f3410e95632a98b12e49" +dependencies = [ + "libcrux-hacl-rs", + "libcrux-macros", +] + +[[package]] +name = "libcrux-secrets" +version = "0.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "03c4ba47b3596f2771213ff162c792e9b93ddc0cdd178a2e407e00bb8ae4afcd" +dependencies = [ + "crabgrind", + "hax-lib 0.4.2", +] + +[[package]] +name = "libcrux-sha2" +version = "0.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "86aa35d8fc9576a41df34af4d95d1f11186c1f65cd6c829329748915ea556d71" +dependencies = [ + "libcrux-hacl-rs", + "libcrux-macros", + "libcrux-traits", +] + +[[package]] +name = "libcrux-sha3" +version = "0.0.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2c8117e86e1f03417d8ebe50ed298c6ee0b05557783a75697d0c59a2ef2dcfc6" +dependencies = [ + "hax-lib 0.4.2", + "libcrux-intrinsics", + "libcrux-platform", + "libcrux-traits", +] + +[[package]] +name = "libcrux-traits" +version = "0.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8958bb5c3780eb7c3355aeeb051629b830e47bfefd36befed93c81b53366bbc4" +dependencies = [ + "libcrux-secrets", + "rand", +] + +[[package]] +name = "libloading" +version = "0.8.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d7c4b02199fee7c5d21a5ae7d8cfa79a6ef5bb2fc834d6e9058e89c825efdc55" +dependencies = [ + "cfg-if", + "windows-link", +] + [[package]] name = "litrs" version = "1.0.1" @@ -500,18 +908,112 @@ version = "2.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e7244eafd1e09e7c4e33043881997aa6ab6dffff3ed2cee3395a278980481d6e" +[[package]] +name = "minimal-lexical" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" + +[[package]] +name = "nom" +version = "7.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a" +dependencies = [ + "memchr", + "minimal-lexical", +] + +[[package]] +name = "num-bigint" +version = "0.4.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c89e69e7e0f03bea5ef08013795c25018e101932225a656383bd384495ecc367" +dependencies = [ + "num-integer", + "num-traits", +] + +[[package]] +name = "num-integer" +version = "0.1.47" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7ce2d95d4b3734dc35aa2f45e1aa22cd416814592a4f9d9205e11affd5b8e10b" +dependencies = [ + "num-traits", +] + +[[package]] +name = "num-traits" +version = "0.2.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841" +dependencies = [ + "autocfg", +] + [[package]] name = "once_cell" version = "1.21.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9f7c3e4beb33f85d45ae3e3a1792185706c8e16d043238c593331cc7cd313b50" +[[package]] +name = "pastey" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2ee67f1008b1ba2321834326597b8e186293b049a023cdef258527550b9935b4" + [[package]] name = "percent-encoding" version = "2.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9b4f627cb1b25917193a259e49bdad08f671f8d9708acfd5fe0a8c1455d87220" +[[package]] +name = "pin-project-lite" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd" + +[[package]] +name = "pkg-config" +version = "0.3.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f6b464fbc74e149a392436b17d523f769e057cb6877f6a5c4618bc6f11800548" + +[[package]] +name = "prettyplease" +version = "0.2.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "479ca8adacdd7ce8f1fb39ce9ecccbfe93a3f1344b3d0d97f20bc0196208f62b" +dependencies = [ + "proc-macro2", + "syn 2.0.119", +] + +[[package]] +name = "proc-macro-error-attr2" +version = "2.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "96de42df36bb9bba5542fe9f1a054b8cc87e172759a1868aa05c1f3acc89dfc5" +dependencies = [ + "proc-macro2", + "quote", +] + +[[package]] +name = "proc-macro-error2" +version = "2.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "11ec05c52be0a07b08061f7dd003e7d7092e0472bc731b4af7bb1ef876109802" +dependencies = [ + "proc-macro-error-attr2", + "proc-macro2", + "quote", + "syn 2.0.119", +] + [[package]] name = "proc-macro2" version = "1.0.107" @@ -545,6 +1047,58 @@ dependencies = [ "proc-macro2", ] +[[package]] +name = "r-efi" +version = "6.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf" + +[[package]] +name = "rand" +version = "0.10.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "65c9fb96cbc91e3478eaae79a69fcd3f1ae4ad052e471fe6732fff548984b4af" +dependencies = [ + "chacha20", + "getrandom 0.4.3", + "rand_core", +] + +[[package]] +name = "rand_core" +version = "0.10.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "63b8176103e19a2643978565ca18b50549f6101881c443590420e4dc998a3c69" + +[[package]] +name = "regex" +version = "1.13.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f020237b6c8eed93db2e2cb53c00c60a8e1bc73da7d073199a1180401450218d" +dependencies = [ + "aho-corasick", + "memchr", + "regex-automata", + "regex-syntax", +] + +[[package]] +name = "regex-automata" +version = "0.4.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ad8553b9b26413251cbf30e620595c7a41b3887f03da04579c0e6b0d6a06b4b2" +dependencies = [ + "aho-corasick", + "memchr", + "regex-syntax", +] + +[[package]] +name = "regex-syntax" +version = "0.8.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d6f6ff9a378485b298a5286656da665ba74413d36db0979633275d2e708145d4" + [[package]] name = "ring" version = "0.17.14" @@ -553,12 +1107,18 @@ checksum = "a4689e6c2294d81e88dc6261c768b63bc4fcdb852be6d1352498b114f61383b7" dependencies = [ "cc", "cfg-if", - "getrandom", + "getrandom 0.2.17", "libc", "untrusted", "windows-sys", ] +[[package]] +name = "rustc-hash" +version = "2.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6b1e7f9a428571be2dc5bc0505c13fb6bf936822b894ec87abf8a08a4e51742d" + [[package]] name = "rustls" version = "0.23.46" @@ -592,6 +1152,12 @@ dependencies = [ "untrusted", ] +[[package]] +name = "rustversion" +version = "1.0.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf54715a573b99ac80df0bc206da022bcd442c974952c7b9720069370852e21f" + [[package]] name = "serde" version = "1.0.229" @@ -599,6 +1165,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4148590afebada386688f18773da617792bf2ef03ffc1e4cbd2b1d45b023e0ba" dependencies = [ "serde_core", + "serde_derive", ] [[package]] @@ -641,10 +1208,16 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a7507d819769d01a365ab707794a4084392c824f54a7a6a7862f8c3d0892b283" dependencies = [ "cfg-if", - "cpufeatures", + "cpufeatures 0.2.17", "digest", ] +[[package]] +name = "shlex" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" + [[package]] name = "shlex" version = "2.0.1" @@ -660,6 +1233,12 @@ dependencies = [ "bitflags", ] +[[package]] +name = "slab" +version = "0.4.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0c790de23124f9ab44544d7ac05d60440adc586479ce501c1d6d7da3cd8c9cf5" + [[package]] name = "smallvec" version = "1.16.3" @@ -795,6 +1374,17 @@ version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b6c140620e7ffbb22c2dee59cafe6084a59b5ffc27a8859a5f0d494b5d52b6be" +[[package]] +name = "uuid" +version = "1.29.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4a0e2d11620c50695fe12bbbfde96b3477fe606e7284c22d505c12ce51214514" +dependencies = [ + "getrandom 0.4.3", + "js-sys", + "wasm-bindgen", +] + [[package]] name = "version_check" version = "0.9.5" @@ -872,6 +1462,57 @@ version = "0.11.1+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b" +[[package]] +name = "wasm-bindgen" +version = "0.2.129" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9bb54f33acc68fd454578d9820b0bde1a1a3d17aa17bb7b6595806d02886d409" +dependencies = [ + "cfg-if", + "once_cell", + "rustversion", + "wasm-bindgen-macro", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-macro" +version = "0.2.129" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2e29d0c35b16e224a7eeb5cd2d25e3e1968fbd65604117b44d3b789d00ee8535" +dependencies = [ + "quote", + "wasm-bindgen-macro-support", +] + +[[package]] +name = "wasm-bindgen-macro-support" +version = "0.2.129" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f501a8bc3719dba86ef8ae4728879c08001bea749eb1333ac5b91e040e2a6b7" +dependencies = [ + "bumpalo", + "proc-macro2", + "quote", + "syn 3.0.9", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-shared" +version = "0.2.129" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "23f0c9c52aa7cd7d77769a4cfe2a9adb1b331f489a41d912ce14513d5ab995c6" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "windows-link" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" + [[package]] name = "windows-sys" version = "0.52.0" diff --git a/README.md b/README.md index 974678e..5b85843 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ A web browser built from the bottom up by AI, using formal verification instead of trust. -- **Memory safe:** 100% safe Rust except `clazel-sys`: 14 `unsafe` blocks (20 lines) that enter the OS sandbox, machine-checked and audited. +- **Memory safe:** 100% safe Rust except `clazel-sys`: 14 `unsafe` blocks (20 lines) that enter the OS sandbox, machine-checked and audited. Shipped dependencies are `libc` and libcrux. - **Verified where it matters:** the kernel's security policy and every parser of untrusted input carry machine-checked proofs (Verus, Kani). - **Honest about it:** each crate declares its verification tier, and the diff --git a/crates/clazel-crypto/Cargo.toml b/crates/clazel-crypto/Cargo.toml new file mode 100644 index 0000000..f6eacb2 --- /dev/null +++ b/crates/clazel-crypto/Cargo.toml @@ -0,0 +1,33 @@ +[package] +name = "clazel-crypto" +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." + +[dependencies] +clazel-tls = { path = "../clazel-tls" } +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 +# every bump is a deliberate re-pin. Every call into these crates is one +# axiom in src/axioms.rs. +libcrux-sha2 = { version = "=0.0.9", default-features = false } +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 } + +# Verification tier (docs/VERIFICATION.md). The crate parses nothing; its +# adapters are checked by Verus against clazel-tls's provider contracts, and +# everything it claims about the cryptography rests on src/axioms.rs. +[package.metadata.clazel] +tier = 0 +target-tier = 0 + +[package.metadata.verus] +verify = true + +[lints] +workspace = true diff --git a/crates/clazel-crypto/README.md b/crates/clazel-crypto/README.md new file mode 100644 index 0000000..5f98f6c --- /dev/null +++ b/crates/clazel-crypto/README.md @@ -0,0 +1,55 @@ +# clazel-crypto + +The libcrux providers for `clazel-tls`'s cryptographic parameters (Phase 3 +item 3.5f). + +`clazel-tls` is proven over abstract providers: its key schedule, record +epochs and key exchange take the cryptography as trait parameters. This crate +instantiates them with [libcrux](https://github.com/cryspen/libcrux), whose +crates used here carry the `verified-hacl` badge (safe Rust compiled from +HACL\* code that is proven memory safe, functionally correct and secret +independent). Its own code is the adapters, which Verus checks against +`clazel-tls`'s provider contracts. + +| `clazel-tls` parameter | Standard | libcrux call | +|---|---|---| +| `schedule::crypto::Crypto::hash` | SHA-256, FIPS 180-4 | `libcrux_sha2::sha256` | +| `Crypto::hmac` | HMAC-SHA256, RFC 2104 | `libcrux_hmac::hmac_sha2_256` | +| `Crypto::extract` | HKDF-Extract, RFC 5869 §2.2 | `libcrux_hkdf::sha2_256::extract` | +| `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}` | + +## The trust boundary + +Every libcrux call is one axiom in `src/axioms.rs`: an `external_body` +wrapper whose `ensures` says only what libcrux documents. The output is the +uninterpreted function of `src/spec.rs` applied to exactly these inputs, +with the documented output length. There is also one proof axiom: the +ChaCha20-Poly1305 tag is 16 octets. That libcrux computes the standard's +function is HACL\*'s proof, recorded in docs/VERIFICATION.md's TCB, and is +never assumed here. A session other than the one that changed +`src/axioms.rs` reviews each change to it. + +Modelling choices: +- **Oversized inputs abort.** libcrux refuses, or panics on, inputs at or + near `u32::MAX` octets, and HACL\*'s preconditions stop just short of it. + Each wrapper checks every variable-length input against `MAX_INPUT` + (2^32 - 256 octets) first and aborts the process above it, so it never + returns a value no axiom covers and never unwinds. No caller in this + browser comes near that size. +- **X25519 refuses an all-zero result.** libcrux's `ecdh` already does this + (RFC 7748 §6.1). `clazel-tls` also checks it (RFC 8446 §7.4.2). +- **The SHA-3 crates are compiled but never called.** `libcrux-hmac` 0.0.9 + depends on `libcrux-sha3` (pre-verification) for its HMAC-SHA3 types, + which brings `libcrux-intrinsics` and `libcrux-platform`, both with + `unsafe`. The HMAC-SHA256 path calls only `libcrux-sha2`. The choice was + made on 2026-10-26; see docs/DEPENDENCIES.md. + +## 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). +- 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/src/axioms.rs b/crates/clazel-crypto/src/axioms.rs new file mode 100644 index 0000000..27c4b91 --- /dev/null +++ b/crates/clazel-crypto/src/axioms.rs @@ -0,0 +1,198 @@ +//! The trust boundary: every call into libcrux, each one axiom. +//! +//! Each wrapper is `external_body`. Verus takes its `ensures` on trust, and +//! the body is a direct call to one libcrux function with no logic beyond +//! length conversion. The `ensures` states only what libcrux documents: the +//! output is the uninterpreted function of [`crate::spec`] applied to these +//! exact inputs, with the documented output length. That libcrux computes +//! the standard's function is HACL*'s proof, recorded in the TCB +//! (docs/VERIFICATION.md), and is never assumed here. +//! +//! The libcrux functions refuse inputs longer than `u32::MAX` octets, and +//! some panic close to that bound: `libcrux-hkdf`'s expand computes its +//! buffer length with a wrapping `u32` sum, so an `info` within 33 octets of +//! `u32::MAX` makes it slice out of range. HACL*'s preconditions also stop +//! short of `u32::MAX` (for HMAC, data plus the 64-octet block). Every +//! wrapper therefore checks each variable-length input against +//! [`MAX_INPUT`] first and calls [`std::process::abort`] instead, so it +//! never returns a value no axiom covers and never unwinds. Callers in this +//! browser never come near that size: a TLS record is at most 2^14 + 256 +//! octets, and handshake messages are bounded by the reassembler. +//! +//! These axioms are counted in the README table. A session other than the +//! one that wrote them reviews every change to this file +//! (docs/phases/phase-3.md 3.5f). + +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +/// The longest input any wrapper passes to libcrux: 2^32 - 256 octets, +/// below every HACL* precondition (the tightest is HKDF-Expand's inner +/// HMAC over 32 + info + 1 octets plus its 64-octet block). +pub const MAX_INPUT: usize = 0xffff_ff00; + +/// SHA-256 of `message`. +// AXIOM: libcrux-sha2 0.0.9 `sha256(&[u8]) -> [u8; 32]` returns SHA-256 of +// its input (verified-hacl); it panics above u32::MAX, so we abort above MAX_INPUT. +#[verifier::external_body] +pub fn sha256(message: &[u8]) -> (out: Vec) + ensures out@ == crate::spec::sha256(message@), out.len() == 32, +{ + if message.len() > MAX_INPUT { + std::process::abort(); + } + libcrux_sha2::sha256(message).to_vec() +} + +/// HMAC-SHA256(key, message). +// AXIOM: libcrux-hmac 0.0.9 `hmac_sha2_256(&mut [u8; 32], key, data)` writes +// HMAC-SHA256(key, data) (verified-hacl); we abort above MAX_INPUT first. +#[verifier::external_body] +pub fn hmac_sha256(key: &[u8], message: &[u8]) -> (out: Vec) + ensures out@ == crate::spec::hmac_sha256(key@, message@), out.len() == 32, +{ + if key.len() > MAX_INPUT || message.len() > MAX_INPUT { + std::process::abort(); + } + let mut tag = [0u8; 32]; + libcrux_hmac::hmac_sha2_256(&mut tag, key, message); + tag.to_vec() +} + +/// HKDF-Extract(salt, IKM) with SHA-256. +// AXIOM: libcrux-hkdf 0.0.9 `sha2_256::extract(prk, salt, ikm)` writes the +// 32-octet HKDF-Extract PRK; errs only above u32::MAX; we abort above MAX_INPUT. +#[verifier::external_body] +pub fn hkdf_extract(salt: &[u8], ikm: &[u8]) -> (out: Vec) + ensures out@ == crate::spec::hkdf_extract(salt@, ikm@), out.len() == 32, +{ + if salt.len() > MAX_INPUT || ikm.len() > MAX_INPUT { + std::process::abort(); + } + let mut prk = [0u8; 32]; + match libcrux_hkdf::sha2_256::extract(&mut prk, salt, ikm) { + Ok(()) => prk.to_vec(), + Err(_) => std::process::abort(), + } +} + +/// HKDF-Expand(PRK, info, length) with SHA-256. +// AXIOM: libcrux-hkdf 0.0.9 `sha2_256::expand(okm, prk, info)` fills okm with +// HKDF-Expand(prk[..32], info, okm.len()); panics near u32::MAX info: abort above MAX_INPUT. +#[verifier::external_body] +pub fn hkdf_expand(prk: &[u8], info: &[u8], length: u16) -> (out: Vec) + requires prk.len() == 32, length <= 8160, + ensures out@ == crate::spec::hkdf_expand(prk@, info@, length as nat), out.len() == length, +{ + // libcrux uses only prk's first 32 octets; `requires` makes that all of it. + if info.len() > MAX_INPUT { + std::process::abort(); + } + let mut okm = vec![0u8; usize::from(length)]; + match libcrux_hkdf::sha2_256::expand(&mut okm, prk, info) { + Ok(()) => okm, + Err(_) => std::process::abort(), + } +} + +/// ChaCha20-Poly1305 encryption: ciphertext then the 16-octet tag. +// AXIOM: libcrux-chacha20poly1305 0.0.10 `encrypt(key, ptxt, ctxt, aad, nonce)` +// writes ciphertext then 16-octet tag into ctxt; errs only above u32::MAX (we: MAX_INPUT). +#[verifier::external_body] +pub fn chacha20poly1305_seal(key: &[u8], nonce: &[u8], ad: &[u8], plaintext: &[u8]) + -> (out: Vec) + requires key.len() == 32, nonce.len() == 12, + ensures out@ == crate::spec::chacha20poly1305_seal(key@, nonce@, ad@, plaintext@), +{ + let (Ok(key), Ok(nonce)) = (<&[u8; 32]>::try_from(key), <&[u8; 12]>::try_from(nonce)) else { + std::process::abort(); + }; + if ad.len() > MAX_INPUT || plaintext.len() > MAX_INPUT { + std::process::abort(); + } + let Some(length) = plaintext.len().checked_add(libcrux_chacha20poly1305::TAG_LEN) else { + std::process::abort(); + }; + let mut out = vec![0u8; length]; + match libcrux_chacha20poly1305::encrypt(key, plaintext, &mut out, ad, nonce) { + Ok(_) => out, + Err(_) => std::process::abort(), + } +} + +/// ChaCha20-Poly1305 decryption, or none when the tag does not verify. +// AXIOM: libcrux-chacha20poly1305 0.0.10 `decrypt(key, ptxt, ctxt, aad, nonce)` +// returns the plaintext iff the tag verifies, else Err (also for ctxt < 16 octets). +#[verifier::external_body] +pub fn chacha20poly1305_open(key: &[u8], nonce: &[u8], ad: &[u8], ciphertext: &[u8]) + -> (out: Option>) + requires key.len() == 32, nonce.len() == 12, + ensures match out { + Some(p) => crate::spec::chacha20poly1305_open(key@, nonce@, ad@, ciphertext@) == Some(p@), + None => crate::spec::chacha20poly1305_open(key@, nonce@, ad@, ciphertext@) is None, + }, +{ + let (Ok(key), Ok(nonce)) = (<&[u8; 32]>::try_from(key), <&[u8; 12]>::try_from(nonce)) else { + std::process::abort(); + }; + if ad.len() > MAX_INPUT || ciphertext.len() > MAX_INPUT { + std::process::abort(); + } + let mut plaintext = vec![0u8; ciphertext.len().saturating_sub(libcrux_chacha20poly1305::TAG_LEN)]; + match libcrux_chacha20poly1305::decrypt(key, &mut plaintext, ciphertext, ad, nonce) { + Ok(_) => Some(plaintext), + Err(_) => None, + } +} + +/// The sealed output is exactly 16 octets longer than the plaintext. +// AXIOM: libcrux-chacha20poly1305 0.0.10 appends exactly TAG_LEN = 16 octets +// (RFC 8439 §2.8); `encrypt`'s output split is (ptxt.len(), 16). +#[verifier::external_body] +pub proof fn axiom_chacha20poly1305_seal_len(key: Seq, nonce: Seq, ad: Seq, + plaintext: Seq) + ensures crate::spec::chacha20poly1305_seal(key, nonce, ad, plaintext).len() == plaintext.len() + 16, +{ +} + +/// X25519(private_key, 9). +// AXIOM: libcrux-curve25519 0.0.9 `secret_to_public(pk, sk)` writes +// X25519(sk, 9) (verified-hacl); both are 32-octet arrays. +#[verifier::external_body] +pub fn x25519_public(private_key: &[u8]) -> (out: Vec) + requires private_key.len() == 32, + ensures out@ == crate::spec::x25519_public(private_key@), out.len() == 32, +{ + let Ok(private_key) = <&[u8; 32]>::try_from(private_key) else { + std::process::abort(); + }; + let mut public = [0u8; 32]; + libcrux_curve25519::secret_to_public(&mut public, private_key); + public.to_vec() +} + +/// X25519(private_key, peer_key), or none for an all-zero result. +// AXIOM: libcrux-curve25519 0.0.9 `ecdh(out, pk, sk)` writes X25519(sk, pk) +// and returns Err exactly when HACL reports failure (an all-zero result). +#[verifier::external_body] +pub fn x25519_shared(private_key: &[u8], peer_key: &[u8]) -> (out: Option>) + requires private_key.len() == 32, peer_key.len() == 32, + ensures match out { + Some(s) => s.len() == 32 && crate::spec::x25519_shared(private_key@, peer_key@) == Some(s@), + None => crate::spec::x25519_shared(private_key@, peer_key@) is None, + }, +{ + let (Ok(private_key), Ok(peer_key)) = + (<&[u8; 32]>::try_from(private_key), <&[u8; 32]>::try_from(peer_key)) else { + std::process::abort(); + }; + let mut shared = [0u8; 32]; + match libcrux_curve25519::ecdh(&mut shared, peer_key, private_key) { + Ok(()) => Some(shared.to_vec()), + Err(_) => None, + } +} + +} // verus! diff --git a/crates/clazel-crypto/src/compare.rs b/crates/clazel-crypto/src/compare.rs new file mode 100644 index 0000000..2a40e37 --- /dev/null +++ b/crates/clazel-crypto/src/compare.rs @@ -0,0 +1,89 @@ +//! Timing-safe comparison of secret byte strings (RFC 8446 §4.4.4, the +//! Finished `verify_data` check; docs/phases/phase-3.md item 3.0). +//! +//! Modelling choices: +//! - **Verus proves the result, not the timing.** The contract says only +//! that [`constant_time_eq`] returns `a@ == b@`. Timing independence rests +//! on the shape of the code: one pass over every index, an OR-accumulator +//! of byte XORs, no early exit, no `break`, no branch on the data inside +//! the loop, and no data-dependent indexing. The only branch on secret +//! data is the final `acc == 0`, which is the standard construction. +//! - **The compiler is trusted not to undo that shape.** LLVM could in +//! principle turn the accumulator into an early exit. We do not use +//! `core::hint::black_box`, because its guarantee is best effort only, so +//! this module claims no more than the shape above. It makes no claim +//! about caches, speculation or the hardware. +//! - **Lengths are public.** The contract requires equal lengths; callers +//! compare fixed-size values (32 octets for SHA-256 Finished), so the +//! length never depends on a secret. +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +/// The byte at `i`, or 0 past the end. Callers keep `i < s.len()`, so the +/// fallback is unreachable; it depends on the index, never on the data. +fn byte_at(s: &[u8], i: usize) -> (out: u8) + requires + i < s.len(), + ensures + out == s@[i as int], +{ + match s.get(i) { + Some(&v) => v, + None => 0, + } +} + +/// Bitwise facts about `u8`: XOR is zero exactly on equal bytes, and an OR is +/// zero exactly when both sides are. +proof fn lemma_xor_zero(x: u8, y: u8) + ensures + (x ^ y) == 0 <==> x == y, +{ + assert((x ^ y) == 0 <==> x == y) by (bit_vector); +} + +proof fn lemma_or_zero(p: u8, q: u8) + ensures + (p | q) == 0 <==> (p == 0 && q == 0), +{ + assert((p | q) == 0 <==> (p == 0 && q == 0)) by (bit_vector); +} + +/// RFC 8446 §4.4.4: compare two Finished verify_data values without a +/// data-dependent branch or early exit. +pub fn constant_time_eq(a: &[u8], b: &[u8]) -> (out: bool) + requires + a.len() == b.len(), + ensures + out == (a@ == b@), +{ + let mut acc: u8 = 0; + let mut i: usize = 0; + while i < a.len() + invariant + i <= a@.len(), + a@.len() == b@.len(), + (acc == 0) <==> (forall|k: int| 0 <= k < i ==> a@[k] == b@[k]), + decreases a@.len() - i, + { + let x = byte_at(a, i); + let y = byte_at(b, i); + proof { + lemma_xor_zero(x, y); + lemma_or_zero(acc, x ^ y); + } + acc |= x ^ y; + // i < len, so this does not saturate. + i = i.saturating_add(1); + } + proof { + if acc == 0 { + assert(a@ =~= b@); + } + } + acc == 0 +} + +} // verus! diff --git a/crates/clazel-crypto/src/lib.rs b/crates/clazel-crypto/src/lib.rs new file mode 100644 index 0000000..b4e84f4 --- /dev/null +++ b/crates/clazel-crypto/src/lib.rs @@ -0,0 +1,23 @@ +//! The libcrux providers for `clazel-tls`'s cryptographic parameters +//! (docs/phases/phase-3.md item 3.5f). +//! +//! `clazel-tls` is proven over abstract providers: its key schedule, record +//! epochs and key exchange take the cryptography as trait parameters. This +//! crate instantiates them with libcrux and adds nothing else: +//! +//! - [`spec`]: the libcrux functions as uninterpreted specification +//! functions. +//! - [`axioms`]: the trust boundary, one `external_body` wrapper per libcrux +//! call, each an `// AXIOM:`. +//! - [`provider`]: the adapters, checked by Verus against `clazel-tls`'s +//! provider contracts. +//! - [`compare`]: the timing-safe comparison for Finished values. +//! +//! 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. + +pub mod axioms; +pub mod compare; +pub mod provider; +pub mod spec; diff --git a/crates/clazel-crypto/src/provider.rs b/crates/clazel-crypto/src/provider.rs new file mode 100644 index 0000000..b418ae0 --- /dev/null +++ b/crates/clazel-crypto/src/provider.rs @@ -0,0 +1,159 @@ +//! The adapters: `clazel-tls`'s provider traits, implemented by the +//! wrappers of [`crate::axioms`]. Verus checks each method against the +//! trait's contract; nothing here is trusted. +use crate::axioms; +use clazel_tls::hello::key_exchange::KeyExchange; +use clazel_tls::record::Aead; +use clazel_tls::schedule::crypto::Crypto; +use clazel_tls::traffic::provider::{Factory, KeyedAead}; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +/// SHA-256, HKDF-SHA256 and HMAC-SHA256 for the key schedule (RFC 8446 +/// §4.4.1 and §7.1), from libcrux. +pub struct Sha256Suite; + +impl Crypto for Sha256Suite { + open spec fn functions(&self) -> clazel_tls::schedule::spec::Crypto { + clazel_tls::schedule::spec::Crypto { + hash: |m: Seq| crate::spec::sha256(m), + extract: |salt: Seq, ikm: Seq| crate::spec::hkdf_extract(salt, ikm), + expand: |prk: Seq, info: Seq, length: nat| crate::spec::hkdf_expand(prk, info, length), + hmac: |key: Seq, message: Seq| crate::spec::hmac_sha256(key, message), + } + } + + fn hash(&self, messages: &[u8]) -> (out: Vec) { + axioms::sha256(messages) + } + + fn extract(&self, salt: &[u8], ikm: &[u8]) -> (out: Vec) { + axioms::hkdf_extract(salt, ikm) + } + + fn expand(&self, secret: &[u8], info: &[u8], length: u16) -> (out: Vec) { + axioms::hkdf_expand(secret, info, length) + } + + fn hmac(&self, key: &[u8], message: &[u8]) -> (out: Vec) { + axioms::hmac_sha256(key, message) + } +} + +/// Makes ChaCha20-Poly1305 record ciphers (RFC 8446 §5.2 and §7.3, RFC 8439 +/// §2.8), from libcrux. +pub struct ChaCha20Poly1305Factory; + +/// One ChaCha20-Poly1305 key, installed once and never exported. +pub struct ChaCha20Poly1305 { + key: Vec, +} + +impl ChaCha20Poly1305 { + /// The installed key is 32 octets. + #[verifier::type_invariant] + spec fn wf(&self) -> bool { + self.key@.len() == 32 + } +} + +impl Aead for ChaCha20Poly1305 { + closed spec fn seal_spec(&self, nonce: Seq, ad: Seq, plaintext: Seq) -> Seq { + crate::spec::chacha20poly1305_seal(self.key@, nonce, ad, plaintext) + } + + closed spec fn open_spec(&self, nonce: Seq, ad: Seq, ciphertext: Seq) -> Option> { + crate::spec::chacha20poly1305_open(self.key@, nonce, ad, ciphertext) + } + + closed spec fn tag_len_spec(&self) -> nat { + 16 + } + + closed spec fn nonce_len_spec(&self) -> nat { + 12 + } + + fn tag_len(&self) -> (n: usize) { + 16 + } + + fn nonce_len(&self) -> (n: usize) { + 12 + } + + fn seal(&self, nonce: &[u8], ad: &[u8], plaintext: &[u8]) -> (ciphertext: Vec) { + proof { use_type_invariant(self); } + axioms::chacha20poly1305_seal(self.key.as_slice(), nonce, ad, plaintext) + } + + fn open(&self, nonce: &[u8], ad: &[u8], ciphertext: &[u8]) -> (plaintext: Option>) { + proof { use_type_invariant(self); } + axioms::chacha20poly1305_open(self.key.as_slice(), nonce, ad, ciphertext) + } + + proof fn lemma_seal_len(&self, nonce: Seq, ad: Seq, plaintext: Seq) { + axioms::axiom_chacha20poly1305_seal_len(self.key@, nonce, ad, plaintext); + } +} + +impl KeyedAead for ChaCha20Poly1305 { + closed spec fn key_spec(&self) -> Seq { + self.key@ + } +} + +impl Factory for ChaCha20Poly1305Factory { + type Cipher = ChaCha20Poly1305; + + open spec fn functions(&self) -> clazel_tls::traffic::spec::Cipher { + clazel_tls::traffic::spec::Cipher { + seal: |key: Seq, nonce: Seq, ad: Seq, plaintext: Seq| + crate::spec::chacha20poly1305_seal(key, nonce, ad, plaintext), + open: |key: Seq, nonce: Seq, ad: Seq, ciphertext: Seq| + crate::spec::chacha20poly1305_open(key, nonce, ad, ciphertext), + } + } + + fn make(&self, key: &[u8]) -> (out: Self::Cipher) { + let mut installed = Vec::new(); + installed.extend_from_slice(key); + let out = ChaCha20Poly1305 { key: installed }; + proof { + assert(out.key@ =~= key@); + assert(out.tag_len_spec() == 16); + assert(out.nonce_len_spec() == 12); + assert forall|n: Seq, ad: Seq, p: Seq| + #[trigger] out.seal_spec(n, ad, p) == (self.functions().seal)(key@, n, ad, p) by {} + assert forall|n: Seq, ad: Seq, ct: Seq| + #[trigger] out.open_spec(n, ad, ct) == (self.functions().open)(key@, n, ad, ct) by {} + } + out + } +} + +/// X25519 for the `key_share` exchange (RFC 8446 §4.2.8.2 and §7.4.2, RFC +/// 7748 §6.1), from libcrux. +pub struct X25519; + +impl KeyExchange for X25519 { + open spec fn functions(&self) -> clazel_tls::hello::join_spec::KeyExchange { + clazel_tls::hello::join_spec::KeyExchange { + public_key: |private_key: Seq| crate::spec::x25519_public(private_key), + shared_secret: |private_key: Seq, peer_key: Seq| + crate::spec::x25519_shared(private_key, peer_key), + } + } + + fn public_key(&self, private_key: &[u8]) -> (out: Vec) { + axioms::x25519_public(private_key) + } + + fn shared_secret(&self, private_key: &[u8], peer_key: &[u8]) -> (out: Option>) { + axioms::x25519_shared(private_key, peer_key) + } +} + +} // verus! diff --git a/crates/clazel-crypto/src/spec.rs b/crates/clazel-crypto/src/spec.rs new file mode 100644 index 0000000..03ecbf8 --- /dev/null +++ b/crates/clazel-crypto/src/spec.rs @@ -0,0 +1,60 @@ +//! The functions libcrux computes, as uninterpreted specification functions. +//! +//! Each is named for the algorithm and the standard it implements, and has +//! no body: what a call returns is fixed only by the axiom in +//! [`crate::axioms`] that wraps the libcrux function, which states the +//! documented input and output types and nothing else (phase-3.md 3.5f). +//! That the libcrux code computes the standard's function is HACL*'s proof +//! and is in the TCB (docs/VERIFICATION.md); it is not restated here. +//! +//! - SHA-256: FIPS 180-4 §6.2, . +//! - HMAC-SHA256: RFC 2104 §2, . +//! - HKDF-SHA256: RFC 5869 §2.2 (Extract) and §2.3 (Expand), +//! . +//! - ChaCha20-Poly1305: RFC 8439 §2.8, +//! . +//! - X25519: RFC 7748 §5 and §6.1, +//! . +//! +//! Modelling choices: +//! - Each function is total over byte sequences. Inputs longer than +//! [`crate::axioms::MAX_INPUT`] (2^32 - 256) octets, which includes +//! everything libcrux refuses or panics on, are never returned from: the +//! wrapper aborts the process instead, so no axiom states a value there. +//! - X25519 returns no shared secret when libcrux reports failure, which it +//! does for an all-zero result (RFC 7748 §6.1, RFC 8446 §7.4.2). +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +/// SHA-256 of `message` (FIPS 180-4 §6.2). +pub uninterp spec fn sha256(message: Seq) -> Seq; + +/// HMAC-SHA256(key, message) (RFC 2104 §2 with SHA-256, B = 64, L = 32). +pub uninterp spec fn hmac_sha256(key: Seq, message: Seq) -> Seq; + +/// HKDF-Extract(salt, IKM) with SHA-256 (RFC 5869 §2.2). +pub uninterp spec fn hkdf_extract(salt: Seq, ikm: Seq) -> Seq; + +/// HKDF-Expand(PRK, info, L) with SHA-256 (RFC 5869 §2.3). +pub uninterp spec fn hkdf_expand(prk: Seq, info: Seq, length: nat) -> Seq; + +/// AEAD_CHACHA20_POLY1305 encryption: ciphertext followed by the 16-octet +/// tag (RFC 8439 §2.8). +pub uninterp spec fn chacha20poly1305_seal(key: Seq, nonce: Seq, ad: Seq, + plaintext: Seq) -> Seq; + +/// AEAD_CHACHA20_POLY1305 decryption: the plaintext, or none when the tag +/// does not verify (RFC 8439 §2.8). +pub uninterp spec fn chacha20poly1305_open(key: Seq, nonce: Seq, ad: Seq, + ciphertext: Seq) -> Option>; + +/// X25519(k, 9): the public key of private scalar `k` (RFC 7748 §6.1). +pub uninterp spec fn x25519_public(private_key: Seq) -> Seq; + +/// X25519(k, u): the shared secret, or none when libcrux refuses it (an +/// all-zero result, RFC 7748 §6.1). +pub uninterp spec fn x25519_shared(private_key: Seq, peer_key: Seq) -> Option>; + +} // verus! diff --git a/crates/clazel-crypto/tests/compare.rs b/crates/clazel-crypto/tests/compare.rs new file mode 100644 index 0000000..31ad334 --- /dev/null +++ b/crates/clazel-crypto/tests/compare.rs @@ -0,0 +1,47 @@ +//! `constant_time_eq` against plain equality on Finished-sized values +//! (RFC 8446 §4.4.4). Timing is not tested here; see the module doc. + +use clazel_crypto::compare::constant_time_eq; + +fn sample() -> Vec { + (0..32u8) + .map(|i| i.wrapping_mul(7).wrapping_add(3)) + .collect() +} + +#[test] +fn equal_32_bytes() { + let a = sample(); + assert!(constant_time_eq(&a, &a.clone())); +} + +#[test] +fn every_single_byte_difference() { + let a = sample(); + for pos in 0..32 { + for flip in [0x01u8, 0x80, 0xff] { + let mut b = a.clone(); + if let Some(byte) = b.get_mut(pos) { + *byte ^= flip; + } + assert!(!constant_time_eq(&a, &b), "position {pos}, flip {flip:#x}"); + assert!(!constant_time_eq(&b, &a), "position {pos}, flip {flip:#x}"); + } + } +} + +#[test] +fn empty_pair_is_equal() { + assert!(constant_time_eq(&[], &[])); +} + +#[test] +fn difference_in_last_byte_only() { + let a = sample(); + let mut b = a.clone(); + if let Some(last) = b.last_mut() { + *last = last.wrapping_add(1); + } + assert_eq!(a.get(..31), b.get(..31)); + assert!(!constant_time_eq(&a, &b)); +} diff --git a/crates/clazel-crypto/tests/known_answers.rs b/crates/clazel-crypto/tests/known_answers.rs new file mode 100644 index 0000000..034a992 --- /dev/null +++ b/crates/clazel-crypto/tests/known_answers.rs @@ -0,0 +1,182 @@ +//! Known-answer tests for every provider, from the standards' own vectors: +//! FIPS 180-2 Appendix B.1 (SHA-256 "abc"), RFC 4231 §4.2 and §4.3 +//! (HMAC-SHA256), RFC 5869 A.1 and A.3 (HKDF-SHA256), RFC 8439 §2.8.2 +//! (ChaCha20-Poly1305) and RFC 7748 §6.1 (X25519). Each is called through +//! the `clazel-tls` trait it implements, as the TLS code calls it. + +use clazel_crypto::provider::{ChaCha20Poly1305Factory, Sha256Suite, X25519}; +use clazel_tls::hello::key_exchange::KeyExchange; +use clazel_tls::record::Aead; +use clazel_tls::schedule::crypto::Crypto; +use clazel_tls::traffic::provider::Factory; + +type TestResult = Result<(), String>; + +fn hex(text: &str) -> Result, String> { + let digits: Vec = text + .bytes() + .filter(|b| !b.is_ascii_whitespace() && *b != b':') + .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() +} + +#[test] +fn sha256_fips_180_2_abc() -> TestResult { + let expected = hex("ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad")?; + assert_eq!(Sha256Suite.hash(b"abc"), expected); + Ok(()) +} + +#[test] +fn hmac_sha256_rfc_4231() -> TestResult { + // §4.2 Test Case 1. + let key = hex("0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b")?; + let tag = hex("b0344c61d8db38535ca8afceaf0bf12b881dc200c9833da726e9376c2e32cff7")?; + assert_eq!(Sha256Suite.hmac(&key, b"Hi There"), tag); + // §4.3 Test Case 2: a key shorter than the output. + let tag = hex("5bdcc146bf60754e6a042426089575c75a003f089d2739839dec58b964ec3843")?; + assert_eq!( + Sha256Suite.hmac(b"Jefe", b"what do ya want for nothing?"), + tag + ); + Ok(()) +} + +#[test] +fn hkdf_sha256_rfc_5869_a1() -> TestResult { + let ikm = hex("0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b")?; + let salt = hex("000102030405060708090a0b0c")?; + let info = hex("f0f1f2f3f4f5f6f7f8f9")?; + let prk = hex("077709362c2e32df0ddc3f0dc47bba6390b6c73bb50f9c3122ec844ad7c2b3e5")?; + let okm = hex( + "3cb25f25faacd57a90434f64d0362f2a2d2d0a90cf1a5a4c5db02d56ecc4c5bf34007208d5b887185865", + )?; + assert_eq!(Sha256Suite.extract(&salt, &ikm), prk); + assert_eq!(Sha256Suite.expand(&prk, &info, 42), okm); + // HKDF-Expand's T(1) is a prefix of every longer output (RFC 5869 §2.3), + // so the 12-octet IV length TLS uses is a prefix of the vector. + assert_eq!( + Sha256Suite.expand(&prk, &info, 12), + okm.get(..12).ok_or("short okm")? + ); + Ok(()) +} + +#[test] +fn hkdf_sha256_rfc_5869_a3_empty_salt_and_info() -> TestResult { + let ikm = hex("0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b")?; + let prk = hex("19ef24a32c717b167f33a91d6f648bdf96596776afdb6377ac434c1c293ccb04")?; + let okm = hex( + "8da4e775a563c18f715f802a063c5a31b8a11f5c5ee1879ec3454e5f3c738d2d9d201395faa4b61a96c8", + )?; + assert_eq!(Sha256Suite.extract(&[], &ikm), prk); + assert_eq!(Sha256Suite.expand(&prk, &[], 42), okm); + Ok(()) +} + +const RFC_8439_PLAINTEXT: &[u8] = b"Ladies and Gentlemen of the class of '99: If I could offer you only one tip for the future, sunscreen would be it."; + +/// RFC 8439 §2.8.2's key, nonce, additional data and sealed output. +struct Vector { + key: Vec, + nonce: Vec, + aad: Vec, + sealed: Vec, +} + +fn rfc_8439_vector() -> Result { + let key = hex("808182838485868788898a8b8c8d8e8f909192939495969798999a9b9c9d9e9f")?; + // §2.8.2: the 32-bit fixed-common part followed by the 8-octet IV. + let nonce = hex("07000000 4041424344454647")?; + let aad = hex("50515253c0c1c2c3c4c5c6c7")?; + let sealed = hex( + "d31a8d34648e60db7b86afbc53ef7ec2a4aded51296e08fea9e2b5a736ee62d6 + 3dbea45e8ca9671282fafb69da92728b1a71de0a9e060b2905d6a5b67ecd3b36 + 92ddbd7f2d778b8c9803aee328091b58fab324e4fad675945585808b4831d7bc + 3ff4def08e4b7a9de576d26586cec64b6116 + 1ae10b594f09e26a7e902ecbd0600691", + )?; + Ok(Vector { + key, + nonce, + aad, + sealed, + }) +} + +#[test] +fn chacha20poly1305_rfc_8439_seal_and_open() -> TestResult { + let Vector { + key, + nonce, + aad, + sealed, + } = rfc_8439_vector()?; + let cipher = ChaCha20Poly1305Factory.make(&key); + assert_eq!((cipher.tag_len(), cipher.nonce_len()), (16, 12)); + assert_eq!(cipher.seal(&nonce, &aad, RFC_8439_PLAINTEXT), sealed); + assert_eq!( + cipher.open(&nonce, &aad, &sealed).as_deref(), + Some(RFC_8439_PLAINTEXT) + ); + Ok(()) +} + +#[test] +fn chacha20poly1305_refuses_tampering() -> TestResult { + let Vector { + key, + nonce, + aad, + sealed, + } = rfc_8439_vector()?; + let cipher = ChaCha20Poly1305Factory.make(&key); + // A flipped bit in the ciphertext, in the tag, or in the additional data. + for position in [0, sealed.len().saturating_sub(1)] { + let mut tampered = sealed.clone(); + let byte = tampered.get_mut(position).ok_or("position")?; + *byte ^= 1; + assert_eq!(cipher.open(&nonce, &aad, &tampered), None); + } + let mut other_aad = aad.clone(); + other_aad.push(0); + assert_eq!(cipher.open(&nonce, &other_aad, &sealed), None); + // Shorter than a tag. + assert_eq!( + cipher.open(&nonce, &aad, sealed.get(..15).ok_or("short")?), + None + ); + Ok(()) +} + +#[test] +fn x25519_rfc_7748_6_1() -> TestResult { + let alice = hex("77076d0a7318a57d3c16c17251b26645df4c2f87ebc0992ab177fba51db92c2a")?; + let alice_public = hex("8520f0098930a754748b7ddcb43ef75a0dbf3a0d26381af4eba4a98eaa9b4e6a")?; + let bob = hex("5dab087e624a8a4b79e17f8b83800ee66f3bb1292618b6fd1c2f8b27ff88e0eb")?; + let bob_public = hex("de9edb7d7b7dc1b4d35b61c2ece435373f8343c85b78674dadfc7e146f882b4f")?; + let shared = hex("4a5d9d5ba4ce2de1728e3bf480350f25e07e21c947d19e3376f09b3c1e161742")?; + assert_eq!(X25519.public_key(&alice), alice_public); + assert_eq!(X25519.public_key(&bob), bob_public); + assert_eq!( + X25519.shared_secret(&alice, &bob_public), + Some(shared.clone()) + ); + assert_eq!(X25519.shared_secret(&bob, &alice_public), Some(shared)); + Ok(()) +} + +#[test] +fn x25519_refuses_an_all_zero_shared_secret() -> TestResult { + // u = 0 is a small-order point: every scalar maps it to zero (RFC 7748 + // §6.1), which RFC 8446 §7.4.2 requires the client to refuse. + let alice = hex("77076d0a7318a57d3c16c17251b26645df4c2f87ebc0992ab177fba51db92c2a")?; + assert_eq!(X25519.shared_secret(&alice, &[0u8; 32]), None); + Ok(()) +} diff --git a/docs/DEPENDENCIES.md b/docs/DEPENDENCIES.md index 37df827..b35ca03 100644 --- a/docs/DEPENDENCIES.md +++ b/docs/DEPENDENCIES.md @@ -46,22 +46,22 @@ Changing a row is a reviewable act. Adding one means saying why below. | verus_state_machines_macros | 0.0.0-2026-09-06-0133 | proof | Verus state-machine macros (proc-macro), required by `vstd`. | | verus_syn | 0.0.0-2026-09-06-0133 | proof | Verus's fork of `syn`, used by its macros. | | verus_prettyplease | 0.0.0-2026-09-06-0133 | proof | Verus macro output formatting. | -| syn | 2.0.119 | proof | Rust parser, used by Verus's macros. | +| syn | 2.0.119 | shipped | Rust parser, used by Verus's macros. Also compiled into the browser for libcrux (`clazel-crypto`), as part of `libcrux-macros`'s proc-macro chain, which runs at compile time only. | | synstructure | 0.13.2 | proof | Derive helper, used by Verus's macros. | | convert_case | 0.4.0 | proof | Identifier case conversion, used by Verus's macros. | | indexmap | 2.14.2 | proof | Ordered map, used by Verus's macros. | | hashbrown | 0.17.1 | proof | Hash table, used by `indexmap`. | | equivalent | 1.0.3 | proof | Key comparison trait, used by `indexmap`. | -| proc-macro2 | 1.0.107 | proof | Token streams for Verus's macros. Also used by `xtask` (with `span-locations`) to lex source files. | -| quote | 1.0.47 | proof | Token generation for Verus's macros. Also locked under `serde_derive` (tooling). | -| unicode-ident | 1.0.27 | proof | Identifier rules for `proc-macro2`. | +| proc-macro2 | 1.0.107 | shipped | Token streams for Verus's macros. Also used by `xtask` (with `span-locations`) to lex source files. Also compiled into the browser for libcrux (`clazel-crypto`), as part of `libcrux-macros`'s proc-macro chain, which runs at compile time only. | +| quote | 1.0.47 | shipped | Token generation for Verus's macros. Also locked under `serde_derive` (tooling). Also compiled into the browser for libcrux (`clazel-crypto`), as part of `libcrux-macros`'s proc-macro chain, which runs at compile time only. | +| unicode-ident | 1.0.27 | shipped | Identifier rules for `proc-macro2`. Also compiled into the browser for libcrux (`clazel-crypto`), as part of `libcrux-macros`'s proc-macro chain, which runs at compile time only. | | encoding_rs | 0.8.35 | test | Firefox's Encoding Standard implementation: the reference engine in `clazel-encoding`'s differential test (`tests/conformance_utf8.rs`). Pinned to 0.8.35, whose only dependency is `cfg-if`; later releases add five more. | | base64 | 0.22.1 | test | RFC 4648 base64 implementation (rust-base64): the reference engine in `clazel-base64`'s differential test (`tests/conformance_base64.rs`). No dependencies. | | mime | 0.3.17 | test | hyperium's media type parser (used by `hyper` and `reqwest`): the reference engine in `clazel-mime`'s differential test (`tests/conformance_mime_types.rs`). No dependencies. | | infer | 0.19.0 | test | A file-type detector by magic numbers (bojand/infer), written without the WHATWG standard: the reference in `clazel-mime`'s sniffing differential test (`tests/conformance_sniffing.rs`). Used without default features, so it has no dependencies (`cfb` is optional). | | psl-types | 2.0.11 | test | Types of the `publicsuffix` crate's API (no dependencies). | | publicsuffix | 2.3.0 | test | An independent Public Suffix List implementation (rust-publicsuffix, used by `cookie_store`), written from the list's own format: the reference engine in `clazel-psl`'s differential test (`tests/conformance_differential.rs`). Used without default features, so it has no `idna` dependency and handles ASCII hosts only; its only dependency is `psl-types`. | -| cfg-if | 1.0.5 | test | `#[cfg]` helper macro, required by `encoding_rs`. | +| cfg-if | 1.0.5 | shipped | `#[cfg]` helper macro, required by `encoding_rs`. Also reached from libcrux (`clazel-crypto`) through normal edges under `cfg(hax)` or `cfg(valgrind_ct_test)`, which our builds never set, so it is locked there but never compiled into the browser. | | percent-encoding | 2.3.2 | test | rust-url's percent-encoding (used by the `url` crate and Servo): a reference engine in `clazel-percent`'s differential test (`tests/conformance_percent.rs`). No dependencies. | | form_urlencoded | 1.2.2 | test | rust-url's `application/x-www-form-urlencoded` serializer: the reference for that percent-encode set in the same test. Its only dependency is `percent-encoding`. | | url | 2.5.8 | test | rust-url, the WHATWG URL parser used by Servo: the reference engine in `clazel-url`'s differential test (`tests/conformance_url.rs`); also a dev-dependency of `clazel-kernel`, whose differential test parses the URLs of its generated traces with it. Used without default features, so its `std` feature (which names `serde` as a weak dependency) is off; its dependencies (`form_urlencoded`, `idna`, `percent-encoding`) are already listed. | @@ -82,12 +82,12 @@ Changing a row is a reviewable act. Adding one means saying why below. | version_check | 0.9.5 | test | Rust version detection in `cookie`'s build script. No dependencies. | | document-features | 0.2.12 | test | Documentation generation helper (proc-macro) named by `cookie_store`. Its only dependency is `litrs`. | | litrs | 1.0.1 | test | Literal parsing, required by `document-features`. No dependencies (its `proc-macro2` feature is off). | -| log | 0.4.34 | test | The `log` facade, required by `cookie_store`. No dependencies. | -| libc | 0.2.190 | shipped | Rust bindings to the C library: struct layouts and constants (`sock_filter`, `sock_fprog`, `CLONE_NEW*`, `SECCOMP_SET_MODE_FILTER`, `SYS_seccomp`, `SYS_landlock_*`, `SYS_ptrace`, `PTRACE_ATTACH`, `PR_SET_NO_NEW_PRIVS`) and the declarations of `prctl`, `syscall`, `unshare`, `fork` and `_exit`, for `clazel-sys` only (CLAUDE.md rules 1 and 8). Reached only on Linux (`[target.'cfg(target_os = "linux")'.dependencies]`), with default features off, so it has no dependencies; macOS needs none. Getting these layouts wrong by hand is undefined behaviour, which is why it is a dependency rather than our own declarations. It is also reached by `cpufeatures` (class `test`, below the dev-only edge of `sha2` in `clazel-pkcs1`), on every target; that edge compiles into test binaries only. | +| log | 0.4.34 | shipped | The `log` facade, required by `cookie_store`. No dependencies. Also reached from libcrux (`clazel-crypto`) through normal edges under `cfg(hax)` or `cfg(valgrind_ct_test)`, which our builds never set, so it is locked there but never compiled into the browser. | +| libc | 0.2.190 | shipped | Rust bindings to the C library: struct layouts and constants (`sock_filter`, `sock_fprog`, `CLONE_NEW*`, `SECCOMP_SET_MODE_FILTER`, `SYS_seccomp`, `SYS_landlock_*`, `SYS_ptrace`, `PTRACE_ATTACH`, `PR_SET_NO_NEW_PRIVS`) and the declarations of `prctl`, `syscall`, `unshare`, `fork` and `_exit`, for `clazel-sys` only (CLAUDE.md rules 1 and 8). Reached only on Linux (`[target.'cfg(target_os = "linux")'.dependencies]`), with default features off, so it has no dependencies; macOS needs none. Getting these layouts wrong by hand is undefined behaviour, which is why it is a dependency rather than our own declarations. It is also reached by `cpufeatures` (class `test`, below the dev-only edge of `sha2` in `clazel-pkcs1`), on every target; that edge compiles into test binaries only. It is also reached by `libcrux-platform` (CPU feature detection for the never-called `libcrux-sha3`, below `clazel-crypto`), on the targets where that crate names it. | | minicbor | 2.3.1 | test | A small CBOR codec (no_std): the reference engine in `clazel-ipc`'s differential test (`tests/conformance_cbor.rs`). Chosen over `ciborium` (which pulls `serde`, `half` and two more). Used without default features (only `alloc`), so it has no dependencies. It accepts non-shortest arguments, which the test accounts for. | | simple-dns | 0.12.0 | test | A DNS message parser and writer (balliegojr/simple-dns): the reference engine in `clazel-dns`'s differential test (`tests/conformance_dns.rs`), which writes random messages with it (with and without name compression), reads them with `clazel-dns` and compares, and compares what both read from the same mutated octets. Chosen as the full-message parser with the fewest dependencies that also writes responses: `dnsparse` has none but reads only the header, questions and answers (and uses `unsafe`), and `dns-parser` has two (`byteorder`, `quick-error`) and writes only queries. Its only dependency is `bitflags`. | | httparse | 1.10.1 | test | The HTTP/1.x message-head parser of hyper (Sean McArthur's `httparse`): the reference engine in `clazel-http`'s differential test (`tests/conformance_http.rs`), which compares the status code, every field and the head length it reads from random and mutated responses with ours. It parses only the head, so the framing (`Content-Length`, chunked) is checked against expectations the test builds by construction. Used without default features (`std` adds nothing to it); no dependencies, and its build script uses none. | -| bitflags | 2.13.2 | test | Bit-flag macro, required by `simple-dns`. No dependencies. | +| bitflags | 2.13.2 | shipped | Bit-flag macro, required by `simple-dns`. No dependencies. Also reached from libcrux (`clazel-crypto`) through normal edges under `cfg(hax)` or `cfg(valgrind_ct_test)`, which our builds never set, so it is locked there but never compiled into the browser. | | sha2 | 0.10.9 | test | RustCrypto's SHA-2: computes SHA-256 for `clazel-tls`'s test-only RFC 5869 reference provider and the message digests in `clazel-pkcs1`'s conformance test (`tests/conformance_pkcs1.rs`), since the verifier takes the digest as input and Wycheproof gives messages. Used without default features. Not a differential engine for the verifier (no RSA in it). Its dependencies: `cfg-if`, `cpufeatures` and `digest`. | | digest | 0.10.7 | test | RustCrypto's hash trait, required by `sha2`. Without default features its dependencies are `block-buffer` and `crypto-common`. | | block-buffer | 0.10.4 | test | Block buffering for `digest`. Its only dependency is `generic-array`. | @@ -95,25 +95,25 @@ Changing a row is a reviewable act. Adding one means saying why below. | generic-array | 0.14.7 | test | Fixed-size arrays with type-level lengths, required by `block-buffer` and `crypto-common`. Its dependencies are `typenum` and, as a build dependency, `version_check` (already listed). | | typenum | 1.20.1 | test | Type-level numbers, required by `generic-array` and `crypto-common`. No dependencies. | | cpufeatures | 0.2.17 | test | CPU feature detection for `sha2`'s hardware paths. Its only dependency is `libc` (already listed, class `shipped`, which is the stricter class). | -| serde_json | 1.0.154 | tooling | `xtask` parses `cargo metadata` output. | -| serde_core | 1.0.229 | test | Required by `serde_json`. | -| itoa | 1.0.18 | test | Integer formatting, required by `serde_json`. | -| memchr | 2.8.3 | tooling | Byte search, required by `serde_json`. | -| zmij | 1.0.23 | tooling | Float formatting, required by `serde_json`. | -| serde | 1.0.229 | test | Locked but never compiled: `serde_json` names it under the always-false `cfg(any())` to pin versions. | -| serde_derive | 1.0.229 | test | Locked but never compiled: `serde_core` names it under `cfg(any())`. | -| syn | 3.0.9 | test | Locked but never compiled: dependency of `serde_derive`. | +| serde_json | 1.0.154 | shipped | `xtask` parses `cargo metadata` output. Also reached from libcrux (`clazel-crypto`) through normal edges under `cfg(hax)` or `cfg(valgrind_ct_test)`, which our builds never set, so it is locked there but never compiled into the browser. | +| serde_core | 1.0.229 | shipped | Required by `serde_json`. Also reached from libcrux (`clazel-crypto`) through normal edges under `cfg(hax)` or `cfg(valgrind_ct_test)`, which our builds never set, so it is locked there but never compiled into the browser. | +| itoa | 1.0.18 | shipped | Integer formatting, required by `serde_json`. Also reached from libcrux (`clazel-crypto`) through normal edges under `cfg(hax)` or `cfg(valgrind_ct_test)`, which our builds never set, so it is locked there but never compiled into the browser. | +| memchr | 2.8.3 | shipped | Byte search, required by `serde_json`. Also reached from libcrux (`clazel-crypto`) through normal edges under `cfg(hax)` or `cfg(valgrind_ct_test)`, which our builds never set, so it is locked there but never compiled into the browser. | +| zmij | 1.0.23 | shipped | Float formatting, required by `serde_json`. Also reached from libcrux (`clazel-crypto`) through normal edges under `cfg(hax)` or `cfg(valgrind_ct_test)`, which our builds never set, so it is locked there but never compiled into the browser. | +| serde | 1.0.229 | shipped | Locked but never compiled: `serde_json` names it under the always-false `cfg(any())` to pin versions. Also reached from libcrux (`clazel-crypto`) through normal edges under `cfg(hax)` or `cfg(valgrind_ct_test)`, which our builds never set, so it is locked there but never compiled into the browser. | +| serde_derive | 1.0.229 | shipped | Locked but never compiled: `serde_core` names it under `cfg(any())`. Also reached from libcrux (`clazel-crypto`) through normal edges under `cfg(hax)` or `cfg(valgrind_ct_test)`, which our builds never set, so it is locked there but never compiled into the browser. | +| syn | 3.0.9 | shipped | Locked but never compiled: dependency of `serde_derive`. Also compiled into the browser for libcrux (`clazel-crypto`), as part of `libcrux-macros`'s proc-macro chain, which runs at compile time only. | | rustls | 0.23.46 | test | The TLS library used by Firefox-adjacent projects and many Rust programs: the reference engine in `clazel-tls`'s differential test (`tests/conformance_tls_formats.rs`). Used without default features, so no cryptography provider is built and nothing but the message codec of `rustls::internal::msgs` (read one handshake message, alert or change_cipher_spec; fragment a payload into records; the number enums) is used. `cargo tree` shows six dependencies under it: `once_cell`, `rustls-pki-types`, `rustls-webpki`, `subtle`, `untrusted` and `zeroize`. rustls forbids `unsafe` (`#![forbid(unsafe_code)]`); `rustls-pki-types` has one `mem::transmute`, and `zeroize`, `once_cell` and `subtle` contain `unsafe`; `rustls-webpki` and `untrusted` have none. Test-class code never ships. | | rustls-pki-types | 1.15.1 | test | rustls's shared types for certificates, keys and names, required by `rustls` and `rustls-webpki`. Its only dependency is `zeroize`. | | rustls-webpki | 0.103.16 | test | rustls's certificate verifier, required by `rustls`. Compiled without its `ring` and `aws-lc-rs` features, so it has no cryptography, and none of its code runs in the test (only the message codec does). Its dependencies are `rustls-pki-types` and `untrusted`; its optional `ring` is named by weak features and appears in the lock only for that reason. | | zeroize | 1.9.1 | test | Zeroing of memory on drop, required by `rustls`, `rustls-pki-types` and `der`'s `alloc` feature. No dependencies as built. | | subtle | 2.6.1 | test | Constant-time comparison helpers, required by `rustls`. No dependencies. | -| once_cell | 1.21.4 | test | Lazily initialised values, required by `rustls`. No dependencies as built. | +| once_cell | 1.21.4 | shipped | Lazily initialised values, required by `rustls`. No dependencies as built. Also reached from libcrux (`clazel-crypto`) through normal edges under `cfg(hax)` or `cfg(valgrind_ct_test)`, which our builds never set, so it is locked there but never compiled into the browser. | | untrusted | 0.9.0 | test | A zero-copy reader for untrusted input, required by `rustls-webpki`. No dependencies. | | ring | 0.17.14 | test | Locked but never compiled: `rustls-webpki` names its optional `ring` dependency in weak features (`ring?/alloc`), so `cargo metadata` lists the edge although `cargo tree` shows none. | -| cc | 1.10.0 | test | Locked but never compiled: build dependency of `ring`. | -| find-msvc-tools | 0.1.15 | test | Locked but never compiled: dependency of `cc`. | -| shlex | 2.0.1 | test | Locked but never compiled: dependency of `cc`. | +| cc | 1.10.0 | shipped | Locked but never compiled: build dependency of `ring`. Also reached from libcrux (`clazel-crypto`) through normal edges under `cfg(hax)` or `cfg(valgrind_ct_test)`, which our builds never set, so it is locked there but never compiled into the browser. | +| find-msvc-tools | 0.1.15 | shipped | Locked but never compiled: dependency of `cc`. Also reached from libcrux (`clazel-crypto`) through normal edges under `cfg(hax)` or `cfg(valgrind_ct_test)`, which our builds never set, so it is locked there but never compiled into the browser. | +| shlex | 2.0.1 | shipped | Locked but never compiled: dependency of `cc`. Also reached from libcrux (`clazel-crypto`) through normal edges under `cfg(hax)` or `cfg(valgrind_ct_test)`, which our builds never set, so it is locked there but never compiled into the browser. | | getrandom | 0.2.17 | test | Locked but never compiled: dependency of `ring`. | | wasi | 0.11.1+wasi-snapshot-preview1 | test | Locked but never compiled: `getrandom`'s WASI target dependency. | | windows-sys | 0.52.0 | test | Locked but never compiled: `ring`'s and `getrandom`'s Windows target dependency. | @@ -128,6 +128,71 @@ Changing a row is a reviewable act. Adding one means saying why below. | windows_x86_64_msvc | 0.52.6 | test | Locked but never compiled: Windows import library, dependency of `windows-targets`. | | der | 0.8.2 | test | RustCrypto's DER implementation (used by `rsa`, `x509-cert` and `pkcs8`): the reference engine in `clazel-der`'s differential test (`tests/conformance_der.rs`). Used with default features off and only `alloc` and `oid`, so its only dependencies are `const-oid` and `zeroize` (the smallest DER crate that parses and writes every type item 3.5a covers; no other candidate was needed). Pinned to 0.8.2, the latest stable release. | | 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-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). | +| libcrux-intrinsics | 0.0.9 | shipped | Support crate of libcrux: Compiled but never called: SIMD intrinsics for `libcrux-sha3`. Badge `pre-verification`; 193 `unsafe` mentions, none on a path we execute. Its build script only sets SIMD cfg flags. | +| libcrux-macros | 0.0.4 | shipped | Support crate of libcrux: libcrux's proc-macros. Runs at compile time only (phase-3.md 3.0, cost 4). Badge `pre-verification`; no `unsafe`. | +| libcrux-platform | 0.0.4 | shipped | Support crate of libcrux: Compiled but never called: CPU feature detection for `libcrux-sha3`'s SIMD paths. Badge `pre-verification`; 2 `unsafe`. | +| libcrux-poly1305 | 0.0.7 | shipped | libcrux, badge `verified-hacl` (safe Rust from proven HACL* code), no `unsafe`. Poly1305, required by `libcrux-chacha20poly1305`. Used by `clazel-crypto` (src/axioms.rs). | +| libcrux-secrets | 0.0.7 | shipped | Support crate of libcrux: libcrux's secret-integer wrapper types (`U8` is plain `u8` unless its `check-secret-independence` feature is on, which we leave off). Badge `pre-verification`; 18 `unsafe` mentions. | +| libcrux-sha2 | 0.0.9 | shipped | libcrux, badge `verified-hacl` (safe Rust from proven HACL* code), no `unsafe`. SHA-256 (FIPS 180-4): `Crypto::hash`, and the HMAC/HKDF inner hash. Used by `clazel-crypto` (src/axioms.rs). | +| libcrux-sha3 | 0.0.11 | shipped | Support crate of libcrux: Compiled but never called: a non-optional dependency of `libcrux-hmac` 0.0.9 for HMAC-SHA3, which we do not use; the HMAC-SHA256 path calls only `libcrux-sha2`. Badge `pre-verification`. Taken knowingly on 2026-10-26 (verified HMAC/HKDF over unexecuted code, rather than our own HMAC/HKDF). Drop it if libcrux makes it optional. | +| libcrux-traits | 0.0.9 | shipped | Support crate of libcrux: libcrux's common traits, required by every libcrux crate used here. Badge `pre-verification`; 4 `unsafe` (`transmute` in `aead/typed_owned.rs`). | +| rand | 0.10.3 | shipped | Compiled but never called: a non-optional dependency of `libcrux-traits` (its key-generation traits). We never ask libcrux for randomness; the X25519 scalar is the caller's. Default features off. | +| rand_core | 0.10.1 | shipped | Compiled but never called: required by `rand`. | +| aho-corasick | 1.1.5 | shipped | Locked but never compiled: an optional dependency, below the `cfg(hax)` chain, of a feature nothing enables. Required by ?. | +| bumpalo | 3.20.3 | shipped | Locked but never compiled: an optional dependency, below the `cfg(hax)` chain, of a feature nothing enables. Required by ?. | +| futures-core | 0.3.34 | shipped | Locked but never compiled: an optional dependency, below the `cfg(hax)` chain, of a feature nothing enables. Required by ?. | +| futures-task | 0.3.34 | shipped | Locked but never compiled: an optional dependency, below the `cfg(hax)` chain, of a feature nothing enables. Required by ?. | +| futures-util | 0.3.34 | shipped | Locked but never compiled: an optional dependency, below the `cfg(hax)` chain, of a feature nothing enables. Required by ?. | +| js-sys | 0.3.106 | shipped | Locked but never compiled: an optional dependency, below the `cfg(hax)` chain, of a feature nothing enables. Required by ?. | +| pin-project-lite | 0.2.17 | shipped | Locked but never compiled: an optional dependency, below the `cfg(hax)` chain, of a feature nothing enables. Required by ?. | +| slab | 0.4.12 | shipped | Locked but never compiled: an optional dependency, below the `cfg(hax)` chain, of a feature nothing enables. Required by ?. | +| wasm-bindgen | 0.2.129 | shipped | Locked but never compiled: an optional dependency, below the `cfg(hax)` chain, of a feature nothing enables. Required by ?. | +| wasm-bindgen-macro | 0.2.129 | shipped | Locked but never compiled: an optional dependency, below the `cfg(hax)` chain, of a feature nothing enables. Required by ?. | +| wasm-bindgen-macro-support | 0.2.129 | shipped | Locked but never compiled: an optional dependency, below the `cfg(hax)` chain, of a feature nothing enables. Required by ?. | +| wasm-bindgen-shared | 0.2.129 | shipped | Locked but never compiled: an optional dependency, below the `cfg(hax)` chain, of a feature nothing enables. Required by ?. | +| autocfg | 1.5.1 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| bindgen | 0.72.1 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| cexpr | 0.6.0 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| chacha20 | 0.10.2 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| clang-sys | 1.9.1 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| core-models | 0.0.7 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| cpufeatures | 0.3.1 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| crabgrind | 0.3.1 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| either | 1.19.0 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| getrandom | 0.4.3 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| glob | 0.3.4 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| hax-lib | 0.3.7 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| hax-lib | 0.4.2 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| hax-lib-macros | 0.3.7 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| hax-lib-macros | 0.4.2 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| hax-lib-macros-types | 0.3.7 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| hax-lib-macros-types | 0.4.2 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| itertools | 0.13.0 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| libloading | 0.8.9 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| minimal-lexical | 0.2.1 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| nom | 7.1.3 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| num-bigint | 0.4.8 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| num-integer | 0.1.47 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| num-traits | 0.2.19 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| pastey | 0.2.3 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| pkg-config | 0.3.34 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| prettyplease | 0.2.37 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| proc-macro-error-attr2 | 2.0.0 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| proc-macro-error2 | 2.0.1 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| r-efi | 6.0.0 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| regex | 1.13.1 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| regex-automata | 0.4.18 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| regex-syntax | 0.8.11 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| rustc-hash | 2.1.3 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| rustversion | 1.0.23 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| shlex | 1.3.0 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| uuid | 1.29.0 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | +| windows-link | 0.2.1 | shipped | Locked but never compiled: reached from libcrux only under `cfg(hax)` (hax's F* extraction) or `cfg(valgrind_ct_test)` (libcrux-secrets's Valgrind constant-time test), which our builds never set. Required by ?. | The only `shipped` package is `libc`, and only `clazel-sys` depends on it diff --git a/docs/VERIFICATION.md b/docs/VERIFICATION.md index 83c1241..59a588d 100644 --- a/docs/VERIFICATION.md +++ b/docs/VERIFICATION.md @@ -162,7 +162,15 @@ We list this openly. Proofs are only as good as their assumptions. - `clazel-sys`, the one crate with `unsafe` (see "The `unsafe` exception" below): a handful of foreign calls that enter the OS sandbox, and `libc`, its only shipped dependency, for struct layouts and constants -- Cryptography, which comes from formally verified libraries (libcrux / HACL\*), not our own code +- Cryptography, which comes from formally verified libraries (libcrux / HACL\*), not our own code. + What that trusts, precisely: HACL\*'s F\* proofs; the toolchain that + translates the verified code to the Rust libcrux ships (in the TCB, not + itself proven); libcrux's hand-written, unverified glue around that code + (each crate's `impl_hacl.rs` and macros, such as `libcrux-hkdf`'s + `impl_hkdf!`); and libcrux's `pre-verification` support crates + (`libcrux-hacl-rs`, `-secrets`, `-traits`, `-macros`). Every call into + libcrux is one axiom in `crates/clazel-crypto/src/axioms.rs`, stating only + libcrux's documented types, output lengths and failure cases - That each spec matches the standard it transcribes. No proof can check this, because the standard is English. It is backed by machine-checked evidence instead of a reviewer (next section), and that evidence is only as