Dans certains domaines, les bugs informtiques peuvent avoir de lourdes pertes
humaines, économiques ou environnementales. On parle alors de logiciel critique,
pour lesquels il faut obtenir de fortes garanties tant au niveau de la sureté
(le programme se comporte bien) que sécurité (le programme est protégé des
intrusions extérieures). Les méthodes formelles, en particulier l'interprétation
abstraite~\cite{cousot1977abstract} permettent de construire des algorithmes qui prouvent ces propriétés
Dans certains domaines, les bugs informatiques peuvent avoir de lourdes pertes humaines, économiques ou environnementales. On parle alors de logiciel critique, pour lesquels il faut obtenir de fortes garanties tant au niveau de la sûreté (le programme se comporte bien) que sécurité (le programme est protégé des intrusions extérieures). Les méthodes formelles, en particulier l'interprétation abstraite~\cite{cousot1977abstract} permettent de construire des algorithmes qui prouvent ces propriétés
au niveau sémantique.
L'équipe Antique a créé un analyseur de C, Astrée, spécialisé dans les
programmes embarqués. Cet analyseur a plusieurs succès industriels tels que la
vérification des commandes de vol de l'Airbus A340 et A380~\cite{astree}. Astrée a déjà
été étendu pour supporter l'analyse de programmes asynchrones~\cite{astreea}.
programmes embarqués. Cet analyseur a plusieurs succès industriels tels que la vérification des commandes de vol de l'Airbus A340 et A380~\cite{astree}. Astrée a déjà été étendu pour supporter l'analyse de programmes asynchrones~\cite{astreea}.
\section{Sujet}
Le projet actuel est d'étendre Astrée pour le rendre capable de prouver des
propriétés de sécurité en plus des propriétés de sureté. La première étape en ce
sens est le support dans Astrée de programmes C comportant des blocs de code
écrit en assembleur. L'assembleur offre un accès plus complet aux
fonctionnalités matérielles de l'ordinateur. Le processeur dispose en effet de
mécanismes de gestion des interruptions, exceptions et de la mémoire.
propriétés de sécurité en plus des propriétés de sureté. La première étape en ce sens est le support dans Astrée de programmes C comportant des blocs de code écrit en assembleur. L'assembleur offre un accès plus complet aux
fonctionnalités matérielles de l'ordinateur. Le processeur dispose en effet de mécanismes de gestion des interruptions, exceptions et de la mémoire.
L'analyse d'un logiciel qui utilise ces mécanismes, tel qu'un OS,
va au delà de la simple analyse d'un programme isolé dans une machine abstraite.
Il y a en effet des interactions entre l'OS et les programmes.
va au delà de la simple analyse d'un programme isolé dans une machine abstraite. Il y a en effet des interactions entre l'OS et les programmes.
Le but du stage est d'écrire la sémantique des interruptions, exceptions et des mécanismes de gestion de la mémoire bas niveau, pour un processeur Intel x86.
Le but du stage est d'écrire la sémantique des interruptions, exceptions et des
mécanismes de gestion de la mémoire bas niveau, pour un processeur Intel x86.
\section{Mission}
Objectif pour le stage :
- choisir un modèle pour décrire l'état mémoire d'une machine exécutant un OS et
\begin{itemize}
\item choisir un modèle pour décrire l'état mémoire d'une machine exécutant un OS et
des programmes ;
- écrire une sémantique dans ce modèle des mécanismes de gestion des
interuptions, des exceptions et des mécanismes de protection de la mémoire.
\item écrire une sémantique dans ce modèle des mécanismes de gestion des
interruptions, des exceptions et des mécanismes de protection de la mémoire.
Si le temps le permet :
- déterminer les propriétés dans ce modèle ;
- trouver une abstraction adéquate permettant de vérifier ces propriétés.
Il est attendu que le stagiaire ait des connaissances en sémantique et
éventuellement en interprétation abstraite. Des connaissances basiques en
architecture sont aussi nécessaires ainsi que de ne pas avoir peur de lire des
manuels d'Intel.
Le stage aura lieu dans l'équipe projet Inria Antique qui se trouve au
département d'informatique de l'ENS. L'équipe Antique, précédemment nommée
Abstraction est le chef de file mondial en interprétation abstraite.
L'équipe Abstraction, puis l'équipe Antique développe depuis 2001 l'analyseur
statique Astrée. Astrée~\cite{blanchet2003static} est un analyseur statique permettant de prouver
automatiquement l'absence d'erreurs d'exécution dans des logiciels emberqués.
Astrée est utilisé par l'industrie des domaines de l'avionique, du nucléaire,
automobile et aérospatial, principalement en Europe et Asie.
\emergencystretch=100em
\item déterminer les propriétés dans ce modèle ;
\item trouver une abstraction adéquate permettant de vérifier ces propriétés.
\end{itemize}
\section{Prérequis}
Il est attendu que le stagiaire ait des connaissances en sémantique et éventuellement en interprétation abstraite. Des connaissances basiques en architecture sont aussi nécessaires ainsi que de ne pas avoir peur de lire des manuels d'Intel.
\section{Équipe d'accueil}
Le stage aura lieu dans l'équipe projet Inria Antique qui se trouve au département d'informatique de l'ENS. L'équipe Antique, anciennement nommée Abstraction est le chef de file mondial en interprétation abstraite. L'interprétation abstraite est une théorie unifiée pour l'approximation de structures mathématiques~\cite{cousot1977abstract} qui a été inventé en 1977 par Patrick Cousot (fondateur de l'équipe Abstraction). L'interprétation abstraite est basée sur les idées que 1) le comportement des systèmes dynamiques peut être observé à différents niveaux d'abstraction et que 2) la comparaison entre deux niveaux d'abstraction peut être formellement définie par le truchement d'objets algébriques (comme des relations, des correspondances de Galois, des opérateurs de clôture, des idéaux etc.). L'interprétation abstraite peut être utilisée pour fournir un cadre à différentes méthodes d'analyses statiques ou pour dériver de nouveaux analyseurs statiques directement de la définition d'une relation d'abstraction. L'équipe Abstraction, puis l'équipe Antique développe depuis 2001 l'analyseur statique Astrée. Astrée~\cite{blanchet2003static} est un analyseur statique permettant de prouver automatiquement l'absence d'erreurs d'exécution dans des logiciels embarqués. Astrée est utilisé par l'industrie des domaines de l'avionique, du nucléaire, automobile et aérospatial, principalement en Europe et Asie.
