AdaCore, fournisseur de confiance d'outils de développement et de vérification de logiciels, annonce aujourd'hui le lancement de sa nouvelle technologie RecordFlux conçue pour faciliter le développement et la sécurité des protocoles de communication binaires. Cette technologie comprend un langage dédié (Domain Specific Language, DSL) permettant de décrire précisément des formats de données binaires et des protocoles de communication complexes, ainsi qu'une boîte à outils pour vérifier les spécifications et générer un code SPARK prouvable pouvant être exécuté sur un processeur cible.
Avec RecordFlux, les utilisateurs peuvent définir et mettre en œuvre des protocoles de communication complexes 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 que ce qui serait possible avec une approche manuelle. La précision du DSL RecordFlux garantit que les spécifications ne sont pas ambiguës, sa nature de haut niveau rend les spécifications facilement compréhensibles par les experts du domaine, et sa puissance expressive permet d’appréhender les protocoles les plus complexes du monde réel. Dans la mesure où le générateur de code RecordFlux produit un code source dans le langage SPARK basé sur les méthodes formelles, les utilisateurs peuvent obtenir des preuves automatisées d'un grand nombre de propriétés de sécurité du logiciel résultant. L'effet net est un code plus sûr, plus fiable, et à moindre coût.
« 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. »
« L'interaction entre les composants logiciels est régie par des spécifications de protocole et de format. Malheureusement, la plupart des documents de spécification sont des textes complexes rédigés en anglais qui doivent être traduits manuellement pour les implémentations logicielles, ce qui laisse place à l'erreur humaine », a déclaré Alex Senier, chef de l'équipe RecordFlux d'AdaCore. « 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. »
À propos de RecordFlux
RecordFlux fait partie de l’ensemble technologique proposé par AdaCore pour créer des implémentations de haute qualité de formats de données binaires et de protocoles de communication. La solution comprend un langage dédié, une boîte à outils complète et un support expert personnalisé. En utilisant SPARK Pro, les développeurs peuvent reprendre le code SPARK généré à partir des spécifications RecordFlux, et prouver automatiquement que le code est exempt d'erreurs d'exécution et qu'il respecte la spécification originale.
Le code généré par RecordFlux est compatible avec GNAT Pro Assurance, la solution complète 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 être utilisées pour atténuer d'autres attaques sur le code de gestion de protocole orienté réseau.