A Security Model for Military Message Systems CARL E. LANDWEHR, CONSTANCE L. HEITMEYER, and JOHN McLEAN Naval Research Laboratory Military systems that process classified information must operate in a secure manner; that is, they must adequately protect information against unauthorized disclosure, modification, and withholding. A goal of current research in computer security is to facilitate the construction of multilevel secure systems, systems that protect information of different classifications from users with different clearances. Security models are used to define the concept of security embodied by a computer system. A single model, called the Bell and LaPadula model, has dominated recent efforts to build secure systems but has deficiencies. We are developing a new approach to defining security models based on the idea that a security model should be derived from a specific application. To evaluate our approach, we have formulated a security model for a family of military message systems. This paper introduces the message system application, describes the problems of using the Bell-LaPadula model in real applications, and presents our security model both informally and formally. Significant aspects of the security model are its definition of multilevel objects and its inclusion of application-dependent security assertions. Prototypes based on this model are being developed. Categories and Subject Descriptors: C.2.0 [Computer-Communication Networks]: General-- Security and protection; D.4.6 [Operating Systems]: Security and Protection--access controls; information flow controls; verification; F.3.1 [Logics and Meaning of Programs]: Specifying and Verifying and Reasoning about Programs--assertions; invariants; specification techniques; H.4.3 [Information Systems Applications]: Communications Applications--electronic mail General Terms: Security, Verification Additional Key Words and Phrases: Storage channels, message systems, confinement 1. INTRODUCTION A system is secure if it adequately protects information that it processes against unauthorized disclosure, unauthorized modification, and unauthorized withhold- ing (also called denial of service). We say "adequately" because no practical system can achieve these goals without qualification; security is inherently relative. A secure system is multilevel secure if it protects information of different classifications from users with different clearances; thus some users are not cleared for all of the information that the system processes. Security models have been developed both to describe the protection that a computer actually provides and to define the security rules it is required to enforce [14]. In our view, a security model should enable users to understand how to operate the system effectively, implementors to understand what security controls to build, and certifiers to determine whether the system's security Authors' address: Computer Science and Systems Branch, Information Technology Division, Naval Research Laboratory, Washington, D.C. 20375. 1984 ACM 0734-2071/84/0198-0222 $00.00 ACM Transactions on Computer Systems, Vol. 2, No. 3, August 1984, pages 198-222.A Security Model for Military Message Systems • 199 controls are consistent with the relevant policies and directives and whether these controls are implemented correctly [13]. In recent years, the Bell and LaPadula model [4, 8], has dominated efforts to build secure systems. The publication of this model advanced the technology of computer security by providing a mathematical basis for examining the security provided by a given system. Moreover, the model was a major component of one of the first disciplined approaches to building secure systems. The model describes a secure computer system abstractly, without regard to the system's application. Its approach is to define a set of system constraints whose enforcement will prevent any application program executed on the system from compromising system security. The model includes subjects, which represent active entities in a system {such as active processes), and objects, which represent passive entities (such as files and inactive processes). Both subjects and objects have security levels, and the constraints on the system take the form of axioms that control the kinds of access subjects may have to objects. One of the axioms, called the *-property ("star-property"), prohibits a subject from simultaneously having read access to one object at a given security level and write access to another object at a lower security level. Its purpose is to prevent subjects from moving data of a given security level to an object marked with a lower security level. Originally, the model applied this constraint to all subjects, since a subject might execute any arbitrary application program, and arbitrary programs executed without this constraint could indeed cause security violations. A system that strictly enforces the axioms of the original Bell-LaPadula model is often impractical: in real systems, users may need to invoke operations that, although they do not violate our intuitive concept of security, would require subjects to violate the *-property. For example, a user may need to extract an UNCLASSIFIED paragraph from a CONFIDENTIAL document and use it in an UNCLASSIFIED document. A system that strictly enforces the *-property would prohibit this operation. Consequently, a class of trusted subjects has been included in the model. These subjects are trusted not to violate security even though they may violate the *-property. Systems based on this less restrictive model usually contain mecha- nisms that permit some operations the *-property prohibits, for example, the trusted processes in KS OS [ 17 ] and SIGMA [ 1 ]. The presence of such mechanisms makes it difficult to determine the actual security policy enforced by the system and complicates the user interface. To avoid these problems, we propose a different approach. Instead of starting with an application-independent abstraction for a secure computer system and trying to make an application fit on top of it, we start with the application and derive the constraints that the system must enforce from both the