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 - Rocquencourt
                        Amphi Turing du bâtiment 1

                          Lundi 9 septembre, 10h30

                               --------------
                               Andrew Tolmach
                               --------------

                         Portland State University

             =================================================
             A Verified Information-Flow Architecture for SAFE
             =================================================

SAFE is a clean-slate effort to build a highly secure computer system,
including pervasive mechanisms for tracking and limiting information flows.
The SAFE hardware supports fine-grained programmable tags, with efficient and
flexible propagation and combination of tags as instructions are executed. The
operating system virtualizes these generic facilities to present an
information-flow abstract machine, on which user programs can label sensitive
data with confidentiality and integrity policies.  This talk will describe a
formal, machine-checked model of the key information-flow mechanisms of the
SAFE hardware and software, together with an end-to-end proof of
noninterference for this model.  This is joint work with Arthur Azevedo de
Amorim (UPenn), Nathan Collins (Portland State), André DeHon (UPenn), Delphine
Demange (UPenn), Catalin Hritcu (UPenn), David Pichardie (INRIA), Benjamin
C. Pierce (UPenn), and Randy Pollack (Harvard).