PRQA présente une nouvelle approche en matière de détection des failles de sécurité et défauts en C et C++

Le nouveau module Dataflow comprend un solveur de problèmes SMT (Satisfiability Modulo Theories), une technologie de pointe conçue pour les produits réalisant des analyses statiques en profondeur. Une suite d’outils uniques de vérifications analytiques pour C et C++ a ainsi été créée, combinant la technologie du solveur SMT aux expertises internes en langage et en analyse syntaxique des flux de commande et de sémantique détaillée.



« Le marché des logiciels embarqués est dominé par l’utilisation des langages C et C++ », explique Fergus Bolger, directeur technique chez PRQA. « La plupart des outils d’analyse statique actuels, en particulier ceux destinés aux logiciels embarqués, se limitent aux couches interface du logiciel, plutôt que de s’intéresser à la sémantique détaillée du code. Pourtant, pour les développeurs de logiciels embarqués, l’analyse du flux de données, à un niveau de fonction précis et détaillé, est tout aussi importante. Elle doit se faire, pour les systèmes critiques basés sur des logiciels embarqués, littéralement au niveau des bits et des octets. »



Grâce à la puissance d'un solveur SMT ayant fait ses preuves, le module Dataflow possède un certain nombre de fonctionnalités de modélisation du code :



• L’interdépendance des variables fait partie de la modélisation du code, que ce soit pour les assignations ou la détermination d’expressions conditionnelles (flux de commande).



• La modélisation utilise une approche bidirectionnelle, où par exemple des tests de conditions, réalisés ultérieurement, peuvent identifier l'utilisation douteuse de variables.

• Les itérations de boucles sont modélisées avec précision, y compris les incrémentations non unitaires, les contrôles de boucles utilisant plusieurs variables et les boucles imbriquées.

• Les espaces-mémoire sont modélisés exactement tel que le compilateur va les allouer, représentant la taille réelle de chaque type ; les unions et opérations

bit-à-bit sont gérées intelligemment.



Cependant, le vrai point fort de la solution de PRQA réside dans l’éventail de vérifications analytiques disponible. En effet, outre toutes les failles bien connues du C et du C++, elles couvrent également les opérations pertinentes et importantes pour les applications embarquées :



• Opérations de pointeurs invalides : opérations mathématiques et de déréférencement sur un pointeur nul, calcul sur ou déréférencement d’un pointeur invalide (par ex. : dépassements négatif et positif du tampon, opérations de pointeurs sur des pointeurs de différents types).

• Opérations mathématiques dangereuses : divisions par zéro, opérations mathématiques produisant un dépassement d'entier, conversion de valeurs négatives en valeur non signée et autres problèmes de conversion rencontrés, opérations de décalage de bits entraînant des valeurs tronquées ou invalides.

• Anomalies de commandes de flux : initialisations ou assignations redondantes, opérations logiques et expressions de commande de flux invariantes, code mort, boucles infinies, variables non définies, valeurs de retour incorrectes.



La solution Dataflow de PRQA intègre l’analyse des appels de fonctions API des bibliothèques standard, ce qui, associé aux vérifications de pointeurs, offre une solution complète de détection des failles de sécurité, basée sur l’analyse du langage. Pour chaque défaut, le chemin et l’historique concernant l’anomalie détectée sont indiqués au moyen de sous-répertoires.



Les développeurs logiciel et les entreprises qui les emploient se doivent de gérer les problèmes de qualité du code, tant en termes de respect des règles de codage visant à prévenir les erreurs qu’en termes de détection juste et précise des bogues. Le nouveau module Dataflow de PRQA apporte une réponse à cet important besoin.