Separation and Integration in MILS: The MILS Constitution

John Rushby

SRI-CSL Technical Report, February 2008


We describe the MILS approach to design, construction, integration, and evaluation of secure systems. The crucial feature of the MILS approach is that it separates the problems of enforcing security policy from those of securely sharing resources. MILS design proceeds in two steps: first, we develop a logical security policy architecture in which the system is deconstructed into interacting components in such a way that the trusted components are as simple as possible; second, we allocate components of the policy architecture to resources that are securely shared through mechanisms for logical separation.

MILS identifies certain standard resources such as processors, networks, consoles, and file systems and publishes protection profiles for their logical separation; a COTS marketplace is developing that provides components evaluated to these profiles. Standard protection profiles and a marketplace for evaluated policy components (such as guards and filters) are also anticipated. Top-down design of a MILS system pays attention to existing protection profiles and strives to target these where appropriate. MILS construction can then incorporate COTS products evaluated to these protection profiles.

MILS integration takes COTS and bespoke policy components and allocates them to physical resources that may be shared using COTS and bespoke components for separation in a way that is faithful to the original policy architecture. Security assurance and evaluation in MILS are assembled in the same way. That is so say, MILS security assurance is compositional: assurance for an overall system is derived from that of its components, integrated according to the specific policy architecture and resource allocation of the system concerned.

Compositional design and assurance for a system property such as security is a radical innovation; we outline the justification for the MILS approach to accomplishing this.

Note on publication history (17 January 2021): This report was written in 2007/8 but not released at the time as I considered it unfinished. However, a copy seems to have "escaped" and as of January 2021 it has 33 citations, so I thought I may as well belatedly make it available here.


BibTeX Entry

	AUTHOR = {John Rushby},
	TITLE = {Separation and Integration in MILS: The MILS Constitution},
	INSTITUTION = {Computer Science Laboratory, SRI International},
	YEAR = 2008,
	ADDRESS = {Menlo Park, CA},
	MONTH = feb,
	NOTE = {Available at \url{}}

Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page