15 primitives BINAIRE prouvées Constant-Time
Preuves formelles de Constant-Time au niveau binaire ARM64 + x86-64 via HACL* (CT-Pass) + Binsec/Rel. Méthodologie CT-slice + composition stricte. Reproductibilité via commits Git PR #19.
| Primitive | Sprint / CFVL | Usage prod réel | Statut |
|---|---|---|---|
| SHA-256 (1 bloc) | 65 / BINSEC-009 | TLS, JWT, signatures | UTILISÉE |
| SHA-256 multi-bloc (4 bl.) | 83 / BINSEC-025 | Hachage volumes | UTILISÉE |
| HMAC-SHA-256 | 66 / BINSEC-010 | TLS, JWT, capability MAC | UTILISÉE |
| Poly1305-32 | 67 / BINSEC-011 | AEAD authentication | UTILISÉE |
| ChaCha20 | 68 / BINSEC-012 | Chiffrement flux (TLS, WireGuard) | UTILISÉE |
| ChaCha20-Poly1305 AEAD | 79 / BINSEC-022 | TLS 1.3, WireGuard, Signal | UTILISÉE |
| HKDF-extract / SHA-256 | 70 / BINSEC-014 | Dérivation clés TLS 1.3 | UTILISÉE |
| HKDF-expand / SHA-256 | 77-B / BINSEC-021 | Dérivation clés TLS 1.3 | UTILISÉE |
| SHA-3 / Keccak-256 | 69 / BINSEC-013 | Ethereum, NIST SP 800-185 | CATALOGUE |
| SHA-512 (2 blocs) | 84 / BINSEC-027 | RFC 6234, certificats | CATALOGUE |
| HMAC-SHA-512 | 84 / BINSEC-028 | IPsec, signatures longues | CATALOGUE |
| HMAC-BLAKE2b-32 | 83 / BINSEC-026 | Argon2, WireGuard | CATALOGUE |
| HKDF-expand / SHA-512 | 85.1 / BINSEC-029 | KDF haute sécurité | CATALOGUE |
| X25519 ECDH ⭐ | 85.2 / BINSEC-030 | TLS 1.3, WireGuard, Signal, SSH | UNIQUE MONDIAL |
| FrodoKEM-64 KEM 🏆 | 88 / BINSEC-036 | Recherche · variante test PQC | 1ÈRE MONDIALE PQC |
8 primitives benchmarkées performance
Mesures de performance temporelle réelles sur Mac Apple Silicon · clang -O2 · N=1000 · CLOCK_MONOTONIC_RAW · mean/p50/p95/p99. liboqs 0.10.1 + libsodium. Standards FIPS 203/204/205 + Round 4 NIST (BIKE, HQC).
| Primitive | Standard | Mesure |
|---|---|---|
| ChaCha20-Poly1305 encrypt 64B | RFC 8439 · libsodium | 310,90 ns |
| HMAC-SHA256 64B input | RFC 2104 · libsodium | 2 787,50 ns |
| HKDF-SHA256 Extract+Expand 32B | RFC 5869 | 3 805,84 ns |
| ML-KEM-1024 encaps | FIPS 203 · NIST PQC | 29,45 µs |
| ML-DSA-87 sign | FIPS 204 · NIST PQC | 494,96 µs |
| BIKE-L3 encaps | Round 4 · diversification | 1 326,91 µs |
| HQC-256 🇫🇷 encaps | Round 4 · INRIA France | 4 720,30 µs |
| SLH-DSA-256s sign | FIPS 205 · réserve ultime | 481,94 ms |
Distinction technique essentielle. Le benchmark performance (tableau 2) mesure le temps d’exécution réel via liboqs/libsodium. La preuve CT binaire (tableau 1) garantit mathématiquement l’absence de fuite par canal temporel au niveau binaire via HACL* + Binsec/Rel. Ces deux propriétés sont complémentaires. CORTEX NK est le seul à publier les DEUX à cette échelle : 15 preuves CT binaires + 8 benchmarks performance.