Commit 6b87553d authored by Marc's avatar Marc
Browse files

First version

parent eed46a81
......@@ -8,3 +8,4 @@
*.blg
*.run.xml
*.synctex.gz
*.log
This diff is collapsed.
......@@ -34,46 +34,29 @@ The first step in this direction is the support in \textsc{Astrée} of C program
C aims to be portable, and thus, platform-independent. Assembly, on the contrary, is eminently dependent on the hardware. Thus, an OS cannot avoid assembly to use hardware features that lie beyond the framework of C. But not everything requires assembly. The larger part of computation and control flow can be written in C and is more clear and less error-prone this way. That's why assembly only exists as small and scattered pieces included in C code.
We also already have a formal semantics of most asm instructions and of larger part of (barely) reasonable interactions between C and assembly.
We also already have a formal semantics of most asm instructions (all user instructions) and of larger part of (barely) reasonable interactions between C and assembly.
\bigskip
However, some instructions
However, some x86 instructions, hardware features and C/asm interactions are not treated yet.
Pour être capable de faire une analyse sur ces codes, il faut avant tout avoir une sémantique de ces langages.
La sémantique du C est décrite par sa norme, et celle de l'assembleur par la documentation des processeurs. Mais il n'existe pas de description précise des interactions entre le C et l'assembleur. C'est en effet un sujet délicat puisqu'il faut faire des hypothèses supplémentaire sur le C pour qu'il s'interface correctement. Il faut par exemple connaître (plus ou moins précisément) la position des variables dans la mémoire, ou encore, connaître la structure de la pile. Certaines de ces hypothèses existent déjà sous forme d'ABI (notamment les conventions d'appel). D'autres dépendent énormément de la compilation, et fonctionnent en particulier dans le cas d'une compilation simple (style dirigé par la syntaxe), peu optimisante. D'autres part, une description aussi précise de ces hypothèses que l'ABI n'est pas toujours nécessaire. Parfois, une abstraction de celles-ci peut suffire à garantir que le code s'exécute correctement.
Les interactions peuvent prendre différentes formes. La plus simple consiste à modifier les variables du C dans un bloc assembleur. Les interactions les plus complexes agissent sur le flot de contrôle. Par exemple, avec un retour précoce de la fonction ou, pire, en modifiant l'adresse de retour.
\bigskip
Le but du stage est de décrire cette sémantique, trouver les hypothèses raisonnables et automatiser cette déduction dans la mesure de ce qui apparaîtra possible.
For all this missing features, we need to define a model and express the semantics in it, then find a suitable abstraction of it.
\section{Mission}
The subject imply a lot of not very explored questions. This means it is possible to choose a very theoretical subject or, on the contrary, a subject with some subtle implementations.
The more interesting part is probably the abstraction of paging. We need a model of the processor, define the semantics of interesting parts of the language and the properties of interest. Secondly, we shall find a good abstraction. Possibly, we could consider an implementation.
The first part should be relatively quick and easy. The question of abstraction might be much more challenging.
Ce sujet pose un certain nombre de questions peu explorées. Ce qui signifie qu'il est possible de choisir un sujet très théorique ou au contraire plein d'implémentations subtiles ou encore un compromis entre les deux.
Les missions d'un stage équilibré entre théorie et implémentation peuvent être :
\begin{itemize}
\item choisir un modèle pour décrire l'état mémoire lors de l'exécution d'un programme C avec de l'assembleur inline ;
\item comprendre la sémantique des blocs inline et trouver les hypothèses nécessaire de compilation au bon fonctionnement du code cible ;
\item implémenter un interpréteur d'une partie (très) restreinte du C qui gère les blocs assembleurs, notamment le flot de contrôle de l'assembleur (sans hypothèses sur les adresses absolues concrètes) ;
\item inférer automatiquement les règles nécessaires à l'exécution d'un programme.
\end{itemize}
Comme on est toujours dans le cadre de l'embarqué, il y a d'autres questions adjacentes qui sont tout aussi intéressantes. Par exemple, comment prouver que la pile est convenablement vidé pour ne pas laisser de données inutiles alors que le flot de contrôle du C est détourné par de l'assembleur. Ou... les possibilités sont colossales !
We can also look at the problem of stack abstraction in mixed C-asm in the case where assembly read a deep call-frame. This need extra assumptions on the compilation.
\section{Prérequis}
\section{Requisites}
Il n'est rien attendu de particulier en plus que ce qu'on fait en L3, si ce n'est de l'enthousiasme.
There is no special requisite beyond what you probably already know, except enthusiasm.
\section{Équipe d'accueil}
\section{The team}
The internship will take place in the \textsc{Inria} project-team \textsc{Antique}, which is in the computer science department of the ENS. \textsc{Antique} team, formerly named \textsc{Abstraction} is the world leader in abstract interpretation. Abstract interpretation is a unifying theory for approximations of mathematical structures~\cite{cousot1977abstract} that was invented in 1977 by Patrick \textsc{Cousot} (founder of \textsc{Abstraction} team). Abstract interpretation is base on the ideas that 1) the behavior of dynamical systems can be observed at various level of abstractions and that 2) the comparison of two abstraction levels can be formally defined by the intermediary of algebraic objects (such as relations, \textsc{Galois} connections, closure operators, ideals, etc.). Abstract interpretation can be used to provide a framework to several static analysis methods or to derive new static analyzers directly from the definition of an abstraction relation. \textsc{Abstraction} team, then \textsc{Antique} team, develop since 2001 the \textsc{Astree} static analyzer. \textsc{Astrée}~\cite{blanchet2003static} is a static analyzer able to automatically prove the absence of runtime errors of embedded software. \textsc{Astrée} is used in industrial applications, such as avionic, nuclear, automotive and astronautics, mainly in Europe and Asia.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment