research-article

Open access

A verified information-flow architecture

Authors:

Arthur Azevedo de Amorim,

Nathan Collins,

Delphine Demange,

Cătălin Hriţcu,

David Pichardie,

Benjamin C. Pierce,

Andrew TolmachAuthors Info & Claims

ACM SIGPLAN Notices, Volume 49, Issue 1

Pages 165 - 178

https://doi.org/10.1145/2578855.2535839

Published: 08 January 2014 Publication History

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.

Supplementary Material

JPG File (d1_right_t7.jpg)

Download
11.35 KB

MP4 File (d1_right_t7.mp4)

Download
166.17 MB

References

[1]

A. Askarov, S. Hunt, A. Sabelfeld, and D. Sands. Termination-insensitive noninterference leaks more than just a bit. ESORICS. 2008.

Digital Library

[2]

A. Askarov and A. Sabelfeld. Tight enforcement of information-release policies for dynamic languages. CSF. 2009.

Digital Library

[3]

T. H. Austin and C. Flanagan. Efficient purely-dynamic information flow analysis. PLAS. 2009.

Digital Library

[4]

A. Banerjee and D. A. Naumann. Stack-based access control and secure information flow. JFP, 15(2):131--177, 2005.

Digital Library

[5]

G. Barthe, D. Pichardie, and T. Rezk. A certified lightweight noninterference Java bytecode verifier. ESOP. 2007.

Digital Library

[6]

L. Beringer. End-to-end multilevel hybrid information flow control. APLAS. 2012.

[7]

J. Brown and T. F. Knight, Jr. A minimally trusted computing base for dynamically ensuring secure information flow. Technical Report 5, MIT CSAIL, 2001. Aries Memo No. 15.

[8]

S. Chen, M. Kozuch, T. Strigkos, B. Falsafi, P. B. Gibbons, T. C. Mowry, V. Ramachandran, O. Ruwase, M. P. Ryan, and E. Vlachos. Flexible hardware acceleration for instruction-grain program monitoring. ISCA. 2008.

Digital Library

[9]

A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. PLDI, 2011.

Digital Library

[10]

A. Chlipala. The Bedrock structured programming system: Combining generative metaprogramming and Hoare logic in an extensible program verifier. ICFP. 2013.

Digital Library

[11]

J. A. Clause, W. Li, and A. Orso. Dytan: a generic dynamic taint analysis framework. ISSTA. 2007.

Digital Library

[12]

M. Dalton, H. Kannan, and C. Kozyrakis. Raksha: a flexible information flow architecture for software security. ISCA, 2007.

Digital Library

[13]

M. Dam, R. Guanciale, N. Khakpour, H. Nemati, and O. Schwarz. Formal verification of information flow security for a simple ARMbased separation kernel. CCS, 2013. To appear.

Digital Library

[14]

A. DeHon, B. Karel, T. F. Knight, Jr., G. Malecha, B. Montagu, R. Morisset, G. Morrisett, B. C. Pierce, R. Pollack, S. Ray, O. Shivers, J. M. Smith, and G. Sullivan. Preliminary design of the SAFE platform. PLOS, 2011.

Digital Library

[15]

D. Y. Deng and G. E. Suh. High-performance parallel accelerator for flexible and efficient run-time monitoring. DSN. 2012.

Digital Library

[16]

U. Dhawan and A. DeHon. Area-efficient near-associative memories on FPGAs. In International Symposium on Field-Programmable Gate Arrays, (FPGA2013), 2013.

Digital Library

[17]

U. Dhawan, A. Kwon, E. Kadric, C. Hriţcu, B. C. Pierce, J. M. Smith, A. DeHon, G. Malecha, G. Morrisett, T. F. Knight, Jr., A. Sutherland, T. Hawkins, A. Zyxnfryx, D. Wittenberg, P. Trei, S. Ray, and G. Sullivan. Hardware support for safety interlocks and introspection. AHNS, 2012.

Digital Library

[18]

J. A. Goguen and J. Meseguer. Unwinding and inference control. IEEE S&P. 1984.

[19]

D. Hedin and A. Sabelfeld. A perspective on information-flow control. Marktoberdorf Summer School. IOS Press, 2011.

[20]

D. Hedin and A. Sabelfeld. Information-flow security for a core of JavaScript. CSF. 2012.

Digital Library

[21]

C. Hriţcu, M. Greenberg, B. Karel, B. C. Pierce, and G. Morrisett. All your IFCException are belong to us. IEEE S&P. 2013.

[22]

C. Hritcu, J. Hughes, B. C. Pierce, A. Spector-Zabusky, D. Vytiniotis, A. Azevedo de Amorim, and L. Lampropoulos. Testing noninterference, quickly. ICFP, 2013.

Digital Library

[23]

J. Jacob. On the derivation of secure components. IEEE S&P. 1989.

[24]

J. B. Jensen, N. Benton, and A. Kennedy. High-level separation logic for low-level code. POPL. 2013.

Digital Library

[25]

M. G. Kang, S. McCamant, P. Poosankam, and D. Song. DTA++: Dynamic taint analysis with targeted control-flow propagation. NDSS. 2011.

[26]

N. Khakpour, O. Schwarz, and M. Dam. Machine assisted proof of ARMv7 instruction level isolation properties. CPP, 2013. To appear.

Digital Library

[27]

G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal verification of an OS kernel. SOSP. 2009.

Digital Library

[28]

M. N. Krohn and E. Tromer. Noninterference for a practical DIFCbased operating system. IEEE S&P. 2009.

Digital Library

[29]

A. Kwon, U. Dhawan, J. M. Smith, T. F. Knight, Jr., and A. DeHon. Low-fat pointers: compact encoding and efficient gate-level implementation of fat pointers for spatial safety and capability-based security. CCS. 2013.

Digital Library

[30]

X. Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363--446, 2009.

Digital Library

[31]

X. Leroy and S. Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. JAR, 41(1):1--31, 2008.

Digital Library

[32]

W. Masri, A. Podgurski, and D. Leon. Detecting and debugging insecure information flows. ISSRE. 2004.

Digital Library

[33]

R. Medel, A. B. Compagnoni, and E. Bonelli. A typed assembly language for non-interference. ICTCS. 2005.

Digital Library

[34]

B. Montagu, B. C. Pierce, and R. Pollack. A theory of information flow labels. CSF. 2013.

Digital Library

[35]

T. C. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke, S. Seefried, C. Lewis, X. Gao, and G. Klein. seL4: from general purpose to a proof of information flow enforcement. IEEE S&P. 2013.

Digital Library

[36]

T. C. Murray, D. Matichuk, M. Brassil, P. Gammie, and G. Klein. Noninterference for operating system kernels. CPP. 2012.

Digital Library

[37]

M. O. Myreen and M. J. C. Gordon. Hoare logic for realistically modelled machine code. TACAS. 2007.

Digital Library

[38]

Z. Ni and Z. Shao. Certified assembly programming with embedded code pointers. POPL. 2006.

Digital Library

[39]

A. Russo and A. Sabelfeld. Dynamic vs. static flow-sensitive security analysis. CSF. 2010.

Digital Library

[40]

A. Sabelfeld and A. Myers. Language-based information-flow security. JSAC, 21(1):5--19, 2003.

Digital Library

[41]

A. Sabelfeld and A. Russo. From dynamic to static and back: Riding the roller coaster of information-flow control research. In Ershov Memorial Conference. 2009.

Digital Library

[42]

J. Sevcík, V. Vafeiadis, F. Z. Nardelli, S. Jagannathan, and P. Sewell. Relaxed-memory concurrency and verified compilation. POPL. 2011.

Digital Library

[43]

H. Shrobe, A. DeHon, and T. F. Knight, Jr. Trust-management, intrusion-tolerance, accountability, and reconstitution architecture (TIARA), 2009.

[44]

D. Stefan, A. Russo, J. C. Mitchell, and D. Mazières. Flexible dynamic information flow control in Haskell. Haskell. 2011.

Digital Library

[45]

G. E. Suh, J. W. Lee, D. Zhang, and S. Devadas. Secure program execution via dynamic information flow tracking. ASPLOS, 2004.

Digital Library

[46]

N. Vachharajani, M. J. Bridges, J. Chang, R. Rangan, G. Ottoni, J. A. Blome, G. A. Reis, M. Vachharajani, and D. I. August. RIFLE: An architectural framework for user-centric information-flow security. MICRO, 2004.

Digital Library

[47]

Venkataramani, I. Doudalis, Y. Solihin, and M. Prvulovic. FlexiTaint: A programmable accelerator for dynamic taint propagation. HPCA, 2008.

[48]

S. A. Zdancewic. Programming Languages for Information Security. PhD thesis, Cornell University, 2002.

Digital Library

Cited By

Mista ARusso A(2023)MUTAGEN: Reliable Coverage-Guided, Property-Based Testing using Exhaustive Mutations2023 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST57152.2023.00025(176-187)Online publication date: Apr-2023
https://doi.org/10.1109/ICST57152.2023.00025
Jero SBurow NWard BSkowyra RKhazan RShrobe HOkhravi H(2022)TAG: Tagged Architecture GuideACM Computing Surveys10.1145/353370455:6(1-34)Online publication date: 7-Dec-2022
https://dl.acm.org/doi/10.1145/3533704
Van Strydonck TPiessens FDevriese D(2019)Linear capabilities for fully abstract compilation of separation-logic-verified codeProceedings of the ACM on Programming Languages10.1145/33416883:ICFP(1-29)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341688
Show More Cited By

Recommendations

A verified information-flow architecture
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

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 ...
A verified information-flow architecture

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 ...
Micro-Policies: Formally Verified, Tag-Based Security Monitors
PLAS'15: Proceedings of the 10th ACM Workshop on Programming Languages and Analysis for Security

Many of today's vulnerabilities arise from the violation of known, but in-practice unenforceable, safety and security policies, including high-level programming models and critical invariants of low-level programs. This project is aimed at showing that ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 49, Issue 1

POPL '14

January 2014

661 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2578855

Editor:
Mark W. Bailey
Hamilton College, Clinton, NY

Issue’s Table of Contents

POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2014
702 pages
ISBN:9781450325448
DOI:10.1145/2535838
General Chair:
Suresh Jagannathan
Purdue University, USA
,
Program Chair:
Peter Sewell
University of Cambridge, UK

Copyright © 2014 Owner/Author.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 January 2014

Published in SIGPLAN Volume 49, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

49
Total Citations
View Citations
1,746
Total Downloads

Downloads (Last 12 months)373
Downloads (Last 6 weeks)119

Reflects downloads up to 18 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Mista ARusso A(2023)MUTAGEN: Reliable Coverage-Guided, Property-Based Testing using Exhaustive Mutations2023 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST57152.2023.00025(176-187)Online publication date: Apr-2023
https://doi.org/10.1109/ICST57152.2023.00025
Jero SBurow NWard BSkowyra RKhazan RShrobe HOkhravi H(2022)TAG: Tagged Architecture GuideACM Computing Surveys10.1145/353370455:6(1-34)Online publication date: 7-Dec-2022
https://dl.acm.org/doi/10.1145/3533704
Van Strydonck TPiessens FDevriese D(2019)Linear capabilities for fully abstract compilation of separation-logic-verified codeProceedings of the ACM on Programming Languages10.1145/33416883:ICFP(1-29)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341688
Patrignani MAhmed AClarke D(2019)Formal Approaches to Secure CompilationACM Computing Surveys10.1145/328098451:6(1-36)Online publication date: 4-Feb-2019
https://dl.acm.org/doi/10.1145/3280984
Bauereiβ TPesenti Gritti APopescu ARaimondi F(2018)CoSMedJournal of Automated Reasoning10.1007/s10817-017-9443-361:1-4(113-139)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10817-017-9443-3
Menon AMurugan SRebeiro CGala NVeezhinathan K(2017)Shakti-TProceedings of the Hardware and Architectural Support for Security and Privacy10.1145/3092627.3092629(1-8)Online publication date: 25-Jun-2017
https://dl.acm.org/doi/10.1145/3092627.3092629
Kanav SLammich PPopescu A(2014)A Conference Management System with Verified Document ConfidentialityProceedings of the 16th International Conference on Computer Aided Verification - Volume 855910.1007/978-3-319-08867-9_11(167-183)Online publication date: 18-Jul-2014
https://dl.acm.org/doi/10.1007/978-3-319-08867-9_11
Baty MWilke PHiet GFontaine ATrieu A(2023)A Generic Framework to Develop and Verify Security Mechanisms at the Microarchitectural Level: Application to Control-Flow Integrity2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00029(372-387)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00029
Koenig J(2022)Grounding Game Semantics in Categorical AlgebraElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.372.26372(368-383)Online publication date: 3-Nov-2022
https://doi.org/10.4204/EPTCS.372.26
Chen ZRizkallah CO'Connor LSusarla PKlein GHeiser GKeller GFischer BBurgueño LCazzola W(2022)Property-Based Testing: Climbing the Stairway to VerificationProceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3567512.3567520(84-97)Online publication date: 29-Nov-2022
https://dl.acm.org/doi/10.1145/3567512.3567520
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Figures

Tables

Media

View Issue’s Table of Contents