Apple publicou os resultados da verificação formal de suas implementações dos algoritmos ML-KEM e ML-DSA

Os especialistas da empresa apresentaram os resultados da verificação formal de suas implementações dos algoritmos resistentes a pós-quânticos ML-KEM e ML-DSA, projetados para proteger os usuários em todo o ecossistema da Apple contra ameaças posedas por computadores quânticos.

A verificação formal é a validação matemática de um sistema ou implementação para demonstrar que satisfaz propriedades específicas e predefinidas.

Engenheiros da Apple e Galois usaram implementações de algoritmos de referência como linha de base, desenvolveram versões otimizadas e realizaram verificação formal para confirmar que as modificações não afetaram a correção de suas saídas. Por exemplo, durante a análise da implementação em assembly do ML-DSA para processadores Apple Silicon, a equipe descobriu um bug — uma etapa faltante em uma versão inicial — que os testes de software convencionais não haviam detectado.

Detalhes técnicos do processo de verificação são fornecidos em "Verificação formal para Apple corecrypto: ML-KEM e ML-DSA em 2026". Parte do kit de ferramentas de verificação foi lançado publicamente, junto com o código-fonte da biblioteca corecrypto, que é usado em todo o ecossistema da Apple.

As implementações ML-KEM e ML-DSA foram incluídas no lançamento de 22 de maio da biblioteca corecrypto, e com o suporte do Apple CryptoKit, desenvolvedores de terceiros agora podem integrá-las em seus próprios aplicativos.

💬 Discutir