Metodología para hipervisores seguros utilizando técnicas de validación formal

Abstract

[EN] The availability of new processors with more processing power for embedded systems has raised the development of applications that tackle problems of greater complexity. Currently, the embedded applications have more features, and as a consequence, more complexity. For this reason, there exists a growing interest in allowing the secure execution of multiple applications that share a single processor and memory. In this context, partitioned system architectures based on hypervisors have evolved as an adequate solution to build secure systems. One of the main challenges in the construction of secure partitioned systems is the verification of the correct operation of the hypervisor, since, the hypervisor is the critical component on which rests the security of the partitioned system. Traditional approaches for Validation and Verification (V&V), such as testing, inspection and analysis, present limitations for the exhaustive validation and verification of the system operation, due to the fact that the input space to validate grows exponentially with respect to the number of inputs to validate. Given this limitations, verification techniques based in formal methods arise as an alternative to complement the traditional validation techniques. This dissertation focuses on the application of formal methods to validate the correctness of the partitioned system, with a special focus on the XtratuM hypervisor. The proposed methodology is evaluated through its application to the hypervisor validation. To this end, we propose a formal model of the hypervisor based in Finite State Machines (FSM), this model enables the definition of the correctness properties that the hypervisor design must fulfill. In addition, this dissertation studies how to ensure the functional correctness of the hypervisor implementation by means of deductive code verification techniques. Last, we study the vulnerabilities that result of the loss of confidentiality (CWE-200 [CWE08b]) of the information managed by the partitioned system. In this context, the vulnerabilities (infoleaks) are modeled, static code analysis techniques are applied to the detection of the vulnerabilities, and last the proposed techniques are validated by means of a practical case study on the Linux kernel that is a component of the partitioned system.

[ES] La disponibilidad de nuevos procesadores más potentes para aplicaciones empotradas ha permitido el desarrollo de aplicaciones que abordan problemas de mayor complejidad. Debido a esto, las aplicaciones empotradas actualmente tienen más funciones y prestaciones, y como consecuencia de esto, una mayor complejidad. Por este motivo, existe un interés creciente en permitir la ejecución de múltiples aplicaciones de forma segura y sin interferencias en un mismo procesador y memoria. En este marco surgen las arquitecturas de sistemas particionados basados en hipervisores como una solución apropiada para construir sistemas seguros. Uno de los principales retos en la construcción de sistemas particionados, es la verificación del correcto funcionamiento del hipervisor, dado que es el componente crítico sobre el que descansa la seguridad de todo el sistema particionado. Las técnicas tradicionales de V&V, como testing, inspección y análisis, presentan limitaciones para la verificación exhaustiva del comportamiento del sistema, debido a que el espacio de entradas a verificar crece de forma exponencial con respecto al número de entradas a verificar. Ante estas limitaciones las técnicas de verificación basadas en métodos formales surgen como una alternativa para completar las técnicas de validación tradicional. Esta disertación se centra en la aplicación de métodos formales para validar la corrección del sistema particionado, en especial del hipervisor XtratuM. La validación de la metodología se realiza aplicando las técnicas propuestas a la validación del hipervisor. Para ello, se propone un modelo formal del hipervisor basado en máquinas de autómatas finitos, este modelo formal permite la definición de las propiedades que el diseño hipervisor debe cumplir para asegurar su corrección. Adicionalmente, esta disertación analiza cómo asegurar la corrección funcional de la implementación del hipervisor por medio de técnicas de verificación deductiva de código. Por último, se estudian las vulnerabilidades de tipo information leak (CWE-200 [CWE08b]) debidas a la perdida de la confidencialidad de la información manejada en el sistema particionado. En este ámbito se modelan las vulnerabilidades, se aplican técnicas de análisis de código para la detección de vulnerabilidades en base al modelo definido y por último se valida la técnica propuesta por medio de un caso práctico sobre el núcleo del sistema operativo Linux que forma parte del sistema particionado.

[CA] La disponibilitat de nous processadors amb major potencia de còmput per a aplicacions empotrades ha permès el desenvolupament de aplicacions que aborden problemes de major complexitat. Degut a açò, les aplicacions empotrades actualment tenen més funcions i prestacions, i com a conseqüència, una major complexitat. Per aquest motiu, existeix un interès creixent en per permetre la execució de múltiples aplicacions de forma segura i sense interferències en un mateix processador i memòria. En aquest marc sorgeixen les arquitectures de sistemes particionats basats en hipervisors com una solució apropiada per a la construcció de sistemes segurs Un dels principals reptes en la construcció de sistemes particionats, es la verificació del correcte funcionament del hipervisor, donat que aquest es el component crític sobre el que descansa la seguretat del sistema particionat complet. Les tècniques tradicionals de V&V, com són el testing, inspecció i anàlisi, presenten limitacions que fan impracticable la seva aplicació per a la verificació exhaustiva del comportament del sistema, degut a que el espai de entrades a verificar creix de forma exponencial amb el nombre de entrades a verificar. Front a aquestes limitacions les tècniques de verificació basades en mètodes formals sorgeixen com una alternativa per a completar les tècniques de validació tradicional. Aquesta dissertació es centra en la aplicació de mètodes formals per a validar la correcció del sistema particionat, en especial d del hipervisor XtratuM. La validació de la metodología es realitza aplicant les tècniques proposades a la validació del hipervisor. Per a aquest fi, es proposa un model formal del hipervisor basat en màquines de estats finits (FSM), aquest model formal permet la definició de les propietats que el disseny del hipervisor deu de complir per assegurar la seva correcció. Addicionalment, aquesta dissertació analitza com assegurar la correcció funcional de la implementació del hipervisor mitjançant tècniques de verificació deductiva de codi. Per últim, s'estudien les vulnerabilitats de tipus information leak (CWE-200 [CWE08b]) degudes a la pèrdua de la confidencialitat de la informació gestionada per el sistema particionat. En aquest àmbit, es modelen les vulnerabilitats, s'apliquen tècniques de anàlisis de codi per a la detecció de les vulnerabilitats en base al model definit, per últim es valida la tècnica proposada mitjançant un cas pràctic sobre el nucli del sistema operatiu Linux que forma part de l'arquitectura particionada.