Foi anunciada a conclusão bem-sucedida da iniciativa de substituição das implementações de algoritmos criptográficos em Python, oferecidas nos módulos hashlib e hmac, por variantes com prova matemática de segurança, desenvolvidas pelo projeto "HACL*". O trabalho de transição para funções com prova matemática de segurança começou em 2022 e foi iniciado após a identificação de um estouro de buffer na implementação do algoritmo SHA3, utilizado no módulo hashlib do Python.
O código com as novas implementações de funções hash criptográficas e algoritmos HMAC (mecanismo de autenticação de mensagens) foi aceito no repositório principal do projeto CPython. Todas as funções hash e HMAC fornecidas por padrão no Python foram substituídas por variantes verificadas. Entre outras coisas, foi adicionada uma implementação do HMAC-BLAKE2, que utiliza instruções SIMD AVX2 para acelerar os cálculos. Espera-se que o código verificado entre na versão de outono do Python 3.14.
As novas implementações das funções criptográficas foram transferidas da biblioteca HACL*, desenvolvida por pesquisadores do Instituto Nacional de Pesquisa em Informática e Automática (INRIA) da França, da Microsoft Research e da Universidade Carnegie Mellon. A biblioteca HACL* suporta as funções criptográficas padrão suficientes para operar com TLS 1.3 e suporte completo à API NaCl (Networking and Cryptography library), como Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC e HKDF. Em termos de desempenho, a biblioteca HACL* é semelhante ao OpenSSL, mas, ao contrário deste, oferece garantias adicionais de segurança e confiabilidade.
O código HACL* é escrito em um subconjunto da linguagem funcional F*, que oferece um sistema de tipos dependentes e refinamentos, permitindo especificar especificações precisas (modelo matemático) e garantir a ausência de erros na implementação por meio de fórmulas SMT e ferramentas auxiliares de prova. O código de referência em F* é traduzido para código em C usando o compilador KaRaMeL e está disponível para integração com outros projetos.
A verificação envolve a definição de especificações detalhadas que descrevem todas as variantes de comportamento do programa e a formação de uma prova matemática de que o código escrito está completamente em conformidade com as especificações elaboradas. A verificação garante que o programa será executado apenas como os desenvolvedores imaginaram e que não contém determinadas classes de erros, como estouro de buffer, desreferenciação de ponteiros, acesso a áreas de memória já liberadas ou liberação dupla de blocos de memória. Durante o processo de compilação, é realizada uma verificação rigorosa de tipos e valores — um componente nunca irá passar para outro componente parâmetros que não atendam às especificações e não terá acesso aos estados internos de outros componentes.
O processo de transição para o código verificado levou dois anos e meio e exigiu a modificação da biblioteca HACL*, cuja funcionalidade foi ampliada com recursos necessários para uma substituição transparente da funcionalidade existente do hashlib. Por exemplo, o HACL* teve suporte adicionado para o modo de operação em fluxo HMAC, modos adicionais de operação para os algoritmos Blake2 foram fornecidos, um novo API para SHA3 foi implementado, cobrindo todas as variantes dos algoritmos da família Keccak, e foram desenvolvidos os meios necessários para notificações de erros (como problemas de alocação de memória), criando scripts para automatizar a transferência de novas versões do HACL* para o repositório Python.
Fonte: opennet.ru
