Malware detection is typically performed using either software scanners running inside the operating system or external devices designed to validate the integrity of the kernel. This thesis proposes a hypervisor-based malware that compromises the system by targeting the hard disk drive and leaving the kernel unmodified. The hypervisor is able to issue read and write commands to the disk while actively hiding these actions from the operating system and any detection software therein. Additionally, the hypervisor’s presence has minimal impact on the performance of the system. The ability to perform these commands compromises the confidentiality, integrity, and availability of the stored data. As a result, this thesis has widespread implications affecting personal, corporate, and government users alike.

Un hyperviseur est un logiciel qui virtualise les ressources d'une machine physique pour permettre à plusieurs systèmes d'exploitation invités de s'exécuter simultanément dessus. L'hyperviseur étant le gestionnaire des ressources, un bug peut être critique pour les systèmes invités. Dans cette thèse nous nous intéressons aux propriétés d'isolation de la mémoire d'un hyperviseur de type 1, qui virtualise la mémoire en utilisant des Shadow Page Tables. Plus précisément, nous présentons un modèle concret et un modèle abstrait de l'hyperviseur, et nous prouvons formellement que les systèmes d'exploitation invités ne peuvent pas altérer ou accéder aux données privées des autres s'ils n'en ont pas la permission. Nous utilisons le langage et l'assistant de preuve développés par Prove & Run pour ce faire. Le modèle concret comporte beaucoup d'optimisations, qui rendent les structures de données et les algorithmes complexes, il est donc difficile de raisonner dessus. C'est pourquoi nous construisons un modèle abstrait dans lequel il est plus facile de raisonner. Nous prouvons les propriétés sur le modèle abstrait, et nous prouvons formellement sa correspondance avec le modèle concret, de telle manière que les preuves sur le modèle abstrait s'appliquent au modèle concret. La preuve correspondance n'est valable que pour des états concrets qui respectent certaines propriétés, nous prouvons que ces propriétés sont des invariants du système concret. La preuve s'articule donc en trois phases : la preuve d'invariants au niveau concret, la preuve de correspondance entre les modèles abstraits et concret, et la preuve des propriétés de sécurité au niveau abstrait. / A hypervisor is a software which virtualizes hardware resources, allowing several guest operating systems to run simultaneously on the same machine. Since the hypervisor manages the access to resources, a bug can be critical for the guest Oses. In this thesis, we focus on memory isolation properties of a type 1 hypervisor, which virtualizes memory using Shadow Page Tables. More precisely, we present a low-level and a high-level model of the hypervisor, and we formally prove that guest OSes cannot access or tamper with private data of other guests, unless they have the authorization to do so. We use the language and the proof assistant developed by Prove & Run. There are many optimizations in the low-level model, which makes the data structures and algorithms complexes. It is therefore difficult to reason on such a model. To circumvent this issue, we design an abstract model in which it is easier to reason. We prove properties on the abstract model, and we prove its correspondence with the low-level model, in such a way that properties proved on the abstract model also hold for the low-level model. The correspondence proof is valid only for low-level states which respect some properties. We prove that these properties are invariants of the low-level system. The proof can be divided into three parts : the proof of invariants preservation on the low-level, the proof of correspondence between abstract and low-level models, and proof of the security properties on the abstract level.

This master's thesis deals with design and implementation of educational application forpaging. Goal of the application is to help students understand and practice some conceptsfrom paging. It will allow students to write parts of these concepts and see how their codework on visualization of simulation of memory system. Application will be implemented asa web application in HTML, CSS and JavaScript. Server, which will be taking care ofcompiling of user code will be a desktop application. This thesis mainly describes pagingand technologies which will be used for this thesis and application design. It also describesimplementations and testing of this work.