En Linux 5.20/6.0 propone un mecanismo para verificar la corrección del kernel

Hace poco se dio a conocer la noticia que se ha realizado una propuesta para ser incluido en el kernel de Linux 5.20 (o quizás la rama se numerará 6.0, todo depende de la decisión de Linus torvalds debido a su comentario que realizo en el lanzamiento del Kernel 5.19).

La propuesta realizada es sobre un conjunto de parches con la implementación del mecanismo RV (Runtime Verification), que es un medio para verificar el correcto funcionamiento en sistemas altamente confiables que garantizan la ausencia de fallos.

La validación se realiza en tiempo de ejecución al adjuntar controladores a puntos de rastreo que verifican el progreso real de la ejecución contra un modelo determinista de referencia predefinido del autómata que determina el comportamiento esperado del sistema.

El desarrollador de Linux, Daniel Bristot de Oliveira menciona:

Durante los últimos años, he estado explorando la posibilidad de verificar el comportamiento del kernel de Linux usando Runtime Verification.

Runtime Verification (RV) es un método ligero (pero riguroso) que complementa las técnicas clásicas de verificación exhaustiva (como la comprobación de modelos y la demostración de teoremas) con un enfoque más práctico para sistemas complejos. En lugar de depender de un modelo detallado de un sistema (por ejemplo, una reimplementación de un nivel de instrucción), RV funciona analizando el rastro de la ejecución real del sistema, comparándolo con una especificación formal del comportamiento del sistema.

El uso de autómatas deterministas para RV es un enfoque bien establecido. En el caso específico del kernel de Linux, puede consultar cómo modelar el comportamiento complejo del kernel de Linux con este artículo:

De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Rómulo Silva. *Verificación formal eficiente para el kernel de Linux.* En: Conferencia Internacional sobre Ingeniería de Software y Métodos Formales. Springer, Cham, 2019. pág. 315-332.

Y cuán eficiente es este enfoque aquí:

De Oliveira, Daniel B.; De Oliveira, Rómulo S.; Cucinotta, Tommaso. *Un modelo de sincronización de subprocesos para el kernel de Linux PREEMPT_RT.* Journal of Systems Architecture, 2020, 107: 101729.

TLDR: es posible modelar comportamientos complejos de forma modular, con una sobrecarga aceptable (incluso para sistemas de producción).

Se menciona que la información de los puntos de rastreo mueve el modelo de un estado a otro, y si el nuevo estado no coincide con los parámetros del modelo, se genera una advertencia o el kernel entra en un estado «panic» (suponiendo que los sistemas altamente confiables detectarán y responderán a tales situaciones).

El modelo de autómata que define las transiciones de un estado a otro se exporta al formato «dot» (graphviz), después de lo cual se traduce utilizando la utilidad dot2c en una representación C, que se carga en forma de un módulo kernel que rastrea las desviaciones. de la ejecución a partir de un modelo predefinido.

La verificación de modelos en tiempo de ejecución se posiciona como un método más liviano y fácil de implementar para verificar la corrección de la ejecución en sistemas de misión crítica, que complementa los métodos clásicos de verificación de confiabilidad, como la verificación de modelos y las pruebas matemáticas del cumplimiento del código con las especificaciones dadas en un lenguaje formal.

El mantenedor del subsistema de seguimiento, Steven Rostedt, lo resumió así:

» Este es el cambio más grande para esta solicitud de extracción. Introduce la verificación en tiempo de ejecución que es necesaria para ejecutar Linux en sistemas críticos para la seguridad. Permite que se inserten modelos de autómatas deterministas en el kernel que se adjuntará a los puntos de seguimiento, donde la información sobre estos puntos de seguimiento moverá el modelo de un estado a otro.

Entre las ventajas que se mencionan de RV se destaca que está la capacidad de proporcionar una verificación rigurosa sin una implementación separada de todo el sistema en un lenguaje de modelado, así como una respuesta flexible a eventos imprevistos, por ejemplo, para bloquear la propagación de una falla en sistemas críticos.

Finalmente si estás interesado en poder conocer más al respecto, puedes consultar los detalles en el siguiente enlace.

Fuente: https://www.phoronix.com/