SSURF
SafeRiver participe au projet R&D SSURF dont la thématique est la mise en oeuvre de techniques de spécification formelles et de méthodes d'analyses dysfonctionnelles tout au long du cycle de vie des logiciels afin de démontrer l'atteinte des objectifs de sûreté et de sécurité.
La sécurité des systèmes d'information est un problème difficile et constitue désormais un domaine de recherche reconnu en informatique. On peut constater que les méthodes empiriques utilisées pour aborder ce problème sont progressivement remplacées par des approches plus formelles. Par exemple, pour atteindre de hauts niveaux de certification, il est nécessaire de fournir un modèle formel du système permettant d'obtenir des preuves formelles mécanisées, de mettre en oeuvre des techniques de test, ou de concevoir des analyses statiques permettant de garantir les propriétés requises.
Le projet proposé consiste à :
- Etudier et caractériser les fonctionnalités qu'un environnement integré de développement (IDE) doit offrir non seulement pour produire des logiciels en conformité avec les exigences requises pour atteindre de hauts niveaux de confiance (EAL 5 6 7), mais aussi pour faciliter le processus d'évaluation de ces logiciels selon les standards (IEC61508, CC)
- Développer un cadre formel générique dans lequel peuvent s'exprimer de nombreuses propriétés de sécurité, comme celles concernant les politiques de contrôle d'accès et leurs implantations, puis à considérer une implantation de ce cadre dans l'IDE du projet.
Les deux parties de ce projet sont fortement liées :
- La première partie a pour vocation de fournir des théories/méthodes/outils permettant d'augmenter la confiance dans un système logiciel dans un contexte général
- La deuxième partie peut être vue comme un fil conducteur du projet, dédié à un domaine particulier, celui des propriétés de sécurité, et plus particulièrement le contrôle d'accès, servant à illustrer et à valider les résultats de la première partie
Evidemment, ces deux composantes du projet partagent les mêmes fondements :
- Sémantique
- Logique et théorie des types
- Réecriture
- Assistants à la preuve
- Compilation
- Sécurité des systèmes informatiques
Ce projet s'appuiera fortement sur l'atelier Focal qui fournit déjà un environnement de développement dans lequel spécifications, propriétés, programmes, et preuves peuvent être développés au même niveau (les preuves étant finalement vérifiées par Coq et les programmes compilés vers OCaml). Néanmoins, Focal ne peut encore être considéré comme un outil achevé et a besoin d'être développé pour devenir un véritable IDE.
Journée du groupe MFDL — 2 Décembre 2010