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.

Quelles propriétés de durée sont contrôlées par Astrée ?

Les erreurs trouvées par Astrée sont :

• Tout usage de C ou C++ défini dans les normes internationales ayant un com­portement indéfini (divisions par zéro, débordements d’index de tableau, manipulations et déréférences de pointeurs nuls et invalides)
• Toute violation de la norme ISO/IEC 9899:1999 relative aux comportements spécifiques d’une implémentation sur une machine donnée (comme la taille des entiers et les débordements arithmétiques)
• Tout usage potentiellement erroné ou incorrect de C ou C++ contraire à des règles optionnelles de bon usage définies par l’utilisateur (comme l’exclusion de l’arithmétique modulaire pour les en­tiers signés même si c’est l’option implantée par le matériel)
• Toute violation d’assertions optionnelles insérées par l’utilisateur dans le code source
• Violations des règles MISRA, CWE, SEI CERT, ISO/IEC et AUTOSAR

Astrée traite précisément et sûrement les calculs de virgule flottante. Toute erreur d’arrondi possible ainsi que leurs effets cumulatifs sont prit en compte. Le même s’applique pour des valeurs −∞, +∞ et NaN dans tous des calculs et des comparaisons.

Comment ça marche

Astrée est basé sur l’interprétation abstraite de la sémantique des programmes analysés et calcule donc une sur-approximation de l’ensemble des comportements possibles du code à l’exécution. Astrée est donc correct et ne peut jamais omettre de signaler une erreur à l’exécution.

Par contre, Astrée est incomplet à cause de la sur-approximation qui peut introduire des comportements et donc des erreurs fictives impossibles dans toutes les exécutions réelles. On parle alors de fausses alarmes. L’objectif est donc de calculer des approximations suffisamment précises pour éviter toute fausse alarme (les vraies alarmes devant conduire à une correction du code).

Astrée est paramétrable et dispose de directives d’analyses pour s’adapter aux besoins spéci­fiques des utilisateurs. Il peut être également facilement étendu pour inclure de nouvelles abst­ractions permettant d’atteindre l’objectif de précision, sans aucune fausse alarme, sur des fa­milles précises de programmes.

Un exemple de famille de programmes pour lequel Astrée est très précis est celui des codes de contrôle commande temps réel en­gendrés automatiquement à partir d’une spécification synchrone de haut niveau (comme SCADE).

Qualification de l’outil

Nous offrons des kits de qualification speciales pour Astrée, qui simplifient votre processus de certification DO-178B/C, ISO 26262 ou IEC 61508.

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