iddqd, o el tipo más difícil de unsafe Rust

• iddqd es una biblioteca de mapas de Rust que toma prestada la clave desde el valor, y se usa para mantener índices en memoria de registros grandes como inventarios de discos y sleds en el plano de control Omicron de Oxide, donde la corrección es crítica
• El BTreeMap estándar guarda claves y valores por separado, lo que vuelve engorroso pasarlos juntos o puede hacer que claves duplicadas se desalineen, pero IdOrdMap hace búsquedas extrayendo la clave de un campo dentro del registro
• unsafe Rust es una vía de escape para expresar programas seguros que el compilador no puede demostrar, y cuando código genérico llama implementaciones de traits provistas por el usuario, debe resistir incluso Rust seguro patológico
• La iteración mutable de iddqd depende del invariante de que todos los índices son distintos para extender tiempos de vida, y una implementación patológica de Ord podía desalinear el B-tree y el conjunto de ítems, creando índices duplicados para el mismo elemento
• La corrección compara tanto clave como índice y, si eso falla, vuelve a un escaneo lineal que no llama código del usuario, además de combinar Miri, pruebas basadas en modelos, inyección de fallos por panic y revisión adversarial con LLM para lograr suficiente confianza

---

El problema que resuelve iddqd

• iddqd es una biblioteca de Rust que ofrece mapas cuya clave se toma prestada desde el valor, y Oxide la usa ampliamente en el plano de control de Omicron
• Omicron es el software que, en el centro de un rack de Oxide, aprovisiona recursos como cómputo y almacenamiento y mantiene el rack funcionando continuamente; si iddqd falla, el plano de control puede comportarse incorrectamente de formas impredecibles y difíciles de diagnosticar
• Una estructura de la biblioteca estándar de Rust como BTreeMap<Email, User> almacena la clave, email, separada del valor
• Para pasar clave y valor juntos, hay que obtener (email, user) con get_key_value, y si en el momento de la consulta se crea una estructura separada como UserRecord, se vuelve difícil de manejar cuando hay muchos tipos de registros
• Si también se duplica email dentro de User, aparece el riesgo de que la clave del mapa y el email dentro del valor no coincidan
• IdOrdMap hace que la clave se extraiga del registro mediante el trait IdOrdItem, y el tipo de clave puede tomarse prestado desde el valor, por ejemplo type Key<'a> = &'a Email
• En Oxide, este patrón encajó bien con registros grandes como los resultados de consultas a base de datos, y resultó útil para indexar registros grandes en todo el plano de control

Funciones adicionales

• iddqd soporta como ciudadanos de primera clase claves complejas tomadas de varios campos, sin recurrir a atajos como dynamic dispatch
• BiHashMap y TriHashMap indexan cada elemento por dos o tres claves respectivamente, evitando el patrón común de mantener varios mapas a mano
• La implementación de Serde serializa como secuencia en lugar de mapa, para permitir serializar en JSON claves que no son strings, y rechaza claves duplicadas
• También soporta serialización en forma de mapa por compatibilidad hacia atrás

Dónde unsafe Rust se vuelve más difícil

• En Rust, el riesgo central es el comportamiento indefinido (undefined behavior, UB); si un código seguro no puede causar UB de ninguna manera, es sound, y si no, es unsound
• Dentro de Rust seguro, el compilador rechaza programas con UB, pero por las limitaciones del análisis estático también rechaza algunos programas que no tienen UB
• La palabra clave unsafe es una vía de escape para expresar ese tipo de programas, donde quien lo escribe asume la responsabilidad de la soundness y le pide al compilador que confíe en ello
• Entre las reglas de Rust que el código unsafe debe respetar están: no permitir data races, no leer memoria no inicializada o ya liberada, no permitir múltiples alias &mut sobre la misma región de memoria, y no modificar datos inmutables
• Estas reglas son especialmente difíciles de razonar por el aliasing mutable, por lo que normalmente hace falta encapsular unsafe detrás de una abstracción segura

Etapas para validar una abstracción segura

• split_at_mut es un método seguro que divide un slice mutable en dos partes, pero esta división no puede expresarse solo con Rust seguro, así que necesita unsafe
• La soundness de split_at_mut depende de invariantes en el código seguro que lo rodea, como haber recibido un &mut [T], haber verificado que mid <= slice.len(), y haber calculado correctamente la longitud restante
• El get de MyVec<T> depende de que len sea correcto y de que esté dentro de rango, y esa condición debe ser preservada por todos los demás métodos del mismo módulo
• La dificultad máxima aparece cuando código unsafe genérico llama código provisto por el usuario
• El código escrito en Rust seguro, por más patológico o adversarial que sea, no debe poder hacer que el código unsafe provoque UB
• Código como collect_exact, que confía en len() de ExactSizeIterator y escribe hasta la capacidad reservada, normalmente es unsound si el iterador devuelve una longitud falsa, porque terminaría escribiendo en memoria no asignada
• std::io::Read también es un trait cuyas implementaciones con errores pueden devolver mal la cantidad de bytes leídos, y Rust RFC 2930 trata este problema
• iddqd cae en esta categoría más difícil porque es una estructura de datos genérica que llama implementaciones de traits provistas por el usuario

Estructura interna de iddqd

• iddqd combina una lista de elementos, ItemSet, con una tabla que contiene índices de slots
• IdHashMap<T> usa un ItemSet<T> y un hashbrown::HashTable que almacena ItemIndex
• ItemSet<T> tiene un Vec<ItemSlot<T>>, y ItemSlot<T> puede ser Occupied(T) o Vacant { next: ItemIndex }
• free_head apunta al slot Vacant liberado más recientemente o a un sentinel que indica que no hay slots libres, y free_head junto con los slots Vacant forman la free chain
• Al insertar un nuevo elemento, primero se revisa free_head para ver si hay un slot reutilizable; si lo hay, se sobrescribe el slot Vacant con Occupied y luego free_head avanza al siguiente valor
• Si no hay slots libres, se hace push de un nuevo slot Occupied al final, luego se obtiene la clave, se calcula el hash y se registra el nuevo índice en la hash table
• La eliminación hace lo inverso: busca y elimina el índice por clave en la hash table, convierte el ItemSlot correspondiente en Vacant y enlaza el free_head anterior como next
• IdOrdMap usa un índice B-tree en lugar de hash table, y BiHashMap y TriHashMap almacenan dos y tres hash tables respectivamente

Iteración mutable y extensión de tiempos de vida

• IdOrdMap::iter_mut itera mutando los elementos en orden de clave
• Un iterador de Rust debe devolver valores que no tomen prestado del propio iterador, y combinadores como collect pueden dejar valores como Vec<&mut T> incluso después de que el iterador ya desapareció
• Para que esto sea seguro, el iterador no debe devolver el mismo valor dos veces
• El borrow checker solo ve accesos secuenciales a una lista y no puede saber que todos los índices son distintos
• iddqd usa extensión de tiempos de vida con std::mem::transmute::<&mut T, &'a mut T>, y esto depende del invariante de que los índices devueltos por self.iter sean todos distintos

El bug causado por una implementación patológica de Ord

• En un IdOrdMap con cinco elementos cuyas claves van de 0 a 4 en orden, si se consulta la clave 0 con la Entry API, el OccupiedEntry guarda internamente el índice 0
• Si después la implementación de Ord de Key cambia para devolver siempre Equal sin importar el valor, OccupiedEntry::remove puede volver a bajar por el B-tree y eliminar el elemento incorrecto basándose solo en la comparación de claves
• Por ejemplo, si primero compara (key = 2, index = 2) en el B-tree, ese entry se elimina por culpa de Equal, mientras que el item set elimina el elemento 0 porque OccupiedEntry conservaba el índice 0
• En ese estado, el B-tree aún contiene el índice 0, pero el slot 0 del item set queda como vacant, y el elemento 2 permanece en el item set aunque ya no tenga un puntero desde el B-tree
• Si luego Ord vuelve a comportarse normalmente y se inserta un elemento con clave 1000, se reutiliza el slot 0 apuntado por free_head
• El resultado es que el B-tree termina con índices duplicados que apuntan al mismo slot, y IterMut puede crear múltiples referencias &mut a la misma memoria, volviéndose unsound

Forma de la corrección y compromiso de rendimiento

• Se cambió la lógica para que al bajar por el B-tree verifique no solo igualdad de clave, sino también igualdad de índice
• Al buscar una clave con un índice conocido, se comparan ambos, (key, index), así que aunque un Ord patológico devuelva Equal, la comparación entre (key = 2, index = 2) y el índice buscado 0 resulta Less por el desempate con el índice
• Para que esta búsqueda tenga éxito, el índice almacenado debe coincidir realmente con el índice buscado
• El desempate evita emparejar el elemento incorrecto, pero no garantiza que siempre se encuentre el elemento correcto
• El B-tree está ordenado por clave y el desempate compara el índice, por lo que ambos órdenes en general son independientes
• Si la búsqueda en el árbol falla, se hace un escaneo lineal del B-tree para eliminar ese índice sin llamar código del usuario
• Ese fallback vuelve lineal una operación de eliminación que normalmente sería logarítmica, pero se considera un compromiso aceptable porque solo se alcanza si hay código de usuario defectuoso

Capas de verificación

• Como iddqd se usa como estructura de datos fundacional, combina revisión analítica con múltiples formas de validación empírica
• Cada bloque unsafe y cada patrón unsafe es analizado por entre uno y tres autores o revisores de Rust
• Encima de cada bloque unsafe se deja el razonamiento en un comentario // SAFETY:, y el lint undocumented_unsafe_blocks de Clippy verifica que el comentario exista
• Las pruebas basadas en ejemplos crean mapas, ejecutan operaciones y luego verifican los resultados; iddqd tiene unit tests internos e integration tests sobre la API pública
• Estas pruebas también existen como doctests, cumpliendo además una función de documentación
• Las pruebas patológicas suministran un Ord defectuoso y otras implementaciones de traits anómalas
• En CI se ejecutan tanto pruebas normales como patológicas bajo Miri para detectar varios tipos de UB
• Condiciones como el invariante de no tener índices duplicados también pueden verificarse en entornos normales de prueba fuera de Miri

Pruebas basadas en modelos e inyección de fallos

• iddqd usa dos capas de pruebas aleatorias: model-based testing comparado contra un oráculo correcto, y fault injection por encima de eso
• El model-based testing, o stateful property-based testing, aplica secuencias aleatorias de operaciones a una instancia del tipo y compara los resultados con un oráculo conocido como correcto
• iddqd ejecuta pruebas basadas en modelos extensivas usando como referencia el oráculo NaiveMap, que es ineficiente pero claramente correcto
• La inyección de fallos consiste en introducir errores aleatorios en el código del usuario, y en iddqd una dimensión especialmente útil fue la seguridad frente a panic
• Aunque el código del usuario haga panic a mitad de una operación, los invariantes del mapa no deben romperse
• Para cada operación del mapa se añade una cuenta regresiva aleatoria de panic, que se reduce en 1 en cada llamada a código del usuario, y al llegar a 0 provoca un panic, permitiendo pruebas aleatorias de seguridad frente a panic
• Este método encontró varios bugs sutiles en iddqd, y algunos derivaban en unsoundness
• Las pruebas basadas en modelos también verifican después de cada operación invariantes internos como no-duplicate-index
• Como estas pruebas son demasiado lentas para ejecutarse bajo Miri, se verifican por separado los invariantes de los que dependen la soundness y la corrección

Revisión adversarial con LLM y técnicas formales

• Un modelo frontier de la generación actual encontró varias implementaciones patológicas de código de usuario que podían corromper el mapa
• En un caso notable, el LLM construyó una ruta donde un asignador personalizado hacía panic y desenrollaba la pila, rompiendo los invariantes del mapa
• Este era un problema de seguridad frente a panic distinto de los panic normales en código de usuario, como los de implementaciones de Ord, que ya cubrían las pruebas existentes
• Como un LLM también puede producir afirmaciones plausibles pero incorrectas sobre soundness, una defensa útil es un red-green TDD con Miri como oráculo
• Ante un bug de soundness, primero se crea una prueba que muestre UB bajo Miri, y después de corregirlo se vuelve a confirmar que esa misma prueba pase
• Un enfoque de probar invariantes del mapa con un model checker como Kani choca con que iddqd es demasiado complejo y la prueba necesaria crece más de lo que la herramienta puede manejar
• Creusot puede ayudar a demostrar que código Rust está libre de panic y otros errores, pero hoy no puede probar invariantes que deben mantenerse incluso si el código del usuario hace panic o se comporta mal
• NaiveMap cumple el papel de especificación más cercana de iddqd, y al ejecutar en CI miles de pruebas basadas en modelos se obtiene una alta confianza en que la implementación coincide con esa especificación
• cargo-anneal es una herramienta en desarrollo de interés porque permitiría poner una prueba de soundness en Lean dentro de un doc comment junto al código unsafe Rust
• iddqd tiene invariantes claros y un alcance limitado pero no trivial, así que es un buen candidato para servir como benchmark de herramientas de verificación formal

Conclusión

• El Rust genérico unsafe es extremadamente difícil porque debe preservar cada invariante incluso frente a implementaciones arbitrarias y adversariales de traits
• El bug de iddqd muestra que una implementación patológica de Ord puede engañar al mapa para crear alias mutables sobre la misma memoria
• Como ninguna técnica por sí sola puede detectar todos los bugs, se combinan razonamiento humano línea por línea sobre unsafe, pruebas basadas en ejemplos, pruebas patológicas, pruebas aleatorias y revisión adversarial con modelos frontier
• Oxide considera que este nivel de rigor está justificado en infraestructura fundacional

[GN⁺]

Comentarios en Lobste.rs

• Si lo entendí bien (lo vi desde el teléfono mientras iba en camino), esto parece resolverse usando un tipo wrapper y HashSet/BTreeSet en lugar de HashMap/BTreeMap
  El tipo wrapper no es estrictamente necesario, pero pensando en la seguridad y el mantenimiento futuro, parece una buena decisión
  Lo único que hace falta es un wrapper de tamaño 0 que envuelva al objeto, con una implementación personalizada de PartialEq/Hash que mire solo los campos relevantes. Si quieres buscar sin construir el valor completo, se puede crear un segundo tipo que implemente AsRef para el tipo de valor
  Esta forma reutiliza tal cual la interfaz existente de HashSet/BTreeSet sin unsafe. En vez de envolver el tipo de valor/clave, también podrías crear un nuevo wrapper de HashSet/BTreeSet que se encargue de ese comportamiento

  • Aquí la clave es una combinación arbitraria de campos y subcampos del tipo de registro, y se expresa con GAT. Además, el patrón de índice entero/slab también se generaliza naturalmente a un mapa con múltiples índices
    También incluye cosas como la API de Entry, acceso mutable/iteración, etc. Dentro de iddqd, la mutabilidad se maneja con bastante cuidado, y en algunos lugares se usan valores atómicos para permitir mutabilidad interna. Ese manejo habría sido bastante difícil sin indirección por índice

• Para verificar formalmente iddqd, al principio yo intentaría usar un model checker como Kani para demostrar que el mapa no rompe sus invariantes internas. Pero me da curiosidad la parte donde dices que iddqd es un poco demasiado complejo para lo que Kani puede manejar, y que la prueba necesaria crece hasta un punto que la herramienta no soporta
  ¿Podrías compartir más detalles sobre esa parte? Me pregunto si significa que la complejidad computacional del algoritmo se degrada al peor caso
  En general, es un caso interesante para métodos formales, y me gustó que tocaras ese tema. Al ver casos exitosos de herramientas de verificación formal ya existentes en proyectos grandes, uno podría pensar ingenuamente que al menos sería posible probar la corrección de una estructura de datos, pero en la práctica se ve que la dificultad varía según la estructura, y que incluso en lenguajes que se consideran más favorables para la demostración que Rust, donde se permite aliasing ilimitado, no es algo fácil en términos prácticos
  Un poco fuera de tema, pero también me da curiosidad cómo hicieron los diagramas. ¿Escribieron un script de una sola vez, o son piezas especiales hechas a medida para el diseño del blog/sitio web de Oxide? No parecen una herramienta genérica

  • Al final del artículo dice “Diagrams courtesy Ben Leonard.”, y Ben Leonard es diseñador de Oxide. Así que probablemente sí sean diagramas hechos a mano
  • Incluso intentando demostrar algo muy básico sobre una implementación de trait concreta y funcional, CBMC se quedaba usando CPU y no terminaba ni después de más de 10 minutos
    También traté de reducir el alcance. Por ejemplo, asumí que hashbrown era correcto, pero eso tampoco ayudó mucho. Para ese punto ya casi me había rendido. Respecto a implementaciones de trait bien portadas, estoy bastante convencido de que iddqd es correcto, y lo que de verdad me interesaba desde el lado de los métodos formales era una prueba que también valiera para implementaciones arbitrarias y defectuosas
    Dicho eso, yo no soy la persona más experta usando Kani. Me encantaría que tú u otra persona lo intentaran
    Primero hice un boceto de los diagramas en Mermaid, y luego el excelente diseñador Ben Leonard los refinó a mano para ajustarlos a nuestra paleta de colores y tema

• El patrón de mapa basado en campos, donde se indexa un objeto usando como clave uno de sus propios campos, es algo que siempre he sentido que también sería bueno poder usar libremente en C#
  Hace tiempo intenté construir algo simple por mi cuenta, pero la interfaz no quedó muy limpia y lo abandoné. Este artículo me da ganas de intentarlo otra vez

  • Sí, es un patrón realmente útil. Lo hice por una necesidad del trabajo, pero después terminé usándolo en todo tipo de lugares, desde codebases de producción como cargo-nextest hasta proyectos personales
    Usar un solo campo como clave es el caso más común, pero iddqd es lo bastante flexible como para usar cualquier combinación de campos, subcampos o funciones puras y baratas de calcular a partir de campos. Por ejemplo, puedes buscar ArtifactKey en https://docs.rs/iddqd/latest/iddqd/ (perdón si no estás familiarizado con la sintaxis de Rust)
    Cuando diseñé iddqd, sentía con fuerza que el usuario debía poder aprovechar todo el poder del sistema de tipos de Rust, sin importar cuántos rodeos tuviera que dar yo como autor de la biblioteca. De verdad quería que iddqd fuera una biblioteca agradable de usar para sus usuarios, especialmente para mis colegas)