Séminaire des équipes de recherche
A Verified Information-Flow Architecture for SAFE
- Date : 9/09/2013
- Lieu : Inria Paris - Rocquencourt, Amphithéâtre Alan Turing - bâtiment 01
- Intervenant(s) : Andrew Tolmach
- Organisateur(s) : Gallium
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 ofnoninterference 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).