Améliorer la sécurité et la fiabilité des logiciels écrits en langages C et C++ grâce à une analyse complète fondée sur des solutions de vérification formelles. Tel est l’objectif affiché par la société française TrustInSoft, éditrice d’outils d'analyse logicielle avancés, en proposant un service de vérification formelle (FVS, Formal Verification Service) de code. Cette solution est conçue pour améliorer la sécurité et la fiabilité des logiciels écrits en langages C/C++ et permet aux utilisateurs de réduire les risques lors des différentes phases de leurs processus de développement en vérifiant rapidement que le code est exempt de bogues.

De ce fait, cette approche réduit la probabilité d'erreurs coûteuses et améliore l'efficacité opérationnelle globale d’une conception.

« Nos services de vérification formelle sont conçus pour fournir aux entreprises une expertise interne en méthodes formelles afin d'améliorer les flux de travail sans interruption, tout en fournissant une preuve mathématique de l'absence d'erreurs d'exécution et de vulnérabilités, explique Caroline Guillaume, P-DG de TrustInSoft. En tirant parti de nos méthodes formelles avancées et de notre outil TrustInSoft Analyzer, nous pouvons fournir une analyse précise et exhaustive qui améliore la sécurité et la fiabilité globales des logiciels des dévelppeurs. »

Concrètement, ce service s'appuie sur le logiciel TrustInSoft Analyzer de TrustInSoft en vue de fournir une analyse complète du code avec une garantie mathématique de détection des erreurs d'exécution et des vulnérabilités critiques. En d’autres termes, il s’agit d’une solution complète de vérification formelle qui étend l’expertise d’équipes internes vers des experts en vérification formelle de TrustInSoft. Ces derniers développent et intègrent des pilotes d'analyse personnalisés adaptés au code source spécifique et aux exigences du projet de chaque utilisateur en garantissant une analyse d'interprétation abstraite, réduisant en conséquence le besoin d'expertise interne en méthodes formelles.

Ainsi, l’approche FVS apporte des ressources d'experts en vérification formelle qui effectuent une analyse de code approfondie et réalisent une analyse réutilisable adaptée à l’environnement logiciel de l’utilisateur afin d’atteindre une couverture de code et une précision d’analyse complètes grâce à TrustInSoft Analyzer.

Enfin, des rapports qui mettent en évidence la couverture obtenue, les bogues identifiés et leurs causes profondes sont fournis aux équipes de développeurs avec des informations directement exploitables pour les phases de correction du code.