Resumen Técnico: Detección Automática de Errores de Conteo de Referencias en Controladores del Kernel Linux

Declaración del Problema

En el kernel monolítico de Linux, los controladores de dispositivos operan al mismo nivel de privilegio que el núcleo del kernel, lo que convierte a los errores en los controladores en un riesgo crítico de seguridad. El conteo de referencias (refcount) es el mecanismo principal utilizado para gestionar manualmente el ciclo de vida de los objetos del kernel. Un refcount rastrea el número de referencias activas a un objeto; un conteo positivo indica que el objeto está en uso, mientras que cero indica que es seguro liberarlo.

Los errores de refcount ocurren cuando el conteo no coincide con el número real de referencias. Conteos de referencia excesivos provocan fugas de memoria, mientras que conteos de referencia insuficientes resultan en vulnerabilidades de uso después de la liberación (UAF). Estos problemas son prevalentes debido a la complejidad de la base de código del kernel (los controladores constituyen aproximadamente el 66.5% del kernel) y a la diversidad de las implementaciones de controladores. Las herramientas de análisis estático existentes a menudo luchan con la escala y la complejidad del kernel de Linux, lo que resulta en altas tasas de falsos positivos o una falta de escalabilidad.

Metodología: DrvHorn

Los autores presentan DrvHorn, una herramienta automatizada novedosa diseñada para detectar errores de refcount específicamente dentro de los controladores del kernel de Linux. La herramienta transforma el problema de verificación de refcount en un problema de verificación de aserciones, aprovechando la interfaz estructurada proporcionada por el kernel de Linux.

Arquitectura Central

DrvHorn opera sobre el código fuente del kernel de Linux compilado a bitcode LLVM. Su flujo de trabajo consta de cuatro etapas principales:

1. Reducción a Verificación de Aserciones:
   En lugar de verificar todo el kernel, DrvHorn se centra en la fase de inicialización del controlador. Aprovecha la observación de que, si la inicialización falla, todos los recursos adquiridos deben liberarse para prevenir fugas. La herramienta genera un objetivo de verificación que llama a la función de inicialización del controlador y afirma que el cambio neto en los refcounts (para dispositivos, nodos del árbol de dispositivos y nodos de firmware) es cero en caso de fallo. Si la aserción falla, se reporta un error.

2. Modelado del Kernel de Linux:
   Para gestionar la complejidad del kernel, DrvHorn reemplaza APIs específicas del kernel con abstracciones simplificadas que preservan el comportamiento del refcount:

   • Árbol de Dispositivos: En lugar de modelar las estructuras de punteros complejas de struct device_node, DrvHorn modela las APIs (por ejemplo, of_get_next_child, of_find_node_by_name) basándose en cuatro tipos distintos de comportamiento (devolver NULL, devolver no NULL, decrementar el refcount, o no decrementar).
   • Dispositivos y Buses: Las APIs que devuelven dispositivos con incremento de refcount (por ejemplo, usb_find_interface) se modelan para devolver punteros a regiones de memoria específicas y no aliasadas, determinadas por el argumento del bus, lo que previene violaciones de aliasing espurias.
   • Gestión de Recursos del Dispositivo (Devres): La herramienta simplifica __devm_add_action() invocando inmediatamente la función de limpieza asociada después del punto de llamada, en lugar de rastrear explícitamente la lista de devres.

3. Segmentación de Programas Agresiva:
   La Eliminación de Código Muerto (DCE) estándar es insuficiente para la escala del kernel. DrvHorn implementa una técnica de segmentación personalizada y agresiva:

   • Argumentos Esenciales: Los argumentos que incrustan struct kref que pueden modificar los refcounts se marcan como esenciales.
   • Recopilación de Instrucciones: La herramienta recopila recursivamente las instrucciones necesarias para la verificación de refcount, incluidas las ramas, retornos y llamadas donde los parámetros dependen de argumentos esenciales.
   • Reemplazo de No Esenciales: Las instrucciones que no se consideran necesarias se eliminan. Las llamadas a funciones con resultados no esenciales se reemplazan con valores no deterministas (usando el atributo writeonly de LLVM para mitigar la pérdida de efectos secundarios).

4. Verificación Basada en CHC:
   El problema de aserción reducido se resuelve utilizando SeaHorn, un solucionador de Cláusulas de Horn con Restricciones (CHC). Los autores eligieron SeaHorn sobre los verificadores de modelos acotados (como SeaBMC) porque los solucionadores CHC son más adecuados para manejar los bucles comunes en las manipulaciones de refcount sin requerir límites manuales de desenrollado de bucles.

Contribuciones Clave

• Invariante Novel: La derivación de un invariante universal de refcount aplicable a todos los controladores: la diferencia de refcount debe ser cero cuando falla la inicialización del controlador.
• Herramienta Automatizada: El desarrollo de DrvHorn, que integra el modelado del kernel, la segmentación agresiva y la resolución CHC para lograr una detección totalmente automatizada.
• Escalabilidad y Precisión: La capacidad de analizar miles de controladores con una tasa de falsos positivos significativamente menor en comparación con herramientas anteriores de vanguardia.
• Impacto en el Mundo Real: El descubrimiento y la corrección de errores previamente desconocidos en el kernel de Linux.

Resultados de la Evaluación

Los autores evaluaron DrvHorn en 3.387 controladores de plataforma en el kernel Linux v6.6 x86-64 (compilado con allyesconfig).

• Detección de Errores: DrvHorn reportó 777 errores potenciales.
• Validación: La inspección manual confirmó 545 como errores reales.
• Falsos Positivos: Hubo 232 falsos positivos, lo que resultó en una tasa de falsos positivos del 29.9%. Los autores señalan que 27 de estos fueron causados por falta de solidez en la política de segmentación (flujo de información indirecto), mientras que la mayoría se debió a un análisis de punteros conservador en el modelo de memoria del solucionador.
• Novelty: 424 de los errores confirmados eran previamente desconocidos.
• Fusiones en la Rama Principal: Los autores enviaron parches para los errores descubiertos, y 45 fueron fusionados en el kernel de Linux.
• Falsos Negativos: Las pruebas contra 17 errores conocidos corregidos desde la versión v6.6 mostraron que DrvHorn solo omitió uno (debido a limitaciones de segmentación en cuanto al flujo de información indirecto), lo que sugiere una baja tasa de falsos negativos.
• Tiempo de Espera: La herramienta agotó el tiempo de espera en 807 controladores (límite de 300 segundos), a menudo debido a bucles anidados complejos en funciones de utilidad.
• Comparación: Al compararse con SeaBMC (verificación de modelos acotados), SeaBMC omitió el 39.4% de los errores reales encontrados por DrvHorn y agotó el tiempo de espera en el 24.2% de ellos, confirmando la superioridad del enfoque basado en CHC para esta tarea específica.

Significado y Afirmaciones

El artículo afirma que DrvHorn logra un equilibrio de escalabilidad y precisión que las herramientas anteriores han luchado por alcanzar en el diverso ecosistema de controladores de Linux. Al centrarse específicamente en los controladores y aprovechar la interfaz de controladores del kernel para derivar un invariante simple, la herramienta evita la necesidad de invariantes complejos y específicos de subsistemas que a menudo plagian otros esfuerzos de verificación.

Los autores enfatizan que, aunque DrvHorn no es ni sólido ni completo (puede omitir errores o reportar falsos positivos), su utilidad práctica se demuestra por el alto número de errores reales y previamente desconocidos descubiertos y la correcta integración aguas arriba de las correcciones. La herramienta representa un paso significativo hacia la verificación estática totalmente automatizada y de alta precisión de los controladores del kernel de Linux, abordando un vector de vulnerabilidad de seguridad crítico.

Limitaciones Reconocidas:

• La herramienta se centra actualmente en la fase de inicialización; la extensión a funciones de limpieza/terminación se deja para trabajos futuros.
• Actualmente no verifica los refcounts para tipos distintos a struct kref.
• La tasa de falsos positivos, aunque menor que en estudios anteriores, sigue siendo no trivial (29.9%), en gran parte debido al modelado de memoria conservador en el solucionador.
• El flujo de información indirecto no se captura completamente por la política de segmentación, lo que conduce a algunos errores omitidos y falsos positivos.