Infrastructures pour les "Petits Objets Portables et Sécurisés"

Méthodes formelles appliquées aux composants de systèmes embarqués.
Jean-Louis Lanet, INRIA Sophia Antipolis

Résumé : Nous abordons la sécurité/innocuité en développant des mécanismes de vérification, basés notamment sur les systèmes de types et le code auto-certifié, qui pourront garantir les propriétés de sécurité d'exécution des applications. Le compromis que nous proposons n'impose donc aucune contrainte structurelle sur le système d'exploitation ou les composants système qui pourront s'y greffer, mais demande en contrepartie que les composants chargés dynamiquement soient fournis avec une preuve formelle de leur innocuité. L'approche préconisée ici repose sur l'intégration de trois domaines de recherche distincts: les systèmes d'exploitation, la sécurité des systèmes, et les méthodes formelles.