La conception d'un noyau orientée par sa ...
Type de document :
Autre communication scientifique (congrès sans actes - poster - séminaire...): Communication dans un congrès avec actes
Titre :
La conception d'un noyau orientée par sa preuve d'isolation mémoire
Auteur(s) :
Jomaa, Narjes [Auteur]
Institut de Recherche sur les Composants logiciels et matériels pour l'Information et la Communication Avancée - UAR 3380 [IRCICA]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Hym, Samuel [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Institut de Recherche sur les Composants logiciels et matériels pour l'Information et la Communication Avancée - UAR 3380 [IRCICA]
Nowak, David [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Institut de Recherche sur les Composants logiciels et matériels pour l'Information et la Communication Avancée - UAR 3380 [IRCICA]
Institut de Recherche sur les Composants logiciels et matériels pour l'Information et la Communication Avancée - UAR 3380 [IRCICA]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Hym, Samuel [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Institut de Recherche sur les Composants logiciels et matériels pour l'Information et la Communication Avancée - UAR 3380 [IRCICA]
Nowak, David [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Institut de Recherche sur les Composants logiciels et matériels pour l'Information et la Communication Avancée - UAR 3380 [IRCICA]
Titre de la manifestation scientifique :
Compas 2018
Ville :
Toulouse
Pays :
France
Date de début de la manifestation scientifique :
2018-07-03
Mot(s)-clé(s) :
preuve formelle
co-design
isolation mémoire
Pip
co-design
isolation mémoire
Pip
Discipline(s) HAL :
Informatique [cs]/Système d'exploitation [cs.OS]
Informatique [cs]/Cryptographie et sécurité [cs.CR]
Informatique [cs]/Systèmes embarqués
Informatique [cs]/Théorie et langage formel [cs.FL]
Informatique [cs]/Cryptographie et sécurité [cs.CR]
Informatique [cs]/Systèmes embarqués
Informatique [cs]/Théorie et langage formel [cs.FL]
Résumé :
La vérification des logiciels critiques tels que les noyaux des systèmes d'exploitation est une activité longue et complexe. Celle-ci nécessite une attention particulière dès les premières phases de conception. Le choix ...
Lire la suite >La vérification des logiciels critiques tels que les noyaux des systèmes d'exploitation est une activité longue et complexe. Celle-ci nécessite une attention particulière dès les premières phases de conception. Le choix des fonctionnalités, la stratégie d'implémentation, le modèle du matériel à gérer, les propriétés à vérifier et l'approche de vérification sont tous à prendre en compte pendant le développement du noyau. Ce papier discute de la stratégie de co-design d'un noyau de système d'exploitation et de sa preuve. L'objectif visé est d'adapter le design du noyau pour réduire la complexité de la production de sa preuve tout en préservant son utilisabilité. La propriété étudiée dans ce papier est une propriété de sécurité, exprimée en terme d'isolation mémoire. L'étude présentée met notamment en évidence l'importance de l'interface d'accès au matériel. In fine c'est cette interface qui est axiomatisée pour construire la preuve du noyau.Lire moins >
Lire la suite >La vérification des logiciels critiques tels que les noyaux des systèmes d'exploitation est une activité longue et complexe. Celle-ci nécessite une attention particulière dès les premières phases de conception. Le choix des fonctionnalités, la stratégie d'implémentation, le modèle du matériel à gérer, les propriétés à vérifier et l'approche de vérification sont tous à prendre en compte pendant le développement du noyau. Ce papier discute de la stratégie de co-design d'un noyau de système d'exploitation et de sa preuve. L'objectif visé est d'adapter le design du noyau pour réduire la complexité de la production de sa preuve tout en préservant son utilisabilité. La propriété étudiée dans ce papier est une propriété de sécurité, exprimée en terme d'isolation mémoire. L'étude présentée met notamment en évidence l'importance de l'interface d'accès au matériel. In fine c'est cette interface qui est axiomatisée pour construire la preuve du noyau.Lire moins >
Langue :
Français
Comité de lecture :
Oui
Audience :
Nationale
Vulgarisation :
Non
Collections :
Source :
Fichiers
- https://hal.archives-ouvertes.fr/hal-01819955/document
- Accès libre
- Accéder au document
- https://hal.archives-ouvertes.fr/hal-01819955/document
- Accès libre
- Accéder au document
- https://hal.archives-ouvertes.fr/hal-01819955/document
- Accès libre
- Accéder au document
- compas2018.pdf
- Accès libre
- Accéder au document
- document
- Accès libre
- Accéder au document