Résumé
Dans sa quête du logiciel parfait, l'industrie du logiciel critique (aéronautique, ferroviaire, nucléaire, médical, etc.), tout particulièrement en France, s'ouvre progressivement à l'utilisation d'outils de vérification formelle en complément, ou même en remplacement, de techniques plus traditionnelles de validation du logiciel basées sur le test et les revues. Les outils de vérification à base d'analyse statique, de preuve déductive ou de model checking fournissent des garanties additionnelles et indépendantes sur un logiciel critique; ils peuvent aussi éliminer le besoin pour certains tests, ce qui réduit les coûts et le temps de la validation.
L'utilité des outils de vérification lors du développement et de la qualification du logiciel critique est, cependant, bornée par la confiance que l'on peut accorder à leurs résultats. Un premier risque est l'infidélité d'un outil de vérification: si ce dernier ne prend pas en compte (par erreur ou par conception) absolument toutes les exécutions possibles du logiciel à vérifier, il peut conclure que le logiciel est correct alors même qu'il part en erreur à l'exécution. Un second risque, plus insidieux, est la mauvaise compilation: les outils de vérification opèrent le plus souvent au niveau du code source ou d'un modèle exécutable; un bug dans les compilateurs et générateurs de codes qui produisent le code machine qui s'exécute au final peut conduire à la production d'un code machine erroné à partir d'un programme source correct.
Ces deux risques sont connus dans le monde du logiciel critique, pris en compte dans les textes réglementaires comme le DO-178 pour l'avionique, et partiellement résolus via de bonnes pratiques. Ces dernières sont cependant coûteuses en performances (pas d'optimisation de code) et en tâches supplémentaires de validation (davantage de revues et de tests).
La proposition VERASCO met en avant une autre solution à ces problèmes, plus radicale et dotée de solides fondations mathématiques: la vérification formelle des compilateurs et des outils de vérification eux-mêmes. Notre objectif est de développer un analyseur statique générique à base d'interprétation abstraite pour le langage C, ainsi que plusieurs domaines abstraits avancés, et de prouver la fidélité de cet analyseur avec l'assistant de preuves Coq. De même, nous allons continuer notre travail sur le compilateur vérifié CompCert C [Leroy 2011], le premier compilateur C réaliste qui a été prouvé correct sur machine, et l'emmener jusqu'au point où il sera utilisable dans l'industrie du logiciel critique. Ensuite, nous tirerons parti du couplage étroit entre compilateur et analyseur statique (découlant du fait qu'ils sont prouvés par rapport à la même sémantique formelle) pour, notamment, propager et exploiter à la compilation des propriétés inférées par l'analyseur. Enfin, nous étudierons les questions de qualification d'outils qui doivent être résolues avant que des outils formellement vérifiés puissent être utilisés dans l'industrie aéronautique.
Le logiciel critique mérite les outils de développement et de vérification les plus fiables que la science informatique peut produire. En allant directement vers une vérification formelle complète de tels outils, notre travail engendrera un niveau de confiance sans précédent dans les résultats de l'analyse statique au niveau source, justifiant ainsi pleinement son rôle dans le développement et la certification de logiciels critiques.
