Analyse statique de code critique

Astrée est un analyseur statique pour les logiciels critiques écrits ou générés en C ou C++.

Astrée est sûr — c’est-à-dire que si aucune erreur n’est signalée, l’absence d’erreurs a été formellement prouvée. En 2020, le National Institute of Standards and Technology des États-Unis a établi qu’Astrée répondait à ses critères pour l’analyse statique de code sûre.

Caractéristiques

• Analyses exceptionnellement rapides et précises, notamment :
  • Analyse des erreurs d’exécution
  • Analyse des conditions de concurrence (data races)
  • Analyse de la non-interférence
  • Analyse avancée de la propagation des valeurs (taint analysis)
  • Détection des vulnérabilités Spectre
  • Analyse des flux de signaux, de données et de contrôle
  • Analyse des couplages de contrôle et des interférences entre composants
  • Analyses de cybersécurité définies par l’utilisateur
  • Analyse des propriétés fonctionnelles des programmes
  • Vérifications des règles de codage MISRA, CERT, JSF, CWE, AUTOSAR, et d’autres recommandations
  • Analyse de nombreuses métriques de code
  • Élimination du code mort
• Prise en charge des programmes en C, C++ et des bases de code mixtes
• Support pour la revue collaborative des résultats d’analyse
• Communication cryptée TLS avec prise en charge d’OpenID
• Rapports générés automatiquement pour la documentation et la certification
• Kits de qualification pour plusieurs normes, dont les normes DO-178B/C, ISO 26262, ou EN-50128
• Interface utilisateur riche en fonctionnalités avec des vues graphiques et textuelles des résultats d’analyse, du code source, du flot de contrôle, et des commentaires utilisateurs
• Mode en ligne de commande pour une intégration facile dans les processus de compilation automatisés
• Plugins pour TargetLink, Jenkins, μVision, JSON et Eclipse
• Licences fixes, flottantes et cloud
• Mises à jour régulières et support technique de grande qualité

Références clients

Astrée a été utilisé pour vérifier l’absence d’erreurs à l’exécution dans le logiciel de com­mande de vol électrique primaire de plusieurs types d’avion Airbus.

Astrée est déployé par l’équipementier automobile Robert Bosch, après une expérimentation intensive d’un an dans sa Division « Automotive Steering ».

Leader mondial dans les moteurs et les ventilateurs pour les systèmes de climatisation et de réfrigération, ebm-papst utilise Astrée pour la vérification entièrement automatique continue de logiciels de contrôle critique pilotés par interruption pour la commutation de moteurs EC à haut rendement pour des systèmes de ventilateurs.

En Avril 2008, Astrée pouvait prouver l’absence de tout erreur d’exécution dans une version C des logiciels d’accostage automatique du Véhicule automatique de transfert européen (ATV) Jules Verne développé pour ravitailler la Station spatiale internationale (ISS). L’analyse était effectuée de façon complètement automatique.

Le fournisseur automobile global Helbako utilise Astrée dans le processus de développement pour démontrer la conformité du code avec MISRA et pour vérifier qu’aucune erreur à l’exécution ne peut arriver dans les logiciels de contròle électronique.

MTU Friedrichshafen utilise Astrée pour démontrer la justesse du logiciel de contrôle pour les générateurs de secours dans les centrales électriques. Les outils combinés avec leurs kits de qualification (QSK et QSLCD) font partie du processus de certification selon l’IEC60880.

Analyse statique des propriétés d’exécution

Astrée fait une analyse statique des codes source permettant de savoir si le langage de programmation est utilisé correctement et s’il peut y avoir des erreurs d’exécution lors de n’importe quelle exécution dans n’importe quel environnement. Cela inclut toute utilisation de C ou C++ qui, selon le standard de langage sélectionné, a un comportement indéfini ou viole des aspects spécifiques au matériel.

En outre, Astrée signale les comportements concurrents non valides, les violations des règles de codage définies par l’utilisateur et diverses propriétés du programme pertinentes pour la sécurité fonctionnelle.

Astrée détecte tous les problèmes suivants :

• division par zéro,
• dépassement des limites des tableaux,
• manipulation et déréférencement de pointeurs erronés (pointeurs NULL, non initialisés, et pointeurs vers de la mémoire désallouée),
• dépassement de capacité arithmétique en nombres entiers et en virgule flottante,
• accès en lecture à des variables non initialisées,
• conditions de concurrence (accès simultanés d’un même emplacement mémoire, en lecture/écriture ou écriture/écriture, par deux threads, sans protéger l’accès par un mutex),
• verrouillages de mutex incohérents (problèmes lock/unlock),
• appels invalides aux services du système d’exploitation (par exemple les appels OSEK à TerminateTask sur une tâche dont les ressources n’ont pas été libérées),
• vulnérabilités Spectre,
• autres erreurs critiques de flots de données ou de contrôle,
• violations des assertions facultatives définies par l’utilisateur pour prouver des propriétés d’exécution supplémentaires (similaires aux diagnostics d’assertions),
• code jamais exécuté (dead code).

Astrée est sûr pour les calculs à virgule flottante et les gère précisément et en toute sécurité. Toutes les erreurs d’arrondi possibles et leurs effets cumulatifs sont prises en compte, ainsi que les valeurs −∞, +∞ et NaN et leurs effets sur les calculs arithmétiques et les comparaisons.

Analyse des flots de données et de contrôle

Astrée suit les accès aux variables globales, variables statiques, et variables locales dont les accès sont effectués en dehors du cadre dans lequel elles sont définies (par exemple, lorsque leurs adresses sont passées en paramètre à une fonction).

Toutes les cibles des pointeurs de données et de fonctions sont calculées automatiquement. La sûreté de l’analyse garantit que toutes les cibles potentielles sont prises en compte.

Visualisation du flot de contrôle

Un dessin vaut mieux qu’un long discours. Les capacités de visualisation de graphes d’Astrée vous aident à découvrir les comportements inattendus de votre logiciel et permettent une compréhension rapide et approfondie des codes tiers ou hérités.

Analyse du flux des signaux

Astrée peut analyser le flux des signaux d’entrée vers les signaux de sortie pour des logiciels complexes. Pour ce faire, Astrée incorpore une analyse de propagation des valeurs (taint analysis) basée sur une analyse sémantique complète, prenant ainsi en compte l’influence des paramètres de configuration de l’application sur le flux des signaux.

L’analyse peut être menée pour une configuration spécifique, ce qui permet de ne voir que les flux de signaux pour cette configuration, ou pour une configuration générique afin de détecter les influences des paramètres sur le signal de sortie.

Analyse des interférences entre composants logiciels

Astrée vous permet de définir des composants logiciels selon vos propres critères, et de spécifier les flux de données ou de contrôle entre les composants qui vous intéressent. Astrée détecte ensuite toutes les interférences potentielles de données et de contrôle entre les composants au niveau du code source, et vous aide à en comprendre les causes afin d’améliorer votre code si nécessaire.

Support pour C++ et bases de code mixtes

Depuis 2020, Astrée peut être appliquée aux bases de code C++ et mixtes C/C++, en supportant toutes les versions modernes de C++ jusqu’à C++17.

L’analyse C++ d’Astrée utilise la même technologie que l’analyse de code C. Elle est conçue pour répondre aux caractéristiques des bases de code C++ et aux caractéristiques des logiciels embarqués critiques en termes de sécurité. Elle est soumise aux mêmes restrictions qu’Astrée pour le C.

Les fonctions d’abstraction de haut niveau et la bibliothèque de modèles du C++ facilitent la conception de logiciels très complexes et dynamiques. L’utilisation intensive de ces fonctionnalités peut enfreindre les principes établis du développement de logiciels embarqués critiques pour la sécurité et conduire à des temps d’analyse et à des résultats insatisfaisants. Le manuel d’Astrée donne des recommandations sur l’utilisation des fonctionnalités de C++ afin de garantir que le code peut être bien analysé. Pour un code C++ moins contraint (moins critique), nous recommandons d’utiliser le RuleChecker autonome.

Conformité aux normes de codage

Le RuleChecker, parfaitement intégré, vous permet de vérifier la conformité de votre code à diverses normes de codage, notamment MISRA, CWE, ISO/IEC, SEI CERT et AUTOSAR. Vous pouvez facilement activer des règles individuelles et même des aspects spécifiques de certaines règles.

L’outil peut également vérifier diverses mesures de code telles que la densité des commentaires ou la complexité cyclomatique. Des extensions personnalisées pour vos propres directives de codage sont disponibles sur demande.

Le RuleChecker peut être utilisé séparément, pour permettre des vérifications encore plus rapides de votre code, ou en conjonction avec les analyses sémantiques sûres offertes par Astrée, pour garantir en outre zéro faux négatif et minimiser les faux positifs sur les règles sémantiques. Aucun vérificateur MISRA autonome concurrent ne peut offrir cela, et aucun environnement de test ne peut égaler la couverture complète des données et des chemins d’accès fournie par l’analyse statique.

Support de qualification

L’utilisation d’Astrée peut être qualifiée selon des normes telles que DO-178B/C, ISO 26262, IEC 61508, EN-50128, les principes de validation des logiciels de la FDA, et d’autres normes de sécurité. Nous proposons des kits spéciaux de support à la qualification qui simplifient et automatisent le processus de qualification.

Personnalisation

Astrée offre de puissants mécanismes d’annotation permettant de fournir des connaissances externes et d’affiner la précision de l’analyse pour des boucles ou des structures de données spécifiques. Des messages détaillés et une interface graphique intuitive vous guident vers la cause exacte de chaque erreur d’exécution potentielle.

Les erreurs réelles peuvent alors être corrigées et, en cas de fausse alerte, l’analyseur peut être réglé pour l’éviter. Cela permet d’effectuer des analyses avec très peu de fausses alarmes, voire aucune.

L’analyseur peut également fonctionner en mode batch pour une intégration facile dans les chaînes d’outils traditionnelles.

Des plugins pour TargetLink, Jenkins et Eclipse sont disponibles et activement supportés.

Evaluation gratuite

Commandez votre version d’évaluation gratuite aujourd’hui ou bien contactez nos distributeurs officiels :

• en France : Antycip, Groupe Hensoldt, Massy, didier.dusclaux@hensoldt.fr, +33 (0)1 70 26 55 35
• au Canada : Joral Technologies, Ottawa, robert.campbell@joraltechnologies.com, 1-877-380-3366
• au Benelux : Indes, Culemborg, Pays-Bas, sales@indes.com, +31 (0)3 45 54 55 35