TrustInSoft apporte les méthodes formelles aux développeurs de code critique en C

Créé le 2 mai 2013, TrustInSoft ouvre aux développeurs de code C, C++ et Java la possibilité de mettre en oeuvre de puissantes méthodes d'analyse statique pour détecter des erreurs complexes à trouver par des approches de test classiques. Le tout avec un framework facile d'accés, basé sur l'outil Frama-C issu des technologies du CEA. ... 

Rendre accessibles à tous les développeurs de code critique en C, C++ et Java les méthodes formelles dans un framework combinant différentes techniques d’analyse statique de code. Tel est le credo de la toute jeune société TrustInSoft, créée le 2 mai 2013 par Fabrice Derepas, son actuel CEO, Benjamin Monate, le directeur technique, et Pascal Cuoq, le directeur scientifique, tous trois issus du CEA. Une jeunesse qui ne cache pas une grande ambition. « Aujourd’hui, TrustInSoft est la seule société à apporter un mélange de techniques et de méthodes de vérification statique de code, utilisées dans le monde du nucléaire et de l’aéronautique, à tout type d’application qui exige sûreté et sécurité, qu’il s’agisse d’un middleware open source dans un équipement VPN (Virtual Private Network) ou d’un code critique embarqué dans une bibliothèque de cryptographie », explique Fabrice Derepas. Ce dernier en veut pour preuve l’exemple d’un firmware open source embarqué dans une box Internet, au sein duquel il restait des erreurs. Des erreurs détectées par la technologie de TrustInSoft, malgré les nombreuses phases de test appliquées à cette couche logicielle.   Pascal Cuoq, Benjamin Monate et Fabrice Derepas, les fondateurs de TrustInSoft, sont tous trois issus du CEA   Pour parvenir à un tel résultat, la société s’appuie sur des travaux menés au sein du CEA-List et de l’Inria depuis plusieurs années et qui ont conduit au développement de la boîte à outils de vérification de logiciels écrits en C, le framework en open source Frama-C. L’originalité de la solution, et son caractère unique sur le marché selon les fondateurs de TrustInSoft, est de faire cohabiter et collaborer dans un même environnement plusieurs techniques d'analyse statique, de vérification de règles de codage, d’analyse par interprétation abstraite, de vérification de spécifications fonctionnelles, de méthodes formelles…   Pallier les limites d'outils antérieurs   Rappelons à cet égard que Frama-C trouve son origine dans la décision en 2005 du CEA-List et de l’Inria de développer conjointement un outil open source palliant les limites d’outils antérieurs (Caduceus à l’Inria et Caveat au sein du CEA-List). Avec, comme ambitions, d’utiliser des techniques d'analyses plus variées et de permettre leur combinaison pour contourner les faiblesses de chacune, de vérifier des logiciels non forcément issus de systèmes embarqués critiques, et enfin d’ouvrir la plate-forme afin que n’importe qui puisse développer ses propres analyseurs.     La technologie de TrustInSoft s'appuie sur le framework Frama-C développé au sein du CEA, qui combine et fait collaborer plusieurs techniques d'analyse statique et d'outils de preuve formelle    Après plus de cinq années de travaux, Frama-C a atteint ses objectifs, d’où la naissance aujourd’hui de TrustInSoft, dont l’objectif principal est de cibler la sécurité des logiciels embarqués. « Notre volonté est de proposer notre technologie, à des coûts d’usage normaux, à ceux qui ont besoin de détecter des bugs très difficiles à trouver avec des méthodes de test classiques et qui s'avèrent autant de failles de sécurité exploitables par des attaquants de plus en plus structurés », commente Fabrice Derepas. A ce jour, le développement de Frama-C est supporté par le CEA-List, et TrustInSoft vient de signer un accord de partenariat avec cet organisme, accord qui stipule la création d’un laboratoire commun pour les développements et une clause d’exclusivité pour l’utilisation commerciale de la technologie.   TrustInSoft, qui a bénéficié de 200 000 euros pour son démarrage, vient d'être distingué et a été élu lauréat 2013 du programme Netva (New Technology Venture Accelerator) qui vise à soutenir les jeunes entreprises innovantes françaises dans leur recherche d’opportunités aux Etats-Unis et à les aider à comprendre les réglementations et le marché des technologies américaines. « Nous avons déjà un premier client aux Etats-Unis, précise Fabrice Derepas. Et nous souhaitons nous déployer sur ce territoire très rapidement. » Là aussi, l’ambition est forte, avec un plan d’embauche d’une dizaine de collaborateurs pour arriver à un effectif de 15 personnes dans deux ans, réparti entre les Etats-Unis et la France. Parallèlement, la jeune société a la volonté de lever des fonds, d’ouvrir le capital de l’entreprise pour soutenir son développement et de « devenir au niveau international une société de référence dans le domaine des outils d’aide à la sécurisation des logiciels », affirme Fabrice Derepas.