Security type system

Once the policy is in place, the software developer can apply the security classes to the program components. Use of a security type system is usually combined with a compiler that can perform the verification of the information flow according to the type system rules. 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. The simple program is given in the following pseudocode:

if y{A} = 1 then x{A,B} := 0 else x{A,B} := 1

Here, an equality check is made on a variable y that is assigned the security class {A}. A variable x with a lower security class ({A,B}) is influenced by this check. This means that information is leaking from class {A} to class {A,B}, which is a violation of the confidentiality policy. This leak should be detected by the security type system.

Designing a security type system requires a function (also known as a security environment) that creates a mapping from variables to security types, or classes. This function can be called Γ, such that Γ(x) = τ, where x is a variable and τ is the security class, or type. Security classes are assigned (also called "judgement") to program components, using the following notation:

• Types are assigned to read operations by: Γ ⊢ e : τ.
• Types are assigned to write operations by: Γ ⊢ S : τ cmd.
• Constants can be assigned any type.

The following bottom-up notation can be used to decompose the program: ⁠assumption₁ ... assumption_n/conclusion⁠. Once the program is decomposed into trivial judgements, by which the type can easily be determined, the types for the less trivial parts of the program can be derived. Each "numerator" is considered in isolation, looking at the type of each statement to see if an allowed type can be derived for the "denominator", based on the defined type system "rules".

The main part of the security type system is the rules. They say how the program should be decomposed and how type verification should be performed. This toy program consists of a conditional test and two possible variable assignments. Rules for these two events are defined as follows:

Assignment:

Γ(x) = τ1, Γ ⊢ a : τ2 Γ ⊢ x := a : τ1 cmd

, where the following condition must hold: τ2 ⊑ τ1

Conditional test:

Γ ⊢ t : τ, Γ ⊢ S1 : τ1 cmd, Γ ⊢ S2 : τ2 cmd Γ ⊢ if t then S1 else S2: τ1 ⊓ τ2 cmd

, where the following condition must hold: τ ⊑ τ1, τ2

Applying this to the simple program introduced above yields:

3	Γ(y) = {A}	Γ(x) = {A,B} cmd, Γ ⊢ 0 : {A,B}	Γ(x) = {A,B} cmd, Γ ⊢ 1 : {A,B}
2	Γ ⊢ y = 1 : {A}	Γ ⊢ x := 0 : {A,B} cmd	Γ ⊢ x := 1 : {A,B} cmd
1	Γ ⊢ if y = 1 then x := 0 else x := 1 : Not typeable

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}. In more formalized terms, {A} ⋢ {A,B}, {A,B} (from the rule of the conditional test). Thus, the program is classified as "not typeable".

The soundness of a security type system can be informally defined as: If program P is well typed, P satisfies non-interference. 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.^[1]

• Fred B. Schneider, Greg Morrisett, and Robert Harper, A Language-Based Approach to Security.
• Andrei Sabelfeld, Andrew C. Myers, Language-Based Information-Flow Security.