iddqd, ou o tipo mais difícil de unsafe Rust

• iddqd é uma biblioteca de mapas Rust que toma emprestadas as chaves a partir dos valores, e mantém índices em memória para registros grandes como discos e inventário de sled no plano de controle Omicron da Oxide, onde a correção é crucial
• O BTreeMap padrão armazena chaves e valores separadamente, o que torna o repasse inconveniente ou pode fazer chaves duplicadas ficarem desencontradas, mas o IdOrdMap faz buscas extraindo a chave de um campo dentro do registro
• unsafe Rust é uma válvula de escape para expressar programas seguros que o compilador não consegue provar, e código genérico precisa suportar até mesmo Rust seguro patológico ao chamar implementações de trait fornecidas pelo usuário
• A iteração mutável de iddqd depende do invariante de que todos os índices são distintos para estender lifetimes, e uma implementação patológica de Ord podia desencontrar a B-tree e o conjunto de itens, criando índices duplicados para o mesmo item
• A correção compara chave e índice juntos e, se isso falhar, recua para uma varredura linear que não chama código do usuário; para obter confiança suficiente, é preciso combinar Miri, testes baseados em modelo, injeção de falhas com panic e revisão adversarial com LLM

---

O problema que o iddqd resolve

• iddqd é uma biblioteca Rust que fornece mapas cujas chaves são emprestadas dos valores, e a Oxide a usa amplamente no plano de controle Omicron
• O Omicron é o software no centro de um rack da Oxide que provisiona recursos como compute e storage e mantém o rack funcionando continuamente; se o iddqd falhar, o plano de controle pode se comportar incorretamente de maneiras imprevisíveis e difíceis de diagnosticar
• Uma estrutura como BTreeMap<Email, User> da biblioteca padrão do Rust armazena o email, que é a chave, separadamente do valor
• Para passar chave e valor juntos, é preciso obter (email, user) com get_key_value, e se um tipo separado como UserRecord for criado no momento da busca, isso fica difícil de lidar quando há muitos tipos de registro
• Se o email também for duplicado dentro de User, surge o risco de o email na chave do mapa e o email dentro do valor ficarem diferentes
• IdOrdMap usa a trait IdOrdItem para extrair a chave do registro, e o tipo da chave pode ser emprestado do valor, como em type Key<'a> = &'a Email
• Na Oxide, esse padrão se encaixou bem em registros grandes, como resultados de consultas ao banco de dados, e foi usado com utilidade para indexar grandes registros em todo o plano de controle

Recursos adicionais

• O iddqd oferece suporte de primeira classe a chaves complexas emprestadas de vários campos, permitindo tratá-las sem desvios como dynamic dispatch
• BiHashMap e TriHashMap indexam cada item por duas ou três chaves, respectivamente, evitando o padrão comum de manter vários mapas manualmente
• As implementações de Serde serializam como sequência, e não como mapa, para permitir serializar chaves não string em JSON, além de rejeitar chaves duplicadas
• Por compatibilidade retroativa, a serialização em formato de mapa também é suportada

Onde unsafe Rust fica mais difícil

• Em Rust, o risco central é o comportamento indefinido (undefined behavior, UB); se código seguro não puder causar UB de forma alguma, ele é sound, caso contrário é unsound
• Dentro do Rust seguro, o compilador rejeita programas com UB, mas, por limitações da análise estática, também rejeita alguns programas sem UB
• A palavra-chave unsafe é a válvula de escape para expressar esses programas, numa abordagem em que quem escreve assume a responsabilidade pela soundness e pede ao compilador que confie nisso
• Entre as regras de Rust que código unsafe precisa respeitar estão: proibição de data races, proibição de ler memória não inicializada ou já liberada, proibição de múltiplos aliases &mut para a mesma região de memória e proibição de modificar dados imutáveis
• Essas regras são difíceis de inferir, especialmente por causa de aliasing mutável, e normalmente é preciso encapsular o unsafe por trás de abstrações seguras

Etapas para validar uma abstração segura

• split_at_mut é um método seguro que divide um slice mutável em duas partes, mas esse tipo de divisão não pode ser expresso apenas com Rust seguro, então unsafe é necessário
• A soundness de split_at_mut depende de invariantes do código seguro ao redor, como receber &mut [T], verificar mid <= slice.len() e calcular corretamente o comprimento restante
• O get de MyVec<T> depende da condição de que len esteja correto e dentro dos limites, e essa condição precisa ser mantida por todos os outros métodos do mesmo módulo
• Quando código genérico unsafe chama código fornecido pelo usuário, o nível de dificuldade é o mais alto
• Código Rust seguro, por mais patológico ou hostil que seja escrito, não deve conseguir fazer código unsafe causar UB
• Código como collect_exact, que confia em len() de ExactSizeIterator e escreve até a capacidade, em geral é unsound porque, se o iterador retornar um tamanho falso, ele acabará escrevendo em memória não alocada
• std::io::Read também é uma trait cujas implementações bugadas podem retornar incorretamente a quantidade de bytes lidos, e a Rust RFC 2930 trata desse problema
• O iddqd se enquadra nessa categoria mais difícil porque é uma estrutura de dados genérica que chama implementações de trait fornecidas pelo usuário

Estrutura interna do iddqd

• O iddqd combina uma lista de itens, ItemSet, com tabelas que armazenam índices de slot
• IdHashMap<T> usa um ItemSet<T> e uma hashbrown::HashTable que armazena ItemIndex
• ItemSet<T> tem um Vec<ItemSlot<T>>, e ItemSlot<T> pode ser Occupied(T) ou Vacant { next: ItemIndex }
• free_head aponta para o slot Vacant liberado mais recentemente, ou para um sentinela que indica ausência de slots livres, e free_head junto com os slots Vacant forma a cadeia livre
• Ao inserir um novo item, o código verifica em free_head se existe um slot reutilizável; se existir, sobrescreve o slot Vacant com Occupied e então move free_head para o próximo valor
• Se não houver slot livre, ele dá push em um novo slot Occupied no fim e depois obtém a chave, calcula o hash e registra o novo índice na hash table
• A remoção faz o inverso: encontra e remove o índice na hash table pela chave, depois transforma o ItemSlot correspondente em Vacant e liga o free_head anterior como next
• IdOrdMap usa um índice B-tree em vez de hash table, e BiHashMap e TriHashMap armazenam duas e três hash tables, respectivamente

Iteração mutável e extensão de lifetime

• IdOrdMap::iter_mut faz iteração mutável dos itens na ordem das chaves
• Em iteradores Rust, os valores retornados não devem tomar emprestado do próprio iterador, e combinadores como collect podem deixar valores como Vec<&mut T> existirem mesmo depois que o iterador já desapareceu
• Para isso ser seguro, o iterador não pode retornar o mesmo valor duas vezes
• O borrow checker não consegue saber, olhando apenas o acesso sequencial à lista, que todos os índices são distintos
• O iddqd usa extensão de lifetime com std::mem::transmute::<&mut T, &'a mut T>, o que depende do invariante de que os índices retornados por self.iter são todos diferentes

O bug causado por uma implementação patológica de Ord

• Em um IdOrdMap com cinco itens inseridos em ordem com chaves de 0 a 4, consultar a chave 0 pela Entry API faz com que um OccupiedEntry armazene internamente o índice 0
• Se depois a implementação de Ord de Key passar a retornar sempre Equal, independentemente do valor, OccupiedEntry::remove poderá remover o item errado ao descer novamente pela B-tree usando apenas comparação de chave
• Por exemplo, se na B-tree ele comparar primeiro com (key = 2, index = 2), esse entry será removido por causa de Equal, enquanto, por causa do índice 0 mantido pelo OccupiedEntry, no item set será removido o item 0
• Nesse estado, o índice 0 continua na B-tree, mas o slot 0 no item set vira vacant, e o item 2 continua no item set mesmo tendo perdido o ponteiro da B-tree
• Se depois Ord voltar a funcionar normalmente e um item com chave 1000 for inserido, o slot 0 apontado por free_head será reutilizado
• O resultado é que a B-tree passa a ter índices duplicados apontando para o mesmo slot, e IterMut pode criar múltiplas referências &mut para a mesma memória, tornando isso unsound

Como a correção funciona e o compromisso de desempenho

• Ao descer pela B-tree, o código foi alterado para verificar igualdade não só da chave, mas também do índice
• Ao procurar uma chave com um índice conhecido, ele compara ambos (key, index), então, mesmo se um Ord patológico retornar Equal, a comparação entre (key = 2, index = 2) e o índice 0 procurado resultará em Less por causa do desempate pelo índice
• Para essa busca ter sucesso, o índice armazenado precisa ser de fato igual ao índice procurado
• O desempate impede correspondência com o item errado, mas não garante que o item correto sempre será encontrado
• A B-tree é ordenada por chave, enquanto o desempate compara índice, então as duas ordens em geral são independentes
• Se a busca na árvore falhar, o código recorre a uma varredura linear na B-tree para remover aquele índice sem chamar código do usuário
• Esse fallback transforma a remoção de tempo logarítmico em tempo linear, mas como ele só é alcançado na presença de código de usuário bugado, isso foi considerado um compromisso aceitável

Camadas de verificação

• Como o iddqd é usado como uma estrutura de dados fundamental, ele combina revisão analítica com várias formas de validação empírica
• Cada bloco unsafe e cada padrão unsafe são analisados por um a três autores e revisores de Rust
• Acima de cada bloco unsafe, comentários // SAFETY: registram o raciocínio, e o lint undocumented_unsafe_blocks do Clippy verifica a presença desses comentários
• Testes baseados em exemplos criam mapas, executam operações e depois verificam os resultados; o iddqd tem testes unitários internos e testes de integração da API pública
• Esses testes também existem como doctests, funcionando ao mesmo tempo como documentação
• Testes patológicos fornecem implementações bugadas de Ord e de outras traits
• No CI, tanto os testes regulares quanto os patológicos rodam sob Miri para detectar vários tipos de UB
• Condições como o invariante de não haver índices duplicados também podem ser verificadas em um ambiente de testes comum, fora do Miri

Testes baseados em modelo e injeção de falhas

• O iddqd usa duas camadas de testes aleatórios: model-based testing comparado com um oracle correto, e fault injection por cima disso
• Model-based testing, ou stateful property-based testing, aplica sequências aleatórias de operações à instância do tipo e compara os resultados com um oracle conhecido como correto
• O iddqd executa testes baseados em modelo extensivos usando o NaiveMap oracle, que é ineficiente, mas claramente correto
• Fault injection consiste em inserir bugs aleatórios no código do usuário, e no iddqd um eixo especialmente útil foi panic safety
• Mesmo que o código do usuário dê panic no meio de uma operação, os invariantes do mapa não podem ser quebrados
• Cada operação do mapa recebe uma contagem regressiva aleatória de panic, e a cada chamada ao código do usuário essa contagem é reduzida em 1; quando chega a 0, ocorre panic, permitindo testes aleatórios de panic safety
• Essa abordagem encontrou vários bugs sutis no iddqd, e alguns levavam a unsoundness
• Os testes baseados em modelo também verificam, após cada operação, invariantes internos como ausência de índices duplicados
• Esses testes são lentos demais para rodar sob Miri, então os invariantes dos quais soundness e correção dependem são verificados separadamente

Revisão adversarial com LLM e técnicas formais

• Modelos de fronteira da geração atual encontraram várias implementações patológicas de código de usuário que conseguiam corromper o mapa
• Em um caso notável, o LLM construiu um caminho em que um allocator customizado dava panic e fazia unwind, quebrando os invariantes do mapa
• Isso era um problema de panic safety diferente dos panics comuns de código de usuário, como implementações de Ord, cobertos pelos testes já existentes
• Como LLMs também podem produzir alegações de soundness plausíveis porém erradas, uma defesa é o red-green TDD usando Miri como oracle
• Em um bug de soundness, primeiro se cria um teste que mostre UB sob Miri, e depois se confirma que o mesmo teste passa após a correção
• Uma abordagem de provar invariantes do mapa com model checkers como Kani esbarra no fato de que o iddqd é complexo demais, fazendo a prova necessária crescer além do que a ferramenta consegue suportar
• Creusot pode ajudar a provar que código Rust está livre de panic e outros erros, mas hoje não consegue provar invariantes que precisam ser mantidos mesmo quando o código do usuário entra em panic ou se comporta incorretamente
• O NaiveMap funciona como a especificação mais próxima do iddqd, e o CI executa os testes baseados em modelo milhares de vezes para obter alta confiança de que a implementação corresponde à especificação
• cargo-anneal é uma ferramenta em desenvolvimento de interesse porque permitiria colocar provas de soundness em Lean em comentários de documentação ao lado do unsafe Rust
• O iddqd tem invariantes claras e um escopo limitado, embora não trivial, o que o torna um candidato a benchmark para ferramentas de verificação formal

Conclusão

• unsafe generic Rust é extremamente difícil porque precisa manter cada invariante mesmo diante de implementações arbitrárias e adversariais de traits
• O bug do iddqd mostra que uma implementação patológica de Ord pode enganar o mapa e criar aliasing mutável para a mesma memória
• Como nenhuma técnica isolada consegue encontrar todos os bugs, são usados em conjunto raciocínio humano linha por linha sobre unsafe, testes baseados em exemplos, testes patológicos, testes aleatórios e revisão adversarial com modelos de fronteira
• A Oxide considera esse nível de rigor justificado em infraestrutura fundamental

[GN⁺]

Comentários do Lobste.rs

• Se entendi direito (estou em trânsito e vi pelo celular), isso parece dar para resolver com um tipo wrapper e usando HashSet/BTreeSet em vez de HashMap/BTreeMap
  O tipo wrapper não é estritamente necessário, mas parece uma boa escolha pensando em segurança e manutenção futura
  Tudo o que você precisa é de um wrapper de tamanho zero em volta do objeto, com implementações customizadas de PartialEq/Hash que olhem só para os campos de interesse. Se quiser buscar sem construir o valor completo, dá para criar um segundo tipo que implemente AsRef para o tipo do valor
  Isso parece uma forma de reaproveitar a interface existente de HashSet/BTreeSet sem unsafe. Em vez de encapsular os tipos de valor/chave, também daria para criar um novo wrapper de HashSet/BTreeSet que fizesse esse papel

  • Aqui, a chave é uma combinação arbitrária de campos e subcampos do tipo de registro, e isso é expresso com GAT. Além disso, o padrão de índice inteiro/slab se generaliza naturalmente para um mapa com múltiplos índices
    Também há coisas como a API Entry, acesso mutável/iteração etc. Dentro do iddqd, a mutabilidade é tratada com bastante cuidado, e em alguns pontos valores atômicos são usados para permitir mutabilidade interna. Isso provavelmente teria sido bem difícil sem indireção por índice

• Para verificar formalmente o iddqd, minha primeira tentativa provavelmente seria usar um model checker como o Kani para provar que o mapa não viola seus invariantes internos. Mas fiquei curioso com a parte em que o iddqd parece ser um pouco complexo demais para o Kani, e a prova necessária cresce além do que a ferramenta consegue lidar
  Você poderia compartilhar mais detalhes sobre isso? Fico me perguntando se isso significa que a complexidade computacional do algoritmo degrada para o pior caso
  No geral, isso parece um estudo de caso interessante em métodos formais, e gostei de ver esse tema abordado. Se você olhar casos de sucesso de ferramentas existentes de verificação formal em projetos grandes, pode ingenuamente imaginar que ao menos algo como a correção de estruturas de dados seria demonstrável, mas na prática o grau de dificuldade varia entre estruturas, e isso mostra que, mesmo em linguagens consideradas mais favoráveis à prova do que Rust, que permite aliasing irrestrito, esse tipo de coisa não é trivial em termos práticos
  Fugindo um pouco do assunto, também fiquei curioso sobre como os diagramas foram feitos. Você escreveu algum script descartável, ou isso foi algo sob medida para combinar com o design do blog/site da Oxide? Não parece uma ferramenta genérica

  • No fim do texto está escrito “Diagrams courtesy Ben Leonard.”, e Ben Leonard é designer da Oxide. Então talvez tenham sido diagramas feitos à mão
  • Mesmo tentando provar algo bem básico sobre implementações concretas e funcionais de trait, o CBMC ficava consumindo CPU e não terminava nem depois de 10 minutos
    Tentei reduzir o escopo. Por exemplo, assumi que o hashbrown estava correto, mas isso também não ajudou muito. Nessa altura eu praticamente desisti. Tenho bastante confiança de que o iddqd está correto para implementações de trait que se comportam bem, e o que realmente me interessava em métodos formais era uma prova que também valesse para implementações arbitrárias e com comportamento incorreto
    Dito isso, eu não sou a pessoa que melhor usa Kani. Seria ótimo se você ou outra pessoa tentasse isso
    Os diagramas foram primeiro esboçados em Mermaid, e depois o excelente designer Ben Leonard os refinou manualmente para virar diagramas alinhados à nossa paleta de cores e tema

• O padrão de mapa baseado em campo, que indexa um objeto usando como chave um de seus campos, é algo que eu sempre quis poder usar em C# também
  Há algum tempo tentei fazer algo simples por conta própria, mas a interface não ficou muito elegante, então abandonei. Este texto me deu vontade de tentar de novo

  • Sim, é um padrão realmente útil. Eu o criei por necessidade no trabalho, mas depois passei a usá-lo em todo tipo de lugar, de codebases de produção como cargo-nextest até projetos pessoais
    Usar apenas um campo como chave é o caso mais comum, mas o iddqd é flexível o bastante para usar qualquer combinação de campos, subcampos ou funções puras e baratas de calcular a partir dos campos. Por exemplo, basta procurar ArtifactKey em https://docs.rs/iddqd/latest/iddqd/ (desculpe se você não estiver acostumado com a sintaxe de Rust)
    Ao projetar o iddqd, eu sentia fortemente que os usuários precisavam poder usar todo o poder do sistema de tipos de Rust, não importando quantas voltas eu, como autor da biblioteca, tivesse de dar para isso. Eu realmente queria que o iddqd fosse uma biblioteca prazerosa de usar para os usuários, especialmente para os meus colegas