- Os algoritmos padrão de hash e HMAC do Python agora foram substituídos por código criptográfico verificado do HACL*
- Cerca de 15.000 linhas de código C foram integradas automaticamente da base do HACL* ao código do Python
- Uma API de streaming foi projetada e verificada de forma genérica para lidar com vários algoritmos de bloco
- Foram enfrentadas questões avançadas de engenharia, como tratamento de falha de alocação de memória, correção de problemas de compilação com AVX2 e otimização do ambiente de CI
- A colaboração entre a comunidade Python e a comunidade de criptografia garantiu ao mesmo tempo segurança real e facilidade de manutenção
Introdução de código totalmente verificado para algoritmos criptográficos no Python
- Após o CVE-2022-37454 relacionado à implementação de SHA3 em 2022, surgiu a questão de migrar a infraestrutura de hash do Python para código verificado
- Ao longo dos 2 anos e meio seguintes, o Python substituiu completamente seus algoritmos padrão de hash e HMAC por implementações verificadas baseadas em HACL*
- Essa substituição foi feita de forma totalmente transparente para o usuário, sem perda de funcionalidade
- O HACL* também implementou recursos adicionais para o Python: vários modos do Blake2, API com suporte a variantes Keccak do SHA3 e otimizações de streaming para HMAC
- A incorporação de novas versões é automatizada por script, o que facilita a manutenção
Entendendo a API de streaming
- A maioria dos algoritmos criptográficos é formada por algoritmos de bloco, que precisam processar a entrada em blocos
- Em ambientes reais de uso, é difícil fornecer entrada exatamente em blocos, por isso é necessária uma API de streaming
- A API de streaming funciona independentemente do tamanho da entrada e também permite extrair resultados intermediários
- Implementações de streaming exigem gerenciamento complexo de estado, e a implementação anterior de SHA3 tinha uma falha grave de segurança relacionada a isso
- Cada algoritmo de hash tem um modo de processamento diferente, o que aumenta a complexidade: por exemplo, Blake2 não permite bloco vazio, e o HMAC pode descartar a chave após a inicialização
Verificação de um algoritmo de streaming genérico
- O método apresentado em um artigo de 2021 consiste em abstrair algoritmos de bloco e então definir sobre eles um algoritmo de streaming genérico
- Depois, ele pode ser aplicado como um template a cada algoritmo, permitindo reutilização
- A generalização inclui todas as condições especiais relevantes:
- possibilidade de especificar o tamanho da saída (SHA3 vs Shake)
- necessidade de entrada antes do processamento (ex.: bloco de chave do Blake2)
- diferenças na forma de processar o bloco final
- informações adicionais que precisam ser preservadas no estado interno
- forma de copiar o estado para extração de resultados intermediários (
stack vs heap)
- estratégia de uso de API individual por algoritmo vs API por família
Garantindo estabilidade de build para integração ao Python
- O CI do Python valida o código em mais de 50 toolchains e arquiteturas, o que faz até problemas pequenos aparecerem
- Durante a implementação de HMAC, surgiu um problema com suporte a instruções AVX2:
- alguns compiladores não conseguem processar o header
immintrin.h sem AVX2
- para resolver isso, foi usado o padrão de struct abstrata em C
- devido à diferença entre o conceito de abstração do C gerado por F* e as structs em C, foi necessário adicionar ao compilador
krml um recurso preciso de análise de visibilidade
Tratamento de falhas de alocação de memória
- O modelo anterior em F* teoricamente já permitia modelar falhas de memória, mas esta foi a primeira aplicação prática
- Para atender às exigências do Python, a estrutura de estado, a definição dos algoritmos e toda a estrutura de streaming foram aprimoradas para propagar falhas de alocação
- Em F*, usa-se o tipo
option; em C, isso é compilado como uma tagged union
- No futuro, existe a possibilidade de migrar para uma abordagem com flag de falha em tempo de execução para reduzir a complexidade
Automação das atualizações de código do HACL*
- O PR inicial do Python usava
sed para remover definições de header desnecessárias, ajustar caminhos e fazer outras alterações
- Depois que a estabilidade do código do HACL* foi confirmada, o
sed complexo foi removido e substituído por um script simples
- Com esse script, qualquer pessoa pode atualizar facilmente o código do HACL* para a versão mais recente dentro da árvore de fontes do Python
Conclusão
- Código criptográfico verificado foi integrado com sucesso ao Python, um ambiente de produção representativo
- Este é um caso que demonstra que essa tecnologia foi além da pesquisa acadêmica e também é prática e fácil de manter em software real
- É um bom exemplo de colaboração entre a comunidade Python e os desenvolvedores do HACL*, e pode influenciar outros projetos no futuro
2 comentários
Como também foi mencionado nos comentários do Hacker News, é difícil entender o que exatamente significa dizer que o ecossistema Python alcançou algo que foi "além da fase de pesquisa acadêmica para também ser prático e sustentável em software real".
Se a intenção era dizer que foi feito um trabalho para abstrair algoritmos de streaming sobre a infraestrutura de hash existente e não verificada, então isso não passa de outro trocadilho "pythonico".
Comentários no Hacker News
A versão do Python não foi especificada. Pelo que pesquisei, esse recurso deve ser incluído na versão 3.14. Não deve aparecer antes de outubro
Uma biblioteca C verificada gerada a partir do F* da Microsoft foi incluída no CPython, e foi escrita uma extensão em C
Fico curioso se vão trazer suporte à saída "streaming" do SHAKE
A criptografia moderna amplamente usada é, na prática, inquebrável, e as guerras criptográficas dos anos 90 agora parecem um tanto ultrapassadas. Fico curioso se alguém tem reflexões sobre o impacto disso na sociedade
Fico curioso sobre o quanto um framework geral de verificação para streaming pode ser reutilizado além de hashes criptográficos
Fico curioso se tudo que importar o módulo de criptografia vai precisar incluir G++ ou algo assim, ou se isso é compilado no próprio CPython
Não entendo muito de criptografia. Fico curioso sobre o que isso significa para Python
Fico curioso sobre quanto do desenvolvimento foi verificado, e o que exatamente isso abrange
Contagem de linhas de código é uma métrica muito inadequada. Ainda mais no contexto de código criptográfico, quando se tenta ostentar números grandes