Certains secteurs industriels, où l'erreur
n'est pas permise pour des raisons de sécurité, sont sensibilisés
depuis longtemps aux méthodes formelles :
le transport terrestre, l'aéronautique, l'énergie nucléaire
sont les plus connus.
Dans les projets devant répondre à des exigences
de qualité,
les méthodes formelles doivent être appliquées
à partir du niveau 4 des normes ITSEC.
Dans des secteurs comme les télécommunications ou l'édition
de logiciels,
les enjeux sont plutôt de nature économique
(combien coûte un effondrement du réseau,
la découverte d'une faille de sécurité, etc.).
Notons que dans le domaine du transport terrestre,
l'utilisation de méthodes formelles (B en l'occurrence)
est déjà un argument de vente ayant fait la différence sur
certains marchés.
La situation pourrait bien évoluer dans le domaine du logiciel,
sous la pression du CSTB2 qui
cherche à faire voter une loi aux USA instaurant
la responsabilité des éditeurs en matière de sécurité
et de faille informatique.
En effet, dans un rapport publié à la suite de la réaction
sécuritaire de septembre 2001, le comité affirme
que les problèmes de sécurité informatique ont été
négligés au cours des dix dernières années, les
performances des logiciels et les fonctionnalités
commerciales ayant été privilégiées au détriment de la sécurité.
En France, plusieurs sociétés s'intéressent de près aux
techniques formelles et y ont investi des moyens,
notamment Matra Tranport International (devenu Siemens),
GEC-Alsthom, RATP,
l'Aérospatiale, Airbus Industrie, Dassault Aviation, GemPlus,
Schlumberger,
France Télécom, Vérilog (devenu Télélogic),
Trusted Logic, Clearsy, et plus récemment
CRIL Technology.
Il faut aussi y ajouter des services de certification
comme le SCSSI.
Les freins qui s'opposent à la diffusion des techniques
formelles sont de nature technique et culturelle.
Sur le plan technique,
la vérification de grands logiciels monolithiques
est hors de portée.
On sait cependant traiter des algorithmes complexes
de petite taille (une à quelques pages),
et des logiciels de taille moyenne reposant sur des principes
simples
(ainsi, la méthode B s'est avérée efficace pour
le traitement d'applications ferroviaires de quelques dizaines
de milliers de lignes de code).
Il est devenu par ailleurs important de considérer
la vérification formelle de propriétés non fonctionnelles (quantitatives).
Il semble réaliste d'attaquer aujourd'hui ce problème,
compte-tenu de la maturation des outils pour la vérification
de propriétés fonctionnelles.
Sur le plan culturel, il est nécessaire de disposer de personnels
convenablement formés et conscients de la portée
des techniques.
L'existence d'une communauté de recherche
à la pointe du domaine
est évidemment une condition favorable
au transfert des technologies au travers de l'enseignement
et des contacts avec le milieu industriel.
Type d'exploitation envisagée, diffusion des résultats et retombées économiques
En dehors des publications scientifiques,
les avancées attendues du projet proposé ici
seront concrétisées par des améliorations aux logiciels libres existants
(Elan, Coq et ses bibliothèques, HCMC, interfaces
pour p-automates)
ou par de nouveaux logiciels libres.
Elles bénéficieront donc automatiquement à l'ensemble des utilisateurs
de ces systèmes.
Parmi les sociétés mentionnées ci-dessus qui
ont des compétences fortes sur les systèmes et techniques
traités dans ce projet sans en être partenaires,
on peut mentionner
par exemple Trusted Logic et Dassault Aviation.
