Article

Proving confidentiality in a file system using DISKSEC

Authors:

M. Frans Kaashoek,

Nickolai ZeldovichAuthors Info & Claims

OSDI'18: Proceedings of the 13th USENIX conference on Operating Systems Design and Implementation

Pages 323 - 338

Published: 08 October 2018 Publication History

Abstract

SFSCQ is the first file system with a machine-checked proof of security. To develop, specify, and prove SFSCQ, this paper introduces DISKSEC, a novel approach for reasoning about confidentiality of storage systems, such as a file system. DISKSEC addresses the challenge of specifying confidentiality using the notion of data noninterference to find a middle ground between strong and precise information-flow-control guarantees and the weaker but more practical discretionary access control. DISKSEC factors out reasoning about confidentiality from other properties (such as functional correctness) using a notion of sealed blocks. Sealed blocks enforce that the file system treats confidential file blocks as opaque in the bulk of the code, greatly reducing the effort of proving data noninterference. An evaluation of SFSCQ shows that its theorems preclude security bugs that have been found in real file systems, that DISKSEC imposes little performance overhead, and that SFSCQ's incremental development effort, on top of DISKSEC and DFSCQ, on which it is based, is moderate.

References

[1]

CVE-2009-4131, 2009. https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2009-4131.

[2]

CVE-2010-1146, 2010. http://cve.mitre.org/cgi-bin/cvename.cgi?name=cve-2010-2066.

[3]

CVE-2010-2017, 2010. https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2010-1641.

[4]

CVE-2010-2066, 2010. http://cve.mitre.org/cgi-bin/cvename.cgi?name=cve-2010-2066.

[5]

CVE-2010-2017, 2010. https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2010-2071.

[6]

CVE-2010-2537, 2010. http://cve.mitre.org/cgi-bin/cvename.cgi?name=cve-2010-2066.

[7]

CVE-2015-8374, 2015. https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2015-8374.

[8]

CVE-2016-1237, 2016. http://cve.mitre.org/cgi-bin/cvename.cgi?name=cve-2010-2066.

[9]

CVE-2017-7495, 2017. https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2017-7495.

[10]

J. Barkley. Introduction to POSIX security, Oct. 1994. http://ftp.gnome.org/mirror/archive/ftp.sunet.se/pub/security/docs/nistpubs/800-7/node18.html.

[11]

B. Blanchet. An efficient cryptographic protocol verifier based on Prolog rules. In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW), pages 82-96, Cape Breton, Nova Scotia, Canada, June 2001.

Digital Library

[12]

H. Chen, D. Ziegler, T. Chajed, A. Chlipala, M. F. Kaashoek, and N. Zeldovich. Using Crash Hoare Logic for certifying the FSCQ file system. In Proceedings of the 25th ACM Symposium on Operating Systems Principles (SOSP), pages 18-37, Monterey, CA, Oct. 2015.

Digital Library

[13]

H. Chen, T. Chajed, A. Konradi, S. Wang, A. Ileri, A. Chlipala, M. F. Kaashoek, and N. Zeldovich. Verifying a high-performance crash-safe file system using a tree specification. In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), pages 270-286, Shanghai, China, Oct. 2017.

Digital Library

[14]

A. Chlipala. Static checking of dynamically-varying security policies in database-backed applications. In Proceedings of the 9th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 105-118, Vancouver, Canada, Oct. 2010.

Digital Library

[15]

D. Costanzo, Z. Shao, and R. Gu. End-to-end verification of information-flow security for C and assembly programs. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 648-664, Santa Barbara, CA, June 2016.

Digital Library

[16]

D. Dolev and A. C. Yao. On the security of public key protocols. In Proceedings of the 22nd Annual IEEE Symposium on Foundations of Computer Science (FOCS), pages 350-357, Nashville, TN, Oct. 1981.

Digital Library

[17]

A. Ferraiuolo, A. Baumann, C. Hawblitzel, and B. Parno. Komodo: Using verification to disentangle secure-enclave hardware from software. In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), pages 287-305, Shanghai, China, Oct. 2017.

Digital Library

[18]

R. Giacobazzi and I. Mastroeni. Abstract noninterference: Parameterizing non-interference by abstract interpretation. In Proceedings of the 31st ACM Symposium on Principles of Programming Languages (POPL), pages 186-197, Venice, Italy, Jan. 2004.

Digital Library

[19]

J. A. Goguen and J. Meseguer. Security policies and security models. In Proceedings of the 3rd IEEE Symposium on Security and Privacy, pages 11-20, Oakland, CA, Apr. 1982.

[20]

C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno, D. Zhang, and B. Zill. Ironclad Apps: End-to-end security via automated full-system verification. In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 165-181, Broomfield, CO, Oct. 2014.

Digital Library

[21]

J. Hsu. Probabilistic Couplings for Probabilistic Reasoning. PhD thesis, University of Pennsylvania, Nov. 2017.

[22]

J. Kara. [PATCH] ext4: Forbid journal_async_commit in data=ordered mode. http://permalink.gmane.org/gmane.comp.file-systems.ext4/46977, Nov. 2014.

[23]

G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski, and G. Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, 32(1):2:1-70, Feb. 2014.

Digital Library

[24]

P. Li and S. Zdancewic. Downgrading policies and relaxed noninterference. In Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (POPL), pages 158-170, Long Beach, CA, Jan. 2005.

Digital Library

[25]

J. McLean. Proving noninterference and functional correctness using traces. Journal of Computer Security, 1(1):37-57, Jan. 1992.

Digital Library

[26]

T. 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. In Proceedings of the 34th IEEE Symposium on Security and Privacy, pages 415-429, San Francisco, CA, May 2013.

Digital Library

[27]

A. Myers and B. Liskov. A decentralized model for information flow control. In Proceedings of the 16th ACM Symposium on Operating Systems Principles (SOSP), pages 129-147, Saint-Malo, France, Oct. 1997.

Digital Library

[28]

A. C. Myers and B. Liskov. Protecting privacy using the decentralized label model. ACM Transactions on Computer Systems, 9(4):410-442, Oct. 2000.

Digital Library

[29]

A. Popescu, J. Hölzl, and T. Nipkow. Proving concurrent noninterference. In Proceedings of the 2nd International Conference on Certified Programs and Proofs (CPP), pages 109-125, Kyoto, Japan, Dec. 2012.

Digital Library

[30]

A. W. Roscoe. CSP and determinism in security modelling. In Proceedings of the 16th IEEE Symposium on Security and Privacy, pages 114-127, Oakland, CA, May 1995.

Digital Library

[31]

M. Rosenblum and J. Ousterhout. The design and implementation of a log-structured file system. In Proceedings of the 13th ACM Symposium on Operating Systems Principles (SOSP), pages 1-15, Pacific Grove, CA, Oct. 1991.

Digital Library

[32]

J. M. Rushby. Proof of separability: A verification technique for a class of security kernels. In Proceedings of the 5th International Symposium on Programming, pages 352-367, Turin, Italy, Apr. 1982.

Digital Library

[33]

B. Schmidt, S. Meier, C. Cremers, and D. Basin. Automated analysis of Diffie-Hellman protocols and advanced security properties. In Proceedings of the 25th IEEE Computer Security Foundations Symposium, pages 78-94, Cambridge, MA, June 2012.

Digital Library

[34]

T. Terauchi and A. Aiken. Secure information flow as a safety problem. In Proceedings of the 12th International Static Analysis Symposium (SAS), pages 352-367, London, UK, Sept. 2005.

Digital Library

[35]

The Coq Development Team. The Coq Proof Assistant, version 8.8.0, Apr. 2018.

[36]

T. Ts'o. [PATCH] ext4: remove calls to ext4_jbd2_file_inode() from delalloc write path. http://lists.openwall.net/linuxext4/2012/11/16/9, Nov. 2012.

[37]

J. Yang, K. Yessenov, and A. Solar-Lezama. A language for automatically enforcing privacy policies. In Proceedings of the 39th ACM Symposium on Principles of Programming Languages (POPL), Philadelphia, PA, Jan. 2012.

Digital Library

[38]

J. Yang, T. Hance, T. H. Austin, A. Solar-Lezama, C. Flanagan, and S. Chong. Precise, dynamic information flow for database-backed applications. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 631-647, Santa Barbara, CA, June 2016.

Digital Library

[39]

A. Yip, X. Wang, N. Zeldovich, and M. F. Kaashoek. Improving application security with data flow assertions. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), pages 291- 304, Big Sky, MT, Oct. 2009.

Digital Library

[40]

J.-K. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche. HACL*: A verified modern cryptographic library. In Proceedings of the 24th ACM Conference on Computer and Communications Security (CCS), Dallas, TX, Oct.-Nov. 2017.

Digital Library

Cited By

Nelson LBornholt JKrishnamurthy ATorlak EWang X(2020)Noninterference specifications for secure systemsACM SIGOPS Operating Systems Review10.1145/3421473.342147854:1(31-39)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421478
Erbsen APhilipoom JGross JSloan RChlipala A(2020)Simple High-Level Code For Cryptographic ArithmeticACM SIGOPS Operating Systems Review10.1145/3421473.342147754:1(23-30)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421477

Proving confidentiality in a file system using DISKSEC
1. Security and privacy
  1. Systems security
2. Software and its engineering
  1. Software organization and properties
    1. Contextual software domains
      1. Operating systems

Recommendations

The zebra striped network file system
The Zebra striped network file system

Zebra is a network file system that increases throughput by striping the file data across multiple servers. Rather than striping each file separately, Zebra forms all the new data from each client into a single stream, which it then stripes using an ...
The Viva File System

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

OSDI'18: Proceedings of the 13th USENIX conference on Operating Systems Design and Implementation

October 2018

815 pages

ISBN:9781931971478

Program Chairs:
Andrea Arpaci-Dusseau
University of Wisconsin-Madison
,
Geoff Voelker
University of California, San Diego

Sponsors

NetApp
Google Inc.
NSF
Microsoft: Microsoft
Facebook: Facebook

In-Cooperation

SIGOPS: ACM Special Interest Group on Operating Systems

Publisher

USENIX Association

United States

Publication History

Published: 08 October 2018

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nelson LBornholt JKrishnamurthy ATorlak EWang X(2020)Noninterference specifications for secure systemsACM SIGOPS Operating Systems Review10.1145/3421473.342147854:1(31-39)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421478
Erbsen APhilipoom JGross JSloan RChlipala A(2020)Simple High-Level Code For Cryptographic ArithmeticACM SIGOPS Operating Systems Review10.1145/3421473.342147754:1(23-30)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421477

View Options

View options

Media

Figures

Other

Tables

View Table of Contents