From dc79c1c0136ce81b8a9c0f2daaff930c99807e22 Mon Sep 17 00:00:00 2001
From: Marc Chevalier <git@marc-chevalier.com>
Date: Mon, 18 Dec 2017 21:21:18 +0100
Subject: [PATCH] More
---
sujet.bib | 2 +-
sujet.tex | 68 ++++++++++++++++++++++++-------------------------------
sujet.txt | 12 +++++-----
3 files changed, 36 insertions(+), 46 deletions(-)
diff --git a/sujet.bib b/sujet.bib
index 855a983..33b3f9d 100644
--- a/sujet.bib
+++ b/sujet.bib
@@ -1,7 +1,7 @@
@inproceedings{cousot1977abstract,
title={Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints},
author={Cousot, Patrick and Cousot, Radhia},
- booktitle={Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages},
+ booktitle={Proceedings of the 4th POPL},
pages={238--252},
year={1977},
organization={ACM}
diff --git a/sujet.tex b/sujet.tex
index 3b79674..f4bfa24 100644
--- a/sujet.tex
+++ b/sujet.tex
@@ -16,57 +16,47 @@
\section{Contexte scientifique}
-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.
+
+
+
+\emergencystretch=1000em
\printbibliography
\end{document}
diff --git a/sujet.txt b/sujet.txt
index b4bc0a0..6f9c674 100644
--- a/sujet.txt
+++ b/sujet.txt
@@ -1,6 +1,6 @@
-Dans certains domaines, les bugs informtiques peuvent avoir de lourdes pertes
+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 sureté
+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[1] abstraite permettent de construire des algorithmes qui
@@ -29,7 +29,7 @@ Objectif pour le stage :
- 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.
+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.
@@ -40,11 +40,11 @@ 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
+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'équipe Abstraction, puis l'équipe Antique développe depuis 2001 l'analyseur
statique Astrée. Astrée[4] est un analyseur statique permettant de prouver
-automatiquement l'absence d'erreurs d'exécution dans des logiciels emberqués.
+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.
@@ -52,5 +52,5 @@ automobile et aérospatial, principalement en Europe et Asie.
static analysis of programs by construction or approximation of fixpoints.
[2] www.astree.ens.fr/
[3] www.astreea.ens.fr/
-[4] Blanchet, Cousot, Cousot, Feret, Mauborgne, Miné, Monniaux et Rival. A
+[4] Blanchet, Cousot, Cousot, Feret, Mauborgne, Miné, Monniaux et Rival. A
static analyzer for large safety-critical software.
--
GitLab