This thesis presents the design of a secured, software based hypervisor for certification purposes. The highest levels of certification require formal methods, which demonstrate the correctness of a product with regard to its specification using mathematical logic. Proven hardware is not available off-the-shelf. In order to reduce the Trusted Computing Base (TCB) and hence, the amount of specification and proofs to produce, virtualization mechanism are software-made. In addition, this enables virtualization on platforms which do not have virtualization-enabled hardware. The challenge for achieving this goal is twofold. On one hand, despite an existing documentation, the instruction set to be analysed has tedious corner cases, implementation-dependant behaviour or even worse, undefined behaviour. On the other hand to infer the system behaviors has to be infered given a discrete instruction flow, in order to remain interposed between the guest and the underlying hardware. For achieving this, the guest's machine code is analysed, and sensitive instructions (which threaten confidentiality or integrity) are replaced by traps, which enable arbitration given the actual guest context. Relying on hypothetically proven processor and memory management unit, only privileged code may bypass the configuration setup by the hypervisor and access the hardware. Thus, analysing unprivileged code is worthless in this case. Micro-kernel design which tends to offload most of the code in userspace, are suitable here. Using that paradigm reduces the overhead induced by certified virtualization.
- Directeur(s) de thèse :Gilles Grimaud, Michaël Hauspie - Rapporteurs : Issa Traoré Univ. Victoria (Canada) – Gaël Thomas (Télécom Sud Paris) - Examinateur : Isabelle Ryl (Inria Paris)
Thesis of the team 2XS defended on 08/12/2016
français
English