Pour garantir la cybersécurité de logiciels embarqués ou au sol dans le domaine aéronautique, la disponibilité de techniques de vérification efficaces et rapides à mettre en œuvre est un enjeu majeur. Dassault Aviation a récemment développé une nouvelle méthode d'analyse du code source de ses logiciels reposant sur l'utilisation de plusieurs outils de la plateforme Frama-C du List.

Cette méthode détecte des vulnérabilités logicielles (ou common weaknesses), et déclenche des contre-mesures pendant l'exécution, le cas échéant, en combinant automatiquement les outils d'analyse statique EVA et dynamique E-ACSL de Frama-C. Ce dernier outil, dont les performances ont été améliorées par le List, a atteint un niveau lui permettant de détecter plus de vulnérabilités que les outils concurrents, pour une moindre consommation mémoire et un temps d'exécution similaire à celui de ses concurrents.

Après une première validation expérimentale concluante, la méthode combinée a été testée sur deux composants de référence fréquemment utilisés pour la sécurité des systèmes d'information : les modules Apache et OpenSSL, utilisés ici par Dassault Aviation dans une application "Proof-of-Concept" pour le support au sol des avions Falcon. Cette étude confirme que la nouvelle fonctionnalité E-ACSL  de Frama-C permet de détecter des familles de vulnérabilités cyber et de rendre plus robustes les applications analysées, tout en assurant les performances requises pour passer à l'échelle sur des cas industriels.