| I am a PhD student at Inria Rennes and Prove & Run, under the supervision of Thomas Jensen and Vincent Siles. My PhD work is about alleviating proof efforts in micro-kernel based systems, I am particulary interested in the memory management part. | 
|
| I am a PhD student at Inria Rennes and Prove & Run, under the supervision of Thomas Jensen and Vincent Siles. My PhD work is about alleviating proof efforts in micro-kernel based systems, I am particulary interested in the memory management part. |
|
We are currently proving some isolation properties on a para-virtualized hypervisor developed at TU Berlin. We conduct our proof of isolation by refinement. It means that we first build a low-level model of the hypervisor in the form of a transition system which represents its behavior precisely. Then we abstract this model into a simpler transition system, in which properties are simpler to express and prove.
We have written our model and conduct our proof with the language and tools developed at Prove & Run. You can download here the abstract model along with the properties we have proved on it (NB: all the lemmas have been proved).
The concrete model is very close to the C/assembler code, therefore for confidentiality reasons, we do not disclose it at the moment.
P. Bolignano, T. Jensen, and V. Siles: Modeling and Abstraction of Memory Management in a Hypervisor. In Fundamental Approaches to Software Engineering - 19th International Conference, FASE 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, pages 214-230, 2016 [pdf] [slides].
"Hyperviseur, même pas peur !" in Binaire blog, january 2016.