research-article

Noninterference specifications for secure systems

Authors:

James Bornholt,

Arvind Krishnamurthy,

Xi WangAuthors Info & Claims

ACM SIGOPS Operating Systems Review, Volume 54, Issue 1

Pages 31 - 39

https://doi.org/10.1145/3421473.3421478

Published: 31 August 2020 Publication History

Abstract

This paper presents an analysis of noninterference specifications used in a range of formally verified systems. The main findings are that these systems use distinct specifications and that they often employ small variations, both complicating their security implications. We categorize these specifications and discuss their trade-offs for reasoning about information flows in systems.

References

[1]

W. E. Boebert and R.Y. Kain. Apractical alternative to hierarchical integrity policies. In Proceedings of the 8th National Computer Security Conference, Gaithersburg, MD, Sept.--Oct. 1985.

[2]

V. Costan and S. Devadas. Intel SGX explained. Report 2016/086, Cryptology ePrint Archive, Feb. 2016.

[3]

D. Costanzo. Formal End-to-End Verification of Information-Flow Security for Complex Systems. PhD thesis, Yale University, Dec. 2016.

[4]

D. Costanzo, Z. Shao, and R. Gu. End-to-end verification of information-flowsecurity forCand assembly programs. In Proceedings of the 37th ACM SIG- PLAN Conference on Programming Language De- sign and Implementation (PLDI), pages 648--664, Santa Barbara, CA, June 2016.

Digital Library

[5]

M. Dam, R. Guanciale, N. Khakpour, H. Nemati, and O. Schwarz. Formal verification of information flow security for a simple ARM-based separation kernel. In Proceedings of the 20th ACM Conference on Computer and Communications Security (CCS), pages 223--234, Berlin, Germany, Nov. 2013.

Digital Library

[6]

L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Con- struction and Analysis of Systems (TACAS), pages 337--340, Budapest, Hungary, Mar.--Apr. 2008.

Digital Library

[7]

D. E. Denning. A lattice model of secure information flow. Communications of the ACM, 19(5): 236--243, May 1976.

Digital Library

[8]

S. Eggert. Security via Noninterference: Analyzing Information Flows. PhD thesis, Kiel University, July 2014.

[9]

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 Op- erating Systems Principles (SOSP), pages 287--305, Shanghai, China, Oct. 2017.

Digital Library

[10]

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.

[11]

P. Graunke. Verified safety and information flow of a block device. Electronic Notes in Theoretical Computer Science, 217:187--202, July 2008.

Digital Library

[12]

J. T. Haigh and W. D. Young. Extending the noninterference version of MLS for SAT. IEEE Trans- actions on Software Engineering, 13(2):141--150, Feb. 1987. 37

Digital Library

[13]

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 Sympo- sium on Operating Systems Design and Implementa- tion (OSDI), pages 165--181, Broomfield, CO, Oct. 2014.

Digital Library

[14]

T. Chajed, A. Chlipala, M. F. Kaashoek, and N. Zeldovich. Proving confidentiality in a file system using DiskSec. In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 323--338, Carlsbad, CA, Oct. 2018.

Digital Library

[15]

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

[16]

B. W. Lampson. A note on the confinement problem. Communications of the ACM, 16(10):613--615, Oct. 1973.

Digital Library

[17]

K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence and Reason- ing (LPAR), pages 348--370, Dakar, Senegal, Apr.-- May 2010.

Digital Library

[18]

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

[19]

T. Murray, D. Matichuk, M. Brassil, P. Gammie, and G. Klein. Noninterference for operating system kernels. In Proceedings of the 2nd International Con- ference on Certified Programs and Proofs, pages 126--142, Kyoto, Japan, Dec. 2012.

Digital Library

[20]

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

[21]

T. Murray, R. Sison, and K. Engelhardt. Covern: A logic for compositional verification of information flow control. In Proceedings of the 3rd IEEE Eu- ropean Symposium on Security and Privacy, pages 16--30, London, United Kingdom, Apr. 2018.

[22]

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

Digital Library

[23]

L. Nelson, J. Bornholt, R. Gu, A. Baumann, E. Torlak, and X. Wang. Scaling symbolic evaluation for automated verification of systems code with Serval. In Proceedings of the 27th ACM Symposium on Op- erating Systems Principles (SOSP), pages 225--242, Huntsville, Ontario, Canada, Oct. 2019.

Digital Library

[24]

T. Nipkow, L. C. Paulson, and M. Wenzel. Is- abelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, Feb. 2016.

[25]

D. Ricketts, V. Robert, D. Jang, Z. Tatlock, and S. Lerner. Automating formal proofs for reactive systems. In Proceedings of the 35th ACM SIG- PLAN Conference on Programming Language De- sign and Implementation (PLDI), pages 452--462, Edinburgh, United Kingdom, June 2014.

Digital Library

[26]

A. Roscoe and M. Goldsmith. What is intransitive noninterference? In Proceedings of the 12th IEEE Computer Security FoundationsWorkshop (CSFW), pages 228--238, Mordano, Italy, June 1999.

Digital Library

[27]

J. Rushby. Design and verification of secure systems. In Proceedings of the 8th ACM Symposium on Operating Systems Principles (SOSP), pages 12-- 21, Pacific Grove, CA, Dec. 1981.

Digital Library

[28]

J. Rushby. Noninterference, transitivity, and channel-control security policies. Technical Report CSL-92-02, SRI International, Dec. 1992.

[29]

A. Sabelfeld and A. Myers. Language-based information-flow security. IEEE Journal on Se- lected Areas in Communications, 21(1):5--19, 2003.

Digital Library

[30]

O. Schwarz. No Hypervisor Is an Island: System- wide Isolation Guarantees for Low Level Code. PhD thesis, KTH, sep 2016.

[31]

H. Sigurbjarnarson, L. Nelson, B. Castro-Karney, J. Bornholt, E. Torlak, and X. Wang. Nickel: A framework for design and verification of information flowcontrol systems. In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 287--306, Carlsbad, CA, Oct. 2018.

Digital Library

[32]

D. Stefan, A. Russo, P. Buiras, A. Levy, J. C. Mitchell, and D. Mazières. Addressing covert termination and timing channels in concurrent information flow systems. In Proceedings of the 8 38 17th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 201--214, Copenhagen, Denmark, Sept. 2012.

Digital Library

[33]

Z. Tatlock. Reducing the Costs of Proof Assistant Based Formal Verification or: Conviction without the Burden of Proof. PhD thesis, University of California, San Diego, 2014.

[34]

The Coq Development Team. The Coq Proof As- sistant, version 8.9.0, Jan. 2019. URL https: //doi.org/10.5281/zenodo.2554024.

[35]

T. Tsai, A. Russo, and J. Hughes. A library for secure multi-threaded information flow in Haskell. In Proceedings of the 20th IEEE Computer Secu- rity Foundations Symposium (CSF), pages 187--202, Venice, Italy, July 2007.

Digital Library

[36]

R. van der Meyden. What, indeed, is intransitive noninterference? In Proceedings of the 12th Euro- pean Symposium on Research in Computer Security, 2007.

Digital Library

[37]

R. van der Meyden and C. Zhang. A comparison of semantic models for noninterference. Theoretical Computer Science, 411(47):4123--4147, Oct. 2010.

Digital Library

[38]

D. von Oheimb. Information flow control revisited: Noninfluence = noninterference + nonleakage. In Proceedings of the 9th European Symposium on Research in Computer Security, pages 225--243, Sophia Antipolis, France, Sept. 2004.

Cited By

Wang ZLan YHe XLv J(2024)A Formal Verification Approach for Linux Kernel DesigningTechnologies10.3390/technologies1208013212:8(132)Online publication date: 12-Aug-2024
https://doi.org/10.3390/technologies12080132
Athalye ACorrigan-Gibbs HKaashoek FTassarotti JZeldovich NWitchel EArpaci-Dusseau ARossbach CKeeton K(2024)Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level ImplementationProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles10.1145/3694715.3695956(655-672)Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1145/3694715.3695956
Hong YLi YTan H(2022)A noninterference trusted dual system security guarantee method based on secure memoryConcurrency and Computation: Practice and Experience10.1002/cpe.746335:2Online publication date: 12-Nov-2022
https://doi.org/10.1002/cpe.7463
Show More Cited By

Recommendations

Formalized structured analysis specifications
Protective Interface Specifications
Abstract.
The interface specification of a procedure describes the procedure's behaviour using pre- and postconditions. These pre- and postconditions are written using various functions. If some of these functions are partial, or underspecified, then the ...
Towards the Composition of Specifications in Event-B

The development of a system can start with the creation of a specification. Following this viewpoint, we claim that often a specification can be constructed from the combination of specifications which can be seen as composition. Event-B is a formal ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGOPS Operating Systems Review

ACM SIGOPS Operating Systems Review Volume 54, Issue 1

July 2020

76 pages

ISSN:0163-5980

DOI:10.1145/3421473

Editors:
Robbert van Renesse
Cornell University, Ithaca, New York
,
Christopher J. Rossbach
Stop D9500, Austin, TX
,
Kishore Pusukuri
1850 Nantucket Cir APT 149 Santa Clara, CA, USA
,
John Chandy
University of Connecticut
,
Antônio Fröhlich
Dederal Univ. of Santa Catarina
,
Ashvin Goel
University of Toronto

Issue’s Table of Contents

Copyright © 2020 Copyright is held by the owner/author(s).

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: 31 August 2020

Published in SIGOPS Volume 54, Issue 1

Check for updates

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
205
Total Downloads

Downloads (Last 12 months)44
Downloads (Last 6 weeks)2

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wang ZLan YHe XLv J(2024)A Formal Verification Approach for Linux Kernel DesigningTechnologies10.3390/technologies1208013212:8(132)Online publication date: 12-Aug-2024
https://doi.org/10.3390/technologies12080132
Athalye ACorrigan-Gibbs HKaashoek FTassarotti JZeldovich NWitchel EArpaci-Dusseau ARossbach CKeeton K(2024)Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level ImplementationProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles10.1145/3694715.3695956(655-672)Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1145/3694715.3695956
Hong YLi YTan H(2022)A noninterference trusted dual system security guarantee method based on secure memoryConcurrency and Computation: Practice and Experience10.1002/cpe.746335:2Online publication date: 12-Nov-2022
https://doi.org/10.1002/cpe.7463
Xu WZhao YCao CNgnie Sighom JWang LJiang ZZou S(2021)Apply Formal Methods in Certifying the SyberX High-Assurance KernelFormal Methods10.1007/978-3-030-90870-6_46(788-798)Online publication date: 20-Nov-2021
https://dl.acm.org/doi/10.1007/978-3-030-90870-6_46

View Options

Get Access

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents