Language-based security

[2][3] Traditionally, the mechanisms used to control the correct behavior of software are implemented at the operating system level.

Since a lot of properties and behavior of the software is lost in compilation, it is significantly more difficult to detect vulnerabilities in machine code.

By evaluating the source code, before the compilation, the theory and implementation of the programming language can also be considered, and more vulnerabilities can be uncovered.

Instead of relying on programmers' memories, we should strive to produce tools that codify what is known about common security vulnerabilities and integrate it directly into the development process."

Common programming errors such as allowing buffer overflows and illegal information flows to occur, can be detected and disallowed in the software used by the consumer.

This is information which can be of value to the code consumer, as it provides some degree of guarantee that the program will not crash due to some specific error.

A goal of LBS is to ensure the presence of certain properties in the source code corresponding to the safety policy of the software.

Information gathered during the compilation can be used to create a certificate that can be provided to the consumer as a proof of safety in the given program.

Such a proof must imply that the consumer can trust the compiler used by the supplier and that the certificate, the information about the source code, can be verified.

An attacker could try to execute a program which does not satisfy noninterference repeatedly and systematically to try to map its behavior.

Several iterations could lead to the disclosure of higher variables, and let the attacker learn sensitive information about for example the systems state.

Whether a program satisfies noninterference or not can be evaluated during compilation assuming the presence of security type systems.

Common exploits of insecure low-level code lets an attacker perform unauthorized reads or writes to memory addresses.

During compilation of an unsafe language run-time checks is added to the low-level code to detect source-level undefined behavior.

The certificate can be produced in different ways, e.g. through Proof-carrying code (PCC) or Typed assembly language (TAL).

However, TAL can handle any security policy that may be expressed by the restrictions of the type system, which can include memory safety and control flow, among others.