[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. / [CAT] 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. / Peiró Frasquet, S. (2016). Metodología para hipervisores seguros utilizando técnicas de validación formal [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/63152 / TESIS
| Identifer | oai:union.ndltd.org:upv.es/oai:riunet.upv.es:10251/63152 |
| Date | 29 April 2016 |
| Creators | Peiró Frasquet, Salvador |
| Contributors | Crespo Lorente, Alfons, Masmano Tello, Miguel Ángel, Simó Ten, José Enrique, Universitat Politècnica de València. Departamento de Ingeniería de Sistemas y Automática - Departament d'Enginyeria de Sistemes i Automàtica |
| Publisher | Universitat Politècnica de València |
| Source Sets | Universitat Politècnica de València |
| Language | English |
| Detected Language | Spanish |
| Type | info:eu-repo/semantics/doctoralThesis, info:eu-repo/semantics/acceptedVersion |
| Rights | http://rightsstatements.org/vocab/InC/1.0/, info:eu-repo/semantics/openAccess |
Page generated in 0.0033 seconds