Vérification assistée par ordinateur

Vérification assistée par ordinateur

Garantissez un haut niveau d’assurance qualité

Le logiciel contrôle des aspects de plus en plus nombreux, complexes et parfois vitaux de notre quotidien. Les méthodes actuelles de développement reposent encore largement sur le codage manuel et les tests. Celles-ci peinent à offrir des garanties fortes sur l’absence de bogues. Nous présentons ici quelques techniques d’analyse de design et de code ainsi que des outils informatiques correspondant afin d’accroître l’assurance qualité.

Date: 13 octobre 2010

Expertises:

Ingénierie des systèmes IT complexes 

Thème d'innovation: Cyber Sécurité 

A propos du projet: CE-IQS 

Les méthodes actuelles de développement reposent largement sur l’humain qui est faillible. Un logiciel peut donc contenir des erreurs. Pour se prémunir des erreurs humaines lors du développement, les industriels peuvent recourir à des étapes de test du produit logiciel, ainsi qu’à des étapes de relecture du logiciel ou de différents plans ou modèles représentant le logiciel. Toutefois, ces méthodes ont une efficacité limitée de part la complexité même des produits logiciels. Face à ce constat, des techniques spécifiques ont été développées pour vérifier les logiciels, en utilisant la puissance de calcul offerte par les ordinateurs.

Vérification et validation - limitations

Le cycle de vie du logiciel suit plusieurs étapes, tout comme l’élaboration d’une maison. Ces étapes sont en général :

  1. L’élaboration du cahier des charges définissant les propriétés souhaitées du logiciel.
  2. Une phase conceptuelle d’élaboration du logiciel incluant l’élaboration de son architecture et la mise au point des éventuels algorithmes spécifiques au problème.
  3. L’implémentation du logiciel.

Des erreurs peuvent être commises à chacune de ces étapes, c’est pourquoi les industriels effectuent des vérifications du travail réalisé à ces différentes étapes :

  1. On peut pour s’assurer que le comportement spécifié dans le cahier des charges est adapté à la situation en faisant tester le comportement en conditions réelles par les utilisateurs finaux au moyen du logiciel final, d’un prototype ou d’un simulateur de comportement.
  2. L’architecture peut être vérifiée par des équipes indépendantes, les algorithmes spécifiques peuvent êtres testés sur des jeux de données spécifiques.
  3. L’implémentation peut être testée par rapport au cahier des charges.

Ces différentes techniques de validation sont limitées et/ou sujettes à l’erreur humaine :

  • Les jeux de tests sont toujours incomplets : certaines combinaisons d’entrées ne seront pas testées. Par exemple, il n’est pas possible de tester entièrement un algorithme de division entière sur 32 bits ; cela prendrait plus d’un demi milliard d’années à raison d’un test toutes les microsecondes. On se cantonne en général à des tests incomplets, mais représentatifs du logiciel.
  • Une relecture par un humain n’apporte pas de garantie absolue d’absence d’erreur .
  • Tout ne peut pas être testé. Par exemple on ne peut pas tester qu’un logiciel ne contient pas de failles de sécurité. Au mieux, on peut tester l’une ou l’autre attaque classique, mais un pirate informatique pourrait découvrir une nouvelle vulnérabilité dans un logiciel.

La recherche en informatique s’est depuis longtemps attaquée à ces problèmes, et des solutions sont maintenant mûres pour être déployées industriellement. Nous présentons ci-dessous trois technologies à portée de main de l’industrie wallonne :

  • Génération automatique de jeux de tests.
  • Analyse automatique de modèles spécifiques.
  • Vérification automatique de code source logiciel.

Génération de jeux de tests

Constituer manuellement un jeu de test est souvent un travail fastidieux : la personne qui élabore ces tests procède souvent par un raisonnement mental où elle envisage des combinaisons d’entrées qui explorent en détail le comportement du logiciel. La recherche du testing a proposé des critères permettant d’estimer la qualité des jeux de test. Cela s’appelle un critère de couverture. Il existe des outils capables de générer des jeux de tests au départ d’une description fonctionnelle d’un logiciel (un modèle) et peuvent assurer la production de jeux de tests garantissant certains critères de couverture. Le prix à payer est la production du modèle et d’un composant permettant d’exécuter les tests généralement exprimés en termes plus abstraits sur l’infrastructure concrète d’implémentation.

Le CETIC dispose de l’expertise dans une série d’outils de ce type, notamment : Qtronic, NModel, Smartesting, de même qu’avec des outils d’estimations de couverture de tests permettant de vérifier la couverture effective (Cobertura, Emma, CoverageValidator…)

Vérification exhaustive de protocoles

Un protocole de communication est un type d’algorithme très particulier visant à coordonner les actions d’un système distribué au moyen de l’échange de messages informatiques. Un protocole de communication peut contenir des erreurs bien connues sous le nom de deadlock, désynchronisation, etc. Détecter qu’un protocole contienne ce type d’erreur est extrêmement fastidieux, surtout si on souhaite que le protocole tolère des retards de transmission ou des pertes de message potentiellement causés par un réseau informatique. La recherche a mené à l’élaboration de techniques automatiques permettant de vérifier le bon comportement d’un protocole face à tous les cas de figure possibles. En utilisant ces techniques, il est possible de vérifier le bon fonctionnement du protocole avant même de l’implémenter.

Le CETIC dispose de l’expertise dans une série d’outils de ce type : SPIN, NuSMV, RODIN…

Vérification automatique de code source

Suite à l’explosion de la fusée Ariane V lors de son vol inaugural, l’Europe a investi d’énormes moyens dans la recherche sur l’analyse de code. Pour rappel, cette catastrophe est due à une erreur logicielle dans un programme Ada. Un nombre à virgule flottante en 64 bits devait être converti en entier de 16 bits. Malheureusement, au moment du crash, ce nombre en 64 bits était trop grand que pour être représenté en 16 bits. La valeur stockée dans cet entier de 16 bits a donc été inexacte. Ces nombres intervenaient dans un calcul de calibration des gyroscopes de la fusée. A la suite de cette erreur, la fusée a perdu son équilibre et s’est détruite.

Explosion de Ariane V, le 4 juin 1996

Détecter ce type d’erreur sur un logiciel est extrêmement fastidieux. Dans le cas de la fusée Ariane V, le code avait passé les différentes étapes de validation, de testing, de revue manuelle et de contrôle qualité. Le testing n’apporte donc pas de certitude quant au bon fonctionnement du code, à moins de couvrir tous les cas de figure, ce qui n’est pas toujours faisable.

L’Europe a donc investi dans le développement de technologies d’interprétation abstraite. Cette technique permet d’analyser du code pour identifier ses propriétés. Suite à cet investissement, différents logiciels d’analyse de code par interprétation abstraite ont vu le jour, dans différents domaines.

Il en est résulté une série d’outils qui ont la capacité de détecter l’entièreté des erreurs d’un type spécifique à partir du code source, sans nécessiter le développement de modèle. Sur cette base seule, ils peuvent fournir une garantie d’absence d’erreur que des vérificateurs humains utilisant des tests ne pourraient jamais fournir. En effet les tests ne peuvent pas prouver l’absence d’erreur.

Parmi ces outils citons en deux qui sont des leaders et qui sont disponibles au CETIC :

  • Polyspace est un de ces outils. Il permet de détecter différents types d’erreurs d’exécution tels que les overflow, les pointeurs nuls, etc. Il aurait pu détecter le bug d’Ariane V et est actuellement systématiquement utilisé pour vérifier le code d’Ariane.
  • L’outil Fortify utilise aussi cette technologie. Il est spécialisé dans la détection des failles de sécurité telles que les buffers overflow ou les SQL injection. Ce sont des faiblesses que peut contenir un code source, et qui le rendent vulnérable à un pirate informatique.

Conclusion

En toute généralité, nous comparons ci-dessous une approche basée sur des tests avec une approche basée sur une vérification automatique.

  • Approche classique de test :
    • Nécessite d’écrire des jeux de tests
    • Nécessite éventuellement d’interfacer le logiciel à une suite de tests
    • La qualité de la couverture dépend de la couverture des jeux de tests, elle est très rarement totale
    • Un test peut porter sur n’importe quel aspect : correction du code, correction du comportement
    • Pas de garantie d’absence d’erreur
  • Vérification automatique exhaustive :
    • Pas de jeux de tests à composer
    • Nécessite éventuellement d’adapter le logiciel à l’outil de tests
    • La couverture est totale
    • L’outil vérifie uniquement ce qui est dans son domaine de compétence
    • Garantie totale sur les propriétés traitées

Les outils cités dans cet article sont, ainsi que les autres outils mentionnés dans cet article, à disposition des entreprises intéressées.