{"id":123602,"date":"2025-04-19T15:05:06","date_gmt":"2025-04-19T13:05:06","guid":{"rendered":"https:\/\/prohoster.info\/blog\/novosti-interneta\/v-python-zadejstvovany-kriptofunkczii-s-matematicheskim-dokazatelstvom-nadyozhnosti"},"modified":"2025-04-19T15:05:06","modified_gmt":"2025-04-19T13:05:06","slug":"v-python-zadejstvovany-kriptofunkczii-s-matematicheskim-dokazatelstvom-nadyozhnosti","status":"publish","type":"post","link":"https:\/\/prohoster.info\/pt\/blog\/news\/v-python-zadejstvovany-kriptofunkczii-s-matematicheskim-dokazatelstvom-nadyozhnosti","title":{"rendered":"No Python, s\u00e3o utilizadas fun\u00e7\u00f5es de criptografia com prova matem\u00e1tica de confiabilidade.","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Foi anunciado o culminar bem-sucedido da iniciativa de substitui\u00e7\u00e3o das implementa\u00e7\u00f5es de algoritmos criptogr\u00e1ficos em Python, oferecidas nos m\u00f3dulos hashlib e hmac, por variantes com provas matem\u00e1ticas de seguran\u00e7a, elaboradas pelo projeto HACL*. O trabalho de transi\u00e7\u00e3o para fun\u00e7\u00f5es com provas matem\u00e1ticas de seguran\u00e7a come\u00e7ou em 2022 e foi iniciado ap\u00f3s a descoberta de uma vulnerabilidade de buffer overflow na implementa\u00e7\u00e3o do algoritmo SHA3 utilizada no m\u00f3dulo hashlib do Python. <\/p>\n
O c\u00f3digo com as novas implementa\u00e7\u00f5es de fun\u00e7\u00f5es hash criptogr\u00e1ficas e algoritmos HMAC (mecanismo de autentica\u00e7\u00e3o de mensagens) foi aceito no reposit\u00f3rio principal do projeto CPython. Todas as fun\u00e7\u00f5es hash e HMAC fornecidas por padr\u00e3o no Python foram substitu\u00eddas por variantes verificadas. Entre outras coisas, foi adicionada uma implementa\u00e7\u00e3o do HMAC-BLAKE2, que utiliza instru\u00e7\u00f5es SIMD AVX2 para acelerar os c\u00e1lculos. Espera-se que o c\u00f3digo verificado entre na vers\u00e3o de outono do Python 3.14. <\/p>\n
Novas implementa\u00e7\u00f5es de fun\u00e7\u00f5es criptogr\u00e1ficas foram transferidas da biblioteca HACL*, desenvolvida por pesquisadores do Instituto Nacional de Pesquisa em Inform\u00e1tica e Automa\u00e7\u00e3o (INRIA) da Fran\u00e7a, da divis\u00e3o da Microsoft Research e da Universidade Carnegie Mellon. A biblioteca HACL* suporta fun\u00e7\u00f5es criptogr\u00e1ficas padr\u00e3o suficientes para o funcionamento do TLS 1.3 e total compatibilidade com a API do 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* \u00e9 semelhante ao OpenSSL, mas, ao contr\u00e1rio deste, oferece garantias adicionais de seguran\u00e7a e confiabilidade. <\/p>\n
O c\u00f3digo HACL* \u00e9 escrito em um subconjunto da linguagem funcional F*, que oferece um sistema de tipos dependentes e refinamentos, permitindo especificar especifica\u00e7\u00f5es precisas (modelo matem\u00e1tico) e garantir a aus\u00eancia de erros na implementa\u00e7\u00e3o por meio de f\u00f3rmulas SMT e ferramentas auxiliares de prova. O c\u00f3digo de refer\u00eancia em F* \u00e9 traduzido para c\u00f3digo em C usando o compilador KaRaMeL e est\u00e1 dispon\u00edvel para integra\u00e7\u00e3o com outros projetos. <\/p>\n
A verifica\u00e7\u00e3o envolve a defini\u00e7\u00e3o de especifica\u00e7\u00f5es detalhadas que descrevem todas as variantes de comportamento do programa, e a formula\u00e7\u00e3o de uma prova matem\u00e1tica de que o c\u00f3digo escrito corresponde completamente \u00e0s especifica\u00e7\u00f5es preparadas. A verifica\u00e7\u00e3o garante que o programa ser\u00e1 executado apenas como planejado pelos desenvolvedores e que n\u00e3o apresenta certas classes de erros, como buffer overflow, desreferencia\u00e7\u00e3o de ponteiros, acesso a \u00e1reas de mem\u00f3ria j\u00e1 liberadas ou libera\u00e7\u00e3o dupla de blocos de mem\u00f3ria. Durante o processo de compila\u00e7\u00e3o, \u00e9 realizada uma verifica\u00e7\u00e3o rigorosa de tipos e valores \u2014 um componente nunca passar\u00e1 par\u00e2metros que n\u00e3o correspondam \u00e0 especifica\u00e7\u00e3o para outro componente e n\u00e3o ter\u00e1 acesso aos estados internos de outros componentes. <\/p>\n
O processo de transi\u00e7\u00e3o para o c\u00f3digo verificado levou dois anos e meio e exigiu a modifica\u00e7\u00e3o da biblioteca HACL*, cuja funcionalidade foi ampliada com recursos necess\u00e1rios para uma substitui\u00e7\u00e3o transparente da funcionalidade existente do hashlib. Por exemplo, o HACL* teve suporte adicionado para o modo de opera\u00e7\u00e3o em fluxo HMAC, modos adicionais de opera\u00e7\u00e3o para os algoritmos Blake2 foram fornecidos, um novo API para SHA3 foi implementado, cobrindo todas as variantes dos algoritmos da fam\u00edlia Keccak, e foram desenvolvidos os meios necess\u00e1rios para notifica\u00e7\u00f5es de erros (como problemas de aloca\u00e7\u00e3o de mem\u00f3ria), criando scripts para automatizar a transfer\u00eancia de novas vers\u00f5es do HACL* para o reposit\u00f3rio Python. \n Fonte: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"