Programming languages

Modern computer applications are typically made up of different software components that are created by, or may act on behalf of, mutually distrustful entities. To ensure the security of computer systems, it is important to restrict the ability of the components to perform actions within the computer system. The Principle of Least Authority states that a component should be given only the ability (or authority) it needs to perform its task, and no more.

Both sound software verification techniques and heuristic software flaw-finding tools benefit from the presence of software annotations that describe the behavior of software components. Function summaries (in the form of logical annotations) allow modular checking of software and more precise reasoning. However, such annotations are difficult to write and not commonly produced by software developers, despite their benefits to static analysis. The Crowdsourcing Annotations project will address this deficiency by encouraging software-community-based crowd-sourced generation of annotations.

The security of our software is critical for consumer confidence, the protection of privacy and valuable intellectual property, and of course national security. Because of our society's increased reliance on software, security breaches can lead to serious personal or corporate losses, and endanger the privacy, liberties, and even the lives of individuals. As threats to software security have become more sophisticated, so too have the techniques and analyses developed to improve it. Symbolic execution has emerged as a fundamental tool for security applications.

Distributed applications (such as web applications and cloud-based applications, where multiple computers cooperate to run the application) are becoming increasingly common. Given the amount of commercial activity and information handled by these distributed applications, it is important that these applications are correct, reliable, and efficient. However, many traditional tools and techniques for programmers cannot be used for distributed applications, making it difficult for programmers to write and debug distributed applications.

Language-based security (the use of programming language abstractions and techniques for security) holds the promise of efficient enforcement of strong, formal, fine-grained, application-specific information security guarantees. However, language-based security has not yet reached its potential, and is not in widespread use for providing rich information security guarantees.