Vérification Dynamique des propriétés de Sécurité – VéDySec

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.