
Vérification statique de code : TrustInSoft renforce dans ses outils les capacités d’analyse formelle du langage Rust Avec la version 2025.10 de de sa chaîne d'outils de vérification formelle TIS Analyzer, la société française TrustInSoft, spécialiste de l'analyse statique exhaustive de code, introduit des capacités d'analyse formelle du langage Rust afin de détecter les comportements indéfinis et indésirables d’un code écrit dans ce langage. Cette version apporte aussi une expérience multithreading améliorée pour les développeurs. Cette évolution de TIS Analyser permet aux équipes travaillant avec Rust ou avec des bases de code mixtes dans des environnements critiques pour la sécurité d’acquérir, selon TrustInSoft, une confiance formelle et mathématique dans la sécurité et la fiabilité de leurs logiciels. Présentée lors du salon Embedded World North America qui s’est déroulé à Anaheim (Californie) du 4 au 6 novembre 2025, cette mise à jour de TIS Analyzer étend ainsi les capacités de vérification formelle de l'outil en direction du langage Rust et des systèmes en temps réel. Avec comme objectif d’aider les équipes de développement travaillant avec Rust ou avec des bases de code multilangages dans des environnements critiques à acquérir une confiance mathématique dans la fiabilité et la sécurité de leurs logiciels. « TIS Analyzer 2025.10 répond aux attentes des développeurs et des équipes de sécurité qui souhaitent avoir à disposition un outil qui ne se contente pas de suppositions, de détections incomplètes et de vérifications non approfondies, explique Caroline Guillaume, le PDG de TrustInSoft. Dans ce sens, cette version de notre outil apporte une confiance formelle et mathématique aux parties les plus récentes et les plus complexes d’un code source. » TrustInSoft indique que le langage Rust occupe désormais une place centrale dans le monde de la programmation système, notamment grâce à sa sécurité mémoire intégrée. Cependant, Rust ne fournit pas toutes les garanties de sécurité, comme la protection contre les dépassements de capacité et l'appel sécurisé aux fonctions C. De plus, selon TrusInSoft, Rust possède un sous-langage non sécurisé où la preuve de la sécurité mémoire incombe à l'utilisateur. Pour rappel, le langage Rust, initié par les ingénieurs de Mozilla dès 2006, est un langage de programmation qui intègre des contrôles de sécurité mémoire au moment de la compilation, agissant ainsi comme une protection contre les vulnérabilités courantes présentes dans les systèmes écrits en C/C++, telles que les dépassements de tampon et l'arithmétique des pointeurs. Ces contrôles de sécurité mémoire procurent des mesures de prévention qui réduisent notamment le besoin de tests d'exécution et de débogage exhaustifs. En mars 2025, TrustInSoft a conclu un partenariat avec la société allemande Ferrous Systems, un pionnier dans les outils et solutions Rust pour les systèmes critiques et embarqués, afin d'intégrer la prise en charge de Rust et les avantages de sa chaîne d'outils de compilation qualifiée, baptisée Ferrocene, au moteur d'analyse formelle de TrustInSoft. Avec cette approche, TIS Analyzer 2025.10 offre désormais les mêmes garanties d'investigation interactive des causes profondes, de couverture de code et de preuves mathématiques aussi bien pour Rust que pour le C et le C++. Ainsi, souligne TrustInSoft, les équipes d'ingénierie qui utilisent Rust avec du C/C++ traditionnel ou qui travaillent dans des environnements critiques, ont la possibilité de détecter les comportements indéfinis et indésirables, les plantages et les vulnérabilités mémoire dans les bases de code multilangages avant leur mise en production. Au-delà, TrustInSoft note que les bogues de concurrence au sein d’un code complexe peuvent parfois être difficiles à déceler. A ce niveau, TIS Analyzer 2025.10 introduit la prise en charge native de l'analyse du code concurrent, notamment pour les systèmes d'exploitation temps réel, les firmwares pilotés par interruptions et les scénarios de multithreading. Dans ce cadre, l’analyseur ne se contente pas de simuler des scénarios mais explore tous les chemins d'exécution, signalant les conditions de concurrence et les comportements non déterministes avec la même rigueur mathématique que pour un code monothread. Enfin, TIS Analyzer 2025.10 complète également la prise en charge des fonctionnalités du langage C23 (ISO/CEI 9899:2024) la dernière norme pour le langage de programmation C publiée officiellement en octobre 2024.

Vérification statique de code : TrustInSoft renforce dans ses outils les capacités d’analyse formelle du langage Rust

Avec la version 2025.10 de de sa chaîne d'outils de vérification formelle TIS Analyzer, la société française TrustInSoft, spécialiste de l'analyse statique exhaustive de code, introduit des capacités d'analyse formelle du langage Rust afin de détecter les comportements indéfinis et indésirables d’un code écrit dans ce langage. Cette version apporte aussi une expérience multithreading améliorée pour les développeurs.

Cette évolution de TIS Analyser permet aux équipes travaillant avec Rust ou avec des bases de code mixtes dans des environnements critiques pour la sécurité d’acquérir, selon TrustInSoft, une confiance formelle et mathématique dans la sécurité et la fiabilité de leurs logiciels.

Présentée lors du salon Embedded World North America qui s’est déroulé à Anaheim (Californie) du 4 au 6 novembre 2025, cette mise à jour de TIS Analyzer étend ainsi les capacités de vérification formelle de l'outil en direction du langage Rust et des systèmes en temps réel. Avec comme objectif d’aider les équipes de développement travaillant avec Rust ou avec des bases de code multilangages dans des environnements critiques à acquérir une confiance mathématique dans la fiabilité et la sécurité de leurs logiciels.

« TIS Analyzer 2025.10 répond aux attentes des développeurs et des équipes de sécurité qui souhaitent avoir à disposition un outil qui ne se contente pas de suppositions, de détections incomplètes et de vérifications non approfondies, explique Caroline Guillaume, le PDG de TrustInSoft. Dans ce sens, cette version de notre outil apporte une confiance formelle et mathématique aux parties les plus récentes et les plus complexes d’un code source. »

TrustInSoft indique que le langage Rust occupe désormais une place centrale dans le monde de la programmation système, notamment grâce à sa sécurité mémoire intégrée. Cependant, Rust ne fournit pas toutes les garanties de sécurité, comme la protection contre les dépassements de capacité et l'appel sécurisé aux fonctions C. De plus, selon TrusInSoft, Rust possède un sous-langage non sécurisé où la preuve de la sécurité mémoire incombe à l'utilisateur.

Pour rappel, le langage Rust, initié par les ingénieurs de Mozilla dès 2006, est un langage de programmation qui intègre des contrôles de sécurité mémoire au moment de la compilation, agissant ainsi comme une protection contre les vulnérabilités courantes présentes dans les systèmes écrits en C/C++, telles que les dépassements de tampon et l'arithmétique des pointeurs. Ces contrôles de sécurité mémoire procurent des mesures de prévention qui réduisent notamment le besoin de tests d'exécution et de débogage exhaustifs.

En mars 2025, TrustInSoft a conclu un partenariat avec la société allemande Ferrous Systems, un pionnier dans les outils et solutions Rust pour les systèmes critiques et embarqués, afin d'intégrer la prise en charge de Rust et les avantages de sa chaîne d'outils de compilation qualifiée, baptisée Ferrocene, au moteur d'analyse formelle de TrustInSoft.

Avec cette approche, TIS Analyzer 2025.10 offre désormais les mêmes garanties d'investigation interactive des causes profondes, de couverture de code et de preuves mathématiques aussi bien pour Rust que pour le C et le C++.

Ainsi, souligne TrustInSoft, les équipes d'ingénierie qui utilisent Rust avec du C/C++ traditionnel ou qui travaillent dans des environnements critiques, ont la possibilité de détecter les comportements indéfinis et indésirables, les plantages et les vulnérabilités mémoire dans les bases de code multilangages avant leur mise en production.

Au-delà, TrustInSoft note que les bogues de concurrence au sein d’un code complexe peuvent parfois être difficiles à déceler. A ce niveau, TIS Analyzer 2025.10 introduit la prise en charge native de l'analyse du code concurrent, notamment pour les systèmes d'exploitation temps réel, les firmwares pilotés par interruptions et les scénarios de multithreading. Dans ce cadre, l’analyseur ne se contente pas de simuler des scénarios mais explore tous les chemins d'exécution, signalant les conditions de concurrence et les comportements non déterministes avec la même rigueur mathématique que pour un code monothread.

Enfin, TIS Analyzer 2025.10 complète également la prise en charge des fonctionnalités du langage C23 (ISO/CEI 9899:2024) la dernière norme pour le langage de programmation C publiée officiellement en octobre 2024.