You do not have permission to edit this page, for the following reasons:

This IP address has been blocked from editing Wikipedia.
This does not affect your ability to read Wikipedia pages.
Most people who see this message have done nothing wrong. Some kinds of blocks restrict editing from specific service providers or telecom companies in response to recent abuse or vandalism, and can sometimes affect other users who are unrelated to that abuse. Review the information below for assistance if you do not believe that you have done anything wrong.

The IP address or range 52.91.0.0/16 has been blocked (disabled) by ‪JJMC89‬ for the following reason(s):

The IP address that you are currently using has been blocked because it is believed to be a web host provider or colocation provider. To prevent abuse, web hosts and colocation providers may be blocked from editing Wikipedia.
You will not be able to edit Wikipedia using a web host or colocation provider because it hides your IP address, much like a proxy or VPN.
We recommend that you attempt to use another connection to edit. For example, if you use a proxy or VPN to connect to the internet, turn it off when editing Wikipedia. If you edit using a mobile connection, try using a Wi-Fi connection, and vice versa. If you are using a corporate internet connection, switch to a different Wi-Fi network. If you have a Wikipedia account, please log in.
If you do not have any other way to edit Wikipedia, you will need to request an IP block exemption.

How to appeal if you are confident that your connection does not use a colocation provider's IP address:
If you are confident that you are not using a web host, you may appeal this block by adding the following text on your talk page: ((unblock|reason=Caught by a colocation web host block but this host or IP is not a web host. My IP address is _______. Place any further information here. ~~~~)). You must fill in the blank with your IP address for this block to be investigated. Your IP address can be determined here. Alternatively, if you wish to keep your IP address private you can use the unblock ticket request system. There are several reasons you might be editing using the IP address of a web host or colocation provider (such as if you are using VPN software or a business network); please use this method of appeal only if you think your IP address is in fact not a web host or colocation provider.

Administrators: The IP block exemption user right should only be applied to allow users to edit using web host in exceptional circumstances, and requests should usually be directed to the functionaries team via email. If you intend to give the IPBE user right, a CheckUser needs to take a look at the account. This can be requested most easily at SPI Quick Checkuser Requests. Unblocking an IP or IP range with this template is highly discouraged without at least contacting the blocking administrator.

This block will expire on 05:26, 2 September 2024.

Even when blocked, you will usually still be able to edit your user talk page, as well as email administrators and other editors.

For information on how to proceed, please read the FAQ for blocked users and the guideline on block appeals. The guide to appealing blocks may also be helpful.

Other useful links: Blocking policy · Help:I have been blocked
Your IP address is in a range that has been blocked on all Wikimedia Foundation wikis. The block was made by ‪Jon Kolbert‬. The reason given is Open proxy/Webhost: See the help page if you are affected .
- Start of block: 04:57, 27 November 2021
- Expiry of block: 04:57, 27 November 2024
Your current IP address is 52.91.194.66. The blocked range is 52.91.0.0/16. Please include all above details in any queries you make. If you believe you were blocked by mistake, you can find additional information and instructions in the No open proxies global policy. Otherwise, to discuss the block please post a request for review on Meta-Wiki. You could also send an email to the stewards VRT queue at stewards@wikimedia.org including all above details.

You can view and copy the source of this page:

((More citations needed section|date=February 2018))
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.

[[Application software|Software applications]] are typically specified and implemented in certain [[programming language]]s, and in order to protect against 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 behavior with respect to the programming language. This area is generally known as language-based security.

== Motivation ==
The use of large software systems, such as [[SCADA]], is taking place all around the world<ref>((cite web|title=Can we learn from SCADA security incidents?|url=http://www.oas.org/cyber/documents/ENISA%20-%20Can%20we%20learn%20from%20SCADA%20security%20incidents%20-%20White%20Paper.pdf|website=www.oas.org|publisher=enisa))</ref> and computer systems constitute the core of many infrastructures. 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 several well known examples of when critical systems fail due to bugs or errors in software, such as ''when shortage of computer memory caused LAX computers to crash and hundreds of flights to be delayed'' (April 30, 2014).<ref>((cite news|title=Air Traffic Control System Failed|url=http://www.computerworld.com/article/2476246/malware-vulnerabilities/-2-billion-air-traffic-control-system-failed-by-running-out-of-computer-memo.html|accessdate=12 May 2014|publisher=www.computerworld.com))</ref><ref>((cite news|title=Software Bug Contributed to Blackout|url=http://www.securityfocus.com/news/8016|accessdate=11 February 2004|publisher=www.securityfocus.com))</ref>

Traditionally, the mechanisms used to control the correct behavior of software are implemented at the operating system level. The operating system handles several possible security violations such as memory access violations, stack overflow violations, access control violations, and many others. This is a crucial part of security in computer systems, however by securing the behavior of software on a more specific level, even stronger security can be achieved. 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.

<blockquote>
"So why do developers keep making the same mistakes? 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."

— D. Evans and D. Larochelle, 2002
</blockquote>

== Objective of Language-based security ==
By using LBS, the security of software can be increased in several areas, depending on the techniques used. Common programming errors such as allowing [[buffer overflow]]s and illegal information flows to occur, can be detected and disallowed 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.

A compiler, taking source code as input, performs several language specific operations on the code in order to translate it into machine readable code. [[Lexical analysis]], [[Preprocessor|preprocessing]], [[parsing]], [[Semantic analysis (compilers)|semantic analysis]], [[Code generation (compiler)|code generation]], and [[code optimization]] are all commonly used operations in compilers. 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, preserving the behavior of the program.

[[File:Model of certifying compiler.png|thumb|Illustrating a certifying compiler]]

During compilation of programs written in a [[Type safety|type-safe]] language, such as [[Java (programming language)|Java]], the source code must type-check successfully before compilation. If the type-check fails, the compilation will not be performed, and the source code needs to be modified. This means that, given a correct compiler, any code compiled from a successfully type-checked 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 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.

The figure illustrates how certification and verification of low-level code could be established by the use of a certifying compiler. The software supplier gains the advantage of not having to reveal the source code, and the consumer is left with the task of verifying the certificate, which is an easy task compared to evaluation and compilation of the source code itself. Verifying the certificate only requires a limited trusted code base containing the compiler and the verifier.

== Techniques ==
=== Program analysis ===
((Main|Program analysis))
The main applications of [[program analysis]] are [[program optimization]] (running time, space requirements, power consumption etc.) and [[program correctness]] (bugs, security vulnerabilities etc.). Program analysis can be applied to compilation ([[static analysis]]), run-time ([[dynamic analysis]]), or both. In language-based security, program analysis can provide several useful features, such as: [[type checking]] (static and dynamic), [[reference monitor|monitoring]], [[taint checking]] and [[control-flow analysis]].

=== Information flow analysis ===
((Main|Information flow (information theory)|l1=Information flow))
Information flow analysis can be described as a set of tools used to analyze the [[Information flow (information theory)#Information flow control|information flow control]] in a program, in order to preserve [[confidentiality]] and [[Data integrity|integrity]] where regular [[access control]] mechanisms come short.

<blockquote>
"By decoupling the right to access information from the right to disseminate it, the flow model goes beyond the access matrix model in its ability to specify secure information flow. A practical system needs both access and flow control to satisfy all security requirements."

— D. Denning, 1976
</blockquote>

Access control enforces checks on ''access'' to information, but is not concerned about what happens after that. An example: A system has two users, Alice and Bob. Alice has a file ''secret.txt'', which is only allowed to be read and edited by her, and she prefers to keep this information to herself. In the system, there also exists a file ''public.txt'', which is free to read and edit for all users in the system. Now suppose that Alice has accidentally downloaded a malicious program. This program can access the system as Alice, bypassing the access control check on ''secret.txt''. The malicious program then copies the content of ''secret.txt'' and places it in ''public.txt'', allowing Bob and all other users to read it. This constitutes a violation of the intended confidentiality policy of the system.

==== Noninterference ====
[[Non-interference (security)|Noninterference]] is a property of programs that does not leak or reveal information of variables with a ''higher'' security classification, depending on the input of variables with a ''lower'' security classification. A program which satisfies noninterference should produce the same ''output'' whenever the corresponding same ''input'' on the ''lower'' variables are used. This must hold for every possible value on the input. This implies that even if ''higher'' variables in the program has different values from one execution to another, this should not be visible on the ''lower'' variables.

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 system]]s.

=== Security type system ===
((Main|Security type system))
A [[security type system]] is a kind of [[type system]] that can be used by software developers in order to check the security properties of their code. In a language with security types, the types of variables and expressions relate to the security policy of the application, and programmers may be able to specify the application security policy via type declarations. Types can be used to reason about various kinds of security policies, including authorization policies (as access control or capabilities) and information flow security. Security type systems can be formally related to the underlying security policy, and a security type system is sound if all programs that type-check satisfy the policy in a semantic sense. For example, a security type system for information flow might enforce noninterference, meaning that type checking reveals whether there is any violation of confidentiality or integrity in the program.

=== Securing low-level code ===
Vulnerabilities in low-level code are bugs or flaws that will lead the program into a state where further behavior of the program is undefined by the source programming language. The behavior of the low-level program will depend on compiler, runtime system or operating system details. This allows for an attacker to drive the program towards an undefined state, and exploit the behavior of the system.

Common exploits of insecure low-level code lets an attacker perform unauthorized reads or writes to memory addresses. The memory addresses can be either random  or chosen by the attacker.

==== Using safe languages ====
An approach to achieve secure low-level code is to use safe high-level languages. A safe language is considered to be completely defined by its programmers' manual.<ref>((cite book|last1=Pierce|first1=Benjamin C.|title=Types and Programming Languages|date=2002|publisher=The MIT Press|isbn=9780262162098|url=https://books.google.com/books?id=ti6zoAC9Ph8C&q=%22safe+language%22))</ref> Any bug that could lead to implementation-dependent behavior in a safe language will either be detected at compile time or lead to a well-defined error behavior at run-runtime. In [[Java (programming language)|Java]], if accessing an array out of bounds, an exception will be thrown. Examples of other safe languages are [[C Sharp (programming language)|C#]], [[Haskell (programming language)|Haskell]] and [[Scala programming language|Scala]].

==== Defensive execution of unsafe languages ====
During compilation of an unsafe language run-time checks is added to the low-level code to detect source-level undefined behavior. An example is the use of [[Buffer overflow protection#Canaries|canaries]], which can terminate a program when discovering bounds violations.
A downside of using run-time checks such as in [[bounds checking]] is that they impose considerable performance overhead.

[[Memory protection]], such as using non-executable stack and/or heap, can also be seen as additional run-time checks. This is used by many modern operating systems.

==== Isolated execution of modules ====
The general idea is to identify sensitive code from application data by analyzing the source code. Once this is done the different data is separated and placed in different modules.  When assuming that each module has total control over the sensitive information it contains, it is possible to specify when and how should leave the module. 
An example is a cryptographic module that can prevent keys from ever leaving the module unencrypted.

=== Certifying compilation ===
Certifying compilation is the idea of producing a certificate during compilation of source code, using the information from the high-level programming language semantics. This certificate should be enclosed with the compiled code in order to provide a form of proof to the consumer that the source code was compiled according to a certain set of rules. The certificate can be produced in different ways, e.g. through [[Proof-carrying code]] (PCC) or [[Typed assembly language]] (TAL).

==== Proof-carrying code  ====
The main aspects of PCC can be summarized in the following steps:<ref>((cite journal|last1=Kozen|first1=Dexter|title=Language Based Security|date=1999|publisher=Cornell University|url=http://www.cs.cornell.edu/~kozen/papers/lbs.pdf))</ref>
# The supplier provides an executable program with various annotations produced by a [[certifying compiler]].
# The consumer provides a verification condition, based on a [[security policy]]. This is sent to the supplier.
# The supplier runs the verification condition in a [[Automated theorem proving|theorem prover]] to produce a proof to the consumer that the program in fact satisfies the security policy.
# The consumer then runs the proof in a [[Automated proof checking|proof checker]] to verify the proof validity.

An example of a certifying compiler is the [http://www.cs.berkeley.edu/~necula/touchstone.html Touchstone compiler], that provides a PCC formal proof of type- and memory safety for programs implemented in Java.

==== Typed assembly language ====
TAL is applicable to programming languages that make use of a [[type system]]. After compilation, the [[object code]] will carry a type annotation that can be checked by an ordinary type checker. The annotation produced here is in many ways similar to the annotations provided by PCC, with some limitations. 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.

== Seminars ==
* [http://www.dagstuhl.de/03411 Dagstuhl Seminar 03411], Language-Based Security, October 5 – 10, 2003.

== References ==
((Reflist))

== Books ==
* G. Barthe, B. Grégoire, T. Rezk, ''Compilation of Certificates'', 2008
* Brian Chess and Gary McGraw, ''Static Analysis for Security'', 2004.

== Further reading ==
* Dexter Kozen, [http://www.cs.cornell.edu/~kozen/papers/lbs.pdf ''Language Based Security''], Cornell University, 1999
* Pieter Agten et al., [http://www.securitee.org/files/rdevel_wistp2012.pdf ''Recent Developments in Low-Level Software Security''], Universiteit Leuven
* Andrei Sabelfeld and Andrew C. Myers, [http://www.cs.cornell.edu/andru/papers/jsac/sm-jsac03.pdf ''Language-Based Information-Flow Security'']
* Fred B. Schneider et al., [http://repository.cmu.edu/cgi/viewcontent.cgi?article=1921&context=compsci ''A Language-Based Approach to Security''], Carnegie Mellon University, 2000

[[Category:Computer security]]

Pages transcluded onto the current version of this page (help):

Language-based security (edit)
Template:Ambox (view source) (template editor protected)
Template:Cite book (view source) (protected)
Template:Cite journal (view source) (protected)
Template:Cite news (view source) (protected)
Template:Cite web (view source) (protected)
Template:Main (view source) (template editor protected)
Template:Main other (view source) (protected)
Template:More citations needed (view source) (template editor protected)
Template:More citations needed section (view source) (template editor protected)
Template:Reflist (view source) (protected)
Template:Reflist/styles.css (view source) (protected)
Template:Sp (view source) (template editor protected)
Module:Arguments (view source) (protected)
Module:Category handler (view source) (protected)
Module:Category handler/blacklist (view source) (protected)
Module:Category handler/config (view source) (protected)
Module:Category handler/data (view source) (protected)
Module:Category handler/shared (view source) (protected)
Module:Check for unknown parameters (view source) (protected)
Module:Citation/CS1 (view source) (protected)
Module:Citation/CS1/COinS (view source) (protected)
Module:Citation/CS1/Configuration (view source) (protected)
Module:Citation/CS1/Date validation (view source) (protected)
Module:Citation/CS1/Identifiers (view source) (protected)
Module:Citation/CS1/Utilities (view source) (protected)
Module:Citation/CS1/Whitelist (view source) (protected)
Module:Citation/CS1/styles.css (view source) (protected)
Module:Format link (view source) (template editor protected)
Module:Hatnote (view source) (template editor protected)
Module:Hatnote/styles.css (view source) (template editor protected)
Module:Hatnote list (view source) (template editor protected)
Module:Labelled list hatnote (view source) (template editor protected)
Module:Message box (view source) (protected)
Module:Message box/ambox.css (view source) (protected)
Module:Message box/configuration (view source) (protected)
Module:Namespace detect/config (view source) (protected)
Module:Namespace detect/data (view source) (protected)
Module:Unsubst (view source) (protected)
Module:Yesno (view source) (protected)

Return to Language-based security.

Retrieved from "https://en.wikipedia.org/wiki/Language-based_security"