A Verified Information-Flow Architecture (bibtex)
by Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
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.
Reference:
A Verified Information-Flow Architecture (Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach), In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, 2014.
Bibtex Entry:
@inproceedings{AmorimCDDHPPPT14,
  title = {A Verified Information-Flow Architecture},
  author = {
    Arthur {Azevedo de Amorim} and
    Nathan Collins and
    Andr\'e DeHon and
    Delphine Demange and
    Catalin Hritcu and
    David Pichardie and
    Benjamin C. Pierce and
    Randy Pollack and
    Andrew Tolmach
  },
  booktitle = {41st ACM SIGPLAN-SIGACT Symposium on Principles
               of Programming Languages (POPL)},
  shortbooktitle = {POPL},
  month = jan,
  year      = {2014},
  publisher = {ACM},
  pages     = {165-178},
  isbn      = {978-1-4503-2544-8},
  ee        = {http://doi.acm.org/10.1145/2535838.2535839},
  url = {http://www.crash-safe.org/node/29},
  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.},
}
Powered by bibtexbrowser