Les menaces de sécurité sont devenues une préoccupation majeure dans les dernières années.  Une faille de sécurité peut être exploitée par des attaquants et leur permettre de récupérer des données confidentielles (données personnelles, médicales ou bancaires ; secrets industriels ou 

défense ; clefs de chiffrement, etc.), d’avoir accès aux services sans y être autorisés, ou de modifier ou corrompre des données sensibles dans un objectif malveillant (usurpation d’identité, espionnage, contournement des contrôles d’accès, volonté de nuisance, guerres hybrides, attentats, etc.).  

 

Les techniques de vérification statique formelle, notamment par interprétation abstraite ou par  vérification déductive, peuvent permettre de démontrer l’absence de vulnérabilités dans un logiciel. Cependant, ces techniques restent complexes à appliquer sur des logiciels industriels. En effet, leurs applications nécessitent une expertise très pointue et demande beaucoup de temps, ce qui engendre un coût très élevé. Dans ce contexte, développer des techniques de vérification dynamique de propriétés de sécurité — plus facile et plus rapide à utiliser que la vérification statique — est nécessaire pour pouvoir appliquer ces techniques à un plus large spectre de projets. La maturation de ces techniques permettra de sécuriser un plus grand nombre de produits, de réduire le nombre de failles de sécurité et par conséquent de diminuer les risques d’attaques sur les logiciels concernés.

 

Le principal objectif du projet VéDySec est la maturation de l’outillage et la  consolidation des méthodologies d’appilication pour la  spécification et la vérification dynamique de propriétés de sécurité afin d’amener cette  technologie au TRL 6.

 

Ce projet est financé par l'Agence de l'Innovation de Défense (AID) via le programme ASTRID Maturation. Les partnaires du projet sont Thales Research & Technology (coordination), CEA List, Université d'Orléans.