This paper presents a lattice model for ensuring secure information flow in computer systems. Dorothy E. Denning proposes a mathematical framework to define secure information flow among security classes. The central component of the model is a lattice structure derived from security classes, justified by the semantics of information flow. The lattice properties allow concise formulations of security requirements and facilitate the construction of mechanisms that enforce security. The model provides a unifying view of systems that restrict information flow, enables classification according to security objectives, and suggests new approaches. It also leads to the development of automatic program certification mechanisms for verifying secure information flow through programs. The model is based on a formal definition of an information flow model FM = ⟨N, P, SC, ⊕, →⟩, where N is a set of logical storage objects, P is a set of processes, SC is a set of security classes, ⊕ is a class-combining operator, and → is a flow relation. The security requirements of the model are that a flow model FM is secure if and only if execution of a sequence of operations cannot give rise to a flow that violates the relation →. The model is shown to form a universally bounded lattice, with SC being a finite partially ordered set and ⊕ being a least upper bound operator. The model also includes a greatest lower bound operator, denoted by ⊗, which is used to define the lattice structure. The paper discusses examples of lattice structures, including a linear ordered lattice and a lattice of subsets. It also describes mechanisms for static and dynamic binding, including access control mechanisms, the Data Mark Machine, and certification mechanisms. The paper highlights the challenges of dynamic binding and proposes solutions to ensure secure information flow. It also discusses the limitations of existing mechanisms and the need for both access and flow control to satisfy all security requirements. The paper concludes with a discussion of the applications of the model, including confinement and database security. It also acknowledges the contributions of other researchers and references relevant literature. The paper is accompanied by a second paper on security kernel validation, which describes the technique used to validate a formal specification of a security kernel.This paper presents a lattice model for ensuring secure information flow in computer systems. Dorothy E. Denning proposes a mathematical framework to define secure information flow among security classes. The central component of the model is a lattice structure derived from security classes, justified by the semantics of information flow. The lattice properties allow concise formulations of security requirements and facilitate the construction of mechanisms that enforce security. The model provides a unifying view of systems that restrict information flow, enables classification according to security objectives, and suggests new approaches. It also leads to the development of automatic program certification mechanisms for verifying secure information flow through programs. The model is based on a formal definition of an information flow model FM = ⟨N, P, SC, ⊕, →⟩, where N is a set of logical storage objects, P is a set of processes, SC is a set of security classes, ⊕ is a class-combining operator, and → is a flow relation. The security requirements of the model are that a flow model FM is secure if and only if execution of a sequence of operations cannot give rise to a flow that violates the relation →. The model is shown to form a universally bounded lattice, with SC being a finite partially ordered set and ⊕ being a least upper bound operator. The model also includes a greatest lower bound operator, denoted by ⊗, which is used to define the lattice structure. The paper discusses examples of lattice structures, including a linear ordered lattice and a lattice of subsets. It also describes mechanisms for static and dynamic binding, including access control mechanisms, the Data Mark Machine, and certification mechanisms. The paper highlights the challenges of dynamic binding and proposes solutions to ensure secure information flow. It also discusses the limitations of existing mechanisms and the need for both access and flow control to satisfy all security requirements. The paper concludes with a discussion of the applications of the model, including confinement and database security. It also acknowledges the contributions of other researchers and references relevant literature. The paper is accompanied by a second paper on security kernel validation, which describes the technique used to validate a formal specification of a security kernel.