Clark–Wilson model


The Clark-Wilson integrity model provides a foundation for specifying and analyzing an integrity policy for a computing system.
The model is primarily concerned with formalizing the notion of information integrity. Information integrity is maintained by preventing corruption of data items in a system due to either error or malicious intent. An integrity policy describes how the data items in the system should be kept valid from one state of the system to the next and specifies the capabilities of various principals in the system. The model uses security labels to grant access to objects via transformation procedures and a restricted interface model.

Origin

The model was described in a 1987 paper by David D. Clark and David R. Wilson. The paper develops the model as a way to formalize the notion of information integrity, especially as compared to the requirements for multilevel security systems described in the Orange Book. Clark and Wilson argue that the existing integrity models such as Biba were better suited to enforcing data integrity rather than information confidentiality. The Biba models are more clearly useful in, for example, banking classification systems to prevent the untrusted modification of information and the tainting of information at higher classification levels, respectively. In contrast, Clark-Wilson is more clearly applicable to business and industry processes in which the integrity of the information content is paramount at any level of classification.

Basic principles

According to Stewart and Chapple's CISSP Study Guide Sixth Edition, the Clark-Wilson model uses a multi-faceted approach in order to enforce data integrity. Instead of defining a formal state machine, the model defines each data item and allows modifications through only a small set of programs. The model uses a three-part relationship of subject/program/object known as a triple or an access control triple. Within this relationship, subjects do not have direct access to objects. Objects can only be accessed through programs. Look to see how this differs from other access control models.
The model’s enforcement and certification rules define data items and processes that provide the basis for an integrity policy. The core of the model is based on the notion of a transaction.
The model contains a number of basic constructs that represent both data items and processes that operate on those data items. The key data type in the Clark-Wilson model is a Constrained Data Item. An Integrity Verification Procedure ensures that all CDIs in the system are valid at a certain state. Transactions that enforce the integrity policy are represented by Transformation Procedures. A TP takes as input a CDI or Unconstrained Data Item and produces a CDI. A TP must transition the system from one valid state to another valid state. UDIs represent system input. A TP must guarantee that it transforms all possible values of a UDI to a “safe” CDI.

Rules

At the heart of the model is the notion of a relationship between an authenticated principal and a set of programs that operate on a set of data items. The components of such a relation, taken together, are referred to as a Clark-Wilson triple. The model must also ensure that different entities are responsible for manipulating the relationships between principals, transactions, and data items. As a short example, a user capable of certifying or creating a relation should not be able to execute the programs specified in that relation.
The model consists of two sets of rules: Certification Rules and Enforcement Rules. The nine rules ensure the external and internal integrity of the data items. To paraphrase these:

Since we must make sure that these TPs are certified to operate on a particular CDI, we must have E1 and E2.

This requires keeping track of triples called "allowed relations".
We need authentication to keep track of this.
When information enters the system it need not be trusted or constrained. We must deal with this appropriately.
Finally, to prevent people from gaining access by changing qualifications of a TP:

CW-lite

A variant of Clark-Wilson is the CW-lite model, which relaxes the original requirement of formal verification of TP semantics. The semantic verification is deferred to a separate model and general formal proof tools.