À propos
Le projet
Depuis quelques années, le langage de programmation Rust vient concurrencer les langages Ada/C/C++ établis dans le monde des logiciels critiques, embarqués ou non. Les acteurs actuels et futurs développant des logiciels critiques en Rust se posent désormais la question de l’opportunité d’utiliser des outils d’analyse formelle pour Rust.
C’est pour répondre à cette question que l’outil Creusot pour Rust a été développé par l’INRIA. L’outil est basé sur les mêmes fondations technologiques que les outils d’analyse formelle d’AdaCore et de TrustInSoft : la plateforme Why3 développée par l’INRIA et les mêmes prouveurs automatiques dont le prouveur Alt-Ergo d’OCamlPro.
Le projet DéCySif vie l’amélioration de tous ces outils afin de converger vers une solution optimale pour la sécurité et la sûreté des systèmes critiques.
Le consortium
Adacore
Fondée en 1994, AdaCore conçoit et fournit des outils de développement et de vérification de logiciels destinés à des applications pour lesquelles la sûreté, la sécurité et la fiabilité sont des éléments critiques. \ L’utilisation des produits AdaCore connaît une croissance continue dans des applications critiques telles que les systèmes spatiaux, l’avionique commerciale, les systèmes militaires, le contrôle aérien, les systèmes ferroviaires, les appareils médicaux ou les services financiers. AdaCore jouit d’une base fournie de clients internationaux en croissance constante; visitez le site www.adacore.com/industries/ pour de plus amples informations. \ Les produits AdaCore sont libres et accompagnés d’un support expert en ligne fourni par les développeurs eux-mêmes. La société possède un siège nord-américain basé à New York et un siège européen basé à Paris.
INRIA - LMF - Toccata
L’INRIA est l’institut national public français de
recherche en sciences de l’informatique. Les membres INRIA du projet
DéCySif appartiennent au Laboratoire Méthodes Formelles
(LMF) et à l’équipe de recherche
Toccata, localisés à Orsay,
France ; et communs à l’Université Paris-Saclay, au CNRS, et au centre de
recherche INRIA Saclay - Île-de-France.
L’objectif général de l’équipe est de promouvoir les spécifications
formelles et les preuves assistées par ordinateur dans le cadre du
développement de logiciels requérant un haut niveau de confiance dans leur
sûreté de fonctionnement et le respect de comportements attendus.
OCamlPro
OCamlPro est un cabinet d’étude en R&D spécialisé dans les problèmes
d’ingénieurie liés aux langages de programmation, aux spécificités métiers
ou à la dette technique. La société est engagée dans l’open source
et contribue aux langages Rust, WebAssembly et OCaml. La société développe
aussi le prouveur SMT Alt-Ergo utilisé dans DéCySif.
OCamlPro est également active dans le domaine de la certification
Critères Communs au niveau EAL6 et l’utilisation des méthodes formelles
(Coq, Lean4, Why3).
TrustInSoft
TrustInSoft commercialise des outils et services d’analyse exhaustive de code source C et C++ permettant d’apporter des garanties mathématiques sur la qualité des logiciels de ses clients. Ces solutions d’analyses de logiciel permettent d’avoir des garanties sur la sécurité et la fiabilité du code source sans modifier le processus de développement. Ces offres sont déployées dans le monde entier chez les développeurs et intégrateurs de composants logiciels issus des industries aéronautique, automobile, ferroviaire, militaire, nucléaire, télécoms, ou l’IoT.
Coordinateur
La société TrustInSoft est le coordinateur du projet. Pour toute demande d’information, veuillez passer par le formulaire de contact.