Un equipo de la empresa Basis ha empleado modelos de lenguaje de gran tamaño (LLM) para verificar formalmente el compilador y optimizador de nftables, el cortafuegos integrado en el núcleo de Linux desde 2014. Durante el proceso, en el que reimplementaron la herramienta en el asistente de pruebas Rocq, descubrieron dos errores que afectan a todas las versiones de Linux distribuidas desde 2022 y que ya fueron comunicados a los responsables del proyecto.
El primer fallo reside en la fusión de campos de tipo bitmask. El optimizador combina dos reglas como «tcp flags syn drop» y «tcp flags ack drop» en una sola «tcp flags { syn, ack } drop». Sin embargo, la semántica del lenguaje de nftables define la consulta contra un conjunto como una coincidencia exacta, de modo que el paquete solo se descarta si su byte de indicadores es exactamente SYN o exactamente ACK, y no si esos bits están simplemente activados. El resultado es que una política restrictiva se transforma silenciosamente en otra mucho más permisiva.
El segundo fallo aparece al fusionar rangos de direcciones solapados en un mapa de veredictos. El optimizador genera un mapa cuyas claves se solapan, por lo que el núcleo rechaza el conjunto de reglas con un error de intervalos en conflicto y el usuario no puede instalarlo.
Basis comprobó además que el fallo más grave no se detectaría con una búsqueda de bugs basada en LLM de forma naive, lo que subraya el valor de combinar modelos generativos con verificación formal para reforzar infraestructuras críticas.