La conception d'un noyau orientée par sa ...
Document type :
Autre communication scientifique (congrès sans actes - poster - séminaire...): Communication dans un congrès avec actes
Title :
La conception d'un noyau orientée par sa preuve d'isolation mémoire
Author(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]
Conference title :
Compas 2018
City :
Toulouse
Country :
France
Start date of the conference :
2018-07-03
Keyword(s) :
preuve formelle
co-design
isolation mémoire
Pip
co-design
isolation mémoire
Pip
HAL domain(s) :
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]
French abstract :
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 ...
Show more >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.Show less >
Show more >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.Show less >
Language :
Français
Peer reviewed article :
Oui
Audience :
Nationale
Popular science :
Non
Collections :
Source :
Files
- https://hal.archives-ouvertes.fr/hal-01819955/document
- Open access
- Access the document
- https://hal.archives-ouvertes.fr/hal-01819955/document
- Open access
- Access the document
- https://hal.archives-ouvertes.fr/hal-01819955/document
- Open access
- Access the document
- compas2018.pdf
- Open access
- Access the document
- document
- Open access
- Access the document