< Terug naar vorige pagina
Publicatie
Cap’ ou pas cap’ ?
Boekbijdrage - Boekhoofdstuk Conferentiebijdrage
Ondertitel:Preuve de programmes pour une machine à capacités en présence de code inconnu
Une machine à capacités est un type de microprocesseur permettant une séparation des
permissions précise grâce à l’utilisation de capacités, mots machine porteurs d’une certaine
autorité. Dans cet article, nous présentons une méthode permettant de vérifier la correction
fonctionnelle de programmes exécutés par la machine alors même que ceux-ci appellent ou
sont appelés par du code inconnu (et potentiellement malveillant). Le bon fonctionnement
de tels programmes repose sur leur utilisation judicieuse des capacités. Du point de vue
logique, notre approche permet donc de tirer parti des garanties fournies par la machine
pour raisonner formellement sur des programmes. Les éléments clefs de cette approche sont
la définition d’une logique de programmes puis d’une relation logique dont on démontre
qu’elle fournit une spécification pour du code inconnu, le tout étant formalisé en Coq.
La méthodologie en question sous-tend le travail précédent des auteurs lié à la formalisa-
tion d’une convention d’appel sûre en présence d’un nouveau type de capacités [GGVS + 21],
mais n’est pas détaillée dans l’article en question. L’article présent se veut être une in-
troduction pédagogique à cette méthodologie, dans un cadre plus simple (sans nouvelles
capacités exotiques), et sur un exemple minimal.
permissions précise grâce à l’utilisation de capacités, mots machine porteurs d’une certaine
autorité. Dans cet article, nous présentons une méthode permettant de vérifier la correction
fonctionnelle de programmes exécutés par la machine alors même que ceux-ci appellent ou
sont appelés par du code inconnu (et potentiellement malveillant). Le bon fonctionnement
de tels programmes repose sur leur utilisation judicieuse des capacités. Du point de vue
logique, notre approche permet donc de tirer parti des garanties fournies par la machine
pour raisonner formellement sur des programmes. Les éléments clefs de cette approche sont
la définition d’une logique de programmes puis d’une relation logique dont on démontre
qu’elle fournit une spécification pour du code inconnu, le tout étant formalisé en Coq.
La méthodologie en question sous-tend le travail précédent des auteurs lié à la formalisa-
tion d’une convention d’appel sûre en présence d’un nouveau type de capacités [GGVS + 21],
mais n’est pas détaillée dans l’article en question. L’article présent se veut être une in-
troduction pédagogique à cette méthodologie, dans un cadre plus simple (sans nouvelles
capacités exotiques), et sur un exemple minimal.
Boek: Journées Francophones des Langages Applicatifs 2021
Aantal pagina's: 17
Jaar van publicatie:2021
Toegankelijkheid:Open