Analyse statique de programmes

Les premières idées d'analyse statique se trouvent dans les toutes premières recherches sur les ordinateurs naissants, à la fin des années 1940^[1]. Le système construit était alors moins cher que l'accès à la ressource (l'ordinateur). Ce qu'on appelle maintenant les preuves de programmes sont les premières traces d'analyse statique et on en trouve la démonstration dans la conférence d'Alan Turing^[2] en 1949, puis plus tard dans le travail sur les méthodes formelles dans les organigrammes de Robert Floyd^[3] et enfin dans la logique de Hoare.

L’analyse statique englobe une famille de méthodes formelles qui dérivent automatiquement de l’information sur le comportement de logiciels ou de matériels informatiques. Une application possible de l’analyse statique est l’aide automatisée au débogage, en particulier la recherche d'erreurs à l’exécution – grosso modo, des événements qui poussent le programme à « planter ». Parmi les erreurs les plus courantes en ce genre, on peut citer les fautes de frappe pures et simples, notamment pour les langages de programmation sensibles à la casse, les formules faisant intervenir des variables non initialisées ou même non-déclarées, les références circulaires, l'emploi de syntaxes non-portables.

L’analyse de programmes (y compris la recherche d'erreurs possibles à l'exécution) n'est pas déterministe : il n’existe aucune méthode « mécanique » qui peut toujours dire sans se tromper au vu d’un programme si celui-ci va ou non produire des erreurs à l’exécution. C’est là un résultat mathématique fondé sur des résultats d'Alonzo Church, Kurt Gödel et Alan Turing dans les années 1930 (voir le problème de l'arrêt et le théorème de Rice).

Cependant, l’application d’un certain nombre de principes lors du codage permet de réduire le risque d'erreurs à l’exécution ; ces principes offrent en outre l’avantage de faciliter la maintenance du code. Par exemple, le fait de ne pas combiner une affectation et un test réduit le risque lié à l’ordre dans lequel les instructions sont exécutées. Autre exemple : le fait d'avoir des instructions de branchement imbriquées sur trop de niveaux est généralement l’indice d’une complexité du code, qui induit une difficulté à le comprendre et à le tester par la suite. Ce genre de motifs (ou patterns en anglais) sont retrouvés en analysant l’arbre syntaxique du code à l’aide d'un parser, de règles de codage et de métriques.

Il existe deux grandes familles d’analyses statiques formelles de programmes :

• le model checking considère des systèmes à état fini, ou qui peuvent être réduits vers des systèmes à états finis par abstraction ;
• l’analyse statique par interprétation abstraite permet d’obtenir une approximation du comportement du système^[4].

Une autre méthode d'analyse statique, parmi les plus empiriques, consiste à faire lire le code source d'une application par une personne expérimentée mais extérieure à l’équipe de développement. Ceci permet de porter un regard neuf sur le code, du point de vue de sa conception comme de sa réalisation.

La relecture de code peut être guidée par des résultats obtenus par des méthodes d'analyse automatique du code, notamment parmi celles qui cherchent à évaluer la complexité du code et le respect de règles éventuelles de codage.

Le premier outil d’analyse statique de programme est l'utilitaire lint développé à la fin des années 1970 pour le langage C^[5]. L’intérêt du monde industriel pour des outils d'analyse statique, spécialement pour le développement de logiciels critiques, s’est développé à la suite de l’explosion du vol inaugural de la fusée Ariane 5 à cause d'un bug informatique – sans doute un des bugs les plus chers de l'histoire^[6]. Depuis la fin des années 1990, la plupart des compilateurs intègrent une analyse statique de code source plus ou moins poussée, ne serait-ce que comme composant de base de leurs options d’optimisation de code. Les fonctionnalités d'indentation automatique et de commentaires sont, elles, le plus souvent assurées par l’environnement de développement intégré : on peut donc dire que les programmes d'analyse statique ont été victimes de leur succès, dans la mesure où leurs méthodes ont été intégrées à d'autres outils.

Exemples :

• Astrée^[7]
• Checkmarx (logiciel payant)
• Checkstyle : Java
• Coverity : C, C++, Java et JavaScript (logiciel payant)
• Cppcheck : C, C++ (logiciel libre)
• FindBugs : Java (logiciel libre)
• Frama-C (en) : C (logiciel libre)
• CodeSonar (GrammaTech) : C, C++, Java (logiciel payant)
• IBM Rational Logiscope
• Kiuwan : Objective-C, Java, JSP, Javascript, PHP, C, C++, ABAP, COBOL, JCL, C#, PL/SQL, Transact-SQL, SQL, Visual Basic, VB.NET, RPG, SQL*Forms, Android ou Hibernate.
• Klocwork (en) : C, C++, Java et C# (logiciel payant)
• LDRA : C, C++
• PMD : Java, C, C++, C#, Groovy, PHP, Ruby, Fortran, JavaScript, PLSQL, Apache Velocity, Scala, Objective C, Matlab, Python, Go, Swift, Salesforce.com Apex et Visualforce.
• PolySpace (MathWorks) : C, C++, Java (logiciel payant)
• Pylint : Python
• RIPS (en) : Java, JSP, PHP
• SonarQube : Java, C#, C/C++, Cobol, PL/SQL, ABAP, Javascript, PHP, Web, XML, etc. (logiciel libre pour la plupart des langages, payant pour le C/C++ notamment)
• Squale : C, C++, Java
• SQuORE (en)
• Testwell CMT++ : C, C++
• Testwell CMTJava : Java
• PVS-Studio : C, C++ (logiciel payant)
• YAG-Suite : Java, PHP (logiciel payant avec une version freemium)

La complexité des analyses réalisées par les outils varie de celles qui considèrent uniquement le comportement d'instructions et de déclarations individuelles^[8], à celles qui prennent en compte l'intégralité du code source du programme.

L'utilisation des informations obtenues par l'analyse va de la détection d'erreurs potentielles de codage (par exemple, l'outil lint) aux méthodes formelles, qui démontrent mathématiquement des propriétés du programme donné (par exemple, que son comportement correspond à sa spécification).

Les métriques logicielles et la rétro‑ingénierie peuvent être décrites comme des formes d'analyse statique. L'extraction des métriques logicielles et l'analyse statique sont de plus en plus utilisées conjointement, notamment lors de la conception de systèmes embarqués, en définissant les soi‑disant objectifs de qualité du logiciel.

L'évaluation automatisée du code source est un domaine qui n'a pas nécessairement été bouleversé par les avancées de l'informatique théorique, et qui n'a pas non plus conduit à une transformation radicale des capacités d'apprentissage automatique des modèles de langage^[9].

L'application commerciale de plus en plus répandue de l'analyse statique consiste à vérifier les propriétés des logiciels utilisés dans les systèmes informatiques critiques pour la sécurité et à détecter le code potentiellement vulnérable. Par exemple, les secteurs suivants ont défini l'utilisation de l'analyse statique du code comme un moyen d'améliorer la qualité de logiciels devenant de plus en plus complexes et volumineux :

1. Logiciels médicaux : la Food and Drug Administration des États‑Unis (FDA) a défini l'utilisation de l'analyse statique pour les dispositifs médicaux.
2. Logiciels nucléaires : au Royaume‑Uni, l'Office for Nuclear Regulation (ONR) recommande l'utilisation de l'analyse statique des systèmes de protection du réacteur^[10],[11].
3. Logiciels aéronautiques (en combinaison avec l'analyse dynamique).
4. Industrie automobile et ingénierie mécanique (les moyens fonctionnels de sécurité sont une composante intégrée de chaque étape du développement des produits automobiles, ISO 26262^[12],[13], section 8).

Une étude de VDC Research de 2012 a montré que 28,7% des ingénieurs en logiciels embarqués interrogés utilisaient des outils d'analyse statique^[14], et que 39,7% prévoyaient de commencer à les utiliser dans un délai de 2 ans^[15]. Une étude de 2010 a montré que 60% des développeurs interrogés dans des projets de recherche européens utilisaient au moins les analyseurs statiques intégrés à leur IDE. Cependant, seulement environ 10% utilisaient un outil d'analyse supplémentaire (et peut‑être plus avancé).

Dans l'industrie de la sécurité des applications, on utilise également le terme Static Application Security Testing (SAST). Le SAST est une composante importante des cycles de développement sécurisé (SDL), tels que le SDL défini par Microsoft, et constitue une pratique courante chez les éditeurs de logiciels^[16].

• Analyse dynamique de programmes
• Liste d'outils d'analyse statique (en)
• Logique de Hoare