Final Report on Seminar 03411: Language-Based Security
Anindya Banerjee, Heiko Mantel, David A. Naumann, Andrei Sabelfeld · 2003
Modern computing systems are particularly vulnerable to security attacks at the application level. Traditionally, security mechanisms have been based on low-level protection such as OS-based monitoring and access control. However, application-level attacks (e.g., the widely-publicized Lovebug and Melissa viruses executed on behalf of a mailer application) operate at a higher-level and circumvent the security mechanisms. Not only is malicious code a threat to security, but also unintended bugs in the specification and implementation of systems can lead to equally disastrous effects. Application-level security is becoming an increasingly popular area of research because there is an increasing demand for applications to provide high assurance that particular security policies are followed. An effective way to achieve high assurance is to counter security threats at the same level as attacks—the application level. Because applications are typically specified and implemented in programming languages, this area is known as language-based security. A direct benefit of language-based security is the ability to naturally express security policies and enforcement mechanisms using the techniques of the well-developed area of programming languages. These techniques facilitate rigorous specifications of security policies as well as their mechanical verification. Language-based techniques are gradually entering standard security practices. For example, the Java byte-code verifier is a language-based enforcement mechanism of particular integrity properties. As another example, the Java Virtual Machine and the .NET runtime system provide a dynamic access control mechanism that inspects the runtime stack to check whether permissions have been granted to code in the calling chain. Despite such forays into mainstream security practices, there are a number of open issues in languagebased security. One problem is to preserve the confidentiality of data by programs. This involves specification and enforcement of a property that guarantees that a program’s public outputs do not (explicitly or implicitly) reveal information about the program’s secret inputs. Recent technical advances allow enforcing confidentiality using a variety of language-based techniques e.g., type systems, data-flow and control-flow analysis, abstract interpretation, model checking, etc. While more and more realistic security properties for more and more expressive languages are being considered, there are critical challenges remaining in the area of language-based security in general and in the area of program confidentiality in particular. To name just a few: