Logo CEA LIST Carnot yt

Validation

L'intégration de logiciels embarqués dans les systèmes requiert leur validation par analyse dynamique (simulation) ou statique (preuve formelle). De nombreuses approches, mathématiques notamment, sont proposées par le CEA LIST pour assurer la validation de propriétés de sécurité et fiabilité.

Avec les microprocesseurs ARM, la simulation matérielle s’ouvre à l’embarqué léger

Déjà utilisée dans le nucléaire et l’aéronautique, la plateforme matérielle virtuelle UNISIM du CEA LIST a enrichi sa librairie à l’occasion d’un projet collaboratif avec Schneider Electric. Les microprocesseurs ARM7 et ARM9, très utilisés dans les systèmes embarqués « légers » (téléphones mobiles…), y ont été intégrés afin de valider les choix de conception architecturale d’interrupteurs moyenne tension.
UNISIM, qui permet de simuler efficacement un système complet de composants matériels, a étendu à cette occasion le registre de ses usages : il peut déjà être utilisé pour la vérification, la validation et la conception logicielle au niveau des couches basses. Dans le cas de Schneider Electric, il a permis d’étudier si une fonction devait plutôt être codée ou implantée physiquement.
Cette validation de choix architecturaux intéresse déjà d’autres industriels : elle fait partie des thèmes retenus par un grand acteur des transports avec lequel le CEA LIST a récemment noué un partenariat.




Combiner les outils pour détecter les failles de sécurité
Une méthodologie innovante de détection des failles de sécurité, sur le matériel et sur le logiciel, a été mise au point avec Telecom Paris Tech et testée sur un driver de l’UART du microprocesseur Léon3 (microprocesseur développé en open source pour l’Agence Spatiale Européenne - ESA).
Dans un premier temps, l’analyse du code VHDL (hardware) a été réalisée par le module Calmos de Telecom Paris Tech, et celle du logiciel par l’outil Frama-C du CEA LIST. Un scénario d’attaque potentiel a été créé puis testé à l’aide de Frama-C et de deux outils de génération de tests, PathCrawler et Cute ; une faille de sécurité a ainsi été mise en évidence.


Cette approche, extrêmement puissante, permet à la fois d’identifier les failles éventuelles ou d’apporter la preuve mathématique qu’un programme écrit en C ne comporte pas de failles. L’institut compte donc renforcer ces méthodes par combinaison d’outils, en utilisant Frama-C en tant que plateforme, pour conforter son expertise en sécurité des logiciels.


Plate-forme Logiciel Frama-C

Validation numérique : transfert industriel pour Fluctuat chez Airbus

La présence dans un programme de nombres à virgule flottante peut déclencher des comportements aberrants aux conséquences potentiellement désastreuses. C’est la raison d’être de Fluctuat, programme de vérification du CEA LIST : après plusieurs années de développement, il a fait l’objet fin 2010 d’un transfert à Airbus. D’autres études menées cette année confirment sa maturité croissante.

Un missile qui manque sa cible, une plateforme pétrolière mal conçue qui coule en pleine mer, un produit de grande consommation rappelé en masse pour cause de logiciel défectueux : ce sont quelques-unes des conséquences récentes et dûment répertoriées des caprices de nombres à virgule flottante. Certes, l’approximation induite par la septième décimale d’un nombre semble avoir peu d’impact. Mais si le programme utilise ce nombre de manière répétitive, la dérive due à cette approximation peut peser de plus en plus lourd et déclencher des comportements aberrants.
Par rapport aux méthodes - essentiellement à base de tests - employées aujourd’hui, la caractéristique majeure de Fluctuat est de couvrir la totalité des comportements possibles du programme grâce à l’utilisation de méthodes sémantiques (interprétation abstraite). Les erreurs de précision sont ainsi identifiées, qu’elles soient dues à des arrondis en précision finie (virgule flottante ou virgule fixe par exemple) où à des erreurs sur les données d’entrée.

Une approche qui n’oublie aucune erreur

Cette approche par modélisation est extrêmement précise. Ainsi, pour chaque erreur constatée, les lignes de programme concernées sont identifiées, ce qui facilite la tâche des développeurs. Le programme étudie aussi le comportement fonctionnel du programme sur des nombres réels, afin de cibler certaines vérifications sur des identités remarquables.
En 2010, de nombreuses études et collaborations industrielles ont confirmé la maturité de l’outil : couplage avec le logiciel de conception SCADE System Designer de la société Esterel Technologies, validation d’un code de navigation spatiale, première analyse d’un code en ADA (Fluctuat ne traitait jusqu’ici que du code C pour le compte d’Astrium).
Le fait majeur de l’année reste toutefois le transfert du programme à Airbus, qui compte l’utiliser pour l’A350 : Fluctuat a acquis à cette occasion ses galons de « quasi-produit». Le programme peut s’utiliser à tous les stades de la vie d’un logiciel, conception comprise, et intéresse donc potentiellement tous les secteurs industriels.




Joomla SEF URLs by Artio