Language-based security

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 able to prevent vulnerabilities which traditional operating-system security is unable to handle.

Applications are typically specified and implemented in programming languages and to protect against the attacks, flaws and bugs an application’s source code might be vulnerable to, there is a need for application-level security; security evaluating the applications behaviour with respect to the programming language. This area is generally known as language-based security.

Imagine a program that should never overwrite critical system data, thereby causing a crash; a property desirable in important systems such as flight control software. For this to be possible it is up to the developer to not leave vulnerabilities in the source code. By analysing the source code at compile-time it is possible to detect places in the code where crashes might occur, and ensure that a program is not compiled and distributed if it does not answer to its required properties. The analysis of the source code must be done differently for each programming language, as function-calls which are known to cause crashes, if not used correctly, are different from for example C to Java.

Program analysis is just one out of several techniques LBS covers.

Motivation

The use of large software systems, such as SCADA, is taking place all around the world and computer systems constitute the core of many modern industries today. The society relies greatly on infrastructure such as water, energy, communication and transportation, which again all rely on fully functionally working computer systems. There are well known examples of when critical systems fails, and consequences their absence causes.

Some system failures is caused by events from the outside world, like natural disasters or fires, but systems also fails because of bugs or errors in the software. This is software which is specified and developed by humans, software which behaves the way humans has told it to behave, and still it fails. When this happens the question about whether the failure could be avoided arises. Is it possible to ensure that software used in computer systems is secure to use?

Traditionally, the mechanisms used to control the correct behaviour of software are implemented at the operating-system level. The operating system enforces security on several possible security breaches such as memory-access violations, stack overflow violations, the launching of programs with excessive privileges and many others. Although this a crucial part of security in computer systems, all evidences points towards the need of securing the behaviour of software on a more specific level. Enforcement done by the operating system is done on low level code, or machine code. Since most programs today are written in some programming language, a lot of the properties of the behaviour of the software are lost on compilation and is considered significantly more difficult to recover when evaluating the machine code. A possible solution to the need of security on a more specific level can thus be to evaluate the source code, the software before compilation, when the theory and implementation of the programming language also can be considered. Something like language based security.

Objective of LBS

By using LBS, the security of software could be increased in several areas. Common programming errors such as allowing buffer overflows and illegal information flows should be possible to detect and disallow in the software used by the consumer. It is also desirable to provide some proof to the consumer about the security properties of the software, making the consumer able to trust the software without having to receive the source code and self checking it for errors.

When source code, written in a specific programming language, is compiled to machine code, the compiler is likely to perform several operations. Lexical analysis, preprocessing, parsing, semantic analysis, code generation, and code optimization are all commonly used among compilers. These operations are done specifically to each programming language and by analyzing the source code and using the theory and implementation of the language, the compiler will attempt to correctly translate the high-level code into low-level code, still achieving the desired behaviour of the program.

During compilation of programs written in a type-safe language, such as Java, the source code must typecheck successfully before compilation. If the typecheck fails, the compilation will not take place, and the source code needs to be modified. This means that, given a correct compiler, any code compiled from a successfully typechecked source program should be clear of invalid-assignment errors. This is information which can be of value to the code consumer, as it provides some degree of guarantee of the program not crashing due to some specific error.

A goal of LBS is to ensure the presence of certain properties of the source code corresponding to the safety policy of the software. When gathering the necessary information to check for these properties and to compile the program, instead of throwing away the information when done, it is desirable to handle the information like a certificate and make it available to the code consumer. By doing so, the consumer can achieve some degree of guarantee that the software behaves accordingly to some desired property.

It is yet to be established any particular standard to let code supplier prove to the consumer that the compiled code had certain properties before compilation. 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.

File:Certifying compiler model.png

An abstract model of sharing compiler-certified code

The figure above illustrates how certification and verification of low-level code could be established by the use of a certifying compiler. The supplier obtains the advantage of not having to reveal the source code to let consumers trust the program, and the consumer is left with the easy job, compared to evaluating and compiling the source code, of verifying the certificate and only needs a limited trusted code base containing of the compiler and the verifier.

Papers

• 􀀀Language based security, Dexter Kozen, Cornell University