Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct:
                  https://webconf.math.cnrs.fr/b/fra-ryy-fjn

			     S É M I N A I R E

                   ______                __    _
                  / ____/___ _____ ___  / /_  (_)_  ______ ___
                 / /   / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
                / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
                \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                                   En ligne

                           Lundi 30 novembre, 10h30

                              -----------------
                              Aïna Linn Georges
                              -----------------

                              Aarhus University

           =======================================================
           Mechanized Program Verification on a Capability Machine
                      in the Presence of Untrusted Code
           =======================================================

A capability machine is a kind of CPU which supports fine-grained privilege
separation using capabilities (a pointer carrying a certain amount of
authority). In this talk, I will present a methodology for verifying the
functional correctness of capability machine programs that call (or are called
by) unknown and potentially malicious code. The key aspects to the approach is
a program logic for reasoning about known code, and a logical relation which
provides a specification for unknown code. The entire setup has been
mechanized in Coq using the Iris framework: https://github.com/logsem/cerise