Bug del borrow checker de Rust: qué significa la soundness

El sistema de tipos de Rust hace una promesa firme: si tu código seguro compila, no puede tener punteros colgantes, carreras de datos ni use-after-free. Por eso, cuando un issue de GitHub mostró un fragmento de Rust aparentemente seguro que imprime basura sacada de un frame de pila ya muerto, y resultó que el agujero llevaba once años en el borrow checker de Rust, mucha gente sintió que el suelo se movía. El bug permite que los requisitos de lifetime de un struct se cuelen mediante una asignación de campo covariante, y con una implementación maliciosa de Drop puedes guardar una referencia a una variable local en un global y leerla después de que la variable ya no exista. AddressSanitizer lo llama stack-use-after-scope. El compilador lo dio por bueno.

Las reacciones fueron previsibles. Algunos dieron por muerta la historia de seguridad de Rust. Otros se encogieron de hombros: los bugs pasan. Ambas posturas se pierden lo realmente interesante. Este bug es un experimento natural limpio sobre lo que valen las garantías estáticas, dónde fallan los razonamientos informales y por qué la distancia entre «el sistema de tipos es sólido» y «el compilador impone un sistema de tipos sólido» es donde viven los bugs más interesantes. Así que vamos a poner a prueba cada una de las creencias comunes que esta historia ha removido.

Mito 1: Un bug de unsoundness significa que el modelo de seguridad de Rust falló

El primer instinto es tratarlo como una grieta en la teoría. No lo es. Nadie reescribió las reglas de los lifetimes. Nadie descubrió que el ownership y el borrowing estén fundamentalmente rotos. El sistema de tipos de Rust, tal como se diseñó en pizarrones y en los RFC, dice que este programa debe rechazarse. Simplemente, el compilador no lo rechazó.

Esa distinción entre especificación e implementación es una de las fallas más antiguas de nuestro campo. Tony Hoare nos dio una teoría preciosa de los procesos secuenciales comunicantes; durante décadas, los compiladores de C compilaron mal código que era perfectamente válido según el estándar. La teoría se sostiene mientras el artefacto pierde agua. Ya hemos escrito sobre cómo la brecha entre especificación e implementación es donde viven los bugs, y este es un caso de libro. Las reglas de lifetime no estaban mal. El código de inferencia de varianza en rustc, la parte que decide cuándo es legal sustituir un &'a T donde se espera un &'static T, tenía un hueco cuando la asignación fluía a través de un campo covariante.

Esta es la forma del exploit, simplificada. Construyes un wrapper cuya implementación de Drop copia su payload a un almacén global 'static. Normalmente el compilador obliga a que el payload sea 'static, así que no pueden entrar referencias a locales. El bug permite blanquear una referencia de vida corta mediante una asignación covariante, de modo que el wrapper termina guardando &l donde l es un 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 línea individual parece inocente. La unsoundness solo existe en la composición: un campo covariante, una asignación que relaja una cota de lifetime y un Drop que mueve el payload a un lugar donde sobrevive a su referente. Esa es la firma de los bugs de implementación en los checkers: el invariante es global, pero la aplicación es local, y una ruta de código se olvidó de comprobar.

Así que no, el modelo de seguridad no falló. Falló la aplicación del modelo de seguridad. Es un fallo más pequeño, pero, como veremos, no es trivial.

Mito 2: Que haya pasado once años sin detectarse significa que el bug es inofensivo

El razonamiento de triaje del propio equipo de Rust fue más o menos este: sería P-crítico si la gente lo estuviera encontrando, pero once años sin avistamientos significan que no puede ser fácil de disparar, así que es P-alto. Hay algo de verdad en eso. Para causar realmente una corrupción de memoria necesitas una implementación de Drop deliberadamente retorcida que mueva datos a una ubicación 'static. Casi nadie escribe eso. La superficie de exposición accidental es minúscula.

Pero «rara vez se dispara por accidente» está cargando mucho peso en esa frase. Las garantías de seguridad no son solo cuestión de accidentes: son lo que puedes dar por sentado cuando el código que te rodea no es amigable. Todo el sentido de un sistema de tipos sólido es que puedes razonar de forma modular: no necesito auditar tu implementación de Drop, porque el compilador ya demostró que ciertas composiciones malas son inexpresables. Una vez que hay un agujero, esa modularidad desaparece. Una dependencia maliciosa, o una dependencia sutilmente incorrecta de un autor bienintencionado, ahora puede hacer algo que el lenguaje prometía imposible.

La historia está llena de bugs «no explotables» que se volvieron muy explotables en cuanto apareció el gadget adecuado. La pregunta práctica, como señaló un comentarista, es si arreglar esto romperá algún crate real del ecosistema, y la respuesta probablemente sea «muy pocos o ninguno», que es buena noticia. Pero la lección correcta de once años silenciosos no es «el bug era inofensivo». Es que la ausencia de evidencia no es evidencia de ausencia, sobre todo para modos de fallo que requieren intención en lugar de azar.

Mito 3: Con suficientes ojos, todos los bugs son superficiales

Este es el mito que más debería avergonzarnos. rustc es uno de los compiladores más escrutados jamás escritos. Es de código abierto, tiene un equipo dedicado de tipos, una comunidad académica activa (RustBelt nos dio hace años un modelo formal de un núcleo de Rust) y millones de usuarios que lo estresan a diario. Y aun así, un agujero de soundness estuvo en la inferencia de lifetimes durante más de una década, atravesando reescrituras completas de la maquinaria que lo rodeaba.

La Ley de Linus asume que los ojos miran el lugar correcto y tienen el modelo correcto en la cabeza. Las unsoundness de sistemas de tipos desbaratan ambas suposiciones. Viven en la intersección de varias características (varianza, orden de drop, coerción, cotas de traits) y cada característica es localmente correcta. Quienes revisan leen el código y ven el invariante previsto, porque el código lo escribieron personas que también veían ese invariante previsto. El sesgo de confirmación está incorporado en el proceso. El contraejemplo exige pensar como un adversario, y pensar de forma adversaria sobre tus propias abstracciones es genuinamente difícil.

Existe todo un sitio, counterexamples.org, que cataloga formas en que reglas de tipos con apariencia plausible se rompen, y el hilo común es la mutabilidad combinada con algo más delicado: exactamente la forma de este bug. No son lecciones nuevas. El sistema de tipos de ML tuvo una famosa unsoundness alrededor de referencias mutables y polimorfismo, que se corrigió con la restricción de valor. Los arrays de Java son covariantes y pueden lanzar ArrayStoreException en tiempo de ejecución porque los diseñadores del lenguaje eligieron la comodidad sobre la soundness. Cuanto más cambia todo, más las mismas tres características (subtipado, mutación y genéricos) se combinan para morder a alguien. Si disfrutas este tipo de arqueología, la historia de sesenta años de Lisp muestra cuánto tiempo llevan evolucionando estas ideas, y las viejas reglas de Rob Pike sobre la simplicidad se leen distinto cuando te das cuenta de que la complejidad es donde nacen los agujeros de soundness.

Los ojos ayudan. No bastan. La postura honesta, que escuché de alguien que construye su propio lenguaje, se parece más a esto: ninguna cantidad de revisión resuelve todos los problemas, así que necesitas métodos mecánicos que no se cansen y que no compartan tus suposiciones.

Mito 4: El razonamiento informal es básicamente una prueba

Cuando se diseñaron las reglas de lifetime de Rust, se argumentaron con cuidado, por gente lista, con muchos ejemplos. Eso es razonamiento informal, y así se construyen prácticamente todos los compiladores de producción. El resultado es un sistema que es sólido hasta donde cualquiera puede saber, lo cual, como hemos aprendido dos veces, no es lo mismo que ser sólido.

La brecha entre ambas cosas es donde entran proyectos como RustBelt y el trabajo en curso sobre un solver de traits de nueva generación. RustBelt, construido en Coq (ahora Rocq) sobre el framework de lógica de separación Iris, verificó con máquina un modelo de las reglas de tipado centrales de Rust, incluidas las partes delicadas como las fronteras de abstracción de unsafe. Fue un hito. Pero fíjate en lo que demostró: un modelo de Rust, no rustc. La prueba cubre el cálculo λRust, y el compilador de producción se ha desviado, ha crecido en funcionalidades y ha acumulado decisiones de implementación que nadie volvió a verificar. Este issue es la factura que llega por esa deriva.

Formalizar un compilador de producción completo es brutalmente caro. CompCert, el compilador de C verificado formalmente, requirió años de esfuerzo experto para un lenguaje mucho más pequeño que Rust, y verifica las pasadas de compilación en lugar de demostrar que el sistema de tipos del código fuente atrapa todos los programas malos. Nadie va a escribir una prueba en Coq de los dos millones de líneas de rustc. El camino realista se parece más a una defensa en profundidad:

• Modelos verificados por máquina de las reglas centrales (al estilo RustBelt), para que la teoría en sí no tenga agujeros.
• Fuzzing sistemático y herramientas de análisis de casos que generan programas adversarios: las esquinas de interacción entre características que los humanos no piensan en probar.
• Pruebas de mutación y basadas en propiedades del checker: si invertir una cota debería hacer fallar un programa, verifica que efectivamente falle. La cultura de testing de SQLite es el modelo aquí.
• Una lista mantenida de problemas de unsoundness conocidos (Rust tiene más de cien etiquetados) tratada como un backlog con prioridad de ingeniería, no como folclore.

Curiosamente, la búsqueda basada en LLM podría terminar siendo un beneficio neto: una herramienta que compone características de forma perversa de manera incansable es exactamente el adversario que le falta al razonamiento informal. El final que muchos esperamos es un Rust especificado formalmente, con un checker probado contra esa especificación, pero mientras tanto, el trabajo es un esfuerzo arduo, poco glamuroso, de resolución de restricciones.

Mito 5: Si la soundness no es absoluta, la seguridad estática es una estafa

La lectura cínica va así: Rust prometió seguridad, la promesa tenía una laguna, luego la promesa era marketing y más vale volver a hacer YOLO con punteros en C. Esto está exactamente al revés, y vale la pena explicar por qué con cierta precisión.

La soundness en un sistema de tipos es un teorema sobre un objeto matemático. Lo que un lenguaje de producción te da es una garantía estadística y económica: clases enteras de bugs (use-after-free, carreras de datos, invalidación de iteradores) pasan de ser «radiación de fondo constante de tu base de código» a eventos tan raros que llegan a la portada cuando se encuentran tras once años. Compara las tasas base. Los bugs de seguridad de memoria en grandes bases de código de C y C++ representan la mayoría de los CVE graves año tras año, y ya nadie se sorprende por ninguno en particular. Los bugs de unsoundness de Rust son tan raros que cada uno obtiene su propio issue de GitHub, su propio hilo de discusión y su propia cultura de postmortem. La rareza que puedes enumerar es un mundo distinto de la rareza que no puedes.

También hay una diferencia en cómo se acumulan los fallos. En C, cada línea es un posible riesgo de seguridad de memoria, así que el costo de la vigilancia escala con el tamaño del código para siempre. En Rust, la vigilancia se concentra en los bordes: bloques unsafe, FFI y (como ahora sabemos) el propio checker del compilador. Esa concentración es lo que hace manejable la auditoría, herramientas como Miri y los métodos formales. La garantía no es binaria; es una reconfiguración drástica de dónde vive tu riesgo.

Un sistema de tipos con un bug conocido que once años de tráfico en producción nunca alcanzaron sigue siendo infinitamente más fuerte que un lenguaje donde el bug es el diseño.

Qué deberías llevarte realmente

Si escribes Rust, no necesitas cambiar nada. Tu código no era silenciosamente inseguro antes de que se abriera este issue; la ruta práctica de explotación requería intención. Si mantienes librerías, el movimiento honesto es el de siempre: mantén pequeña la superficie de unsafe, ejecuta Miri en las partes complicadas y no trates al borrow checker como un oráculo para el código malicioso de otros; trátalo como una herramienta extremadamente confiable para atrapar tus propios errores.

Si construyes lenguajes o compiladores, este bug es un regalo: un ejemplar raro y bien documentado de cómo la soundness realmente falla en producción. No en la teoría, sino en la aplicación; no en una sola característica, sino en la intersección de características; no atrapado por la revisión, sino por construcción adversaria. Los equipos que se toman esto en serio, financiando reescrituras del solver de traits, retrabajos de restricciones de regiones y herramientas cercanas a la verificación, son los que dentro de diez años tendrán garantías que signifiquen algo.

Y para todos: recalibra lo que es una garantía. Durante décadas hemos confundido «probado» con «argumentado convincentemente y nunca contradicho todavía», en sistemas de tipos, protocolos criptográficos y consenso distribuido. La versión adulta de la confianza no consiste en asumir que el puente es perfecto. Consiste en saber que el puente tiene inspectores que publican sus hallazgos, arreglan lo que encuentran y mantienen una lista pública de las grietas que todavía no han reparado. En ese sentido, que hayan pasado once años hasta encontrar un agujero no es una acusación. Es la evidencia de que el sistema, el humano que rodea al compilador, funciona más o menos como debería.