Commit 395aa812 authored by Marc's avatar Marc
Browse files

Fixes

parent 72cb5dec
......@@ -3,12 +3,12 @@
\usepackage[fr, hyperref]{cheche}
\title{Abstraction of paging and other related x86 stuff}
\title{Abstraction of paging and other low-level features}
\date{}
\author{
Jérôme \textsc{Feret}\\
\href{mailto:jerome.feret@ens.fr}{\texttt{jerome.feret@ens.fr}}\\\\
Assité par\\Marc \textsc{Chevalier}\\
helped by\\Marc \textsc{Chevalier}\\
\href{mailto:marc.chevalier@ens.fr}{\texttt{marc.chevalier@ens.fr}}
}
......@@ -26,31 +26,23 @@ In some contexts, bugs might lead to serious casualties or grave economic or env
\section{Research subject}
To guarantee that a critical system behaves correctly, each layer must be certified. We often look at the final software. This is of course a necessary first step, but it is incomplete. Indeed, we need to ensure the good functioning of the operating system (if applicable), the hardware, and so on. We have often no choice but trusting the hardware, for want of an implementation to certify, but we could certainly look at the OS.
To guarantee that a critical system behaves correctly, each layer must be certified. We often look at the final software. This is of course a necessary first step, but it is incomplete. Indeed, we need to ensure the good functioning of the operating system (if applicable), the hardware, and so on. We have often no choice but trusting the hardware, because of the absence of an implementation to certify, nevertheless we could certainly look at the OS.
The study case is the analysis of an embedded OS. Especially, we want to prove memory isolation between processes.
The case study is the analysis of an embedded OS. Especially, we want to prove memory isolation between processes. The first step in this direction is the support in \textsc{Astrée} of C programs including inline x86 assembly blocs. 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.
The first step in this direction is the support in \textsc{Astrée} of C programs including inline x86 assembly blocs.
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 assembly instructions (all user instructions) and of larger part of (barely) reasonable interactions between C and assembly.
\bigskip
However, some x86 instructions, hardware features and C/asm interactions are not treated yet.
For all this missing features, we need to define a model and express the semantics in it, then find a suitable abstraction of it.
We also already have a formal semantics of most assembly instructions (all user instructions) and of larger part of (barely) reasonable interactions between C and assembly. However, some x86 instructions, hardware features and C/asm interactions are not treated yet. 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 implies 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.
A lot of things remains to do. As a consequence, 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 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, derive an static analysis accordingly by the means of abstract interpretation, and implement the so-obtained analysis as an independent abstract domain of the \textsc{Astrée} analyzer.
The first part should be relatively quick and easy. The question of abstraction might be much more challenging.
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 and adequate abstraction.
Another interesting issue is related to the problem of stack abstraction stack abstraction in mixed C-asm in the case where assembly read a deep call-frame. This need extra assumptions on the compilation and adequate abstraction. Then an independent abstract domain can be derived accordingly.
We expect the intern to solve one of these two issues. Yet, the offer is quite open, and it is also possible to investigate about another issue related to the analysis of the security properties of the host platform.
\section{Requisites}
......@@ -65,3 +57,23 @@ The internship will take place in the \textsc{Inria} project-team \textsc{Antiqu
\printbibliography
\end{document}
# Research subject
To guarantee that a critical system behaves correctly, each layer must be certified. We often look at the final software. This is of course a necessary first step, but it is incomplete. Indeed, we need to ensure the good functioning of the operating system (if applicable), the hardware, and so on. We have often no choice but trusting the hardware, because of the absence of an implementation to certify, nevertheless we could certainly look at the OS.
The case study is the analysis of an embedded OS. Especially, we want to prove memory isolation between processes. The first step in this direction is the support in Astrée of C programs including inline x86 assembly blocs. 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 assembly instructions (all user instructions) and of larger part of (barely) reasonable interactions between C and assembly. However, some x86 instructions, hardware features and C/asm interactions are not treated yet. For all this missing features, we need to define a model and express the semantics in it, then find a suitable abstraction of it.
# Mission
A lot of things remains to do. As a consequence, 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, derive an static analysis accordingly by the means of abstract interpretation, and implement the so-obtained analysis as an independent abstract domain of the Astrée analyzer.
The first part should be relatively quick and easy. The question of abstraction might be much more challenging.
Another interesting issue is related to the problem of stack abstraction stack abstraction in mixed C-asm in the case where assembly read a deep call-frame. This need extra assumptions on the compilation and adequate abstraction. Then an independent abstract domain can be derived accordingly.
We expect the intern to solve one of these two issues. Yet, the offer is quite open, and it is also possible to investigate about another issue related to the analysis of the security properties of the host platform.
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