Ingénierie de logiciels sécuritaires (SECVannes)

Description

L'ingénierie des systèmes à haut degré de fiabilité et de sécurité est un problème complexe qui nécessite l'apport des méthodes formelles, notamment pour spécifier sans ambiguïté le comportement de ces systèmes ainsi que pour vérifier/valider leur bon fonctionnement tout au long de leur cycle de vie. Ce module vise à donner une base théorique et formelle solide sur les aspects nécessaires à l'ingénierie de systèmes critiques à partir de la spécification jusqu'au système final en utilisent les techniques de raffinement et de preuve. L'accent sera mis également sur la mise en oeuvre de ces techniques pour détecter des failles de sûreté et de sécurité. Cette UE sert de point de depart pour la recherche dans le domaine de l'ingénierie des systèmes de confiance à logiciel prépondérant en fournissant l'état de l'art du domaine et en indiquant les différents axes de recherches.

Mots-clés

Ingénierie des systèmes critiques, Méthodes formelles, Propriétés de sûreté, Propriétés de cybersécurité

Contenu

Partie 1 : Introduction - méthodes formelles pour l'ingenierie des systèmes critiques - importance de la préservation des propriètes de sûreté pour les systèmes critiques Partie 2 : logique de Hoare - triple de Hoare, spécification formelle, règles d'inférence - correction partielle et totale pour les systèmes Partie 3 : méthode event-B - notions mathématiques - méthode event-B (spécifications formelles, raffinement, génération automatique de code) - obligations de preuves et préservation de propriétes Partie 4 : Au delà de la sûreté : la cybersécurité des systèmes critiques - complémentarité entre sûreté et cybersécurité - prise en compte de la cybersécurité dans les systèmes critiques

Compétences acquises

Savoir : - Savoir modéliser les systèmes critiques à l'aide des spécifications formelles. - Connaitre les bases de la technique de preuve de propriétés des systèmes critiques. - Connaitre et comprendre les principaux risques et mesures de cybersécurité associés aux systèmes critiques. Savoir-faire : - Aptitude à developper les implémentations à partir de leurs spécifications formelles en utilisant la technique de raffinement. - Aptitude à spécifier et prouver des propriétés de sûreté et cybersécurité des systèmes critiques.

Enseignant

Elena Leroux