En génie logiciel, il est important de s'assurer qu'un système logiciel se comporte correctement et de manière fiable. Ceci est particulièrement crucial pour les systèmes critiques, tels que les services bancaires en ligne, le commerce électronique et les systèmes en temps réel. Une technique prometteuse pour vérifier les propriétés de ces systèmes est appelée des scores de preuve, qui utilise une méthode appelée réécriture du terme.
Un score de preuve est composé de déclarations et de réécritures de telle sorte que si tous les composants évaluent comme souhaité, le problème est résolu. Cette méthode établit un équilibre entre l'automatisation et l'effort manuel: les machines gèrent les tâches de routine comme la substitution, la simplification et la réduction, tandis que les humains se concentrent sur les tâches les plus intéressantes, telles que les stratégies de preuve décider. De plus, même les preuves partiellement terminées peuvent fournir des commentaires précieux, indiquant souvent quoi essayer ensuite.
Cette technique a été mise en pratique par le biais de langues de spécification algébrique, en particulier la famille OBJ, comme OBJ3, Cafeobj et Maude, qui sont conçues pour être exécutables via la réécriture du terme. Un avantage clé des scores de preuve est qu'ils utilisent les mêmes mécanismes de syntaxe et d'évaluation que le langage utilisé pour spécifier le système, ce qui rend le processus de vérification lisse et étroitement intégré.
Par conséquent, cette méthode a été appliquée avec succès à un large éventail de systèmes et de protocoles. Cependant, cette méthode présente également plusieurs inconvénients, qui l'ont limité à des environnements principalement académiques.
Pour comprendre cet écart, une équipe de recherche dirigée par le professeur Kazuhiro Ogata, avec le professeur adjoint Duong Dinh Tran du Japon Advanced Institute of Science and Technology (JAIST), a mené une étude sur les scores passés, présents et futurs de preuve. « Les scores de preuve ont prouvé leur capacité à vérifier que les systèmes, y compris ceux sur lesquels nous comptons chaque jour, répondent à leurs conceptions.
« Dans cette étude, nous analysons le passé et le présent des scores de preuve pour comprendre leurs défis actuels et trouver des moyens d'améliorer leur applicabilité », Prof. Ogata et Asst. Le professeur Tran explique. Leur étude est publiée dans la revue Enquêtes informatiques ACM.
Des scores de preuve ont été proposés pour la première fois dans les années 1990 par le chercheur Joseph A. Goguen. Depuis lors, il a été implémenté dans plusieurs langues OBJ. Dans l'étude, les chercheurs ont exploré les fondements théoriques des scores de preuve et analysé leurs implémentations dans différentes langues OBJ.
Les chercheurs ont également étudié plusieurs cas où des scores de preuve ont été appliqués avec succès, notamment la communication, l'authentification et les protocoles de commerce électronique, les systèmes en temps réel, les protocoles cryptographiques modernes, dans les protocoles cryptographiques post-quanttum, qui sont des méthodes de chiffrement conçues pour être sûres par rapport aux prochains ordinateurs quantiques puissants.
Cette analyse a révélé les points forts des scores de preuve. Plus particulièrement, la même syntaxe utilisée pour spécifier un système peut également être utilisée pour prouver les propriétés du système. Contrairement aux méthodes traditionnelles de fourniture du théorème, qui peuvent être très abstraites, cette propriété des scores de preuve garantit que chaque étape de la preuve est fondée sur la définition formelle du système, ce qui rend la preuve plus transparente et accessible. En outre, les scores de preuve sont écrits en programmes et, par conséquent, sont aussi flexibles que les programmes.
Cependant, cette analyse a également révélé leur principal point faible, c'est-à-dire que les scores de preuve sont programmés par des humains, qui doivent s'assurer que tous les cas possibles ont été traités, les faisant soumettre à des erreurs humaines. Aucune des implémentations précédentes n'a averti les utilisateurs si un cas n'avait été manqué, ce qui est particulièrement problématique avec de grandes preuves. C'est l'une des principales raisons pour lesquelles les scores de preuve n'ont pas été plus largement adoptés.
Alors que des assistants de preuve ont été développés pour résoudre cette faiblesse, ils affaiblissent généralement les avantages des scores de preuve. Cependant, il y a un assistant de preuve appelé CIMPG pour CafeOBJ, qui conserve également les mérites des scores de preuve.
Les chercheurs ont également mis en évidence d'autres problèmes ouverts, notamment la nécessité de preuves plus faciles et lisibles par l'homme, accessibles à un public plus large au-delà des chercheurs, ainsi que pour plus de bibliothèques publiques.
Pour résoudre ces problèmes ouverts, les chercheurs suggèrent que les systèmes modernes devraient fournir un environnement de développement intégré, comme ceux utilisés pour les langages de programmation populaires, qui fourniraient un support graphique et interactif pour l'écriture et la gestion des scores de preuve. Ils suggèrent également d'examiner les dernières fonctionnalités de Maude.
« Les scores de preuve s'avéreront essentiels aux systèmes critiques émergents qui façonneront notre future société », ont déclaré les chercheurs. « Des protocoles de communication utilisés dans les services bancaires en ligne et le commerce électronique à la blockchain et à la cryptographie post-quantum, leur potentiel de création de systèmes fiables est important. »
Dans l'ensemble, cette étude met non seulement le rôle critique des scores de preuve, mais présente également une feuille de route pour les rendre plus pratiques et largement accessibles.
