Formal Proof of Dynamic Memory Isolation ...
Type de document :
Communication dans un congrès avec actes
DOI :
Titre :
Formal Proof of Dynamic Memory Isolation Based on MMU
Auteur(s) :
Jomaa, Narjes [Auteur]
Extra Small Extra Safe [2XS]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Nowak, David [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Extra Small Extra Safe [2XS]
Grimaud, Gilles [Auteur]
Extra Small Extra Safe [2XS]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Hym, Samuel [Auteur]
Extra Small Extra Safe [2XS]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Extra Small Extra Safe [2XS]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Nowak, David [Auteur]

Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Extra Small Extra Safe [2XS]
Grimaud, Gilles [Auteur]

Extra Small Extra Safe [2XS]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Hym, Samuel [Auteur]

Extra Small Extra Safe [2XS]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Titre de la manifestation scientifique :
10th International Symposium on Theoretical Aspects of Software Engineering
Ville :
Shanghai
Pays :
Chine
Date de début de la manifestation scientifique :
2016-07-17
Date de publication :
2016-08-11
Mot(s)-clé(s) en anglais :
Coq
Formal proof
Memory isolation
Microkernel
Micro-kernel
Formal proof
Memory isolation
Microkernel
Micro-kernel
Discipline(s) HAL :
Informatique [cs]/Logique en informatique [cs.LO]
Informatique [cs]/Système d'exploitation [cs.OS]
Informatique [cs]/Système d'exploitation [cs.OS]
Résumé en anglais : [en]
For security and safety reasons, it is essential to ensure memory isolation between processes. The memory manager is thus a critical part of the kernel of an operating system. It is common for kernels to ensure memory ...
Lire la suite >For security and safety reasons, it is essential to ensure memory isolation between processes. The memory manager is thus a critical part of the kernel of an operating system. It is common for kernels to ensure memory isolation through a piece of hardware called memory management unit (MMU). However an MMU by itself does not provide memory isolation. It is only a tool the kernel can use to ensure this property. In this paper we show how a proof assistant such as Coq can be used to model a hardware architecture with an MMU, and an abstract model of microkernel supporting preemptive scheduling and memory manager. We proceed by making formally explicit the consistency properties that must be preserved in order for memory isolation to be preserved.Lire moins >
Lire la suite >For security and safety reasons, it is essential to ensure memory isolation between processes. The memory manager is thus a critical part of the kernel of an operating system. It is common for kernels to ensure memory isolation through a piece of hardware called memory management unit (MMU). However an MMU by itself does not provide memory isolation. It is only a tool the kernel can use to ensure this property. In this paper we show how a proof assistant such as Coq can be used to model a hardware architecture with an MMU, and an abstract model of microkernel supporting preemptive scheduling and memory manager. We proceed by making formally explicit the consistency properties that must be preserved in order for memory isolation to be preserved.Lire moins >
Langue :
Anglais
Comité de lecture :
Oui
Audience :
Internationale
Vulgarisation :
Non
Collections :
Source :
Fichiers
- https://hal.archives-ouvertes.fr/hal-01369769/document
- Accès libre
- Accéder au document
- https://hal.archives-ouvertes.fr/hal-01369769/document
- Accès libre
- Accéder au document
- https://hal.archives-ouvertes.fr/hal-01369769/document
- Accès libre
- Accéder au document
- document
- Accès libre
- Accéder au document
- TASE2016.pdf
- Accès libre
- Accéder au document