Após anos de muito estudo e dedicação, os programadores do Project Everest — uma equipe formada por, dentre outros, profissionais da Microsoft — finalmente apresentaram uma versão funcional do EverCrypt, um provedor criptográfico que veio com a proposta de ser à prova de erros e vulnerabilidades. A ideia por trás do software é que ele seja capaz de analisar todos os possíveis comportamentos de um programa e garantir que ele cumpra com as especificações.
Antes de mais nada, vale a pena explicar que um provedor criptográfico é, a grosso modo, a base para qualquer implementação de codificação. Ele é o componente responsável por orquestrar os algoritmos de forma que ele atenda às necessidades de segurança do protocolo em questão. O grande problema é que as bibliotecas criptográficas existentes atualmente possuem bugs que podem virar vetores de exploração por parte de criminosos cibernéticos.
Na maioria das vezes, essas falhas nascem justamente da complexidade de se escrever uma biblioteca que precisa lidar com um número absurdo de algoritmos e implementações distintas — sempre sendo aprimorada, é claro, para o máximo de desempenho possível. Tal como em qualquer outro software, um bug em um provedor criptográfico nada mais é do que o resultado de uma série de acontecimentos não-previstos pelo seu criador, que resulta em um cenário inédito contendo a brecha em questão.
Para resolver esse problema, os responsáveis pelo EverCrypt trabalharam em cima do conceito de “verificação formal”: eles conseguiram garantir — e provar matematicamente — que o código fará apenas o que ele foi feito para fazer, impossibilitando um desvio para circunstâncias e cenários não-planejados. Como se não fosse o suficiente, a biblioteca também promete ser invulnerável a ataques de temporização, no qual o atacante consegue extrair informações ao analisar o tempo decorrido para executar os algoritmos.
Para desenvolver o EverCrypt, os engenheiros do Project Everest tiveram que projetar uma nova linguagem do zero. Eles criaram a F* (leia-se “F-star”), que é focada em verificação formal e cujos códigos podem ser exportados para uma série de outras linguagens mais tradicionais. No caso da biblioteca criptográfica, após ser escrita em F*, ela é compilada em uma mistura de C e Assembly. Embora o provedor ainda não suporte todos os algoritmos disponíveis no mercado, sua tabela de compatibilidade deve aumentar em breve.
Por mais que seja difícil — e coerente — acreditar que o EverCrypt seja realmente “inhackeável”, porções da biblioteca já estão sendo utilizadas em várias aplicações famosas, incluindo o próprio kernel do Windows, o navegador Firefox, a rede descentralizada Tezos e a VPN Wireguard. Vejamos como será o desenvolvimento dessa novidade.
Fonte: EverCrypt, Quanta Magazine, Microsoft