Apple hat mathematische Beweise entwickelt, um Implementierungen post-quanten-sicherer Kryptografie (ML-KEM, ML-DSA) in der corecrypto-Bibliothek zu verifizieren. Die Methode entdeckte Fehler, die herkömmliche Tests übersahen.
- Apple veröffentlichte Forschung und Code vom 22. Mai zur formalen Verifikation seiner Post-Quanten-Kryptografie
- Kern ist corecrypto, die low-level Bibliothek auf iPhone, iPad, Mac und anderen Plattformen
- Formale Prüfungen gegen NIST-Spezifikationen deckten einen fehlenden Schritt in einer frühen ML-DSA-Implementierung auf
- Eigenes Workflow mit Isabelle, SAW, Cryptol und neuem Cryptol-to-Isabelle-Übersetzer (mit Galois)
- Verifikation umfasst sowohl portable-C als auch handoptimierte ARM64-Assembly für Apple Silicon
- Apple gibt an, dass herkömmliche Tests solche subtilen Implementierungsfehler nicht erkannt hätten
Quelle: AppleInsider
Hinweis: Dieser Artikel wurde mithilfe von KI erstellt.
