Security type system

In simple terms, a security type system can be used to detect if there exists any kind of violation of confidentiality or integrity in a program, i.e. the programmer wants to detect if the program is in line with the information flow policy or not.

In a program, the following security classes (SC) are introduced: The information flow policy should define the direction that information is allowed to flow, which is dependent on whether the policy allows read or write operations.

The policy should also be a lattice, that is, it has a greatest lower-bound and least upper-bound (there always exists a combination between security classes).

In the case of integrity, information will flow in the opposite direction, thus the policy will be inverted.

Once the policy is in place, the software developer can apply the security classes to the program components.

For the sake of simplicity, a very simple computer program, together with the information flow policy as described in the previous section, can be used as a demonstration.

Rules for these two events are defined as follows: Applying this to the simple program introduced above yields: The type system detects the policy violation in line 2, where a read operation of security class {A} is performed, followed by two write operations of a less strict security class {A,B}.

Volpano, Smith and Irvine were the first to prove soundness of a security type system for a deterministic imperative programming language with a standard (non-instrumented) semantics using the notion of non-interference.