Bug no borrow checker do Rust: o que soundness significa de verdade

O sistema de tipos do Rust faz uma promessa séria: se o seu código seguro compila, ele não pode ter ponteiros pendentes, data races ou use-after-free. Por isso, quando uma issue no GitHub mostrou um trecho de Rust aparentemente seguro que imprime lixo vindo de um stack frame já desfeito, e descobriu-se que o problema estava no borrow checker havia onze anos, muita gente sentiu o chão tremer. O bug deixa passar os requisitos de lifetime de uma struct por meio de atribuição de campo covariante e, com uma impl de Drop maliciosa, dá para guardar uma referência a uma variável local em um global e lê-la depois que a variável deixou de existir. O AddressSanitizer chama isso de stack-use-after-scope. O compilador simplesmente aceitou.

As reações foram previsíveis. Alguns declararam que a história de segurança do Rust tinha morrido. Outros deram de ombros: bugs acontecem. Os dois lados perdem o que há de realmente interessante aqui. Este bug é um experimento natural limpo sobre o valor das garantias estáticas, sobre onde o raciocínio informal deixa de funcionar e por que a distância entre “o sistema de tipos é sound” e “o compilador impõe um sistema de tipos sound” é onde moram os bugs mais interessantes. Então vamos testar cada crença comum que essa história despertou.

Mito 1: Um bug de unsoundness significa que o modelo de segurança do Rust falhou

O primeiro instinto é tratar isso como uma rachadura na teoria. Não é. Ninguém reescreveu as regras de lifetimes. Ninguém descobriu que ownership e borrowing estão fundamentalmente quebrados. O sistema de tipos do Rust, como foi projetado em quadros brancos e em RFCs, diz que este programa deve ser rejeitado. O compilador simplesmente não conseguiu rejeitá-lo.

Essa distinção entre especificação e implementação é uma das falhas geológicas mais antigas da nossa área. Tony Hoare nos deu uma teoria linda sobre processos sequenciais comunicantes; por décadas, compiladores de C compilaram de forma errada código que era perfeitamente válido segundo o padrão. A teoria se sustenta enquanto o artefato vaza. Já escrevemos sobre como a lacuna entre especificação e implementação é onde os bugs moram, e este é um caso clássico. As regras de lifetime não estavam erradas. O código de inferência de variância no rustc, a parte que decide quando é legal substituir um &'a T por um &'static T onde se espera o segundo, tinha um buraco quando a atribuição passava por um campo covariante.

Aqui está o formato do exploit, simplificado. Você cria um wrapper cuja impl de Drop copia o payload para um armazenamento global 'static. Normalmente o compilador força o payload a ser 'static, então referências a locais não conseguem entrar. O bug permite lavar uma referência de vida curta por meio de uma atribuição covariante, de modo que o wrapper acaba guardando &l, onde l é uma String local:

struct Q<T: 'static + Send>(Option<T>);
impl<T: 'static + Send> Drop for Q<T> {
fn drop(&mut self) {
if let Some(t) = self.0.take() {
KEPT.lock().unwrap().push(Box::new(t)); // escapes to 'static!
}
}
}
fn main() {
{
let l = String::from("hello world, this is long enough");
let mut q = Q(None);
q.0 = Some(&l); // should be rejected; 'static required
} // <- drop runs here, stashing &l in KEPT
// l is gone; KEPT now holds a dangling &'static String
}

Cada linha individual parece inocente. A unsoundness existe apenas na composição: um campo covariante, uma atribuição que afrouxa um limite de lifetime e um Drop que move o payload para um lugar onde ele sobrevive ao seu referente. Essa é a assinatura típica de bugs de implementação em checkers: o invariante é global, mas a aplicação é local, e um caminho de código esqueceu de verificar.

Então não, o modelo de segurança não falhou. Falhou a aplicação do modelo de segurança. É uma falha menor, mas, como veremos, não é trivial.

Mito 2: Onze anos sem detecção significam que o bug é inofensivo

O próprio raciocínio de triagem da equipe do Rust foi mais ou menos este: seria P-critical se as pessoas estivessem esbarrando nele, mas onze anos sem nenhum relato significam que não deve ser fácil de disparar, então é P-high. Há verdade nisso. Para causar de fato unsafety de memória, você precisa de uma impl de Drop deliberadamente perversa que mova dados para um local 'static. Quase ninguém escreve isso. A superfície de exposição acidental é minúscula.

Mas “raramente disparado por acidente” está fazendo muito trabalho nessa frase. Garantias de segurança não são só sobre acidentes; são sobre o que você pode confiar quando o código ao redor não é amigável. O sentido inteiro de um sistema de tipos sound é que você pode raciocinar de forma modular: não preciso auditar a sua impl de Drop, porque o compilador já provou que certas composições ruins são inexpressíveis. Quando existe um buraco, essa modularidade desaparece. Uma dependência maliciosa, ou uma dependência sutilmente errada de um autor bem-intencionado, agora pode fazer algo que a linguagem prometia ser impossível.

A história está cheia de bugs “inexploráveis” que se tornaram muito exploráveis quando apareceu o gadget certo. A pergunta prática, como um comentarista colocou, é se corrigir isso vai quebrar algum crate real do ecossistema, e a resposta provavelmente é “muito poucos ou nenhum”, o que é boa notícia. Mas a lição correta de onze anos silenciosos não é “o bug era inofensivo”. É que ausência de evidência não é evidência de ausência, especialmente para modos de falha que exigem intenção em vez de azar.

Mito 3: Olhos suficientes tornam todos os bugs superficiais

Esse é o mito que mais deveria nos envergonhar. O rustc é um dos compiladores mais examinados já escritos. É open source, tem uma equipe dedicada de types, uma comunidade acadêmica ativa (o RustBelt nos deu um modelo formal de um núcleo do Rust anos atrás) e milhões de usuários testando-o todos os dias. E mesmo assim, um buraco de soundness ficou escondido na inferência de lifetimes por mais de uma década, atravessando reescritas completas da maquinaria ao redor.

A Lei de Linus pressupõe que os olhos estão olhando para o lugar certo, com o modelo certo na cabeça. Unsoundness de sistemas de tipos derrota as duas premissas. Elas vivem na interseção de vários recursos (variância, ordem de drop, coerção, trait bounds), e cada recurso é localmente correto. Os revisores leem o código e enxergam o invariante pretendido, porque o código foi escrito por pessoas que também enxergavam o mesmo invariante. O viés de confirmação está embutido no processo. O contraexemplo exige pensar como um adversário, e pensar de forma adversarial sobre as próprias abstrações é genuinamente difícil.

Existe um site inteiro, counterexamples.org, que cataloga maneiras de regras de tipo plausíveis quebrarem, e o fio comum é mutabilidade combinada com outra coisa complicada, exatamente o formato deste bug. Essas não são lições novas. O sistema de tipos do ML teve uma unsoundness famosa envolvendo referências mutáveis e polimorfismo, corrigida com a value restriction. Os arrays do Java são covariantes e podem lançar ArrayStoreException em tempo de execução porque os designers da linguagem escolheram conveniência em vez de soundness. Quanto mais as coisas mudam, mais as mesmas três características (subtipagem, mutação e genéricos) se combinam para pegar alguém de surpresa. Se você gosta desse tipo de arqueologia, a história de sessenta anos do Lisp mostra há quanto tempo essas ideias vêm evoluindo, e as regras antigas do Rob Pike sobre simplicidade soam diferentes quando você percebe que é na complexidade que os buracos de soundness se reproduzem.

Olhos ajudam. Mas não bastam. A posição honesta, que ouvi de alguém que está construindo a própria linguagem, é mais ou menos esta: nenhuma quantidade de revisão resolve todos os problemas, então você precisa de métodos mecânicos que não se cansam e não compartilham as suas premissas.

Mito 4: Raciocínio informal é basicamente uma prova

Quando as regras de lifetime do Rust foram projetadas, elas foram argumentadas com cuidado, por gente inteligente, com muitos exemplos. Isso é raciocínio informal, e é assim que praticamente todos os compiladores de produção são construídos. O resultado é um sistema que é sound na medida em que alguém consegue perceber, o que, como aprendemos duas vezes agora, não é a mesma coisa que ser sound.

A lacuna entre as duas coisas é onde entram projetos como o RustBelt e o trabalho em andamento sobre um trait solver de nova geração. O RustBelt, construído em Coq (agora Rocq) sobre o framework de separation logic Iris, verificou por máquina um modelo das regras de tipagem centrais do Rust, incluindo as partes mais assustadoras, como as fronteiras de abstração de unsafe. Foi um marco. Mas repare no que ele provou: um modelo do Rust, não o rustc. A prova cobre o cálculo λRust, e o compilador de produção se afastou, ganhou funcionalidades e acumulou decisões de implementação que ninguém reverificou. Este problema é a conta chegando por causa desse afastamento.

Formalizar um compilador de produção inteiro é brutalmente caro. O CompCert, o compilador de C formalmente verificado, levou anos de esforço de especialistas para uma linguagem muito menor que o Rust, e verifica passes de compilação em vez de provar que o sistema de tipos do código-fonte captura todo programa ruim. Ninguém vai escrever uma prova em Coq para os dois milhões de linhas do rustc. O caminho realista se parece mais com defesa em profundidade:

• Modelos verificados por máquina das regras centrais (no estilo RustBelt), para que a própria teoria não tenha buracos.
• Ferramentas sistemáticas de fuzzing e análise de casos que geram programas adversariais, os cantos de interação entre recursos que os humanos não pensam em testar.
• Testes de mutação e de propriedades do checker: se trocar um limite deveria fazer um programa falhar, verifique se ele falha. A cultura de testes do SQLite é o modelo aqui.
• Uma lista mantida de problemas de unsoundness conhecidos (o Rust tem mais de cem marcados), tratada como backlog com prioridade de engenharia, não como folclore.

Curiosamente, a busca baseada em LLMs pode acabar sendo um saldo positivo: uma ferramenta que compõe recursos de forma incansável e perversa é exatamente o adversário que o raciocínio informal não tem. O objetivo final que muitos de nós esperamos é um Rust com especificação formal e um checker provado contra essa especificação, mas entre aqui e lá o trabalho é árduo, pouco glamouroso e de resolução de restrições.

Mito 5: Se soundness não é absoluta, a segurança estática é uma farsa

A leitura cínica vai assim: o Rust prometeu segurança, a promessa tinha uma brecha, logo a promessa era marketing e podemos voltar a usar ponteiros em C sem medo. Isso está exatamente ao contrário, e vale explicar o motivo com alguma precisão.

Soundness em um sistema de tipos é um teorema sobre um objeto matemático. O que uma linguagem de produção oferece é uma garantia estatística e econômica: classes inteiras de bugs (use-after-free, data races, invalidação de iteradores) saem do status de “radiação de fundo constante da sua base de código” e viram eventos raros o bastante para chegar à capa quando encontrados após onze anos. Compare as taxas base. Bugs de segurança de memória em grandes bases de C e C++ respondem pela maioria das CVEs graves ano após ano, e ninguém mais se surpreende com nenhuma delas individualmente. Já os bugs de unsoundness do Rust são tão raros que cada um ganha sua própria issue no GitHub, sua própria thread de discussão e sua própria cultura de postmortem. Raridade que você consegue enumerar é um mundo diferente de raridade que você não consegue.

Há também uma diferença em como as falhas se acumulam. Em C, cada linha é um possível risco de segurança de memória, então o custo da vigilância cresce com o tamanho do código para sempre. Em Rust, a vigilância se concentra nas bordas: blocos unsafe, FFI e (como agora sabemos) o próprio checker do compilador. Essa concentração é o que torna auditoria, ferramentas como o Miri e métodos formais viáveis de fato. A garantia não é binária; é uma reorganização drástica de onde mora o seu risco.

Um sistema de tipos com um bug conhecido que onze anos de tráfego de produção nunca atingiram ainda é infinitamente mais forte do que uma linguagem em que o bug é o próprio design.

O que você deve levar de fato

Se você escreve Rust, não precisa mudar nada. Seu código não era silenciosamente inseguro antes desta issue ser aberta; o caminho prático de exploit exigia intenção. Se você mantém bibliotecas, o movimento honesto continua sendo o de sempre: mantenha a superfície de unsafe pequena, rode o Miri nas partes complicadas e não trate o borrow checker como um oráculo para o código malicioso dos outros. Trate-o como uma ferramenta extremamente confiável para pegar os seus próprios erros.

Se você constrói linguagens ou compiladores, este bug é um presente: um espécime raro e bem documentado de como a soundness falha de verdade em produção. Não na teoria, mas na aplicação; não em um recurso isolado, mas na interseção de recursos; não pego pela revisão, mas por construção adversarial. As equipes que levam isso a sério, financiando reescritas de trait solvers, retrabalho de restrições de regiões e ferramentas próximas de verificação, são as que terão garantias que farão sentido daqui a dez anos.

E, para todos: recalibre o que é uma garantia. Por décadas confundimos “provado” com “argumentado de forma convincente e nunca contradito até agora”, em sistemas de tipos, protocolos criptográficos e consenso distribuído. A versão adulta da confiança não é presumir que a ponte é perfeita. É saber que a ponte tem inspetores que publicam suas descobertas, corrigem o que encontram e mantêm uma lista pública das rachaduras que ainda não foram consertadas. Nesse quesito, onze anos para encontrar um buraco não são uma acusação. São a evidência de que o sistema, o humano ao redor do compilador, está funcionando mais ou menos como deveria.