Security type system

In computer science, a type system can be described as a syntactic framework which contains a set of rules that are used to assign a type property (int, boolean, char etc.) to various components of a computer program, such as variables or functions. A security type system works in a similar way, only with a main focus on the security of the computer program, through information flow control. Thus, the various components of the program are assigned security types, or labels. The aim of a such system is to ultimately be able to verify that a given program conforms to the type system rules and satisfies non-interference. Security type systems is one of many security techniques used in the field of language-based security, and is tightly connected to information flow and information flow policies.

In simple terms, by using a security type system, you want to detect if there exists any kind of violiation of confidentiality or integrity in your program, i.e. you want to detect if the program is in line with the information flow policy or not.

A simple information flow policy

A Hasse diagram, describing a simple confidentiality information flow policy.

Suppose you have two users, A and B. In your program, you introduce the following security classes (SC):

SC = {∅, {A}, {B}, {A,B}}, where ∅ is the empty set.

In your information flow policy, you want to define the direction that information is allowed to flow, which is dependent on whether you are specifying a policy for read or write operations. In this example, we will consider read operations (confidentiality). We define that the following flows should be allowed:

→ = {({A}, {A}), ({B}, {B}), ({A,B}, {A,B}), ({A,B}, {A}), ({A,B}, {B}), ({A}, ∅), ({B}, ∅), ({A,B}, ∅)}

This can also be described as a superset (⊇). In words: information is allowed to flow towards stricter levels of confidentiality. Using the combination operator (⊕), we can express how security classes can perform read operations with respect to other security classes. For example:

{A} ⊕ {A,B} = {A} — the only security class that can read from both {A} and {A,B} is {A}.
{A} ⊕ {B} = ∅ — neither {A} or {B} are allowed to read from both {A} and {B}.

This can also be described as an intersection (∩) between security classes.

An information flow policy can be illustrated as a Hasse diagram. You also want your policy to 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.

Information flow policy in security type systems

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 simplycity, let us consider a very simple computer program together with the information flow policy as described in the previous section. The simple program is given in the following pseudocode:

if y_{A} = 1 then x_{A,B} := 0 else x_{A,B} := 1

Here we see that an equality check is made on a variable y that is assigned the security class {A}. We further see that 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 our confidentiality policy. This leak should be detected by the security type system.

Example

In order to design a security type system, we need to formalize a couple of things. First of all, we need a function (also known as a security environment) that creates a mapping from variables to security types, or classes. We denote this function Γ, such that Γ(x) = τ, where x is a variable and τ is the security class, or type. We assign security classes (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.

We will use the following bottom-up notation to decompose our program: assumption₁ ... assumption_n/conclusion. Once the program is decomposed into trivial judgements, where we easily can determine the type, we can work our way down again to obtain the types for the less trivial parts of the program. We consider each "numerator" in isolation, looking at the types of each statement to see if we are able to derive an allowed type to the "denominator", based on the defined type system rules.

Rules

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

Assignment:

Γ(x) = τ₁, Γ ⊢ a : τ₂

Γ ⊢ x := a : τ₁ cmd

, where the following condition must hold: τ₂ ⊑ τ₁

Conditional test:

Γ ⊢ t : τ, Γ ⊢ S₁ : τ₁ cmd, Γ ⊢ S₂ : τ₂ cmd

Γ ⊢ if t then S₁ else S₂: τ₁ ⊓ τ₂ cmd

, where the following condition must hold: τ ⊑ τ₁, τ₂

Applying this to the simple program we introduced above, we get:

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 typable`

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 typable.

Soundness

The soundness of a security type system can be informally defined as: If program P is well typed, P satisfies non-interference.