Vérification modulaires de programmes avec effets en Coq

Ces dernières années, plusieurs mécanismes de sécurité des architectures matérielles modernes (notamment x86) se sont révélés vulnérables à des attaques permettant de mettre en défaut les propriétés qu’ils sont censés assurer. Certaines de ces attaques n’étaient pas le fruit d’erreurs d’implémentation, mais relevaient d’incohérences au niveau des spécifications. C’est dans ce contexte que Thomas LETAN a, dans le cadre de sa thèse de doctorat, cherché à proposer des approches basées sur les méthodes formelles afin de spécifier formellement les mécanismes d’application de politiques de sécurité basées sur des mécanismes matériels et vérifier que ces derniers assurent bien les propriétés de sécurité recherchées. Une telle démarche présuppose l’existence d’un modèle de l’architecture matériel. Les travaux présentés à Formal Methods 2018 proposent une approche en ce sens, dont les principaux objectifs sont (1) de permettre une définition incrémentale du modèle, composant par composant ; et (2) de vérifier les propriétés de la composition de ces composants.

Les architectures matérielles modernes (x86, ARM, etc.) sont de plus en plus complexes. Leur surface d’attaque a augmenté en conséquences. Bien que les composants de ces systèmes sont conçus et parfois même vérifiés avec attention, leur composition est généralement regardée avec moins d’attention. Nous nous intéressons aux attaques tirant parti d’incohérences au niveau des spécifications des composants, quand un attaquant est capable de contourner les protections mises en place par un composant en se servant légitimement d’un second composant.

Dans cet article, nous présentons FreeSpec, un formalisme qui s’inspire des effets algébriques, une abstraction récente du domaine de la programmation fonctionnelle. Dans FreeSpec, les composants matériels sont modélisés comme des programmes avec effets dont la réalisation est déléguée à d’autres composants. Grâce à FreeSpec, il est possible de définir de manière incrémentale un système, composants par composants, puis de vérifier de manière modulaire la composition de ces composants. En complément de ce formalisme théorique, nous avons développé un cadriciel complet pour l’assistant de preuves Coq.

pdf
Modular Verification of Programs with Effects -Effect Handlers in Coq
469.88 Ko

Vérification modulaires de programmes avec effets en Coq

Modular Verification of Programs with Effects -Effect Handlers in Coq