Imagine a internet e os nossos telemóveis como uma cidade enorme e movimentada onde biliões de mensagens viajam entre edifícios a cada segundo. Para manter esta cidade a funcionar, estas mensagens precisam de uma linguagem universal para que um telemóvel em Nova Iorque possa falar com uma torre em Tóquio sem ficar confuso. Esta linguagem chama-se ASN.1, e é como a gramática e o vocabulário que dizem aos computadores exatamente como empacotar a informação em caixas digitais minúsculas e eficientes. Mas aqui está a parte complicada: para poupar espaço e aumentar a velocidade, estas caixas são empacotadas de forma tão apertada que nem sequer estão alinhadas com linhas limpas de bytes (como as palavras padrão de um computador); em vez disso, são compactadas até ao último bit, a menor partícula de dados. Este método específico de empacotamento supercompacto é chamado UPER.

O problema é que escrever um tradutor (ou "parser") para desempacotar estas caixas minúsculas ao nível do bit é incrivelmente difícil. Se o tradutor cometer um erro minúsculo — como ler mal um único bit ou esquecer uma regra sobre como lidar com informação nova e desconhecida — pode fazer com que todo o sistema falhe, deixe escapar segredos ou permita que hackers se infiltrem. Durante anos, os engenheiros tentaram corrigir estes erros testando os tradutores com milhões de mensagens aleatórias, esperando detetar os bugs. Mas isto é como tentar encontrar uma agulha num palheiro apenas sacudindo o palheiro; pode encontrar algumas agulhas, mas nunca poderá ter a certeza de que encontrou todas elas, ou que as que encontrou são realmente as verdadeiras.

Surge o VUPER, uma nova ferramenta criada por investigadores da Universidade Estadual de Penn que muda as regras do jogo. Em vez de apenas sacudir o palheiro, o VUPER constrói um tradutor matematicamente perfeito do zero. Pense nisto como criar um dicionário e um livro de gramática "padrão ouro" que é provado por um matemático computacional como sendo 100% correto. Os investigadores utilizaram este tradutor perfeito para testar outros 11 parsers populares usados em redes 5G reais e em sistemas de comunicação veículo-para-tudo (V2X). Eles descobriram que muitos destes tradutores amplamente utilizados eram, na verdade, bastante não conformes, falhando em 20 tipos diferentes de regras. Em alguns casos, esta não conformidade permitiu que hackers causassem o bloqueio de telemóveis ou enganassem as redes para enviarem mensagens não encriptadas. O VUPER prova que, embora nem sempre possamos confiar nos tradutores que temos, agora podemos construir outros que são matematicamente garantidos como seguros, e usá-los para corrigir os que estão avariados.

A História do VUPER: Construindo o Tradutor Perfeito

No mundo das redes de computadores, os dados são como um longo fluxo de água a correr através de tubagens. Para enviar uma mensagem, um computador "serializa" os dados, espremendo a informação num fluxo compacto de bits. Para a receber, outro computador "faz o parsing" (analisa) o fluxo, espremendo os bits de volta numa mensagem legível. No mundo de alto risco das redes celulares 5G e da comunicação veículo-para-tudo (V2X), este processo utiliza um conjunto específico de regras chamado UPER (Unaligned Packed Encoding Rules - Regras de Codificação Empacotada Não Alinhada). É chamado de "não alinhado" porque não se importa com limites de bytes organizados; empacota os dados o mais apertado possível, bit a bit, para poupar largura de banda.

O desafio é que o livro de regras oficial para o UPER é escrito em texto descritivo denso, não em código. Isto deixa os engenheiros a adivinhar como implementar as regras, levando a erros subtis. Os investigadores por trás do VUPER decidiram parar de adivinhar. Eles construíram um framework que prova formalmente que o parser é correto. Eles não se limitaram a escrever código e esperar que funcionasse; utilizaram uma ferramenta matemática poderosa chamada provedor Rocq para verificar cada passo da lógica.

O Teste de "Ida e Volta" (Round-Trip)

Para entender como o VPR funciona, imagine que tem um tradutor mágico que transforma um livro num código secreto e vice-versa. Um teste de "ida e volta" significa que pega numa frase, transforma-a em código e depois transforma esse código de volta numa frase. Se obtiver exatamente a mesma frase de volta, o tradutor está a funcionar.

No entanto, o UPER tem um detalhe especial: extensões. À medida que a tecnologia evolui (como a transição do 4G para o 5G), novas funcionalidades são adicionadas às mensagens. Um tradutor antigo precisa de ser capaz de ler uma mensagem nova, ignorar as partes novas que não compreende e ainda assim fazer sentido das partes antigas. Isto é chamado de compatibilidade progressiva (forward compatibility). O VUPER lida com isto provando duas coisas:

1. Ida e Volta Estrita: Se a mensagem for da mesma versão, o tradutor deve transformá-la de volta no exato mesmo padrão de bits. Sem bits extra, sem bits em falta.
2. Ida e Volta Fraca: Se a mensagem tiver extensões novas e desconhecidas, o tradutor pode saltá-las, mas deve ainda ser capaz de transformar as partes conhecidas de volta numa mensagem válida. Não precisa de corresponder bit a bit ao original (porque as partes desconhecidas foram removidas), mas não deve corromper o resto.

Encontrando os Bugs

Os investigadores construíram um "oráculo de confiança" — um parser perfeito gerado pelo VUPER — e utilizaram-no para testar outros 11 parsers. Estes incluíam 7 ferramentas de código aberto (como asn1c e pycrate) e 4 parsers comerciais usados dentro de estações base reais de 4G e 5G (o hardware que liga o seu telemóvel à rede).

Eles não enviaram apenas lixo aleatório; utilizaram um "fuzzer" inteligente que compreendia a estrutura das mensagens para criar milhões de casos de teste complicados. Quando compararam os resultados, encontraram 20 tipos diferentes de inconsistências nos outros parsers.

Aqui estão algumas das descobertas mais interessantes:

• O Problema do "Demasiado Longo": Alguns parsers aceitavam números que eram demasiado grandes para o espaço alocado, ou comprimentos que não correspondiam aos dados. Isto é como um carteiro aceitar uma carta que diz "Tenho 5 páginas", mas que na verdade tem 100 páginas, fazendo com a caixa de correio transbordar e colapsar.
• A Confusão da "Extensão Desconhecida": Quando uma mensagem tinha novas funcionalidades que o parser antigo não conhecia, alguns parsers ficavam confusos e começavam a ler a parte errada da mensagem, pensando que era algo inteiramente diferente. Isto é como um tradutor que vê uma palavra nova numa língua estrangeira, fica confuso e depois traduz o resto da frase incorretamente.
• O Erro do "Valor Padrão": As regras dizem que, se um valor for o "padrão", ele não deve ser enviado de todo para poupar espaço. Mas alguns parsers ainda estavam a enviar esse valor, ou falhavam ao reconhecer quando ele estava em falta.

O Perigo no Mundo Real

O artigo não se limitou a encontrar bugs teóricos; demonstrou como estes poderiam ser explorados. Os investigadores demonstraram quatro ataques concretos:

1. Bloquear um Telemóvel: Ao enviar uma mensagem com uma lista de IDs de rede que era ligeiramente demasiado longa (violando uma restrição), causaram o bloqueio do software de um telemóvel, levando a um Ataque de Negação de Serviço (DoS).
2. Bloquear uma Torre: Uma estação base comprometida poderia enviar uma mensagem malformada para outra torre, fazendo com que a segunda torre colapsasse ao tentar processá-la.
3. Fugas de Segredos: Se um parser interpretar mal uma mensagem devido a uma extensão desconhecida, pode pensar que uma configuração de segurança está "desligada" quando na verdade está "ligada", ou vice-versa. Isto poderia levar a uma situação em que um telemóvel pensa que está a comunicar de forma segura, mas a rede está, na verdade, a enviar dados em texto simples, permitindo que espiões os leiam.
4. Identificação de Dispositivos (Fingerprinting): Como diferentes parsers lidam com erros de formas diferentes, um hacker poderia enviar mensagens de "truque" específicas e observar como o dispositivo reage. Se o dispositivo aceitar uma mensagem estranha, o hacker sabe que está a usar uma marca específica de hardware (como um modem Samsung), permitindo-lhe visar esse dispositivo específico com exploits conhecidos.

Desempenho e o Futuro

Os investigadores admitem que o seu parser perfeito e matematicamente verificado não é o mais rápido do mundo. É cerca de 4 vezes mais lento do que as bibliotecas C altamente otimizadas atualmente usadas na indústria. No entanto, é 4 vezes mais rápido do que os parsers baseados em Python.

O objetivo do VUPER não é substituir imediatamente os parsers rápidos, mas sim servir como uma implementação de referência. Tal como um mestre chef pode provar um prato e dizer exatamente o que está errado na receita, o VUPER pode dizer aos engenheiros exatamente onde os seus parsers estão a falhar. Os investigadores esperam que, ao usar o VUPER para encontrar e corrigir estes bugs, a indústria consiga eventualmente construir parsers que sejam simultaneamente rápidos e matematicamente garantidos como seguros.

No final, o VUPER mostra que, no mundo complexo e de alta velocidade do 5G e além, já não podemos confiar em testes "bons o suficiente". Precisamos de tradutores matematicamente provados para manter a nossa cidade digital segura, protegida e a funcionar sem problemas.