PhD - Spécification à plusieurs niveaux et vérification des propriétés de cybersécurité pour les programmes C critiques

DÉTAILS OPPORTUNITÉ

Récompense totale

0 $

Université étatique

CEA Tech

Région

Europe de l'Ouest

Pays hôte

France

Date limite

31 oct. 2021

Niveau d'études

Doctorat

Type d'opportunité

Doctorat

Spécialités

Informatique et sciences technologiques

Financement d'opportunité

Non financé

Pays éligibles

Cette opportunité est destiné à tous les pays

Région éligible

Toutes les régions

SL-DRT-21-0866

DOMAINE DE RECHERCHE

Cyber sécurité: matériel et logiciels

ABSTRAIT

Cette rubrique traite de la spécification formelle et de la vérification des propriétés logicielles, en particulier des propriétés de cybersécurité. Les outils de vérification déductive permettent à leurs utilisateurs de prouver mathématiquement qu'une implémentation logicielle donnée est correcte par rapport à un ensemble de propriétés formellement spécifiées. C'est notamment le cas du plug-in WP du framework Frama-C pour les programmes C et les spécifications ACSL. Un autre plug-in, MetAcsl, a été récemment développé afin de faciliter l'expression et la vérification des propriétés de haut niveau, en mettant l'accent sur les propriétés liées à la cybersécurité (par exemple, l'isolation de la mémoire, la confidentialité ou l'intégrité). Notamment, MetAcsl permet aux utilisateurs de poser des contraintes sur tous les accès en lecture ou en écriture dans le programme. outils de vérification. Cela est dû à deux raisons principales. Premièrement, ces logiciels ont tendance à utiliser des opérations de bas niveau (par exemple, des opérateurs binaires ou des castings de pointeurs), qui sont difficiles à représenter dans le monde logique, ce qui rend la preuve beaucoup plus complexe. Deuxièmement, la quantité et la complexité de propriétés pour la plupart indépendantes, notamment les invariants de structures de données complexes, peuvent empêcher les prouveurs automatisés de réussir.Cependant, il arrive souvent que chaque fonction n'ait un impact que sur une infime partie des propriétés, laissant la plupart d'entre eux n'ont pas été touchés. Comme toutes les propriétés doivent a priori être considérées dans le contexte de la preuve, celle-ci est donc inutilement encombrée. De plus, dans un certain nombre de cas, la preuve de la préservation du bien impacté pourrait se faire beaucoup plus facilement à un niveau plus abstrait. En outre, les propriétés de niveau supérieur sont généralement plus facilement compréhensibles, ce qui facilite la tâche de l'équipe de validation. De même, un modèle exécutable abstrait peut être animé et évalué plus facilement que le code réel. L'objectif de cette thèse est de proposer un cadre de spécification et de vérification multi-niveaux pour les programmes C. Cela comprendra la vérification d'une partie des propriétés sur une version abstraite du logiciel en cours d'analyse. La version abstraite prendra la forme d'un code C plus simple (faisant abstraction de parties du système concret), codant par exemple un système de transition, tout en restant suffisamment représentatif pour permettre aux utilisateurs de déclarer leurs propriétés d'intérêt. Comme c'est le cas dans les techniques existantes basées sur le raffinement (en particulier la méthode B), les liens entre le système abstrait et le code réel devront être rigoureusement établis afin d'assurer l'exactitude de l'ensemble du développement. La vérification du code réel sera donc facilitée, car il suffira de montrer qu'il respecte les propriétés de raffinement pour pouvoir en déduire que les propriétés de haut niveau énoncées sur le système abstrait sont également valables pour le code réel. la vérification des propriétés de raffinement peut tirer parti du travail effectué dans le plug-in MetAcsl. Par exemple, MetAcsl propose déjà des fonctionnalités pour prouver plus facilement que si une fonction ne modifie pas l'empreinte d'une propriété (c'est-à-dire les emplacements lus par la propriété), alors la propriété est conservée par la fonction. Le doctorat sera dédié à la définition d'une méthodologie pour spécifier une représentation abstraite d'une implémentation logicielle concrète. En particulier, un moyen de définir les liens entre les structures de données et la fonction des deux systèmes, ainsi que leurs propriétés, sera défini. En outre, les propriétés de raffinement garantissant que si une propriété est prouvée sur le système abstrait, alors sa contrepartie concrète tient également seront formellement énoncées.La technique proposée doit pouvoir être déployée sur des logiciels industriels complexes (en utilisant des structures de données optimisées, avec des opérations de bas niveau et de nombreux invariants qui doivent être préservés), afin de vérifier les propriétés de cybersécurité. Pour garantir cela, une approche ascendante peut être suivie, à partir d'une mise en œuvre concrète existante et des propriétés réelles qui doivent être prouvées sur cette mise en œuvre. Par exemple, on peut vouloir prouver à un niveau abstrait qu'un mécanisme de gestion des ressources (allocateur de mémoire, gestionnaire de tâches dans un micro noyau, ...) respecte une politique d'accès donnée. Encore une fois, MetAcsl pourrait être utilisé pour prouver les propriétés de raffinement vers le code réel. Une deuxième étape de la thèse sera consacrée au développement d'un outil d'automatisation des abstractions et des raffinements. Là encore, l'outil sera évalué sur des études de cas concrètes, soit open source, soit réalisées dans le cadre de projets industriels.