From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
Este artigo preenche a lacuna entre especificações de protocolos formais e implementações do mundo real ao utilizar o monitor de tempo de execução SpecMon para verificar se as execuções observadas do WhatsApp Web e do Signal Desktop estão em conformidade com modelos recém-desenvolvidos compatíveis com o Tamarin, confirmando, assim, propriedades de segurança e revelando diferenças não documentadas entre as aplicações.
Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo
Na era digital, bilhões de pessoas dependem de aplicativos de mensagens para compartilhar seus pensamentos mais privados, proteger seus dados financeiros e coordenar suas vidas diárias. Nos bastidores dessas aplicações, reside um conjunto complexo de regras conhecido como protocolo, que atua como o projeto de como as mensagens são trancadas, enviadas e destrancadas. O mais famoso desses projetos é o protocolo Signal, um sistema projetado para garantir que, mesmo que um hacker intercepte uma mensagem, ele não consiga lê-la. Durante anos, especialistas em segurança usaram ferramentas de computador poderosas para provar que este projeto é matematicamente sólido. Eles mostraram que, se as regras forem seguidas perfeitamente, o sistema é inquebrável. No entanto, um projeto não é o mesmo que um edifício. Só porque um design parece perfeito no papel, não significa que a equipe de construção seguiu todas as instruções, usou os materiais corretos ou evitou erros acidentais ao construir as paredes. No mundo do software, a lacuna entre o design teórico e o código real executado no telefone de um usuário é onde as vulnerabilidades costem se esconder.
Uma equipe de pesquisadores do Centro de Segurança da Informação CISPA Helmholtz partiu com o objetivo de preencher essa lacuna. Eles queriam saber se as versões do mundo real do protocolo Signal, conforme rodam dentro dos aplicativos WhatsApp e Signal, realmente seguem as regras estritas que foram projetadas para obedecer. Em vez de tentar ler todo o código-fonte dessas aplicações massivas — uma tarefa dificultada pelo fato de partes delas serem ocultas ou fechadas — os pesquisadores construíram um cão de guarda especializado. Este cão de guarda, chamado SpecMon, observa a aplicação enquanto ela execra, ouvindo cada conversa que ela tem com a rede e cada cálculo que ela realiza com suas chaves de segurança. Ele compara essas ações ao vivo contra o modelo teórico perfeito em tempo real. Se a aplicação tentar pegar um atalho, pular uma etapa ou usar um método diferente do permitido pelo projeto, o cão de guarda levanta um alarme.
Os pesquisadores aplicaram este método a duas aplicações importantes: o Signal Desktop, que é aberto para qualquer pessoa inspecionar, e o WhatsApp Web, que é um sistema proprietário e fechado, pertencente a uma enorme corporação. Para a aplicação Signal Desktop, eles começaram com um modelo matemático existente e altamente detalhado do protocolo e adicionaram os detalhes específicos e desordenados encontrados no software real, como a forma como ele lida com novos tipos de criptografia projetados para resistir a futuros computadores quânticos. Para o WhatsApp, eles tiveram que trabalhar de trás para frente. Começando sem um modelo prévio, eles observaram o comportamento da aplicação, gravaram suas ações e construíram um novo projeto personalizado do zero que correspondia exatamente ao que o software estava fazendo. Este foi um feito significativo, pois marcou a primeira vez que um modelo formal foi derivado diretamente da implementação da versão do protocolo do WhatsApp.
Uma vez que esses modelos estavam prontos, os pesquisadores os colocaram à prova. Eles executaram milhares de conversas simuladas, incluindo cenários onde as mensagens eram atrasadas, enviadas fora de ordem ou onde a conexão de rede era interrompida. Em todos os casos, as aplicações se comportaram exatamente como os modelos previam, confirmando que os mecanismos centrais de segurança estavam funcionando corretamente. Os pesquisadores também injetaram erros deliberadamente no software para ver se o seu cão de guarda os detectaria. Eles fizeram os aplicativos reutilizarem chaves de criptografia antigas, pularem verificações de assinatura ou vazarem dados secretos de maneiras inesperadas. O sistema detectou cada um desses erros de segurança, provando que a ferramenta de monitoramento é sensível o suficiente para detectar desvios perigosos das regras.
No entanto, o monitoramento também revelou diferenças sutis entre as duas aplicações que não eram imediatamente óbvias. Os pesquisadores descobriram que o WhatsApp lida com os "recibos de leitura" — as notificações que informam ao remetente que uma mensagem foi visualizada — de forma diferente do Signal. No Signal, esses recibos são envolvidos pela mesma criptografia forte das mensagens e participam da atualização contínua das chaves de segurança. No WhatsApp, esses recibos são enviados fora dessa camada criptografada, o que significa que não disparam as mesmas atualizações de segurança. Embora os pesquisadores não tenham encontrado uma maneira de quebrar a segurança do WhatsApp com base nessa diferença, eles observaram que isso significa que a aplicação pode levar mais tempo para recuperar sua segurança caso uma chave secreta venha a ser roubada. Eles também confirmaram que o WhatsApp ainda não inclui certos recursos avançados de privacidade, como ocultar a identidade do remetente do servidor, que estão presentes no aplicativo Signal.
O estudo demonstra que é possível observar softwares complexos do mundo real em ação e verificar se eles aderem às suas promessas de segurança sem a necessidade de ver cada linha de seu código-fonte. O processo foi eficiente, levando apenas algumas semanas para configurar e executar, e adicionou muito pouco atraso à velocidade das aplicações. Ao criar um sistema onde o modelo teórico e o monitoramento ao vivo compartilham a mesma linguagem, os pesquisadores forneceram uma maneira para que desenvolvedores e especialistas em segurança verifiquem continuamente se suas aplicações permanecem seguras à medida que evoluem. Esta abordagem oferece um novo caminho para construir confiança nas ferramentas digitais que usamos todos os dias, garantindo que os edifícios em que vivemos sejam tão seguros quanto os projetos dos quais foram construídos.
Afogado em artigos na sua área?
Receba digests diários dos artigos mais recentes que correspondam às suas palavras-chave de pesquisa — com resumos técnicos, no seu idioma.