EverCrypt: unha biblioteca de verificación criptográfica

proxecto everest

Investigadores de Instituto Estatal de Investigación en Informática e Automatización (INRIA), Presentáronse Microsoft Research e Carnegie Mellon University a primeira edición de proba de a biblioteca de criptografía EverCrypt desenvolvido dentro do proxecto Everest e empregando métodos matemáticos de verificación de fiabilidade formal.

Pola súa capacidade e rendemento, EverCrypt está moi preto das bibliotecas de criptografía existentes (OpenSSL) pero que, a diferenza deles, ofrece garantías adicionais de fiabilidade e seguridade.

Por exemplo o proceso de verificación resúmese na definición de especificacións detalladas que describen todos os comportamentos do programa e a proba matemática de que o código escrito cumpre as especificacións preparadas.

A diferenza dos métodos de control de calidade baseados na evidencia, a verificación proporciona garantías fiables que o programa só se executará como pretendían os desenvolvedores e non hai tipos específicos de erros.

Por exemplo, cumprimento da especificación garante un traballo seguro coa memoria e a ausencia de erros que levan ao desbordamento do búfer, aos punteiros de desreferencia, ao acceso a áreas de memoria xa liberadas ou á dobre liberación de bloques de memoria.

Que é EverCrypt?

EverCrypt proporciona unha comprobación robusta de tipos e valores- Un compoñente nunca pasará parámetros ao outro compoñente que non cumpra e non terá acceso aos estados internos dos outros compoñentes.

O comportamento de entrada / saída axústase plenamente a accións de función matemática sinxelas, que se definen nos estándares criptográficos.

Para protexer contra ataques en canles de terceiros, comportamento durante os cálculos (por exemplo, a duración da execución ou a presenza de accesos a certa memoria) non depende dos datos secretos que se procesan.

O código do proxecto está escrito na linguaxe funcional F * (Estrela F) , que proporciona un sistema de tipos e refinamentos dependentes, que permiten establecer especificacións exactas (modelo matemático) para os programas e garantir a corrección e a ausencia de erros na implementación mediante fórmulas SMT e ferramentas de proba auxiliares.

O código en F * distribúese baixo a licenza Apache 2.0 e os módulos finais en C e o ensamblador baixo a licenza MIT.

Baseado no código de referencia F *, ensamblador, C, OCaml, xérase JavaScript e o código de montaxe web.

Algunhas partes do código preparado polo proxecto xa se usan en Firefox, o núcleo de Windows , a cadea de bloques de Tezos e VPN Wireguard.

Compoñentes de EverCrypt

En esencia, EverCrypt combina dous proxectos antes dispares de HACL * e Vale, proporcionando unha API unificada baseada nelas e facéndoas axeitadas para o seu uso en proxectos reais.

HACL * está escrito en baixo* e o seu obxectivo é proporcionar primitivas criptográficas para o seu uso en programas C que usan as API de estilo libsodium e NaCL.

O proxecto Vale desenvolveu unha linguaxe específica dominio para crear verificacións no ensamblador.

Combínanse aproximadamente 110 mil liñas de código HACL * en idioma baixo * e 25 mil liñas de código para Vale e reescríbense en preto de 70 mil liñas de código na linguaxe universal F *, que tamén se está a desenvolver como parte do proxecto Everest.

A primeira versión da biblioteca EverCrypt presenta implementacións verificadas dos seguintes algoritmos criptográficos proposto en versións C ou ensamblador (cando se usa o.

Destes, na páxina do proxecto destacan os seguintes:

  • Algoritmos hash: todas as variantes de SHA2, SHA3, SHA1 e MD5
  • Códigos de autenticación: HMAC sobre SHA1, SHA2-256, SHA2-384 e SHA2-512 para a autenticación de orixe de datos
  • Algoritmo de xeración de claves HKDF (Función de derivación de claves de extracción e expansión baseada en HMAC)
  • Cifrado de fluxo ChaCha20 (versión C non optimizada dispoñible)
  • Algoritmo de autenticación de mensaxes (MAC) Poly1305 (versión C e ensamblador)
  • Protocolo Diffie-Hellman en curvas elípticas Curve25519 (versións C e ensamblador con optimizacións baseadas en instrucións BMI2 e ADX)
  • Modo de cifrado en bloque AEAD (cifrado autenticado) ChachaPoly (versión C non optimizada)
  • Modo de cifrado de bloques AEAD AES-GCM (versión ensambladora con optimizacións AES-NI).

No primeiro versión alfa, a verificación do código xa se completou en boa parte, pero aínda hai algunhas áreas descubertas.

Ademais, A API aínda non está estabilizada, que se ampliará nas seguintes versións alfa (Está previsto unificar estruturas para todas as API.

Entre os fallos, tamén se destaca o soporte para a arquitectura x86_64 (na primeira etapa, o obxectivo principal é a fiabilidade, mentres que a optimización e as plataformas implementaranse en segundo lugar).

Fuente: https://jonathan.protzenko.fr


O contido do artigo adhírese aos nosos principios de ética editorial. Para informar dun erro faga clic en aquí.

Sexa o primeiro en opinar sobre

Deixa o teu comentario

Enderezo de correo electrónico non será publicado.

*

*

  1. Responsable dos datos: Miguel Ángel Gatón
  2. Finalidade dos datos: controlar SPAM, xestión de comentarios.
  3. Lexitimación: o seu consentimento
  4. Comunicación dos datos: os datos non serán comunicados a terceiros salvo obrigación legal.
  5. Almacenamento de datos: base de datos aloxada por Occentus Networks (UE)
  6. Dereitos: en calquera momento pode limitar, recuperar e eliminar a súa información.