Types et Sécurité

Cours optionnel du Master SSI, Université Paris-Est Créteil.

Emmanuel Polonowski

Objectif du cours

Présenter les avancées récentes dans le domaine de la sémantique des langages de programmation (et de la théorie des types) et leur application à la sécurité.

Cette année, nous nous concentrerons sur une application concrète de la sémantique des langages de programmation -- la sémantique axiomatique -- à des développements réels. Le cours se divise en deux parties :

  1. Introduction au bagage théorique minimal nécessaire pour comprendre la sémantique axiomatique : rappels de typage, logique de Hoare, calcul de plus petite précondition, génération des obligations de preuve ; pour un petit langage impératif avec tableaux et procédures.
  2. Illustration de la théorie en utilisant l'outil industriel SPARK et/ou GNATprove/Why3 pour certifier des programmes non triviaux écrits en Ada (en salle de TP).

Programme

SéanceContenu de la séance
1Introduction
2Rappels
3Sémantique axiomatique du mini-Ada
4Génération des obligations de preuve
5Introduction de l'outil (TP)
6Implantation d'exemples (TP)
7Tableaux
8Implantation d'exemples (TP)
9Procédures
10Implantation d'exemples (TP)
11Implantation d'exemples (TP)

Bibliographie

[1] J. Barnes. High Integrity Software, The SPARK Approach to Safety and Security, Addison-Wesley, 2003.

[2] G. Winskel. The Formal Semantics of Programming Languages, MIT Press, 1993.

[3] M. Gordon. Specification and Verification I, University of Cambridge, 1988.

Liens