L’outil d’analyse statique de code Ada d’Adacore qualifié pour l’avionique et le ferroviaire

CodePeer, l’outil d’analyse de code statique pour le langage Ada édité par la société Adacore, est désormais qualifié comme outil de vérification pour les projets de développement de code critique dans l’avionique, ...conformément à la spécification DO-178C, et dans le ferroviaire, selon la norme EN 50128: 2011 SIL 4. Selon Adacore, l’outil CodePeer est donc reconnu par les autorités de certification avionique comme la FAA aux États-Unis et l'EASA en Europe comme technologie logicielle capable de donner l'assurance qu’un logiciel est conforme à la définition de ses exigences.

Rappelons que CodePeer analyse un programme en Ada avant son exécution et détecte des erreurs très tôt dans le cycle de conception. Via des méthodes mathématiques avancées, il analyse chaque ligne de code et, compte tenu de toutes les entrées possibles et des chemins existants dans le programme, il détecte les bogues et les vulnérabilités existantes. En l'absence d'erreur potentielle signalée, CodePeer garantit alors formellement que le code est exempt de vulnérabilités.

Dans le cas de code critique dans l’avionique, CodePeer met en évidence notamment les débordements (overflow) sur les entiers et les nombres en virgule flottante, les divisions par zéro, les variables non initialisées, les violations sur les index des tableaux, etc.

Dans le cas de développements pour le ferroviaire, il permet par exemple de détecter les pointeurs nuls, de lire les valeurs qui sont en dehors d’un type ou d’un sous-type Ada, les dépassements des mémoires tampons, etc. Au-delà, l’outil analyse les flux de contrôle (codes inaccessibles, boucles infinies…) et les flux de données (variables et paramètres non initialisés, variables jamais lues…).

"Dans les domaines critiques pour la sécurité, les développeurs doivent avoir des assurances très fortes sur l'outil qu'ils utilisent pour évaluer si leur code est fiable, explique Arnaud Charlet, directeur technique chez AdaCore. Il s’agit d’avoir confiance, et donc de limiter au maximum la nécessité d'un examen manuel du code. CodePeer, via les tests spécifiques qu’il a subis pour l'avionique et le ferroviaire, répond à cette problématique."