Sites Inria

English version

Equipe de recherche EVEREST

Environnements de vérification et sécurité du logiciel

  • Responsable : Gilles Barthe
  • Centre(s) de recherche : CRI Sophia Antipolis - Méditerranée
  • Domaine : Algorithmique, programmation, logiciels et architectures
  • Thème : Programmation, vérification et preuves

Présentation de l'équipe

L'équipe-projet EVEREST vise à promouvoir l'utilisation des méthodes formelles dans le cadre de la sécurité des systèmes. Les domaines d'application privilégiés sont les petits objets portables sécurisés, et notamment les cartes à puce, les systèmes d'exploitation, et les applications mobiles et embarquées.

Axes de recherche

Notre programme de recherche se focalise sur les trois thèmes suivants:
  • plateformes sécurisées: nous concevons des plateformes sécurisées, en nous appuyant sur des méthodes vérification issues du domaine des langages de programmation, comme par exemple les systèmes de types et le code auto-certifié. Nous étudions en particulier les machines virtuelles Java et JavaCard, et les systèmes d'exploitation sécurisés. Nous modélisons les plateformes et prouvons leur correction à l'aide d'assistants à la preuve.
  • vérification d'applications: nous développons JACK (Java Applet Correctness Kit), un environnement de vérification des programmes Java annotés en JML. Dans le cadre de ces travaux, nous étudions notamment un mécanisme d'insertion automatiques d'annotations JML garantissant des propriétés de sécurité génériques, et les extensions de JML. Nous développons également des mécanismes de vérification compositionnelle pour les applications Java.
  • théorie: nous étudions la théorie des types, qui forme le noyau théorique des assistants de preuve que nous utilisons pour la vérification des plateformes et applications, et la logique temporelle, qui forme le noyau théorique des outils de model-checking et de vérification compositionnelle que nous utilisons pour la vérification des composants. Nous étudions également les modèles mathématiques permettant le raisonnement sur les algorithmes cryptographiques.

Relations industrielles et internationales

  • ACI Sécurité GECCOO: Génération de code certifié pour les applications orientées objets: spécification, raffinement, preuve et détection d'erreurs
  • ACI Sécurité Spops: Sécurité et sûreté des systèmes d'exploitation ouverts pour petits objets portables sécurisés
  • Projet RNTL CASTLES: Conception d'Analyses Statiques et de Tests pour le Logiciel Embarqué Sécurisé
  • Projets IST Verificard, Profundis, Types, Appsem II

Mots-clés : Méthodes formelles vérification Sécurité

Suivez Inria