Avec la technologie logicielle innovante RecordFlux, AdaCore, éditeur d’outils de développement logiciel pour applications critiques, propose la possibilité de développer de manière sûre et démontrable des protocoles de communication sous forme binaire, l'une des parties les plus critiques de la pile logicielle en matière de sécurité.
Cette technologie s’appuie d’une part sur un langage spécifique (DSL,Domain Specific Language) qui permet de décrire précisément des formats de données binaires et des protocoles de communication complexes, et d’autre part sur une boîte à outils destinée à vérifier les spécifications et générer un code en langage Spark prouvable (au sens mathématique du terme) et pouvant être exécuté sur un processeur cible.
Selon AdaCore, avec RecordFlux, les utilisateurs peuvent définir et mettre en œuvre des protocoles de communication et prouver des propriétés de sécurité, telles que la sécurité de la mémoire, à un coût et avec un effort bien moindres par rapport à une approche manuelle. La précision du langage utilisé dans RecordFlux garantit ainsi que les spécifications ne sont pas ambiguës, tandis que la manière dont il est conçu, comme un langage de haut niveau, rend les spécifications compréhensibles par les experts du domaine. De plus sa puissance "expressive", toujours selon AdaCore, permet d’appréhender les protocoles les plus complexes du monde réel.
De fait, dans la mesure où le générateur de code RecordFlux produit un code source dans le langage Spark - sous-ensemble d’Ada fondé sur la mise en œuvre de méthodes formelles -, les utilisateurs peuvent obtenir des preuves automatisées d'un grand nombre de propriétés concernant la sécurité du logiciel : pas de dépassement de mémoire tampon, absence d'erreurs de dépassement d'entiers et même preuve des propriétés fonctionnelles.
« L'interaction entre les composants logiciels est régie par des spécifications de protocole et de format, explique Alex Senier, chef de l'équipe RecordFlux d'AdaCore. Malheureusement, la plupart des documents de spécification sont des textes complexes rédigés en anglais qui doivent être traduits manuellement pour les implantations logicielles, ce qui laisse place à l'erreur humaine. De ce fait, les erreurs logiques et les failles critiques sont souvent mal atténuées du fait de l'utilisation généralisée de langages de programmation peu sûrs, ce qui entraîne de graves vulnérabilités en matière de sécurité. Avec RecordFlux, nous visons à fournir une solution qui permet d'économiser du temps et de l'argent en automatisant la génération de code prouvable tout en garantissant l'absence de vulnérabilités de bas niveau, telles que les débordements de mémoire tampon, que des pirates pourraient exploiter. »
RecordFlux fait désormais partie de l’ensemble technologique proposé par AdaCore. Ainsi, en utilisant l’environnement SPARK Pro, les développeurs peuvent reprendre le code Spark généré à partir des spécifications RecordFlux, et prouver automatiquement que ce code est exempt d'erreurs d'exécution et qu'il respecte la spécification originale. Le code généré par RecordFlux est aussi compatible avec GNAT Pro Assurance, la solution d'AdaCore pour les projets présentant les exigences les plus strictes en matière de fiabilité, de maintenance à long terme ou de certification. Les options de durcissement à la compilation fournies par GNAT Pro Assurance peuvent en outre être utilisées pour atténuer d'autres attaques sur le code de gestion de protocoles orientés réseau.
