Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                            Lundi 29 avril, 10h30

                                --------------
                                Marc Chevalier
                                --------------

                                     ENS

             ====================================================
             Proving the security of an embedded operating system
                        using abstract interpretation
             ====================================================

Software failures can be very grievous, causing deaths, losing money, etc.  In
this situation, we may want to prove that the code is correct: it does not
crash, it does what we expect, it does not leak sensitive information...
Abstract interpretation provides a way for proving such properties using
overapproximation of the semantics.  Our study case is the operating system of
a host platform in planes that lies at the boundary between trusted and
untrusted world. Thus, we want to prove that untrusted code can't affect
trusted code. We need to extend the C analyzer we are developing since the OS
code contains blocks of inline x86 assembly in the C code. Moreover, the
properties we want to prove are not expressible at the C level: we need the
more precise semantics of assembly.