article

Creating High Confidence in a Separation Kernel

Authors:

W. B. Martin,

P. D. White,

F. S. TaylorAuthors Info & Claims

Automated Software Engineering, Volume 9, Issue 3

Pages 263 - 284

https://doi.org/10.1023/A:1016324624000

Published: 01 August 2002 Publication History

Publisher Site

Abstract

Separation of processes is the foundation for security and safety properties of systems. This paper reports on a collaborative effort of Government, Industry and Academia to achieve high confidence in the separation of processes. To this end, this paper will discuss (1) what a separation kernel is, (2) why the separation of processes is fundamental to security systems, (3) how high confidence in the separation property of the kernel was obtained, and (4) some of the ways government, industry, and academia cooperated to achieve high confidence in a separation kernel.

i>What is separation Strict separation is the inability of one process to interfere with another. In a separation kernel, the word i>separation is interpreted very strictly. Any means for one process to disturb another, be it by communication primitives, by sharing of data, or by subtle uses of kernel primitives not intended for communication, is ruled out when two processes are separated.

i>Why is separation fundamental Strict separation between processes enables the evaluation of a system to check that the system meets its security policy. For example, if a red process is strictly separated from a black process, then it can be concluded that there is no flow of information from red to black.

i>How was high confidence achieved We have collaborated and shared our expertise in the use of SPECWARE. SPECWARE is a i>correct by construction method, in which high level specifications are built up from modules using specification combinators. Refinements of the specifications are made until an implementation is achieved. These refinements are also subject to combinators. The high confidence in the separation property of the kernel stems from the use of formal methods in the development of the kernel.

i>How did we collaborate Staff from the Kestrel Institute (developers of SPECWARE), the Department of Defense (DoD), and Motorola (developers of the kernel) cooperated in the creation of the Mathematically Analyzed Separation Kernel (MASK). DoD provided the separation kernel concept, and expertise in computer security and high confidence development. Kestrel provided expertise in SPECWARE. Motorola combined its own the expertise with that of DoD and Kestrel in creating MASK.

References

[1]

Kestrel Institute, 3260 Hillview Avenue, Palo Alto, California 94304. Specware Language Manual , 2.0.3 edn., March 1998.

Google Scholar

[2]

Pierce, B. C. 1991. Basic Category Theory for Computer Scientists . Cambridge, MA: MIT Press.

Digital Library

Google Scholar

[3]

Rushby, J. 1981. Design and verification of secure systems. In Proceedings of the Eighth Symposium on Operating Systems Principles , Vol. 15.

Digital Library

Google Scholar

Cited By

View all

Sewell TKam FHeiser G(2018)High-assurance timing analysis for a high-assurance real-time operating systemReal-Time Systems10.1007/s11241-017-9286-353:5(812-853)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.1007/s11241-017-9286-3
Zhao YYang ZMa D(2017)A survey on formal specification and verification of separation kernelsFrontiers of Computer Science: Selected Publications from Chinese Universities10.5555/3128671.312868111:4(585-607)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.5555/3128671.3128681
Klein GAndronick JElphinstone KMurray TSewell TKolanski RHeiser G(2014)Comprehensive formal verification of an OS microkernelACM Transactions on Computer Systems (TOCS)10.1145/256053732:1(1-70)Online publication date: 26-Feb-2014
https://dl.acm.org/doi/10.1145/2560537
Show More Cited By

Index Terms

Creating High Confidence in a Separation Kernel
1. Information systems
  1. Data management systems
    1. Database design and models
      1. Data model extensions
2. Software and its engineering
  1. Software creation and management
    1. Software development process management
    2. Software verification and validation
      1. Formal software verification
      2. Process validation
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Government, industry, and academia: Teaming to design high confidence information security applications
FMSP '00: Proceedings of the third workshop on Formal methods in software practice

A trusted computing base requires true separation of processes. Modern approaches relegate separation to a component of the operating system called the kernel. Although the kernel represents only a small portion of the code of the entire operating ...
Formal specification and verification of data separation in a separation kernel for an embedded system
CCS '06: Proceedings of the 13th ACM conference on Computer and communications security

Although many algorithms, hardware designs, and security protocols have been formally verified, formal verification of the security of software is still rare. This is due in large part to the large size of software, which results in huge costs for ...
A survey on formal specification and verification of separation kernels

Separation kernels are fundamental software of safety and security-critical systems, which provide their hosted applications with spatial and temporal separation as well as controlled information flows among partitions. The application of separation ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Automated Software Engineering

Automated Software Engineering Volume 9, Issue 3

August 2002

123 pages

ISSN:0928-8910

Issue’s Table of Contents

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 August 2002

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Sewell TKam FHeiser G(2018)High-assurance timing analysis for a high-assurance real-time operating systemReal-Time Systems10.1007/s11241-017-9286-353:5(812-853)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.1007/s11241-017-9286-3
Zhao YYang ZMa D(2017)A survey on formal specification and verification of separation kernelsFrontiers of Computer Science: Selected Publications from Chinese Universities10.5555/3128671.312868111:4(585-607)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.5555/3128671.3128681
Klein GAndronick JElphinstone KMurray TSewell TKolanski RHeiser G(2014)Comprehensive formal verification of an OS microkernelACM Transactions on Computer Systems (TOCS)10.1145/256053732:1(1-70)Online publication date: 26-Feb-2014
https://dl.acm.org/doi/10.1145/2560537
Löhr HSadeghi AStüble CWeber MWinandy M(2009)Modeling Trusted Computing Support in a Protection Profile for High Assurance Security KernelsProceedings of the 2nd International Conference on Trusted Computing10.1007/978-3-642-00587-9_4(45-62)Online publication date: 19-Feb-2009
https://dl.acm.org/doi/10.1007/978-3-642-00587-9_4

Abstract

References

Cited By

Index Terms

Recommendations

Government, industry, and academia: Teaming to design high confidence information security applications

Formal specification and verification of data separation in a separation kernel for an embedded system

A survey on formal specification and verification of separation kernels

Comments

Information

Published In

Publisher

Publication History

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations