Projet ANR-14-CE28-0014 – AnaStaSec : Analyse Statique pour la Sécurité
Programme : Sciences et technologies logicielles (DS0704) 2014
Année de financement : 2014
Coordinateur du projet : Monsieur Jérôme FERET (INRIA Paris-Rocquencourt)
Partenaires : AIRBUS GROUP SAS; PME; Laboratoire public; Laboratoire d'Intégration des Systèmes et des Technologies; Laboratoire public; TPE
Montant : 755793.0 euros
Date de début : 2014
Durée : 60 mois
Résumé : Une structure émergente dans notre société basée sur le traitement de l'information est la notion de systèmes complexes sécurisés interagissant par l'intermédiaire d'un réseau hétérogène avec un monde ouvert essentiellement inconnu et potentiellement malicieux. Cette perspective s'applique à une large gamme de systèmes, allant du système d'information d'une entreprise au composants connectés d'une maison, tous ces réseaux étant connectés au monde extérieur. C'est en particulier le cas pour certains systèmes informatiques embarqués dans des avions, qui communiquent avec le sol par l'intermédiaire de communications non sécurisés. De plus, la demande croissante de nouvelles fonctionnalités, telles que la connectivité à bord, par exemple au moyen d'appareils mobiles, et la pression pour réduire les coûts, conduisent aux développements de réseaux de plus en plus connectés et intégrés. Par exemple, les avions modernes sont pourvus de beaucoup de systèmes informatiques, allant des systèmes critiques avioniques de la cabine de pilotage aux programmes de divertissement pour les passagers. Certains systèmes ont de fortes contraintes de sûreté et de sécurité. Malgré une certaine séparation physique des sous systèmes et des réseaux, l'existence de ressources de communication partagées pose le problème des intrusions éventuelles. 
Plusieurs méthodes ont été développées et ont toujours besoin d'être étudiées davantage pour assurer les propriétés de sécurité et de confidentialité de tels systèmes. Mais, la plupart de ces techniques sont basées sur des modèles, et ne donnent aucune garantie sur les implantations finales. Pourtant, la plupart des incidents de sécurité est due à des attaques qui exploitent des failles subtiles au niveau logiciel. Ainsi, les systèmes devraient être analysés et prouvés également au niveau logiciel (c'est à dire au niveau des codes sources et des codes binaires) afin de garantir formellement que les propriétés de sécurités sont aussi valides pour les systèmes réels. 
A cause de la taille de ces systèmes, et parce que ces systèmes évoluent au cours du temps, la seule solution économiquement viable est d'effectuer des analyses automatiques. De telles analyses de propriétés de sécurité et de confidentialité n'ont jamais été réalisées sur des systèmes de grande taille où les aspects de sécurités dépendent fortement d'autres propriétés logicielles. D'ailleurs, même établir la correspondance entre les modèles haut-niveau et la grande base de logiciels qui implante ces modèles représente un objectif important et difficile. Le but de ce projet est de développer des nouveaux concepts et les technologies pour accomplir cet objectif. 
Ainsi, ce projet permettra la vérification formelle de propriétés de sécurité de systèmes embarqués, en utilisant des analyses statiques automatiques à différent niveaux de représentation: modèles, code source, et code binaires.  Parmi les retombées attendues, un ensemble de prototypes académiques seront produits, pour permettre l'analyse de grands systèmes industriels et des processus industriels, basés sur l'analyse statique, pour évaluer la sécurité de ces systèmes seront élaborés.