Quase sempre que você abre um navegador seguro do Google Chrome, um novo sistema criptográfico desenvolvido pelo MIT está ajudando a proteger melhor seus dados.

Em um artigo apresentado no recente Simpósio IEEE sobre Segurança e Privacidade, Pesquisadores do MIT detalham um sistema que, pela primeira vez, gera automaticamente código de criptografia otimizado que geralmente é escrito à mão. Implantado no início de 2018, o sistema agora está sendo amplamente usado pelo Google e outras empresas de tecnologia.

O artigo agora demonstra para outros pesquisadores da área como métodos automatizados podem ser implementados para evitar erros de origem humana na geração de criptocódigo, e como os principais ajustes aos componentes do sistema podem ajudar a alcançar um desempenho superior.

Para proteger as comunicações online, os protocolos criptográficos executam algoritmos matemáticos complexos que fazem algumas aritméticas complexas em grandes números. Por trás das cenas, Contudo, um pequeno grupo de especialistas escreve e reescreve esses algoritmos manualmente. Para cada algoritmo, eles devem pesar várias técnicas matemáticas e arquiteturas de chips para otimizar o desempenho. Quando a matemática ou arquitetura subjacente muda, eles essencialmente começam do zero. Além de ser trabalhoso, esse processo manual pode produzir algoritmos não ótimos e geralmente apresenta bugs que são detectados e corrigidos posteriormente.

Pesquisadores do Laboratório de Ciência da Computação e Inteligência Artificial (CSAIL), em vez disso, projetaram a "Criptografia Fiat, "um sistema que gera - e verifica simultaneamente - algoritmos criptográficos otimizados para todas as plataformas de hardware. Em testes, os pesquisadores descobriram que seu sistema pode gerar algoritmos que correspondem ao desempenho do melhor código escrito à mão, mas muito mais rápido.

O código gerado automaticamente pelos pesquisadores povoou o BoringSSL do Google, uma biblioteca criptográfica de código aberto. Google Chrome, Aplicativos Android, e outros programas usam BoringSSL para gerar as várias chaves e certificados usados ​​para criptografar e descriptografar dados. De acordo com os pesquisadores, cerca de 90 por cento das comunicações seguras do Chrome atualmente executam seu código.

"A criptografia é implementada fazendo aritmética em grandes números. [A criptografia Fiat] torna mais simples implementar os algoritmos matemáticos ... porque automatizamos a construção do código e fornecemos provas de que o código está correto, "diz o co-autor do artigo Adam Chlipala, pesquisador do CSAIL e professor associado de engenharia elétrica e ciência da computação e chefe do grupo de Linguagens de Programação e Verificação. "É basicamente como pegar um processo executado em cérebros humanos e entendê-lo bem o suficiente para escrever um código que imite esse processo."

Jonathan Protzenko da Microsoft Research, um especialista em criptografia que não estava envolvido nesta pesquisa, vê o trabalho como uma mudança no pensamento da indústria.

"A criptografia Fiat sendo usada no BoringSSL beneficia toda a comunidade [criptográfica], "ele diz." [É] um sinal de que os tempos estão mudando e que grandes projetos de software estão percebendo que a criptografia insegura é um risco, [e mostra] que o software verificado é maduro o suficiente para entrar no mercado. É minha esperança que mais e mais projetos de software estabelecidos façam a mudança para a criptografia verificada. Talvez nos próximos anos, o software verificado se tornará utilizável não apenas para algoritmos criptográficos, mas também para outros domínios de aplicativo. "

Juntando-se a Chlipala no papel estão:o primeiro autor Andres Erbsen e os co-autores Jade Philipoom e Jason Gross, que são todos alunos de pós-graduação do CSAIL; bem como Robert Sloan MEng '17.

Dividindo os bits

Os protocolos de criptografia usam algoritmos matemáticos para gerar chaves públicas e privadas, que são basicamente uma longa sequência de bits. Os algoritmos usam essas chaves para fornecer canais de comunicação seguros entre um navegador e um servidor. Uma das famílias mais populares, eficientes e seguras de algoritmos criptográficos é chamada de criptografia de curva elíptica (ECC). Basicamente, ele gera chaves de vários tamanhos para os usuários, escolhendo pontos numéricos aleatoriamente ao longo de uma linha curva numerada em um gráfico.

A maioria dos chips não consegue armazenar números tão grandes em um só lugar, então eles os dividem brevemente em dígitos menores que são armazenados em unidades chamadas registradores. Mas o número de registros e a quantidade de armazenamento que eles fornecem variam de um chip para outro. "Você tem que dividir as partes em vários lugares diferentes, mas acontece que a forma como você divide os bits tem diferentes consequências de desempenho, "Chlipala diz.

Tradicionalmente, especialistas que escrevem algoritmos ECC implementam manualmente essas decisões de divisão de bits em seu código. Em seu trabalho, os pesquisadores do MIT alavancaram essas decisões humanas para gerar automaticamente uma biblioteca de algoritmos ECC otimizados para qualquer hardware.

Seus pesquisadores exploraram primeiro as implementações existentes de algoritmos ECC manuscritos, nas linguagens de programação C e assembly, e transferiu essas técnicas para sua biblioteca de código. Isso gera uma lista dos algoritmos de melhor desempenho para cada arquitetura. Então, ele usa um compilador - um programa que converte linguagens de programação em códigos que os computadores entendem - que se provou correto com uma ferramenta de revisão de texto, chamado Coq. Basicamente, todo código produzido por esse compilador será sempre verificado matematicamente. Em seguida, ele simula cada algoritmo e seleciona o de melhor desempenho para cada arquitetura de chip.

Próximo, os pesquisadores estão trabalhando em maneiras de fazer seu compilador rodar ainda mais rápido na busca de algoritmos otimizados.

Compilação otimizada

Há uma inovação adicional que garante que o sistema selecione rapidamente as melhores implementações de divisão de bits. Os pesquisadores equiparam seu compilador baseado em Coq com uma técnica de otimização, chamada de "avaliação parcial, "que basicamente calcula previamente certas variáveis ​​para acelerar as coisas durante o cálculo.

No sistema dos pesquisadores, ele pré-calcula todos os métodos de divisão de bits. Ao combiná-los com uma determinada arquitetura de chip, ele descarta imediatamente todos os algoritmos que simplesmente não funcionam para essa arquitetura. Isso reduz drasticamente o tempo que leva para pesquisar na biblioteca. Depois que o sistema zera no algoritmo ideal, ele finaliza a compilação do código.

A partir desse, os pesquisadores então reuniram uma biblioteca das melhores maneiras de dividir algoritmos ECC para uma variedade de arquiteturas de chip. Agora está implementado no BoringSSL, portanto, os usuários estão principalmente desenhando a partir do código dos pesquisadores. A biblioteca pode ser atualizada automaticamente de forma semelhante para novas arquiteturas e novos tipos de matemática.

"Essencialmente, escrevemos uma biblioteca que, de uma vez por todas, está correto para todas as maneiras pelas quais você pode dividir os números, "Chlipala diz." Você pode explorar automaticamente o espaço de possíveis representações dos grandes números, compilar cada representação para medir o desempenho, e pegue o que correr mais rápido para um determinado cenário. "

Esta história foi republicada por cortesia do MIT News (web.mit.edu/newsoffice/), um site popular que cobre notícias sobre pesquisas do MIT, inovação e ensino.