A Verified Information-Flow Architecture

Abstract : SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, 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 that allows user programs to label sensitive data with rich confidentiality policies. We present a formal, machine-checked model of the key hardware and software mechanisms used to control information flow in SAFE and an end-to-end proof of noninterference for this model.
Type de document :
Communication dans un congrès
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014, San Diego, CA, United States. 2014, 〈10.1145/2535838.2535839〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00918847
Contributeur : Ben Smyth <>
Soumis le : dimanche 15 décembre 2013 - 17:05:03
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Lien texte intégral

Identifiants

Citation

Arthur Azevedo de Amorim, Nathan Collins, André Dehon, Delphine Demange, Catalin Hritcu, et al.. A Verified Information-Flow Architecture. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014, San Diego, CA, United States. 2014, 〈10.1145/2535838.2535839〉. 〈hal-00918847〉

Partager

Métriques

Consultations de la notice

1074