Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-00918847
Contributor : Ben Smyth <>
Submitted on : Sunday, December 15, 2013 - 5:05:03 PM
Last modification on : Wednesday, June 16, 2021 - 3:41:16 AM

Links full text

Identifiers

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. ⟨10.1145/2535838.2535839⟩. ⟨hal-00918847⟩

Share

Metrics

Record views

1431