email Admissions
en
Menu
email

Security of embedded systems and IoTs

Teaching goals

L’UE ACF vise à initier les étudiants à l’utilisation de méthodes formelles pour la spécification et le développement de logiciels sûrs. L’accent est mis sur la compréhension des formules logiques et sur leur utilisation pour la spécification de propriétés de programmes. Les programmes considérés seront définis dans un style fonctionnel. L’outil de développement formel utilisé est Isabelle/HOL et le langage d’exportation et d’intégration choisi est Scala.

Course description

L’UE ACF vise à initier les étudiants à l’utilisation de méthodes formelles pour la spécification et le développement de logiciels sûrs.

Skills

A l’issue de cette UE, l’étudiant doit être capable de programmer une application dans un langage de type fonctionnel et de définir en logique les propriétés attendues de cette application. Il doit, également, être en mesure de formaliser les programmes et les propriétés à l’aide d’un assistant de preuve et de mener à bien leur vérification dans cet outil.

Content

  • Cours
    • Logique propositionnelle, logique du premier ordre et modèles.
    • Termes, fonctions, lambda-calcul et types
    • Fonctions récursives
    • Principes et tactiques de preuve
    • Programmation certifiée
    • Techniques de vérification de programmes
  • Travaux pratiques
    • Mise en situation : tentative de programmation correcte d’un algorithme non trivial
    • Initiation à la programmation et à la preuve dans un assistant de preuve (Isabelle/HOL)
    • Initiation à la programmation Scala
    • Projet 1 : programmation et vérification d’un outil de comparaison de
      politique de sécurité pour un firewall simplifié
    • Projet 2 : programmation et vérification d’un analyseur statique
    • Projet 3 : programmation et vérification d’un outil de validation de transaction commerciales

Prerequisite

Maitrise de la programmation. Connaissances de base en logique.

Bibliography

Biography

Thomas Genet is a professor in computer science at ISTIC (Université de Rennes) and a researcher in the Celtique team at IRISA. His research focuses on Verification, Term Rewriting, Tree Automata, Reachability analysis over Term Rewriting Systems, Cryptographic Protocol Verification and Blockchains and smart contract semantics.