Security type system

Last updated October 02, 2022

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.

A simple information flow policy

Suppose there are two users, A and B. In a program, the following security classes (SC) are introduced:

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

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. This example considers read operations (confidentiality). The following flows are 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. The combination operator (⊕) 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} nor {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. 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.

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

Example

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

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) = τ₁, Γ ⊢ 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 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".

Soundness

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

Related Research Articles

A computer program is a sequence or set of instructions in a programming language for a computer to execute. Computer programs are one component of software, which also includes documentation and other intangible components.

Simple Network Management Protocol (SNMP) is an Internet Standard protocol for collecting and organizing information about managed devices on IP networks and for modifying that information to change device behaviour. Devices that typically support SNMP include cable modems, routers, switches, servers, workstations, printers, and more.

In the security engineering subspecialty of computer science, a trusted system is one that is relied upon to a specified extent to enforce a specified security policy. This is equivalent to saying that a trusted system is one whose failure would break a security policy.

In software engineering and computer science, abstraction is:

In computer science, program analysis is the process of automatically analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness. Program analysis focuses on two major areas: program optimization and program correctness. The first focuses on improving the program’s performance while reducing the resource usage while the latter focuses on ensuring that the program does what it is supposed to do.

In computer science, imperative programming is a programming paradigm of software that uses statements that change a program's state. In much the same way that the imperative mood in natural languages expresses commands, an imperative program consists of commands for the computer to perform. Imperative programming focuses on describing how a program operates step by step, rather than on high-level descriptions of its expected results.

In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term". Usually the terms are various constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term. Type systems formalize and enforce the otherwise implicit categories the programmer uses for algebraic data types, data structures, or other components.

In type theory, a typing rule is an inference rule that describes how a type system assigns a type to a syntactic construction. These rules may be applied by the type system to determine if a program is well-typed and what type expressions have. A prototypical example of the use of typing rules is in defining type inference in the simply typed lambda calculus, which is the internal language of Cartesian closed categories.

Data-flow analysis is a technique for gathering information about the possible set of values calculated at various points in a computer program. A program's control-flow graph (CFG) is used to determine those parts of a program to which a particular value assigned to a variable might propagate. The information gathered is often used by compilers when optimizing a program. A canonical example of a data-flow analysis is reaching definitions.

The simply typed lambda calculus, a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus.

The Clark–Wilson integrity model provides a foundation for specifying and analyzing an integrity policy for a computing system.

Information flow in an information theoretical context is the transfer of information from a variable $to a variable in a given process. Not all flows may be desirable; for example, a system should not leak any secret to public observers.$

In computer science, the syntax of a computer language is the rules that defines the combinations of symbols that are considered to be correctly structured statements or expressions in that language. This applies both to programming languages, where the document represents source code, and to markup languages, where the document represents data.

In computer science, information hiding is the principle of segregation of the design decisions in a computer program that are most likely to change, thus protecting other parts of the program from extensive modification if the design decision is changed. The protection involves providing a stable interface which protects the remainder of the program from the implementation. Written in another way, information hiding is the ability to prevent certain aspects of a class or software component from being accessible to its clients, using either programming language features or an explicit exporting policy.

<span class="mw-page-title-main">Security information and event management</span> Computer security

Security information and event management (SIEM) is a field within the field of computer security, where software products and services combine security information management (SIM) and security event management (SEM). They provide real-time analysis of security alerts generated by applications and network hardware. Vendors sell SIEM as software, as appliances, or as managed services; these products are also used to log security data and generate reports for compliance purposes. The term and the initialism SIEM was coined by Mark Nicolett and Amrit Williams of Gartner in 2005.

A Hindley–Milner (HM) type system is a classical type system for the lambda calculus with parametric polymorphism. It is also known as Damas–Milner or Damas–Hindley–Milner. It was first described by J. Roger Hindley and later rediscovered by Robin Milner. Luis Damas contributed a close formal analysis and proof of the method in his PhD thesis.

In mathematical logic, category theory, and computer science, kappa calculus is a formal system for defining first-order functions.

<span class="mw-page-title-main">Computer access control</span>

In computer security, general access control includes identification, authorization, authentication, access approval, and audit. A more narrow definition of access control would cover only access approval, whereby the system makes a decision to grant or reject an access request from an already authenticated subject, based on what the subject is authorized to access. Authentication and access control are often combined into a single operation, so that access is approved based on successful authentication, or based on an anonymous access token. Authentication methods and tokens include passwords, biometric scans, physical keys, electronic keys and devices, hidden paths, social barriers, and monitoring by humans and automated systems.

In computer science, language-based security (LBS) is a set of techniques that may be used to strengthen the security of applications on a high level by using the properties of programming languages. LBS is considered to enforce computer security on an application-level, making it possible to prevent vulnerabilities which traditional operating system security is unable to handle.

In mathematical logic, the intersection type discipline is a branch of type theory encompassing type systems that use the intersection type constructor $to assign multiple types to a single term. In particular, if a term can be assigned both' the type and the type, then can be assigned the intersection type . Therefore, the intersection type constructor can be used to express finite heterogeneous ad hoc polymorphism . For example, the λ-term can be assigned the type in most intersection type systems, assuming for the term variable both the function type and the corresponding argument type .$