Cap’ ou pas cap’ ? Preuve de programmes pour une machine à capacités en présence de code inconnu

Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal

Research output: Chapter in Book/Report/Conference proceedingConference paper

19 Downloads (Pure)

Abstract

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.
Original languageFrench
Title of host publicationJournées Francophones des Langages Applicatifs 2021
PublisherInstitut de Recherche en Informatique Fondamentale
Number of pages17
Publication statusPublished - 7 Apr 2021
EventJournées Francophones des Langages Applicatifs -
Duration: 3 Feb 20216 Feb 2021

Conference

ConferenceJournées Francophones des Langages Applicatifs
Period3/02/216/02/21

Cite this