Pesquisadores do Instituto Estadual de Pesquisa em Informática e Automação (INRIA), Microsoft Research e Carnegie Mellon University apresentaram a primeira edição de teste de a biblioteca criptográfica EverCrypt desenvolvido no âmbito do projeto Everest e usando métodos matemáticos de verificação formal de confiabilidade.
Por seus recursos e desempenho, EverCrypt está muito perto de bibliotecas de criptografia existentes (OpenSSL), mas que, ao contrário deles, oferece garantias adicionais de confiabilidade e segurança.
Por exemplo o processo de verificação se resume a definir especificações detalhadas que descrevem todos os comportamentos do programa e a prova matemática de que o código escrito atende às especificações preparadas.
Ao contrário dos métodos de controle de qualidade baseados em evidências, verificação fornece garantias confiáveis que o programa será executado apenas como pretendido pelos desenvolvedores e não há tipos específicos de erros.
Por exemplo, conformidade com a especificação garante um trabalho seguro com a memória e a ausência de erros que levem ao estouro do buffer, para desreferenciar ponteiros, para acessar áreas de memória já liberadas ou para liberação dupla de blocos de memória.
O que é EverCrypt?
EverCrypt fornece verificação robusta de tipo e valor- Um componente nunca passará parâmetros para o outro componente não compatível e não terá acesso aos estados internos dos outros componentes.
O comportamento de entrada / saída está totalmente em conformidade com as ações simples da função matemática, que são definidos em padrões criptográficos.
Para se proteger contra ataques em canais de terceiros, comportamento durante os cálculos (por exemplo, a duração da execução ou a presença de acessos a determinada memória) ele não depende dos dados secretos que são processados.
O código do projeto está escrito na linguagem funcional F * (Estrela F) , que fornece um sistema de tipos dependentes e refinamentos, que permitem estabelecer especificações exatas (modelo matemático) para os programas e garantir a correção e a ausência de erros na implementação por meio de fórmulas SMT e ferramentas de teste auxiliares.
O código em F * é distribuído sob a licença Apache 2.0, e os módulos finais em C e o montador sob a licença MIT.
Com base no código de referência F *, assembler, C, OCaml, JavaScript é gerado e o código de montagem da web.
Algumas partes do código preparado pelo projeto já são usados no Firefox, o kernel do Windows , o blockchain de Tezos e VPN Wireguard.
Componentes EverCrypt
Em essência, EverCrypt combina dois projetos anteriormente díspares de HACL * e Vale, fornecendo uma API unificada com base neles e os tornando adequados para uso em projetos reais.
HACL * é escrito em baixo* e seu objetivo é fornecer primitivas criptográficas para uso em programas C que eles usam as APIs de estilo libsodium e NaCL.
O projeto Vale desenvolveu uma linguagem específica domínio para criar verificações no montador.
Cerca de 110 mil linhas de código HACL * em linguagem Low * e 25 mil linhas de código Vale são combinadas e são reescritos em cerca de 70 mil linhas de código na linguagem universal F *, que também está sendo desenvolvida como parte do projeto Everest.
A primeira versão da biblioteca EverCrypt apresenta implementações verificadas dos seguintes algoritmos criptográficos proposto nas versões C ou assembler (ao usar o.
Destes, os seguintes se destacam na página do projeto:
- Algoritmos de hash: todas as variantes de SHA2, SHA3, SHA1 e MD5
- Códigos de autenticação: HMAC sobre SHA1, SHA2-256, SHA2-384 e SHA2-512 para autenticação da fonte de dados
- Algoritmo de geração de chave HKDF (função de derivação de chave de extração e expansão baseada em HMAC)
- Criptografia de fluxo ChaCha20 (versão C não otimizada disponível)
- Algoritmo de autenticação de mensagem Poly1305 (MAC) (versão C e assembler)
- Protocolo Diffie-Hellman em curvas elípticas Curve25519 (versões C e assembler com otimizações baseadas nas instruções BMI2 e ADX)
- Modo de cifra de bloco AEAD (cifra autenticada) ChachaPoly (versão C não otimizada)
- Modo de criptografia de bloco AEAD AES-GCM (versão assembler com otimizações AES-NI).
Em primeiro versão alfa, a verificação do código já foi concluída em grande parte, mas ainda existem algumas áreas descobertas.
Além disso, API ainda não está estabilizado, que será expandido nas seguintes versões alfa (Está planejado para unificar estruturas para todas as APIs.
Entre as falhas, destaca-se também o suporte para a arquitetura x86_64 (na primeira etapa, o objetivo principal é a confiabilidade, enquanto a otimização e as plataformas serão implementadas em segundo lugar).
fonte: https://jonathan.protzenko.fr