Formal security models: Bell-LaPadula, Biba, Clark-Wilson, and Brewer-Nash

State machines, Bell-LaPadula confidentiality, and Biba integrity

At the core of formal security engineering is the Finite State Machine (FSM) model: a system has a set of subjects, objects, states, and transition rules. Under the Basic Security Theorem, if the system boots into a verified secure initial state (including secure failure/recovery states) and every state transition preserves the security invariant, the system remains provably secure.

The Bell-LaPadula model (developed for the U.S. Department of Defense) is an information-flow lattice model designed exclusively to protect Confidentiality. It enforces two core rules between a subject’s clearance and an object’s classification: the Simple Security Property ("No Read Up" - a Secret user cannot read Top Secret files) and the *-Property, pronounced Star Property ("No Write Down" - a Top Secret user or process cannot write or copy data into a Secret or Unclassified file, preventing accidental or malicious leakage). When a subject must communicate downward, it requires a tightly audited Trusted Subject exception.

The Biba model is the exact mathematical dual of Bell-LaPadula, designed exclusively to protect Integrity. Biba assigns integrity levels to subjects and objects and reverses the arrows: the Simple Integrity Property enforces "No Read Down" (a high-integrity flight-control process must never read unvalidated low-integrity inputs that could poison its state), and the *-Integrity Property enforces "No Write Up" (a low-integrity subject cannot overwrite a high-integrity configuration file).

Clark-Wilson: commercial integrity through well-formed transactions

While Biba works well for military integrity levels, commercial enterprises like banks and Meridian’s ERP ledger need to accept untrusted external inputs (such as a customer order or a sensor packet) and safely update high-integrity records. The Clark-Wilson model solves this using a three-part access triple: (User/Subject, Transformation Procedure, Constrained Data Item).

In Clark-Wilson, subjects are never allowed to modify a high-integrity Constrained Data Item (CDI) directly. Instead, raw untrusted input enters as an Unconstrained Data Item (UDI) and is processed exclusively through a certified Transformation Procedure (TP - such as a parameterized API handler that validates double-entry accounting rules) to become or update a CDI. Meanwhile, an Integrity Verification Procedure (IVP) periodically audits CDIs to confirm the ledger remains internally consistent, and strict Separation of Duties ensures the developer who certifies a TP cannot also execute it on production data.

Brewer-Nash, Graham-Denning, and Non-Interference

Three additional models frequently appear in architectural design. The Brewer-Nash (Chinese Wall) model addresses dynamic conflicts of interest in consulting, legal, and multi-tenant defense contracting: a user starts with permission to view any client folder, but the moment they open Orbital Client Alpha’s propulsion files, the security kernel dynamically erases their ability to view competing Orbital Client Beta’s files.

The Graham-Denning model defines eight primitive protection rules governing how subjects and objects are securely created, deleted, and assigned access rights in an Access Control Matrix (later formalized by Harrison-Ruzzo-Ullman, or HRU, regarding the decidability of safety). Finally, the Goguen-Meseguer Non-Interference model goes beyond Bell-LaPadula’s file-write rules to prevent covert channels: it guarantees that actions taken by a high-clearance subject produce zero observable changes in system state, timing, or resource usage visible to a low-clearance subject.