Hispanopedia Wiki
Los controladores de dispositivos son programas que permiten que el software o los programas informáticos de nivel superior interactúen con un dispositivo de hardware . Estos componentes de software actúan como enlace entre los dispositivos y los sistemas operativos , comunicándose con cada uno de ellos y ejecutando comandos. Proporcionan una capa de abstracción para el software superior y también median la comunicación entre el núcleo del sistema operativo y los dispositivos inferiores.
Por lo general, los sistemas operativos incluyen soporte para los controladores de dispositivos más comunes, y los fabricantes de hardware suelen proporcionar los controladores para sus dispositivos en la mayoría de las plataformas. El rápido crecimiento de los dispositivos de hardware y la complejidad de los componentes de software han hecho que el desarrollo de controladores sea engorroso y complejo. A medida que el tamaño y la funcionalidad de los controladores aumentaron, estos se convirtieron en un factor clave para definir la fiabilidad del sistema. Esto impulsó la síntesis y verificación automáticas de los controladores. Este artículo analiza algunos enfoques para la síntesis y verificación de controladores.
Motivación para la síntesis y verificación automática de controladores
Los controladores de dispositivos son el principal componente que falla en la mayoría de los sistemas. El proyecto Berkeley Open Infrastructure for Network Computing (BOINC) descubrió que los fallos del sistema operativo se deben principalmente a un código de controlador de dispositivo mal escrito. [ 1 ] En Windows XP , los controladores representan el 85 % de los fallos reportados. En el kernel de Linux 2.4.1, el código del controlador de dispositivos representa aproximadamente el 70 % del tamaño del código. [ 2 ] El fallo del controlador puede provocar el fallo de todo el sistema, ya que se ejecuta en modo kernel . Estos hallazgos dieron lugar a diversas metodologías y técnicas para la verificación de controladores de dispositivos. Una alternativa fue desarrollar técnicas que pudieran sintetizar controladores de dispositivos de forma robusta. Una menor intervención humana en el proceso de desarrollo y una especificación adecuada del dispositivo y los sistemas operativos pueden conducir a controladores más fiables.
Otra motivación para la síntesis de controladores es la gran cantidad de variantes de sistemas operativos y combinaciones de dispositivos. Cada una de ellas tiene su propio conjunto de controles de entrada/salida y especificaciones , lo que dificulta la compatibilidad de los dispositivos de hardware con cada sistema operativo. Por lo tanto, para poder usar un dispositivo con un sistema operativo, se requiere la disponibilidad de la combinación de controladores correspondiente. Los fabricantes de hardware suelen proporcionar controladores para Windows, Linux y Mac OS, pero debido a los altos costos de desarrollo o adaptación y a las dificultades de soporte técnico , no pueden proporcionar controladores para todas las plataformas. Una técnica de síntesis automatizada puede ayudar a los fabricantes a proporcionar controladores compatibles con cualquier dispositivo en cualquier sistema operativo.
Verificación de los controladores de dispositivos
Existen dos desafíos que limitan las pruebas de los controladores de dispositivos.
- Es muy difícil determinar la operación o el momento exacto en que se produce un fallo en la interacción entre el controlador y el núcleo. El sistema podría entrar en un estado inconsistente y el fallo se reportaría mucho tiempo después, lo que dificultaría determinar la causa real del mismo.
- Los controladores que funcionan correctamente en circunstancias normales pueden fallar en casos raros y excepcionales, y las técnicas de prueba tradicionales pueden no ser útiles para detectar el comportamiento de los controladores en casos extremos.
La ola de verificación de controladores de dispositivos fue iniciada por Microsoft a través de su proyecto SLAM ya en el año 2000. La motivación del proyecto fue que se detectaron 500 000 fallos diarios causados por un solo controlador de vídeo, lo que generó preocupación por la gran vulnerabilidad que suponía el uso de controladores de dispositivos complejos. Para más detalles, consulte el discurso de Bill Gates. Desde entonces, se han propuesto numerosas técnicas estáticas y de tiempo de ejecución para la detección y el aislamiento de errores.
Análisis estático
El análisis estático consiste en analizar el programa para comprobar si cumple con las propiedades críticas de seguridad especificadas. Por ejemplo, el software del sistema debe cumplir con reglas como "verificar los permisos del usuario antes de escribir en las estructuras de datos del kernel", "no hacer referencia a punteros nulos sin comprobar", "prohibir el desbordamiento del tamaño del búfer", etc. Estas comprobaciones pueden realizarse sin ejecutar el código que se está revisando. El proceso de prueba tradicional (ejecución dinámica) requiere escribir muchos casos de prueba para ejercitar estas rutas y llevar al sistema a estados de error. Este proceso puede ser largo y laborioso, y no es una solución práctica. Otro enfoque teóricamente posible es la inspección manual, pero resulta impracticable en sistemas modernos con millones de líneas de código, lo que hace que la lógica sea demasiado compleja para ser analizada por humanos.
Técnicas de compilación
Las reglas que tienen una correspondencia directa con el código fuente se pueden verificar mediante un compilador. Las infracciones de reglas se pueden detectar comprobando si la operación en el código fuente carece de sentido. Por ejemplo, reglas como "habilitar una interrupción después de haber sido deshabilitada" se pueden verificar analizando el orden de las llamadas a funciones. Sin embargo, si el sistema de tipos del código fuente no puede especificar las reglas en su semántica, los compiladores no pueden detectar errores de ese tipo. Muchos lenguajes con tipado seguro permiten que el compilador detecte las infracciones de seguridad de memoria resultantes de conversiones de tipo inseguras.
Otro enfoque consiste en utilizar la compilación de metanivel (MC) [ 3 ] . Los metacompiladores diseñados para este fin pueden extender los compiladores con verificadores y optimizadores ligeros y específicos del sistema. Estas extensiones deben ser escritas por los implementadores del sistema en un lenguaje de alto nivel y enlazadas dinámicamente a los compiladores para realizar un análisis estático riguroso.
Verificación de modelos de software
La verificación de modelos de software es el análisis algorítmico de programas para probar propiedades de su ejecución. [ 4 ] Esto automatiza el razonamiento sobre el comportamiento del programa con respecto a las especificaciones correctas dadas. La verificación de modelos y la ejecución simbólica se utilizan para verificar las propiedades críticas de seguridad de los controladores de dispositivos. La entrada al verificador de modelos es el programa y las propiedades de seguridad temporal. La salida es la prueba de que el programa es correcto o una demostración de que existe una violación de la especificación mediante un contraejemplo en forma de una ruta de ejecución específica.
La herramienta SDV (Static Driver Verifier) [ 5 ] de Microsoft utiliza análisis estático para controladores de dispositivos Windows. El motor de análisis de back-end SLAM utiliza comprobación de modelos y ejecución simbólica para la verificación estática en tiempo de compilación. Las reglas que deben observar los controladores para cada API se especifican en un lenguaje similar a C, SLIC (Specification Language for Interface Checking). El motor de análisis encuentra todas las rutas que pueden conducir a violaciones de las reglas de uso de la API y las presenta como rutas de error a nivel de código fuente a través del código fuente del controlador. Internamente, abstrae el código C en un programa booleano y un conjunto de predicados que son reglas que deben observarse en este programa. Luego, utiliza la comprobación de modelos simbólicos [ 6 ] para validar los predicados en el programa booleano.
El verificador de modelos BLAST (Berkeley Lazy Abstraction Software verification Tool) [ 7 ] se utiliza para detectar errores de seguridad de memoria y bloqueo incorrecto en el código del kernel de Linux. Emplea un algoritmo de abstracción denominado abstracción perezosa [ 8 ] para construir el modelo a partir del código C del controlador. Ha demostrado su eficacia en la verificación de propiedades de seguridad temporal de programas C con hasta 50 000 líneas de código. También se utiliza para determinar si un cambio en el código fuente afecta la prueba de propiedad en la versión anterior, y se ha demostrado su funcionamiento en un controlador de dispositivo de Windows.
Avinux [ 9 ] es otra herramienta que facilita el análisis automático de unidades de dispositivos Linux y está construida sobre el verificador de modelos acotado CBMC . [ 10 ] Existen métodos de localización de fallos para encontrar la ubicación del error, ya que estas herramientas de verificación de modelos devuelven un rastro de contraejemplos largo y es difícil encontrar la ubicación exacta del fallo. [ 11 ]
Análisis en tiempo de ejecución
El análisis dinámico de programas se realiza ejecutando el programa con suficientes entradas de prueba para producir comportamientos interesantes. Safe Drive [ 12 ] es un sistema de bajo consumo de recursos para detectar y recuperarse de violaciones de seguridad de tipos en controladores de dispositivos. Con solo un 4 % de cambios en el código fuente de los controladores de red de Linux, pudieron implementar SafeDrive y brindar una mejor protección y recuperación al kernel de Linux. Un proyecto similar que utiliza hardware para aislar los controladores de dispositivos del kernel principal es Nook. [ 13 ] Colocan los controladores de dispositivos en un dominio de protección de hardware separado llamado "nooks" y tienen una configuración de permisos separada para cada página, asegurando que un controlador no modifique páginas que no estén en su dominio pero puede leer todos los datos del kernel ya que comparten el mismo espacio de direcciones.
Otro trabajo similar en este campo trata sobre la recuperación automática de sistemas operativos debido a fallos en los controladores. Minix 3 [ 14 ] es un sistema operativo que puede aislar fallos importantes, detectar defectos y reemplazar componentes defectuosos sobre la marcha.
Síntesis de controladores de dispositivos
Una alternativa a la verificación y el aislamiento de fallos consiste en implementar técnicas en el proceso de desarrollo de controladores de dispositivos para hacerlo más robusto. A partir de las especificaciones del dispositivo y las funciones del sistema operativo, un método consiste en sintetizar el controlador para dicho dispositivo. Esto ayuda a reducir los errores humanos, así como el coste y el tiempo necesarios para desarrollar el software del sistema. Todos los métodos de síntesis se basan en algún tipo de especificación proporcionada por los fabricantes del hardware y las funciones del sistema operativo.
lenguajes de especificación de interfaz
El código operativo del hardware suele ser de bajo nivel y propenso a errores. El ingeniero de desarrollo de código se basa en la documentación del hardware, que normalmente contiene información imprecisa o inexacta. Existen varios lenguajes de definición de interfaz (IDL) para expresar las funcionalidades del hardware. Los sistemas operativos modernos utilizan estos IDL para integrar componentes o para ocultar la heterogeneidad, como en el caso de las llamadas a procedimientos remotos (RPL). Lo mismo se aplica a las funcionalidades del hardware. En esta sección, analizaremos la escritura de controladores de dispositivos en lenguajes específicos de dominio, lo que ayuda a abstraer la codificación de bajo nivel y a utilizar compiladores específicos para generar el código.
Devil [ 15 ] permite una definición de alto nivel de la comunicación con el dispositivo. Los componentes de hardware se expresan como puertos de E/S y registros mapeados en memoria. Estas especificaciones se convierten luego en un conjunto de macros C que se pueden llamar desde el código del controlador, eliminando así el error que el programador podría cometer al escribir funciones de bajo nivel. NDL [ 16 ] es una mejora de Devil que describe el controlador en términos de su interfaz operativa. Utiliza la sintaxis de definición de interfaz de Devil e incluye un conjunto de definiciones de registros, protocolos para acceder a esos registros y una colección de funciones del dispositivo. Las funciones del dispositivo se traducen luego en una serie de operaciones sobre esa interfaz. Para generar un controlador de dispositivo, primero se deben escribir las funcionalidades del controlador en estos lenguajes de especificación de interfaz y luego usar un compilador que generará el código del controlador de bajo nivel.
HAIL (Hardware Access Interface Language) [ 17 ] es otro lenguaje de especificación de controladores de dispositivos específico del dominio. El desarrollador del controlador necesita escribir lo siguiente.
- Descripción del mapa de registros, que describe los distintos registros y campos de bits del dispositivo a partir de la hoja de datos del dispositivo.
- Descripción del espacio de direcciones para acceder al autobús.
- Instanciación del dispositivo en el sistema particular.
- Especificación invariante, que restringe el acceso al dispositivo.
El compilador HAIL toma estas entradas y traduce la especificación a código C.
codiseño de hardware y software
En el codiseño de hardware y software, el diseñador especifica la estructura y el comportamiento del sistema mediante máquinas de estados finitos que se comunican entre sí. Posteriormente, se realizan una serie de pruebas, simulaciones y verificaciones formales en estas máquinas de estados antes de decidir qué componentes se integran en el hardware y cuáles en el software. El hardware se suele implementar en matrices de puertas programables en campo (FPGA) o circuitos integrados de aplicación específica (ASIC), mientras que el software se traduce a un lenguaje de programación de bajo nivel. Este enfoque se aplica principalmente a sistemas embebidos, que se definen como un conjunto de partes programables que interactúan continuamente con el entorno mediante sensores. Las técnicas existentes [ 18 ] están destinadas a generar microcontroladores sencillos y sus controladores.
Síntesis de controladores independientes
En la síntesis independiente, tanto el dispositivo como el software del sistema se desarrollan por separado. El dispositivo se modela utilizando cualquier lenguaje de descripción de hardware (HDL), y el desarrollador de software no tiene acceso a las especificaciones HDL. Los desarrolladores de hardware definen la interfaz del dispositivo en la hoja de datos. A partir de esta hoja, el desarrollador del controlador extrae la distribución de registros y memoria del dispositivo, así como el modelo de comportamiento en forma de máquinas de estados finitos . Esto se expresa en los lenguajes específicos de dominio descritos en la sección de lenguaje de interfaz. El paso final consiste en generar el código a partir de estas especificaciones.
La herramienta Termite [ 19 ] toma tres especificaciones para generar el controlador.
- Especificación del dispositivo : La especificación de los registros, la memoria y los servicios de interrupción del dispositivo se obtiene de la hoja de datos del dispositivo.
- Especificación de la clase de dispositivo : Esta se puede obtener del estándar del protocolo de E/S del dispositivo correspondiente. Por ejemplo, para Ethernet, el estándar Ethernet LAN describe el comportamiento común de estos dispositivos controladores. Generalmente, esto se codifica como un conjunto de eventos, como la transmisión de paquetes, la finalización de la negociación automática y el cambio de estado del enlace, entre otros.
- Especificación del sistema operativo : Describe la interfaz del sistema operativo con el controlador. Más específicamente, especifica las solicitudes que el sistema operativo puede realizar al controlador, el orden de estas solicitudes y lo que el sistema operativo espera del controlador a cambio. Define una máquina de estados donde cada transición corresponde a una invocación del controlador por parte del sistema operativo, una devolución de llamada realizada por el controlador o un evento especificado por el protocolo.
Con estas especificaciones, Termite generará la implementación del controlador que traduce cualquier secuencia válida de solicitudes del sistema operativo en una secuencia de comandos del dispositivo. Gracias a la especificación formal de las interfaces, Termite puede generar el código del controlador que incorpora las propiedades de seguridad y disponibilidad .
RevNIC [ 20 ] ha realizado otro esfuerzo de hacking muy interesante, generando una máquina de estados de controlador mediante ingeniería inversa de un controlador existente para crear controladores interportables y seguros para nuevas plataformas. Para realizar la ingeniería inversa de un controlador, intercepta las operaciones de E/S del hardware ejecutando el controlador mediante ejecuciones simbólicas y concretas. La salida de la interceptación se introduce en un sintetizador, que reconstruye un grafo de flujo de control del controlador original a partir de estos múltiples rastros, junto con la plantilla estándar para la clase de dispositivo correspondiente. Mediante estos métodos, los investigadores han portado algunos controladores de Windows para interfaces de red a otros sistemas operativos Linux y embebidos.
Crítica
Si bien muchas de las herramientas de análisis estático son ampliamente utilizadas, muchas de las herramientas de síntesis y verificación de controladores no han tenido una aceptación generalizada en la práctica. Una de las razones es que los controladores suelen ser compatibles con múltiples dispositivos y el proceso de síntesis generalmente genera un controlador por cada dispositivo compatible, lo que puede dar lugar a un gran número de controladores. Otra razón es que los controladores también realizan algún tipo de procesamiento y el modelo de máquina de estados de los controladores no puede representar dicho procesamiento. [ 21 ]
Conclusión
Las diversas técnicas de verificación y síntesis analizadas en este artículo presentan ventajas y desventajas. Por ejemplo, el aislamiento de fallos en tiempo de ejecución conlleva una sobrecarga de rendimiento, mientras que el análisis estático no abarca todas las clases de errores. La automatización completa de la síntesis de controladores de dispositivos aún se encuentra en sus primeras etapas y ofrece una prometedora línea de investigación futura. El progreso se verá facilitado si los numerosos lenguajes disponibles actualmente para la especificación de interfaces se consolidan en un único formato, compatible universalmente con los fabricantes de dispositivos y los equipos de sistemas operativos. El beneficio de este esfuerzo de estandarización podría ser la consecución, en el futuro, de la síntesis totalmente automatizada de controladores de dispositivos fiables.
Referencias
- ↑ Archana Ganapathi, Viji Ganapathi y David Patterson. " Análisis de fallos del kernel de Windows XP ". En Actas de la Conferencia de Administración de Sistemas de Grandes Instalaciones de 2006, 2006.
- ↑ A. Chou, J. Yang, B. Chelf, S. Hallem y D. Engler. Un estudio empírico de errores en sistemas operativos. En SOSP, 2001
- ↑ Engler, Dawson y Chelf, Benjamin y Chou, Andy y Hallem, Seth. " Verificación de reglas del sistema mediante extensiones de compilador específicas del sistema, escritas por programadores ". En Actas de la 4.ª conferencia sobre diseño e implementación de sistemas operativos, 2000.
- ^ Jhala, Ranjit y Majumdar, Rupak. "Comprobación del modelo de software". En Encuesta de Computación ACM. 2009
- ↑ Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram Rajamani y Abdullah Ustuner. " Análisis estático exhaustivo de controladores de dispositivos ", en SIGOPS Oper. Syst. Rev, vol. 40, 2006.
- ↑ McMillan, Kenneth L. "Verificación simbólica de modelos". Kluwer Academic Publishers, 1993.
- ^ Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar y Gregoire Sutre. " Verificación de Software con BLAST ". En GIRAR, 2003.
- ↑ Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar y Gregoire Sutre. "Abstracción perezosa", en ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, 2002.
- ↑ H. Post, W. Küchlin. "Integración del análisis estático para la verificación de controladores de dispositivos Linux". En la 6.ª Conferencia Internacional sobre Métodos Formales Integrados, 2007.
- ↑ Edmund Clarke, Daniel Kroening y Flavio Lerda. "Una herramienta para comprobar programas ANSI-C". En TACAS, 2004.
- ↑ Thomas Ball, Mayur Naik y Sriram K. Rajamani. "Del síntoma a la causa: localización de errores en trazas de contraejemplos". ACM SIGPLAN Notices, 2003.
- ↑ Feng Zhou, Jeremy Condit, Zachary Anderson, Ilya Bagrak, Rob Ennals, Matthew Harren, George Necula y Eric Brewer. " SafeDrive: Extensiones seguras y recuperables mediante técnicas basadas en el lenguaje ". En 7th OSDI, 2006.
- ↑ Michael M. Swift, Steven Martin, Henry M. Levy y Susan J. Eggers. " Nooks: una arquitectura para controladores de dispositivos confiables ". En 10th ACM SIGOPS, 2002.
- ↑ Jorrit N. Herder, Herbert Bos, Ben Gras, Philip Homburg y Andrew S. Tanenbaum. " MINIX 3: un sistema operativo altamente fiable y autorreparable ". En SIGOPS Oper. Syst. Rev. 40, 2006.
- ↑ Fabrice Merillon, Laurent Reveillere, Charles Consel, Renaud Marlet y Gilles Muller. « Devil: un IDL para programación de hardware ». En Actas de la 4.ª conferencia sobre diseño e implementación de sistemas operativos, vol. 4, 2000.
- ↑ Christopher L. Conway y Stephen A. Edwards. " NDL: un lenguaje específico de dominio para controladores de dispositivos ". ACM SIGPLAN Notices 39, 2004.
- ↑ J. Sun, W. Yuan, M. Kallahalla y N. Islam. " HAIL: Un lenguaje para un acceso fácil y correcto a los dispositivos ". En Actas de la Conferencia ACM sobre Software Integrado, 2005.
- ↑ Felice Balarin et al. " Codiseño de hardware y software de sistemas embebidos. El enfoque POLIS ". Kluwer Academic Publishers, 1997.
- ↑ Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur y Gernot Heiser. «Síntesis automática de controladores de dispositivos con Termite». En Actas del 22.º Simposio ACM sobre Principios de Sistemas Operativos, 2009.
- ↑ Vitaly Chipounov y George Candea. " Ingeniería inversa de controladores de dispositivos binarios con RevNIC ". 5.ª ACM SIGOPS/EuroSys, 2010.
- ↑ Asim Kadav y Michael M. Swift "Comprendiendo los controladores de dispositivos modernos" En Actas de la 17.ª Conferencia ACM sobre soporte arquitectónico para lenguajes de programación y sistemas operativos
Enlaces externos
- Future Chips: Un sitio web dedicado al codiseño de hardware y software.
- Avinux, hacia la verificación automática de controladores de dispositivos Linux
- BLAST: Herramienta de verificación de software de abstracción perezosa de Berkeley
- Verificador de controladores estáticos de Microsoft
- SafeDrive: extensiones seguras y recuperables mediante técnicas basadas en el lenguaje.
- Nook : Mejorando la fiabilidad de los sistemas operativos básicos.
- BugAssist : Una herramienta para localizar fallos
- Ingeniería inversa de controladores de dispositivos. Archivado el 8 de enero de 2011 en Wayback Machine.
- HAIL, un lenguaje para un acceso fácil y correcto a los dispositivos. Archivado el 19 de mayo de 2010 en Wayback Machine.
- Controladores de dispositivos
