Apple folosește verificare formală pentru criptarea post-cuantică din corecrypto - compania spune că dovezile matematice au găsit erori ratate de testarea clasică

Apple își întărește criptarea „post-cuantică” prin verificare formală, după ce testarea clasică a ratat erori , o schimbare cu impact operațional direct asupra bibliotecii corecrypto , folosită pe iPhone, iPad și Mac, potrivit AppleInsider . Miza este pregătirea pentru un scenariu în care calculatoarele cuantice ar putea sparge o parte din criptografia cu cheie publică folosită astăzi. Apple spune că, pentru noile implementări, testarea software convențională nu mai oferă garanții suficiente pentru sisteme de criptare rulate pe peste 2,5 miliarde de dispozitive active, motiv pentru care a apelat la „verificare formală” – o metodă care folosește demonstrații matematice pentru a valida că un cod respectă exact o specificație. Ce schimbă Apple în practică: verificare formală pentru corecrypto Apple a publicat pe 22 mai cercetare și cod-sursă care descriu cum a verificat părți din „stiva” sa de criptografie post-cuantică. Efortul se concentrează pe corecrypto, biblioteca criptografică de nivel jos pe care se sprijină multiple componente de securitate din ecosistem. Compania a construit un sistem propriu de verificare formală care compară implementările post-cuantice cu specificațiile oficiale NIST (Institutul Național de Standarde și Tehnologie din SUA). În acest cadru, Apple afirmă că demonstrează matematic că implementările sale pentru ML-KEM și ML-DSA corespund standardelor acestor algoritmi. De ce contează: erori „invizibile” pot slăbi criptarea fără să se vadă Apple susține că verificarea formală a identificat probleme pe care testarea tradițională le-a ratat în timpul dezvoltării. Un exemplu menționat este o etapă lipsă într-o implementare timpurie ML-DSA, care ar fi putut produce rezultate criptografice incorecte în cazuri rare. Tot în cadrul proiectului, cercetarea a identificat și corectat o eroare într-o demonstrație (proof) realizată de o terță parte și folosită în proces. Riscul, potrivit explicațiilor din material, este că astfel de bug-uri pot „corupe” calcule criptografice fără să declanșeze testele existente și fără simptome evidente (crash-uri, avertismente, erori vizibile). Iar pentru că corecrypto stă la baza criptării, funcțiilor de hashing (amprentare criptografică), semnăturilor digitale și generării de numere aleatoare, o vulnerabilitate critică în bibliotecă poate afecta un număr mare de aplicații și servicii care folosesc cadrele de securitate Apple. Unde ajung protecțiile post-cuantice AppleInsider notează că protecțiile post-cuantice au ajuns deja în iMessage , iar Apple extinde tehnologia către: servicii VPN; rețelistică TLS (protocolul folosit pe scară largă pentru conexiuni securizate pe internet); interfețe pentru dezvoltatori, prin API-urile CryptoKit. În arhitectura Apple, corecrypto are un rol central: cadre precum Security framework, CryptoKit și CommonCrypto se bazează pe această bibliotecă, ceea ce face ca schimbările de aici să se propage în întreg ecosistemul. De ce e mai greu decât criptografia „clasică” Materialul subliniază că algoritmii post-cuantici precum ML-KEM și ML-DSA folosesc aritmetică polinomială amplă și operații matematice „adânci”, unde pot apărea erori subtile de tip carry/borrow (transport/împrumut) în calcule. În plus, industria are mai puțină experiență practică cu aceste scheme decât cu criptografia pe curbe eliptice, folosită pe scară largă în ultimii ani. Apple își poziționează astfel criptografia post-cuantică drept infrastructură de bază în propria stivă de securitate, iar trecerea de la testare la demonstrații matematice indică o schimbare de metodă pentru a reduce riscul de defecte greu de detectat înainte de o implementare mai largă. [...]